Scoped type variables

[Simon Peyton-Jones]

| > 	g =3D \x::(Int,Bool) -> let-type (a,b) =3D (Int,Bool) in e
| >=20
| > But notice that the RHS of a pattern-matching let-type is=20
| statically=20
| > guaranteed to have the right shape.  So I don't allow
| >=20
| > 	let-type (a,b) =3D c in ...
| >=20
| > (where c is  a type variable).
|=20
| Really? I disagree. Making pattern type sygnatures perform=20
| unification of the variable with the supplied signature is=20
| useful for resolving ambiguities, and backward-compatible=20
| (valid programs will remain valid), and doesn't allow=20
| "unwanted generality" to cause trouble (when an expression=20
| has a more general type than needed).

I was meaning in the translation into System F of the program.
Under my proposal (=3D yours) if one writes

	f (x::(a,b)) =3D e

then f is forced to have type

	f :: (T1, T2) -> ...

for some T1, T2.  In saying that let-type can't pattern-match against
a type variable c, I'm just saying that f cannot have type

	f :: forall c. c -> ....

I think I just didn't express myself well enough.

Simon