Scoped type variables

[Ross Paterson]

On Wed, Feb 08, 2006 at 05:48:24PM -0000, Simon Peyton-Jones wrote:
> | >    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).
> [...]
> 	f (MkT (x::a) (f::a->Int)) = ...
> 
> You can imagine that either (a) both bind 'a' to the skolem, but must do
> consistently; or (b) that (x::a) binds 'a', and (f::a->Int) is a bound
> occurrence.  It doesn't matter which you choose, I think.

Another possibility would be to allow an optional explicit quantifier
before the data constructor, mirroring the old datatype syntax for
existentials:

	data T = forall a. MkT a (a->Int)

	f (forall a. MkT x f) = ...