So here is the offending program: class IsNil a where isNil :: a -> Bool instance IsNil [b] where isNil [] = True isNil _ = False f x y = let g = isNil in (g x, g y) The monomorphism restriction applies to the binding of "g" since there is no type signature. Thus it is not legal to derive "forall a . IsNil a => a -> Bool", but two legal possibilities are - forall b . [b] -> Bool, and - a -> Bool (without quantification and with "IsNil a" among the predicates). These two choices lead to different types for "f": - forall a b . [a] -> [b] -> (Bool,Bool), and - forall a . IsNil a => a -> a -> (Bool,Bool) Interesting. Every now and then I propagate for replacing the MR by two forms of binding: pat = expr -- call by NAME binding, fully polymorphic and overloaded pat := expr -- call by NEED binding, completely monomorphic The point is to make the programmer aware of when monomorphism applies, so its consequences are not surprising, and also aware (with an = binding) that there is a risk of recomputation. It sounds as though Clean has adopted a similar idea. With "g = isNil", the type of f becomes forall a b. (IsNil a, IsNil b) -> a -> b -> (Bool, Bool) With "g := isNil", it becomes forall a. IsNil a => a -> a -> (Bool, Bool) The two incomparable types for f become types of two different programs; problem solved (in this example at least). Karl-Filip, would this idea restore the principal type property in general? John Hughes