Can't deduce f = f₁ from f x = f₁ y?

Question

{-# LANGUAGE GADTs #-}

data Foo x y where
  Composition :: Foo b c -> Foo a b -> Foo a c
  FMap :: Functor f => (a->b) -> Foo (f a) (f b)

asFunction :: Foo a b -> a->b
asFunction (FMap m) = fmap m
-- asFunction (Composition (FMap m) (FMap n)) = fmap m . fmap n
asFunction (Composition m n) = asFunction m . asFunction n

This works as expected... until you uncomment the second clause of asFunction! This is actually just an inlined version of a special case the two other patterns already match, so I'd expect it to be ok. But (ghc-7.6.2, or also ghc-7.4.1)

Could not deduce (f ~ f1)
from the context (b1 ~ f a1, b ~ f b2, Functor f)
  bound by a pattern with constructor
             FMap :: forall (f :: * -> *) a b.
                     Functor f =>
                     (a -> b) -> Foo (f a) (f b),
           in an equation for \`asFunction'
  ...

Why does this happen, and why then not in the other clauses? What exactly should be done to prevent this trouble in more complicated applications?

Answer 1

This may be related to a feature left/right decomposition of coercions that was temporarily removed from GHC's type inference system in order to support more flexible ("unsaturated") type functions, and then reintroduced when it was found to have annoying effects like this.