Some points about type checking of simply typed $\lambda$-calculus?
Your example is poorly chosen. In $(\lambda x : \mathsf{bool} . x) \, \mathsf{true}$ you can obviously read off the type from the $\lambda$-abstraction because it tells you that $x$ should have type $\mathsf{bool}$. A more relevant example is
$$
((\lambda f : \mathsf{bool} \to \mathsf{bool} . f) (\lambda x : \mathsf{bool} . x)) \, \mathsf{true} : \mathsf{bool}
$$
Now we are faced with determining $T$ by looking at $(\lambda f : \mathsf{bool} \to \mathsf{bool} . f) (\lambda x : \mathsf{bool} . x)$.

The usual algorithm to be used for this sort of thing is bidirectional typechecking: some terms have their types checked but others have their types inferred. No unification is required, because all types are inferred immediately. (Unification happens when we postpone decisions until a later time.)