The OCaml type checker uses Didier Rémy’s efficient method of type generalization to avoid scanning the type environment and infer types accurately and quickly. Rémy’s algorithm views generalization as dependency tracking, similar to automated memory management techniques like regions and generational garbage collection. It is intriguing how the algorithm smoothly extends to various type-checking tasks, including MLF. Unfortunately, the algorithm is little known and underdocumented, yet it plays a crucial role in the OCaml type checker’s efficiency. By understanding Rémy’s algorithm, developers can decipher and improve upon the workings of the OCaml type checker.
https://okmij.org/ftp/ML/generalization.html