PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Andrea Vezzosi]

On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> [...]
> Type inference
> ~~~~~~~~~
> I'm a little unclear about the implications for inference.  One route
> might be this.   Suppose we are trying to solve a constraint
>      [W]  (a:'(k1,ks)) ~ '( t1, t2 )
> where a is an untouchable type variable.  (if it was touchable we'd
> simply unify it.)  Then we can replace it with a constraint
>     [W]   '(Fst a, Snd a) ~ '( t1, t2)
>
> Is that it?  Or do we need more?  I'm a bit concerned about constraints like
>     F a ~ e
> where a:'(k1,k2), and we have a type instance like  F '(a,b) = ...
>

F a ~ F '(Fst a, Snd a) has to hold, so one does need to expand a for
constraints like F a ~ e in this case. One way to think of it is that
patterns like '(a,b) are the same as value-level ~(a,b) ones.

-- Andrea