Decomposition of given equalities

[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.