[MLton] Bug with "polymorphic" exns

Matthew Fluet fluet@cs.cornell.edu
Mon, 24 Jan 2005 18:01:02 -0500 (EST)

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

Note, that in any situation like this, where (implicit or
explicit) type variables are bound at a val declaration that binds to a 
non-expansive expression whose type does not mention the type variables, 
then within that non-expansive expression, we can substitute an arbitrary 
mono-type (say, unit) for the type variables, without changing the meaning 
of the program.

We cannot substitute away the type variables in the entire valbind, 
because some non-expansive expressions may use the type-variables:

val 'a id = fn (x: 'a) => x
and     x = let exception E of 'a in () end;