Sorry, but I cannot resist to mention an alternative language construct to scoped type variables which gives you the same power of annotating any subexpression with type information. I did mention it in my ICFP 2001 paper on Compositional Explanations of Types as a side note. The nice property of this language construct is that all type variables scope only over a single type; you never have to look if the same type variable appears somewhere else far away in your program. The idea is that a type may contain part of a type environment (so actually it is no longer a type but a typing). This typ environment constructs the relation to other types. Instead of f :: forall a. [a] -> ... f xs = ... where g :: a -> [a] g x = x:xs you write f :: [a] -> ... f xs = ... where g :: (xs::[b]) => b -> [b] g x = x:xs So (xs::[b]) is this new type environment that is part of the type of g. Whether you want to write it similar to a class context, is a matter of taste. This extended type (typing) is the principal monomorphic typing for the function g. Every subexpression has a principal monomorphic typing and hence you can annotate any expression with a typing. Type variables always scope only over a typing. This system of typings works fine for the Hindley-Milner system and also for Haskell 98 classes. I have to admit that I never looked beyond; so I don't know which problems may crop up for rank-n, existentials etc. Ciao, Olaf