Re: Restrictions on polytypes with type families

I'm not sure the use case being discussed here is really what I'm after. This use case has a type family application appearing within a forall

Maybe (forall a. F [a]) ...

This actually seems to work OK when I test it, though I haven't looked closely at the internal machinery. I'm more concerned with using a forall within a type family application, something like

Maybe (F (forall a. ...)) ...

And, responding to earlier comments, yes, this is wandering towards impredicative types, but that, by itself, doesn't seem to cause a problem. Is there a problem if there is a "hidden" forall? For example:

type instance F Int = (forall a. a -> a) type instance F Bool = Double foo :: b -> F b

Here, foo has what I'm calling a "hidden" forall -- it may have a forall or it may not, depending on the choice of b. I don't immediately see a problem with this (the type seems well-formed even if we don't float the forall to the top), but type inference isn't my strong point. Richard On Apr 3, 2013, at 9:55 PM, Manuel M T Chakravarty wrote:

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

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs