Basically, type checking proceeds in one of two modes: inferring or checking. The former is when there is no signature is given; the latter, if there is a user-supplied signature. GHC can infer ambiguous signatures, but it cannot check them. This is of course very confusing and we need to fix this (by preventing GHC from inferring ambiguous signatures). The issue is also discussed in the mailing list thread I cited in my previous reply.
As the error message demonstrates, the inferred type is not correctly represented - GHC doesn't really infer an ambiguous type, it infers a type with a specific idea of what the type variable should match. Representing that as an unconstrained forall-ed type variable just doesn't seem accurate (as the unconstrained type variable won't match the internal type variable) and it is this misrepresentation of the inferred type that leads to the ambiguity. Here is a variation to make this point clearer: {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-} class Fun d where type Memo d :: * -> * abst :: (d -> a) -> Memo d a appl :: Memo d a -> (d -> a) f = abst . appl -- f' :: forall d a. (Fun d) => Memo d a -> Memo d a f' = abst . (id :: (d->a)->(d->a)) . appl There is a perfectly valid type signature for f', as given in comment, but GHCi gives an incorrect one (the same as for f): *Main> :browse Main class Fun d where abst :: (d -> a) -> Memo d a appl :: Memo d a -> d -> a f :: (Fun d) => Memo d a -> Memo d a f' :: (Fun d) => Memo d a -> Memo d a What I suspect is that GHCi does infer the correct type, with constrained 'd', but prints it incorrectly (no forall to indicate the use of scoped variable). Perhaps GHCi should always indicate in its type output which type variables have been unified with type variables that no longer occur in the output type (here the local 'd'). If ScopedTypeVariables are enabled, that might be done via explicit forall, if the internal type variable occurs in the source file (as for f' here). Otherwise, one might use type equalities. In other words, I'd expect :browse output more like this: f :: forall a d. (Fun d, d~_d) => Memo d a -> Memo d a f' :: forall a d. (Fun d) => Memo d a -> Memo d a making the first signature obviously ambiguous, and the second signature simply valid. Claus