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)
data InnerEq (j :: BOX) (k :: BOX) (i :: j) (a :: k) where InnerEq :: forall (f :: j -> k). f i ~ a => InnerEq j k i a
class TypeCompare (k :: BOX) (t :: k -> *) where maybeInnerEq :: forall (j :: BOX) (f :: j -> k) (i :: j) (a :: k). t (f i) -> t a -> Maybe (InnerEq j k i a)
instance forall (j :: BOX) (k :: BOX) (i :: j). TypeCompare k (InnerEq j k i) where maybeInnerEq :: forall (j2 :: BOX) (f :: j2 -> k) (i2 :: j2) (a :: k). InnerEq j k i (f i2) -> InnerEq j k i a -> Maybe (InnerEq j2 k i2 a) maybeInnerEq (InnerEq (f1 :: j -> k) (co1 :: f1 i ~ f i2)) (InnerEq (f2 :: j -> k) (co2 :: f2 i ~ a)) = Just (InnerEq (f3 :: j2 -> k) (co3 :: f3 i2 ~ a))
GHC must infer `f3` and `co3`. The only thing of kind `j2 -> k` lying around is f. So, we choose f3 := f. Now, we need to prove `f i2 ~ a`. Using the two equalities we have, we can rewrite this as a need
to prove `f1 i ~ f2 i`. I can't see a way of doing this. Now, GHC complains that it cannot (renaming to my variables) deduce (i ~ i2) from (f1 i ~ f i2). But, this is exactly the case where the kinds *don't* match up. So, I agree that GHC can't deduce that equality, but I think that, even if it could, it wouldn't be able to type-check the whole term.... unless I've made a mistake somewhere.
I don't see an immediate way to fix the problem, but I haven't thought much about it.
Does this help? Does anyone see a mistake in what I've done?
Richard
On Dec 18, 2013, at 6:38 PM, Gábor Lehel
Hello,
The upcoming GHC 7.8 recently gave me this error:
Could not deduce (i ~ i1) from the context (f1 i ~ f i1)
Which is strange to me: shouldn't (f1 i ~ f i1) exactly imply (f1 ~ f, i ~ i1)? (Or with nicer variable names: (f a ~ g b) => (f ~ g, a ~ b)?)
When I inquired about this in #haskell on IRC, a person going by the name xnyhps had this to say:
I've also noticed that, given type equality constraints are never decomposed. I'm quite curious why.
and later:
It's especially weird because a given f a ~ g b can not be used to solve a wanted f a ~ g b, because the wanted constraint is decomposed before it can interact with the given constraint.
I'm not quite so well versed in the workings of GHC's type checker as she or he is, but I don't understand why it's this way either.
Is this a relic of https://ghc.haskell.org/trac/ghc/ticket/5591 and https://ghc.haskell.org/trac/ghc/ticket/7205? Is there a principled reason this shouldn't be true? Is it an intentional limitation of the constraint solver? Or is it just a bug?
Thanks in advance, Gábor
P.S. I got the error on this line: https://github.com/glaebhoerl/type-eq/blob/master/Type/Eq.hs#L181, possibly after having added kind annotations to `InnerEq` (which also gets a less general kind inferred than the one I expect). If it's important I can try to create a reduced test case. _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users