Restrictions on polytypes with type families

Gabriel Dos Reis gdr at integrable-solutions.net
Thu Apr 4 03:39:08 CEST 2013


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



More information about the ghc-devs mailing list