Scoped type variables

Mon Dec 20 04:22:15 EST 2004

| Some design choices are unclear, at least to me. First, the
| separation of body and signature. I am used to locally introduced
| identifiers being visible locally too (i.e. requiring minimal
| scrolling through a file). This would break, meaning that I have to
| know which identifier was used in the signature. Related to this, how
| does this work out for signatures of class members and their
| instances, often separated over different files? A change in a type
| variable in a signature in a class inside a library might then break
| my instance of that class. Or is this mechanism only meant for let
| bound values? 

My intention was that in an instance declaration, only the type
variables introduced in the head of the declaration (instance Eq a => Eq
[a] where...) would scope over the bodies.  The class declaration would
be irrelevant.

| The following then also might be admitted:
| 
| 	f :: (forall a . a -> a) -> ...
|          v = f (\x -> x::a)

I'm suggesting *only* the outermost forall'd variables of the
definition. That's bad enough!   Nesting is overkill, and the scoping
rules would be complex to describe.

| Second, for a duplicate introduction of 'a' in:
| 
| 	f :: [a] -> [a]
| 	f (x::a) = <body>
| 
| Is the 'a' introduced in 'f (x::a)' shadowing the 'a' introduced in
| 'f :: [a] -> [a]'? If so, the separation of body and signature is
| slightly less of a problem because the 'a' introduced in the pattern
| will not create a 'duplicate identifier introduction' error message
| or a type mismatch (here between [a] and a).

The rule today in GHC is that a second use of a scoped type variable is
an *occurrence*.  Thus
	f = \(x::a) -> \(y::a) -> ..
the first 'a' binds the a, the second is an occurrence of it.   Yes,
it's a hack.  One could imagine requiring different syntax for the
binding occurrences, for example, but it's a really convenient one, and
hasn't given rise to difficulties that I know of.  So I'm proposing to
stick with it.

Simon