[MLton] free type variables in datatype decs

[Andreas Rossberg]

I pondered about Claudio's example a bit more. And I believe that the weak
side condition in rule 17 is unsound already, even without any extensions!
If I'm not mistaken, it allows successful elaboration of the following bogus
program:

  (fn r => ( 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
           ) NONE : unit * int

The point is, that rule 17 may choose the same type name for both datatype
declarations, because it is in T of C in neither subproof. And the argument
r can then be assigned type t option ref, as Claudio pointed out.

Can others confirm my reading of the rules? If so, I will add that to the
defects list.