The variations are in the implementation detail, the type checking algorithm that Kiselyov describes in your link is extensionally equivalent to Algorithm W. OC

The variations are in the implementation detail, the type checking algorithm that Kiselyov describes in your link is extensionally equivalent to Algorithm W. OCaml's type checker is slightly different to HM, but only to deal with the type semantics of things that HM was not originally meant to deal with (like mutable references for instance). The link Kiselyov mentions is between Garbage collection (-ish, really it's more lifetime analysis a la Rust) and when it is appropriate to generalise a free type variable and how they both interact with aliasing. Take the following expression: fun (x) let y = x in y Here's what we expect: * It has type `forall 'a . 'a -> 'a` (Keeping the universal quantification explicit). * The value held in `y` outlives the scope of `y`, because it is aliased in `x`. But the naïve solution results in: * The type `forall 'a 'b . 'a -> 'b` (Any function of this type is pure sorcery) * The value of `y` (and `x`) gets deallocated at the end of `y`'s scope. The solution is that each type variable should keep track of the scope it was introduced in (like de Bruijn indices), and when generalising, we only universally quantify variables at more deeply nested scopes (which corresponds to deallocating unreachable things).