If a type theory such as Martin-Löf's dependent type theory (MLTT) is to be used as a foundation for mathematics, decidable type checking is certainly nice to have: it guarantees that for every proof candidate supplied, it can be computed whether the candidate is admissible as a valid proof or not.
However, is the decidability of every possible term truly essential? Are there practically relevant examples of terms for which type-checking is undecidable in, say, extensional MLTT, or does proving the undecidability of extensional MLTT require complicated constructions (as in Gödel's incompleteness theorems)?
In practice, would it not be possible to formalize all constructive mathematics in a proof checker implementing extensional MLTT?