[Resending to the list, I used the wrong address. Sorry for the duplicate copies.]
On 19 dec. 2013, at 05:30, Richard Eisenberg
I'd say GHC has it right in this case.
(f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the kinds match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's initial problem, we have (with all type, kind, and coercion variables made explicit)
But even when it can know the kinds match up it doesn’t decompose it. For example: — {-# LANGUAGE TypeFamilies #-} foo :: (f a ~ g b) => f a -> g b foo = id — Ends up with 2 errors (7.6.3): Could not deduce (a ~ b) from the context (f a ~ g b) Could not deduce (f ~ g) from the context (f a ~ g b) So the wanted constraint f a ~ g b was decomposed, meaning the kind of a and b, and f and g were already found to be equal. Even with an explicit kind signature on every variable it doesn't work: foo :: (f a ~ g b) => (f :: * -> *) (a :: *) -> (g :: * -> *) (b :: *) I can’t think of an example where f a ~ g b holds, but the kinds of a and b are different. Thijs (“xnyhps”)