Re: Restrictions on polytypes with type families

Gabriel Dos Reis :

On Wed, Apr 3, 2013 at 8:01 PM, Manuel M T Chakravarty 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