Scoped type variables

[Ben Rudiak-Gould]

Simon PJ thinks that Haskell' should include scoped type variables, and I 
tend to agree. But I'm unhappy with one aspect of the way they're 
implemented in GHC. 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. Even looking at the context it can be hard to tell, 
because GHC's scoping rules for type variables are fairly complicated and 
subject to change. This situation never arises in the expression language or 
in Haskell 98's type language, and I don't think it should arise in Haskell 
at all.

What I'd like to propose is that if Haskell' adopts scoped type variables, 
they work this way instead:

    1. Implicit forall-quantification happens if and only if the type does
       not begin with an explicit forall. GHC almost follows this rule,
       except that "forall." (with no variables listed) doesn't suppress
       implicit quantification---but Simon informs me that this is a bug
       that will be fixed.

    2. Implicit quantification quantifies over all free variables in the
       type, thus closing it. GHC's current behavior is to quantify over
       a type variable iff there isn't a type variable with that name in
       scope.

Some care is needed in the case of class method signatures: (return :: a -> 
m a) is the same as (return :: forall a. a -> m a) but not the same as 
(return :: forall a m. a -> m a). On the other hand the practical type of 
return as a top-level function is (Monad m => a -> m a), which is the same 
as (forall m a. Monad m => a -> m a), so this isn't quite an exception 
depending on how you look at it. I suppose it is a counterexample to my 
claim that Haskell 98's type language doesn't confuse free and bound 
variables, though.

If rule 2 were accepted into Haskell' and/or GHC, then code which uses 
implicit quantification and GHC scoped type variables in the same type would 
have to be changed to explicitly quantify those types; other programs 
(including all valid Haskell 98 programs) would continue to work unchanged. 
Note that the signature "x :: a", where a refers to a scoped type variable, 
would have to be changed to "x :: forall. a", which is potentially 
confusable with "x :: forall a. a"; maybe the syntax "forall _. a" should be 
introduced to make this clearer. The cleanest solution would be to abandon 
implicit quantification, but I don't suppose anyone would go for that.

With these two rules in effect, there's a pretty good case for adopting rule 3:

    3. Every type signature brings all its bound type variables into scope.

Currently GHC has fairly complicated rules regarding what gets placed into 
scope: e.g.

     f :: [a] -> [a]
     f = ...

brings nothing into scope,

     f :: forall a. [a] -> [a]
     f = ...

brings a into scope,

     f :: forall a. [a] -> [a]
     (f,g) = ...

brings nothing into scope (for reasons explained in [1]), and

     f :: forall a. (forall b. b -> b) -> a
     f = ...

brings a but not b into scope. Of course, b doesn't correspond to any type 
that's accessible in its lexical scope, but that doesn't matter; it's 
probably better that attempting to use b fail with a "not available here" 
error message than that it fail with a "no such type variable" message, or 
succeed and pull in another b from an enclosing scope.

There are some interesting corner cases. For example, rank-3 types:

     f :: ((forall a. a -> X) -> Y) -> Z
     f g = g (\x -> <exp>)

should a denote x's type within <exp>? It's a bit strange if it does, since 
the internal System F type variable that a refers to isn't bound in the same 
place as a itself. It's also a bit strange if it doesn't, since the 
identification is unambiguous.

What about shadowing within a type:

     f :: forall a. (forall a. a -> a) -> a

I can't see any reason to allow such expressions in the first place.

What about type synonyms with bound variables? Probably they should be 
alpha-renamed into something inaccessible. It seems too confusing to bring 
them into scope, especially since they may belong to another module and this 
would introduce a new notion of exporting type variables.

I like rule 3 because of its simplicity, but a rule that, say, brought only 
rank-1 explicitly quantified type variables into scope would probably be 
good enough. Rules 1 and 2 seem more important. I feel like a new language 
standard should specify something cleaner and more orthogonal than GHC's 
current system.

-- Ben

[1]http://www.mail-archive.com/glasgow-haskell-users@haskell.org/msg09117.html