The Hindley-Milner type inference algorithm is popular and practical.
However, since it is based on solving equations between types it has
proven difficult to extend with subtyping, where one must deal with
inequalities rather than equations.
In this talk, I demonstrate a simple language with subtyping, and show
how to infer principal types for it. The syntax, semantics and even
typing rules of this language are exactly those of ML, augmented with
the standard subtyping rule. The novelty appears in the definition of
the set of types themselves: by adopting a more algebraic and less
syntactic approach to constructing the lattice of types, we can build
in enough structure that an analogue of unification can be used to
infer types.