Some kind of local scope in pattern bindings

[lambdageek]

Consider implementing SML data type definitions:

   datatype 'a option = NONE | SOME of 'a

The whole data definition is a pattern in the rest of the module, but the variable a should scope locally over the value constructors which are themselves in scope in the rest of the module.

If we were working with terms, we'd just use a Bind to introduce a scope so that the a ranged over the value constructors.

But since NONE and SOME are constructor names that scope over the rest of the module, what we actually want is to use a LocalBind as a pattern. (This is in some sense a complement to Shift which is all about lifting terms out of scopes whereas this would be limiting the scope of a pattern)