OK, OK, I yield! This message is about lexically scoped type variables. I've gradually become convinced that if you write f :: [a] -> [a] f x = <body> then the type variable 'a' should be in scope in <body>. At present in GHC you have to write f (x :: [a]) = <body> to bring 'a' into scope. I've fought against this because it seems funny for a 'forall' in a type signature to bring a type variable into scope in perhaps-distant function body, but it's just so convenient and "natural". Furthermore, as Martin Sulzmann points out, you might have type variables that are mentioned only in the context of the type: g :: Foo a b => [a] -> [a] g = ... GHC provides no way to bring 'b' into scope at the moment, and that seems bad design. If I do this, which I'm inclined to, it could break some programs, because (with -fglasgow-exts) all type signatures will bring scoped type variables into scope in their function body. Here's an example that will break f :: [a] -> [a] f x = my_id x where my_id :: a -> a my_id y = y The type signature for my_id will become monomorphic, since 'a' is now in scope, so the application (my_id x) will fail saying can't unify 'a' with '[a]'. In some ways that makes sense. If you used 'b' instead in the defn of my_id, it'd be fine, because my_id would get the type (forall b. b->b). Fixing such breakages is easy. So there it is. Any one have strong opinions? (This is in addition to the existing mechanism for bringing scoped type variables into scope via pattern type signatures, of course.) Simon