What OCaml's type checker do is a little bit fancier: Damas-Milner type inference uses an "occurs check" to prevent the type equation solver from unifying a ty

What OCaml's type checker do is a little bit fancier: Damas-Milner type inference uses an "occurs check" to prevent the type equation solver from unifying a type variable with a compound type expression containing the same variable. The "obviously correct" way to perform this check is eagerly - as soon as possible. However, performance-wise, delaying the occurs check can speed up the inference process - and this is exactly what OCaml does. The downside is that the resulting algorithm is quite involved, because the solver can now run into type expressions containing cycles, so naively recursively walking type expressions can cause an infinite loop.