> OCaml generalization is based on tracking of so-called levels of a type.
The level tracking reminds me of a recent paper exploring SimpleSub[0], a simpler alternative of adding subtyping to ML-style type systems. It also gets rid of the algorithm W's repeated generalization (introducing foralls and turning a type into a polytype) and instantiation (changing the universally quantified type variables to fresh type variables). They have slightly different operations on levels, e.g. extrude. I wonder if this level tracking is independently invented again.