Restrictions on polytypes with type families

[Manuel M T Chakravarty]

Gabriel Dos Reis <gdr at integrable-solutions.net>:
> On Wed, Apr 3, 2013 at 8:01 PM, Manuel M T Chakravarty
> <chak at cse.unsw.edu.au> wrote:
>> E.g., given
>> 
>>  type family F a :: *
>> 
>> the equality
>> 
>>  Maybe (forall a. F [a]) ~ G b
>> 
>> would need to be broken down to
>> 
>>  x ~  F [a], Maybe (forall a. x) ~ G b
>> 
>> but you cannot do that, because you just moved 'a' out of its scope. Maybe
>> you can move the forall out as well?
> 
> yes, why wouldn't you pull it out as well:
> 
>   x ~ forall a. F [a], Maybe x ~ G b
> 
> where you systematically introduce fresh  type
> variables for an quantified type expressions?

One universally quantified variable may appear as the argument to two type family applications (or more generally, have two occurrences, of which only one is under the type family).

Moreover, the whole equality solution mechanism quite fundamentally depends on producing equalities of the form

  x ~ F b1 ... bn

for type family applications. Sticking a forall in there may lead to trouble with the proof theory. In particular, it would compromise the analogy to CHRs (constraint handling rules) which inspired our solution.

Manuel