Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the Subject Reduction Property and the fact that any typable term is strongly $\beta$-normalising)
- If $\tau$ has an inhabitant, then it has one in $\beta$-normal form.
It follows that given an inhabitation problem $\Gamma \vdash X : \tau$ we can effectively construct an algorithm that nondeterministically guesses step by step the shape of a normal solution: either (i) $X \equiv xY_1 \dots Y_n$ or (ii) $X \equiv \lambda z.Y$:
(i) If for some $n \geq 0$ there a judgment $x : \sigma_1 \to \dots \to \sigma_n \to \tau$ in $\Gamma$, then nondeterministically select it, set $X \equiv xY_1\dots Y_n$ and (only if $n>0$) consider parallel problems $$\Gamma \vdash Y_1 : \sigma_1, \dots, \Gamma \vdash Y_n : \sigma_n$$ (ii) If $\tau \equiv \tau_1 \to \tau_2$, then for a fresh variable $z$, set $X \equiv \lambda z.Y$ and consider the problem $$\Gamma, z : \tau_1 \vdash Y : \tau_2.$$
Furthermore, since all types in the constraints at each step of the algorithm are proper subtypes of the original input , the number of steps of the algorithm is at most polynomial in the size of $\tau$. Therefore the algorithm above is a decision procedure for the inhabitation problem.
My question is the following: is there something wrong in the above reasoning? Maybe not, but in this case why I've been searching all day for a decision procedure for the inhabitation problem for simple types, but all the proofs I can find are rather long and use complicated machinery (e.g. long normal forms, Curry-Howard isomorphism, etc...)?
