The reason mentioned ("since we can cause the type checker to loop infinitely") is not a proof of undecidability, but merely a proof that the OCaml compiler is not an algorithm that decides type-checking.
Thanks, I've updated the description to mention the undecidable problem, and not an implementation issue