I think I can explain why Haskell compilers behave as they do with regards to Levent Erkok's problem, and how to fix it. It seems the compilers are more powerful than we imagine, but are compelled to conceal their power and to lie to us. First, let us distill the problem to the following few lines:
f:: (Show fa) => fb -> fa f = undefined
g:: (Show ga) => ga -> gb g = undefined
-- h:: (Show fa) => t -> fa h b = f (g (h b))
This code loads and checks. If we ask the compiler for the type of h, we get the type of h that was commented out in the code above. If we remove the comment and reload the code, we get an error: Ambiguous type variable(s) `fa' in the constraint `Show fa' arising from use of `h' at /tmp/p.lhs:12 In the first argument of `g', namely `(h b)' In the first argument of `f', namely `(g (h b))' This behavior seems rather puzzling: the compiler refuses to accept its own type. The problem is that the compiler is slightly lying to us. When we ask for the type *Main> :type h forall fa t. (Show fa) => t -> fa the real type of h is forall t. t -> (function-of-t) The real type of h is not totally polymorphic : it is dependent! It goes without saying that such types cannot be expressed in Haskell. It is stunning that the compiler managed to infer such a dependent type, albeit it has no way to properly print it. The compiler could have used the following notation: forall fa t | t -> fa. (Show fa) => t -> fa Perhaps even more stunning is that we can test our hypothesis. We can explicitly specify the functional dependence between types. We will use lexically-scoped type variables, described in the eponymous paper by Simon Peyton-Jones and Mark Shields. The following works in GHC 5.04.1, given -fglasgow-exts flag.
h1:: (Show t2) => t1 -> t2 h1 b :: g1a = (f (g ((h1 b)::g1a)))
Original example by Levent Erkok's also works.