[ehamberg]

> The advantage of this approach would be allowing function overloading (similarly to C++ or Java) informally without interfaces or type classes.

I might be misunderstanding something, but how does this allow function overloading more than ordinary let-polymorphism? Functions can already have a type like, say, ∀a.a→Int. It's also quite common to do type inference in two steps where the first pass creates type variables and a list of constraints. The set of constraints are then passed to a unification algorithm, see e.g. http://www.seas.upenn.edu/~cis552/lectures/stub/FunTypes.htm....

[exDM69]

In a classic Hindley-Milner type inference algorithm, you can't have a function "add(int, int) -> int" and "add(float, float) -> float". E.g. in Haskell, you'd need a type class for this.

Modern functional programming languages use a type inference algorithm more sophisticated than the original H-M algorithm which are more flexible than the original algorithm. The link you gave as an example is Haskell with a handful of language extensions related to the type checker - something entirely different to the H-M algorithm.

There can be other ways of implementing a similar type checker in a different manner, this was just a fun idea I came up with.