[emillon]

Yes. For example, if you generalize reference values, you can type ref [] as ∀a. (a list) ref, then store [4] to it, then retrieve a float from the head of the stored list, thus breaking the type system. It is a bit similar to array type variance problem that struck Java. One solution is to distinguish between syntactic forms that may allocate memory (eg, function applications) and the ones that can not (eg, abstractions, constants, variables), and only generalize the latter ones.

(Operationally speaking, the two forms (let and abs+app) are always equivalent, though).

[groovy2shoes]

Thank you, that was a much more detailed response than I was expecting.

Would it be correct to assume, then, that a pure ML would allow HM to be trivially modified to support the equivalence?