The HM type system is designed to be as fast and efficient as possible. And the OCaml typechecker is quite optimized (sometimes to the detriment of readability)

The HM type system is designed to be as fast and efficient as possible. And the OCaml typechecker is quite optimized (sometimes to the detriment of readability). Outside of GADTs heavy code, it feels unlikely to me that the exhaustiveness check matters much to the compilation time. To add some data to the discussion, I have been recently measuring the compilation profile of some OCaml libraries, and the average time spent in the typechecker is around 40% (https://www.polychoron.fr/ocaml/2021/08/19/measuring_compilation_times.html#compilation-profile https://www.polychoron.fr/ocaml/2021/08/19/measuring_compila...). Thus the complexity of the OCaml type system can only have a limited effect on OCaml compilation time. And this measure does include interface files, where the compilation pipeline is reduced to just parsing, typechecking, and dumping the computed file to the disk.