ML type systems and Hindley-Milner type inference

Two texts I've come across in the last few days dealing with type systems for ML-like languages and Hindley-Milner type inference.

First, from a rather simple question about principal typings and principal types in the Caml list came a link to the paper ML Has Principal Typings by Carlos Camarão and Lucília Figueiredo; it shows a type system for ML that has principal typings, whereas the usual Damas-Milner type system found in ML languages has not.

Then, LtU links today to A modern eye on ML type inference, some seemingly interesting lecture notes that explain Hindley-Milner type inference in current terms, including extensions. I didn't read it yet, but will do.