Hi all! I've been spending some time the last year writing up a formalization of the Haskell type system (actually, most of the static semantics). In doing so, I've come across an oddity. It seems that Haskell does not have the principal type property, ie there are Haskell expressions which, in a given typing environment, can be assigned at least two types that are not generic instances of each other but can not be assigned any type more generic that the two. The culprit is the monomorphism restriction. I was kind of surprised, thinking that principal types were likely to hold for Haskell, but it seems not. The monomorphism restriction goes like this in my inference rules: If a declaration group contains a pattern binding with a nonvariable pattern or one where there is no type signature for the variable, then the context parts of the type schemes derived for the bound variables must be empty. The difference to for instance "Typing Haskell in Haskell" is that my formalization is a set of inference rules (starting from the draft static semantics by Peyton Jones and Wadler), so many different types can be derived for the same typing environment and expression, wheras THIH is a program which computes a single type. 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) These two are incomparable (neither is a generic instance of the other). I can not see that it is legal to derive a type for "g" which will allow some type for "f" that is more general than both of these. As far as I can see, the inference algorithm from "Typing Haskell in Haskell" would give the second type, which is also what GHC derives. The trick here is the instance declaration for "IsNil [a]" which has an empty instance context, ie it is not important what the element type is. So, is this already well known in the Haskell community, or is it a new result? Of course, it is not a result until one has *proved* that *no* type more general than the two above is derivable, but it is a strong conjecture. In the "Type Classes in Haskell" paper from TOPLAS, the smaller system without the monomorphism restriction was conjectured to have principal types. Also, the Haskell Report (section 4.1.4) states: "Haskell 's extended Hindley-Milner type system can infer the principal type of all expressions, including the proper use of overloaded class methods (although certain ambiguous overloadings could arise, as described in Section 4.3.4)." But there is no ambiguity involved here. Cheers, /kff Jones: Typing Haskell in Haskell, in Proceedings of the Third Haskell Workshop Hall et al: Type Classes in Haskell, TOPLAS vol 18 no 2 Peyton Jones and Wadler: A Static Semantics for Haskell, draft paper, Glasgow