PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
sanzhiyan at gmail.com
Wed Sep 19 19:26:57 CEST 2012
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.
More information about the Glasgow-haskell-users