[rntz]

You could elaborate polymorphic values to type functions; and if you were compiling ML to System F or System F-omega, that is certainly what you would do. But in practice this might produce performance problems (I shouldn't have to call a function every time I use the empty list just because it has polymorphic type!). I must admit I'm not sure what SML and Haskell compilers actually do.

So in some sense the value restriction is there to prevent us from having to make the ugly choice between unsafety on the one hand, and inefficiency and unintuitive behavior on the other.