[MLton] Bug with "polymorphic" exns

[Matthew Fluet]

> > I recently discovered that MLton rejects the following program:
> > 
> >    val x = let exception E of 'a in () end;
> > 
> > Although not very useful code, it should be accepted.
> 
> I disagree that it should be accepted.  The type variable 'a is
> implicitly bound at the outermost val declaration (val x = ...), and
> let expressions are expansive.  Hence, the value restriction requires
> the program to be rejected.  MLton's error message correctly indicates
> the problem, although it doesn't explicitly mention the value
> restriction because I felt it was too technical of a term to appear in
> an error message.
> 
> Error: z.sml 1.9.
>   Can't bind type variable: 'a.
>     in: val 'a x = let exception E of 'a in () end

I think Andreas is right.  At first, I thought along your reasoning above, 
that let expressions are expansive.  But, the point is that the type of 
the let expression (namely, unit) does not mention the type variable.  
Hence, the consequent:

C |- val 'a x = let exception E of 'a in () end => VE' in Env

is derivable by Rule 15 as:

U = tyvars('a) 
(* U = {'a} *)
C + U |- x = let exception E of 'a in () end => VE
(* VE = {x |-> (([],unit), v)} *)
VE' = Clos_{C,let exception E of 'a in () end} VE 
(* VE' = {x |-> (([],unit), v)} *)
U \cap tyvars(VE') = {}
(* {'a} \cap {} = {} *)


Contrast this with

C |- val 'a x = let exception E of 'a in fn x => E x end => VE' in Env

which is _not_ derivable by Rule 15:

U = tyvars('a) 
(* U = {'a} *)
C + U |- x = let exception E of 'a in fn x => E x end => VE
(* VE = {x |-> (([],'a -> exn), v)} *)
VE' = Clos_{C,let exception E of 'a in fn x => E x end} VE 
(* VE' = {x |-> (([],'a -> exn), v)} *)
U \cap tyvars(VE') <> {} (*!!!*)
(* {'a} \cap {'a} = {'a} *)