Restrictions on polytypes with type families

[Gabriel Dos Reis]

Hi Manuel,

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?

-- Gaby