On Wed, Apr 3, 2013 at 12:53 PM, Simon Peyton-Jones <simo...@microsoft.com> wrote: > 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 > > > > Simon
I wouldn't expect any (technical) problem to arise. I suspect the new formulation [1, 2] of MLF is doing something like this already. Implementation wise, well, it might be like moving to GADT :-) Also, if you are doing it for type families, do it for data families too :-) [1] http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski:x...@tcs2011.pdf [2] http://www.sciencedirect.com/science/article/pii/S0890540109000145 -- Gaby _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
