On Fri, Apr 5, 2013 at 1:32 PM, Dimitrios Vytiniotis <dimit...@microsoft.com > wrote:
> Hmm, no I don’t think that Flattening is a very serious problem: > > Firstly, we can somehow get around that if we use implication constraints > and higher-order flattening > > variables. We have discussed that (but not implemented). For example. > > > > forall a. F [a] ~ G Int > > > > becomes: > > > > forall a. fsk a ~ G Int > > > > forall a. true => fsk a ~ F [a] > > > > Secondly: flattening under a Forall is not terribly important, unless you > have type families that dispatch on > > polymorphic types, which is admittedly a rather rare case. We lose some > completeness but that’s ok. > > > > For me, a more serious problem are polymorphic RHS, which give rise to > exactly the same problems for type > > inference as impredicative polymorphism. For instance: > > > > type instance F Int = forall a. a -> [a] > > > > g :: F Int > > g = undefined > > > > main = g 3 > > > > Should this type check or not? And then all our discussions about > impredicativity, explicit type applications etc become > > relevant again. > > > > Thanks! > > d- > If the problem with foralls on the RHS is that it devolves into ImpredicativeTypes, what about only allowing them when ImpredicativeTypes is on? > > > > > > > > > > *From:* Simon Peyton-Jones > *Sent:* Friday, April 05, 2013 8:24 AM > *To:* Manuel M T Chakravarty > *Cc:* Iavor Diatchki; ghc-devs; Dimitrios Vytiniotis > *Subject:* RE: Restrictions on polytypes with type families > > > > Manuel has an excellent point. See the Note below in TcCanonical! I have > no clue how to deal with this > > > > Simon > > > > Note [Flattening under a forall] > > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > > Under a forall, we > > (a) MUST apply the inert subsitution > > (b) MUST NOT flatten type family applications > > Hence FMSubstOnly. > > > > For (a) consider c ~ a, a ~ T (forall b. (b, [c]) > > If we don't apply the c~a substitution to the second constraint > > we won't see the occurs-check error. > > > > For (b) consider (a ~ forall b. F a b), we don't want to flatten > > to (a ~ forall b.fsk, F a b ~ fsk) > > because now the 'b' has escaped its scope. We'd have to flatten to > > (a ~ forall b. fsk b, forall b. F a b ~ fsk b) > > and we have not begun to think about how to make that work! > > > > > > *From:* Manuel M T Chakravarty > [mailto:c...@cse.unsw.edu.au<c...@cse.unsw.edu.au>] > > *Sent:* 04 April 2013 02:01 > *To:* Simon Peyton-Jones > *Cc:* Iavor Diatchki; ghc-devs > *Subject:* Re: Restrictions on polytypes with type families > > > > Simon Peyton-Jones <simo...@microsoft.com>: > > isn't this moving directly into the territory of impredicative types? > > > > Ahem, maybe you are right. Impredicativity means that you can > > *instantiate a type variable with a polytype* > > > > So if we allow, say (Eq (forall a.a->a)) then we’ve instantiated Eq’s type > variable with a polytype. Ditto Maybe (forall a. a->a). > > > > But this is only bad from an inference point of view, especially for > implicit instantiation. Eg if we had > > class C a where > > op :: Int -> a > > > > then if we have > > f :: C (forall a. a->a) =>... > > f = ...op... > > > > do we expect op to be polymorphic?? > > > > For type families maybe things are easier because there is no implicit > instantiation. > > > > But I’m not sure > > > > These kinds of issues are the reason that my conclusion at the time was > (as Richard put it) > > > > Or, are > | there any that are restricted because someone needs to think hard before > | lifting it, and no one has yet done that thinking? > > > > At the time, there were also problems with what the type equality solver > was supposed to do with foralls. > > > > I know, for example, > | that the unify function in types/Unify.lhs will have to be completed to > | work with foralls, but this doesn't seem hard. > > > > The solver changed quite a bit since I rewrote Tom's original prototype. > So, maybe it is easy now, but maybe it is more tricky than you think. The > idea of rewriting complex terms into equalities at the point of each > application of a type synonym family (aka type function) assumes that you > can pull subterms out of a term into a separate equality, but how is this > going to work if a forall is in the way? 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? > > > > Manuel > > > > > > > > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://www.haskell.org/mailman/listinfo/ghc-devs > > -- Your ship was destroyed in a monadic eruption.
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
