Also, I think one should not call it Hindley-Milner. A key clever part of the HM algorithm is how it infers types for polymorphic functions, which this code doe

Also, I think one should not call it Hindley-Milner. A key clever part of the HM algorithm is how it infers types for polymorphic functions, which this code doesn't do. For just the idea in this post, I suggest calling it something like "unification-based type inference", or "type inference using equational constraints".