On Wed, Apr 3, 2013 at 12:53 PM, Simon Peyton-Jones
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:xmlf@tcs2011.pdf [2] http://www.sciencedirect.com/science/article/pii/S0890540109000145 -- Gaby