Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the so called Subject Reduction Property and the fact that any typable term is strongly $\beta$-normalising)

- If $\tau$ has an inhabitant (i.e. $\varnothing \vdash M : \tau$ for some $M$), 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 = 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 = \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: what'sis 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...). There must be something that I don't see.?

Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the so called Subject Reduction Property and the fact that any typable term is strongly $\beta$-normalising)

- If $\tau$ has an inhabitant (i.e. $\varnothing \vdash M : \tau$ for some $M$), 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 = 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 = \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: what's wrong in the above reasoning? 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...). There must be something that I don't see.

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 = 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 = \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...)?