[MLton] free type variables in datatype decs

Matthew Fluet fluet@cs.cornell.edu
Thu, 3 Feb 2005 14:42:38 -0500 (EST)


> > 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.

They also left out type declarations, for which MLton infers scope:

val id = fn (x : 'a) =>
  let type t = 'a
  in x : t
  end