My 2¢ from an interactive theorem proving perspective: In so-called computational type theory, typechecking is indeed allowed to be undecidable, and you get a lot of cool expressive power (e.g. well-behaved quotients and subtypes) as a result. This was one of the big ideas behind NuPRL back in the day, and Istari[0] more recently.

[0] www.istarilogic.org