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))
Here's a simplified version. h :: (Show ha) => t -> ha h b = g (h b) Same problem occurs. Though this is strange. Consider type inference for h b = g (h b) We generate the following constraints: th = tb -> ga, Show ga -- results from g (h b) th = tb -> gb -- taking into account h b = g (h b) In case of h :: (Show ha) => t -> ha h b = g (h b) we additionally generate th = t -> ha, Show ha Overall, we find th = tb -> ga, Show ga th = tb -> gb, th = t -> ha, Show ha (*) Note that this implies ga=ha, gb=ha The error message Ambiguous type variable(s) `ha' in the constraint `Show ha' arising from use of `g' at HaskellMay03.hs:16 In the definition of `h'': g (h' b) suggests that ghc does not apply the unifier ha=ga. I suspect the type computed out of the constraints from (*) is as follows: (Show ga, Show ha) => t -> ha Indeed hugs says ERROR HaskellMay03.hs:13 - Cannot justify constraints in explicitly typed binding *** Expression : h *** Type : Show a => b -> a *** Given context : Show a *** Constraints : Show c That is, the type (Show ga, Show ha) => t -> ha does not conform to the annotation (Show ha) => t -> ha. In case we use scoped type variables h2:: (Show t2) => t1 -> t2 h2 b :: g1a = g ((h2 b)::g1a) we impose some additional constraints (ga=g1a, ha=g1a). This seems to resolve the problem, though, as my above calculation shows there shouldn't be a problem in the first place. E.g. Chameleon accepts without problem h :: (Show ha) => t -> ha h b = g (h b) or h :: (Show ha) => t -> ha h b = g ((h b)::ha) This is the Chameleon equivalent to h2. Scoped type variables in Chameleon refer to type annotations. You can try this out by calling chameleon -d HaskellMay03.hs where HaskellMay03.hs = hconstraint Show -- Chameleon does not know the Prelude. -- We have to introduce type class constraints -- explicitely g:: (Show ga) => ga -> gb g = undefined h :: (Show ha) => t -> ha h b = g (h b) h' :: (Show ha) => t -> ha h' b = g ((h' b)::ha) Martin