Scoped type variables

Fri Dec 17 12:51:03 EST 2004

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