Scoped type variables

[Simon Peyton-Jones]

| I think we should "do the simplest thing that could possibly work",
| and then see if we really need more.  By "work", I mean a compatible
| extension of H98 that makes it possible to add type signatures for
| local bindings (which isn't always possible in H98).  How about:
| 
|  * no implicit binding of type variables: to bind, use "forall".
| 
|  * pattern type annotations allowed only at the top level of pattern
|    bindings and lambda arguments (not on sub-patterns or arguments of
|    function bindings).
| 
|  * no result type annotations (except on pattern bindings, where
they're
|    equivalent to top-level pattern type annotations).
| 

I agree with the "simplest thing" plan.  But if HPrime is to include
existentials, we MUST have a way to name the type variables they bind,
otherwise we can't write signatures that involve them.  Stephanie and
Dimitrios and I are working on this scheme:

* Scoped type variables stand for type *variables*, not types.

* Type variables are brought into scope only by one of two ways:
   a) The forall'd variables of a declaration type signature
	  f :: forall a b. <type>
            f x y = e

   b) A pattern type signature may bring into scope a skolem bound
	in the same pattern:
		data T where
		  MkT :: a -> (a->Int) -> T
		f (MkT (x::a) f) = ...

	The skolem bound by MkT can be bound *only* in the patterns that

	are the arguments to MkT (i.e. pretty much right away).

The idea is that scoped type variables can be bound either at, or very
close to, the point at which they are actually abstracted.

This is a good topic to debate.  S+D+I will try to put forth a set of
rules shortly.

Simon