[MLton] Question about Definition of SML :)

[Stephen Weeks]

> > What prevents the type inference from assigning x the type "int list
> > ref", which has no type variables?  I don't see how closure can come
> > into play here.
> 
> Nothing prevents it.

This seems like a problem to me, since the Definition requires if some
elaboration succeeds (i.e. there is an element in the inductively
defined relation), then the type inference should find it.  So, you
have to find some way to prevent the elaboration that avoids type
variables entirely.

> During inference the variable will be free and if the closure binds
> all free type variables as parameters for a resulting type scheme
> then there is no such arbitrary instantiation.  Hence I would judge
> it invalid due to value-restriction and the fact that I insist on
> binding all free type variables explicitly at every closure
> operation.

It makes sense, but I don't quite see how to fit this idea in the
mathematical framework of the Definition.  You seem to need some way
to look at properties of the set of possible elaborations, which is
much more than a side condition on some inference rule.  It also
sounds like there is some similar confusion as Andreas talked about
between type variables as in the Definition and "unknown types" (often
represented or displayed as type variables) used in an implementation.

But I will gladly await your document to see more detail :-).