> 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 al

> 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. [0]: https://dl.acm.org/doi/pdf/10.1145/3409006 https://dl.acm.org/doi/pdf/10.1145/3409006