
4 Apr
2013
4 Apr
'13
1:39 a.m.
Hi Manuel,
On Wed, Apr 3, 2013 at 8:01 PM, Manuel M T Chakravarty
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