[MLton] free type variables in datatype decs

[Stephen Weeks]

> The simplest example possibly is:
> 
>    datatype t = C of 'a
>    fun cast x = case C x of C x' => x'
>    val ouch = 1 + cast "string"

> My guess is that they simply screwed up the restriction when they added 
> the respective one previously missing for datatype specifications - 
> somebody accidentally did a cut&paste instead of copy&paste.

Plausible.

> As far as I can see, specifying the more liberal rules correctly
> actually requires changing the Definition to do proper binding
> analysis for type variables, instead of vacuously accepting them in
> type expressions and verifying there use after the fact.  In
> particular, this implies a change to rule 44, requiring alpha to be
> in U of C, and to all rules that bind type variables, in order to
> extend U appropriately. I reckon that is what MLton does internally.

MLton has a pass, scope inference, that runs before type inference and
determines the scope of each implicitly-scoped type variable.  That
seems to be what 4.6 specifies, except that 4.6 doesn't state as
clearly as it might that every type variable must be scoped somewhere.
I think it's reasonable to interpret the sentence "we still must
account for the scope of an explicit type variable ..." as implying
this.  Of course there's still the problem that they left out
datatypes from that sentence.

> > MLton implements a fixed version of rule 28 where "Clos" is replaced
> > by "Clos_C", i.e. free type variables aren't closed over, just as in
> > rule 15.
> 
> That does not seem to be what MLton really implements, because it 
> correctly rejects the non-local example as well, where 'a does not 
> appear in C

MLton rejects the non-local example above because scope inference
determines that 'a is not scoped anywhere.