Ticket created by ~lnde3 on ~bfiedler/typing-is-hard

The word "surprisingly" would require further explanation. While most (all?) dependent type systems have undecidable inference, they generally have decidable type-checking as long as they do not feature non-terminating terms (see e.g. Martin-Löf type theory, and the calculus of constructions).

Ticket created by ~lnde3 on ~bfiedler/typing-is-hard

The first reason mentioned is suspicious: "undecidable, as type checking in System F is undecidable". For a properly annotated version of System F (Church-style), type checking is decidable, while type inference is not. For Curry-style System F, both are undecidable.

Ticket created by ~lnde3 on ~bfiedler/typing-is-hard

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.