Restrictions on polytypes with type families

[Richard Eisenberg]

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 <chak at cse.unsw.edu.au> wrote:

> Gabriel Dos Reis <gdr at integrable-solutions.net>:
>> 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?
> 
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs