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 <c...@cse.unsw.edu.au> wrote: > Gabriel Dos Reis <g...@integrable-solutions.net>: >> On Wed, Apr 3, 2013 at 8:01 PM, Manuel M T Chakravarty >> <c...@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@haskell.org > http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
