Decidability of dependent typing on primitive recursive languages
Not only is the answer to this question yes, but this is exactly the strategy that modern implementations like Coq and Agda take! To be precise, the type checker has to preform evaluation when deciding definitional equality so it would, if given the right language, be possible to write an infinite loop and ask whether a term was definitionally equal to another term. Because of the way we define definitional equality in most cases, this demands evaluation.
The calculus of constructions (CoC) is actually strongly normalizing. Type checking of CoC is decidable and requires no termination checking. But to make this theory more useful, we add the ability to define inductive types and recursions over them. This way, we get the calculus of inductive constructions (CIC), which Coq is based on.based on). You can view this as a means of adding terms to our language that add computational content that would otherwise not be present.
Note than many inductive types can already be represented in CoC without the aid of CIC, but CoC cannot represent everything CIC can. Coq and Agda both have termination checkers which accept all primitive recursive functions, and both also allow encoding the Ackermann function. You can see more about this in a question I once asked here on a characterization of the class of primitive recursive functions.
Good refrences on Agda's termination checker are

http://www2.tcs.ifi.lmu.de/~abel/foetus/
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker

There is also a lot of work on sized types to provide an alternative to termination checking as well as some work on abstract interpretation based solutions. Currently however, checking for a generalization (see Foetus) of primitive recursion is as far as the state of the art in mainstream implementations goes — at least as far as I am aware.