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).
Thanks for your thoughts. I've detailed the reason why I find it surprising (namely naïve implementations of dependent types have undeciable type-checking).