Lambda the Ultimate

HMF: Simple type inference for first-class polymorphism - Daan Leijen, Draft April 8, 2008.

HMF is a conservative extension of Hindley-Milner type inference with first-class polymorphism and regular System F types. The system
distinguishes itself from other proposals with simple type rules and a very simple type inference algorithm that is just a small extension
of the usual Damas-Milner algorithm. Given the relative simplicity and expressive power, we feel that HMF can be a very attractive
type system in practice. There is a reference implementation of the type system available at: http://research.microsoft.com/users/daan/pubs.html.

An excellent paper even in its current draft form. I also placed this under the learning category, because Daan's writing style is lucid enough that the concepts can be understood by relative newcomers to the field of type theory