
On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones
[...] 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