There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why things work out all right when type-checking in a "standard" dependent type theory (I'll be deliberately vague, since these issues tend to crop up regardless):
Fact 1: If ${\cal D}$ is a derivation of $\Gamma\vdash t:A$, then there is a derivation ${\cal D}'$ of $\Gamma \vdash A:s$ for some kind $s$, and for every subterm $u\leq t$, there is some type $B$, a context $\Delta$ and a derivation $\cal D''$ of $\Delta\vdash u:B$.
This nice fact is somewhat hard to prove, and offset by a pretty nasty counter-fact:
Fact 2: In general, $\cal D'$ and $\cal D''$ are not sub-derivations of $\cal D$!
This depends a bit on the precise formulation of your type system, but most "operational" systems implemented in practice do satisfy Fact 2.
This means that you cannot "pass to sub-terms" when reasoning by induction on derivations, or conclude that the inductive statement is true about the type of the term you're trying to prove something about.
This fact bites you quite harshly when trying to prove seemingly innocent statements, e.g. that systems with typed conversion are equivalent to those with untyped conversion.
However, in the case of type inference, you can give a simultaneous type and sort (the type of the type) inference algorithm by induction on the structure of the term, which may involve a type-directed algorithm as Andrej suggests. For a given term $t$ (and context $\Gamma$, you either fail or find $A, s$ such that $\Gamma\vdash t:A$ and $\Gamma\vdash A : s$. You do not need to use the inductive hypothesis to find the latter derivation, and so in particular you avoid the problem explained above.
The crucial case (and the only case which really requires conversion) is application:
infer(t u):
type_t, sort_t <- infer(t)
type_t' <- normalize(type_t)
type_u, sort_u <- infer(u)
type_u' <- normalize(type_u)
if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
return B, sort_t (or the appropriate sort)
else fail
Every call to normalize was done on well-typed terms, as this is the invariant for infer's success.
By the way, as it is implemented, Coq does not have decidable type checking, as it normalizes the body of fix statements before attempting to type check them.
At any rate, the bounds on the normal forms of well-typed terms are so astronomical, that the decidability theorem is mostly academic at this point anyways. In practice, you run the type checking algorithm for as long as you have patience for, and try a different route if it hasn't finished by then.
