[MLton] free type variables in datatype decs

[Stephen Weeks]

I don't see the mistake in the Definition that allows either Claudio's
or Andreas's example.  Page 21 of the Definition says

  Although not assumed in our definitions, it is intended that every
  context C = T,U,E has the property that tynames E <= T.  Thus, T may
  be thought of, loosely, as containing all the type names which "have
  been generated".

and further says

  the following precise result may easily be demonstrated:

  Let S be a sentence T,U,E |- phrase ==> A such that tynames E <= T
  and let S' be a sentence T',U',E' |- phrase' => A' occurring in a
  proof of S; then also tynames E' <= T'

So, when a rule in the Definition has a side constraint 

 t not in (T of C)

if their property is indeed maintained, then the side constraint
implies 

  t not in tynames C

That is, the existing side constraint is stronger than the one being
proposed to replace it.  Both examples seem to be relying on reaching
a situation where the property is false, but I can't see how that
would happen.  I agree that, given the clear statement of the intended
property in the Definition, it would be an error if one could reach
such a situation.

Take Andreas's example.  Let e be

  (let datatype t = C of string in r := SOME (C "1") end,
   let datatype t = C of int in case !r of SOME (C n) => n+1 end)

The instantiation of rule 14 is

   C |- r ==> (VE, t option ref)   
   C + VE |- e ==> unit * int  
   tynames VE <= T of C
  --------------------------------------------
   C |- r => e ==> t option ref -> unit * int

If you're going to assign r the type "t option ref", then VE(r) = t
option ref, hence t is in tynames VE and the side constraint forces t
to be in T of C.  Then, in the proof for e, the side constraint on
rule 17 makes it impossible to choose t as the type name for any
datatype.