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
