Consider the basic system of simple types usually known as TAλ. One can prove that (as a consequence of the so called Subject Reduction Property and the fact that any typable term is strongly β-normalising)
If τ has an inhabitant, then it has one in β-normal form.
It follows that given an inhabitation problem Γ ⊢ X : τ we can effectively construct an algorithm that nondeterministically guesses step by step the shape of a normal solution: either (i) X is xY_1...Y_n or (ii) X is λz.Y:
(i) If for some n ≥ 0 there a judgment x : σ_1 → ... → σ_n → τ in Γ, then nondeterministically select it, set X = xY_1...Y_n and (only if n > 0) consider parallel problems Γ ⊢ Y_1 : σ_1,...,Γ ⊢ Y_n : σ_n
(ii) If τ is τ_1 → τ_2, then for a fresh variable z, set X = λz.Y and consider the problem Γ, z : τ_1 ⊢ Y : τ_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 τ. 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.
Sorry, I'm not used to unicode and SO doesn't support LaTeX. I also asked the same question on MO https://mathoverflow.net/questions/140045/is-there-an-easy-decision-algorithm-for-the-inhabitation-problem-for-simple-type, but the lambda calculus group doesn't seem too active there.