I wrote:
What I don't like is that given a signature like
x :: a -> a
there's no way to tell, looking at it in isolation, whether a is free or bound in the type. [...]
Here's a completely different idea for solving this. It occurs to me that there isn't all that much difference between capitalized and lowercase identifiers in the type language. One set is for type constants and the other for type variables, but one man's variable is another man's constant, as the epigram goes. In Haskell 98 type signatures, the difference between them is precisely that type variables are bound within the type, and type constants are bound in the environment. Maybe scoped type variables should be capitalized. At the usage point this definitely makes sense: you really shouldn't care whether the thing you're pulling in from the environment was bound at the top level or in a nested scope. And implicit quantification does the right thing. As for binding, I suppose the simplest solution would be explicit quantification of the capitalized variables, e.g. f :: forall N. [N] -> ... f x = ... or f (x :: exists N. [N]) = ... Really, the latter binding should be in the pattern, not in the type signature, but that's trickier (from a purely syntactic standpoint). What do people think of this? I've never seen anyone suggest capitalized type variables before, but it seems to make sense. -- Ben