[lptk]

> It would be difficult to just stumble on a system like Simple-sub without that guidance

Actually, I'm not sure it would be that hard (Simple-sub author here). If you look at the core of the algorithm closely, you'll see it's really not special: you create type variables, add constraints on them, propagate the constraints, and that's mostly it. In fact, it's perfectly in line all previous work on subtyping inference, going back at least to Pottier's 1998 thesis — that thesis already had many ingredients of MLsub. The three big things MLsub brought to the table, in my opinion, were: 1. the idea to coalesce constraint graphs into compact type expressions, which are easier to read and understand; 2. using the algebraic insight to develop an elegant and simple principality proof (but I'm not sure it's really worth it; AFAIK the proof sketch I provided would also work); and 3. to provide a simpler subsumption checking algorithm. Specifically in terms of pure type inference (so, ignoring points 2 and 3), it's possible to imagine making the leap to compact types without the algebra insight. But this is just speculation, and it's of course impossible to tell a posteriori.

> If you want to add subtyping to a language with a more sophisticated type system, or add new features to a language that already has subtyping

In that case I think Simple-sub is a good place to start, as it does not presuppose all the algebraic structure that MLsub does; Simple-sub shows that principal type inference really doesn't need much at all form the type system. Now, you're free to add more structure to your subtyping lattice if you want to be able to simplify types more, and if you want to make checking subsumption easier, but the choice is in your hands.

> you should probably take a long hard look at it from an algebraic point of view to make sure they interact the way you want

That's still definitely true!