Scoped type variables

[Mark P Jones]

Hi Simon!

| This is the message that Marcin referred to, proposing a change in
| the semantics of scoped type variables.  I may just go ahead and
| implement it in GHC.   (The implementation is easy: delete a couple
| of lines; and I guess the same is so for Hugs.  The question is =
whether
| it's a desirable change.)

I think that it is an undesirable change.  For example, the type
theoretic and practical implications of the current semantics are
known quantities.  I'm not aware of similar foundations to support
the new semantics.  Nor have I seen any believable motivation for
the change.  For example:

| I must say that I agree with Marcin's point.  When we write
| 	f x =3D e
| we mean that x is a name for whatever argument f is given.   Marcin
| argues that the same should apply for=20
| 	f (x :: (a,b)) =3D e
| Namely, that x is a name for the argument, a is a name for the type of
| the fst of x, and slly b.
|=20
| Arguments in favour:
| 	- It's more like term-variable pattern matching

Term variables in a pattern are binding occurrences, but type
variables are not.  Making the latter look more like the former
would appear to be a recipe for unnecessary confusion given that
that they are actually different.

(As an aside, pushing an argument like the above, you might also
argue that when we write "f x =3D e" we mean that "f" is a name for
whatever function "x" is passed to as an argument.  I'm sure we
can all agree here: that would definitely be "slly"!)

There's good precedent for the current semantics, both in practice
(e.g., Standard ML) and in theory (e.g., typed lambda-calculi).  It
would be a mistake to switch to an untested and unusual semantics,
especially without compelling motivating examples.

All the best,
Mark