Decidability of type inference and type checking in MLTT
Certainly the decision problem


  Given a (pre-)term $a$ Is there a type $A$ such that $\vdash a :A$ is derivable in MLTT?


Sometimes written $\vdash a\ :\ ?$ (and called the type inference problem) is decidable, which is to say it doesn't matter whether $a$ is well-typed or not to get an answer. Indeed, all proof checkers based on MLTT implement some version of this decision algorithm!

Obviously, the problem in a non-empty context ($\Gamma\vdash a\ :\ ?$) is decidable as well, usually you need to solve the latter to solve the former.

This should answer questions 1 and 2. The algorithm does not involve normalizing $a$, which in general would be bad news, since it is undecidable whether an untyped term normalizes to anything. However the type checking algorithm does involve normalizing types, which are by construction well-typed themselves.

As a result, normalization of well-typed terms is a necessary condition for the type inference problem to be decidable.

You might want to check Nordström, Petersson and Smith for an introduction.



I'm not aware of any generic description of a type inference algorithm for normalizing type theories, though Pollack gives a pretty good overview (though the state of the art has improved) in Typechecking in Pure Type Systems.