Restrictions on polytypes with type families

[Gabriel Dos Reis]

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

-- Gaby