Restrictions on polytypes with type families

[Gabriel Dos Reis]

On Fri, Apr 5, 2013 at 6:32 AM, Dimitrios Vytiniotis
<dimitris at 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.

I would expect a saturated type family application to be expanded right
away so that g effectively has type forall a . a -> [a], as if in fact we
had type FInt = forall a . -> [a].  As long as you stay away from inferring
type constructors, I suspect you should be fine.

-- Gaby