Scoped type variables

[jgbm]

Goal here is to implement scoped type variables a la Gofer.

At the moment, a type signature in a pattern, like

(p :: t) <- x => m

is interpreted as a let binding

p <- (let y :: t ; y = x in y) => m

This works for monomorphic ts; it's completely broken if there are type variables in t, as the type of x will not be as general as t.

The new plan, rather than translating typed patterns into let bindings, is to implement typing for them directly. In

(p :: t) <- x => m

if t matches the type of x, then the resulting substitution is added to the current substitution; otherwise, typing fails.

One decision in the design of scoped type variables is whether type variables in patterns should be treated as patterns (i.e., can be instantiated to non-variable types) or simply as variables. The above design takes the latter approach... so this should type:

f :: #n -> #n 
f (Proxy :: Proxy n) = #n 

but this should not

f :: #5 -> #5 
f (Proxy :: Proxy n) = #n 

We can change this design decision simply by replacing "matches" in the above design with "unifies".

As a follow-on task, we've never had support for proxy patterns, because most uses of them (as in the above) were broken. Now we should be able to support them, allowing:

f :: #n -> #(n+1)
f #n = #(n+1)

In XMPEG, this shouldn't require any new syntax---we just now have type variables in a Gen scoping over the contained expression. Since we've never actually written down a type checker for XMPEG, this is an easy change to make.