Is it impossible to deduce f = f₁ from fx = f₁ y?

Question

{-# LANGUAGE GADTs #-} data Foo xy where Composition :: Foo bc -> Foo ab -> Foo ac FMap :: Functor f => (a->b) -> Foo (fa) (fb) asFunction :: Foo ab -> a->b asFunction (FMap m) = fmap m -- asFunction (Composition (FMap m) (FMap n)) = fmap m . fmap n asFunction (Composition mn) = asFunction m . asFunction n 

This works as expected ... until you uncomment the second asFunction ! This is actually just a built-in version of the special case in which the other two templates already match, so I expect that everything will be alright. 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 (fa) (fb),     in an equation for \`asFunction' ... 

Why is this happening, and why then not in other articles? What exactly needs to be done to prevent this problem in more complex applications?

Answer 1

This may be due to decomposition of forced actions on the left and right, which was temporarily removed from the GHC type output system in order to support more flexible ("unsaturated") type functions, and then reintroduced when it was found to be annoying .