How one does prove that if algorithm W failed for a given program $e$ and context $\Gamma$, then there is no substitution $S$ and type $\tau$ such that $S\Gamma \vdash e : \tau$ ?
The original paper states that from the completeness proof one can derive that "it is decidable whether $e$ has any type at all under the assumptions $\Gamma$". However, I didn't found this proof in the literature.
The algorithm W has some failures cases: the unification algorithm failed, an identifier was not found in the context, a recursive call failed, etc.
I more interested in the hard cases, the easy ones I can do myself.
One hard case seems to be the failure of the unification. In this case we know about the soundness and completeness of both recursive calls and, also, the non-existence of a unifier for $S_2\tau_1$ and $\tau_2\rightarrow \alpha$. How those informations can be used to prove $\neg \exists \tau \:S, S\Gamma \vdash e_1 \: e_2 : \tau $ ?
This part of algorithm W may be relevant here:
$W(\Gamma, e_1\: e_2) =$
$\quad (\tau_1,S_1) \leftarrow W(\Gamma, e_1)$
$\quad (\tau_2,S_2) \leftarrow W(S_1\Gamma, e_2)$
$\quad S \leftarrow \mathrm{unify}(S_2\tau_1, \tau_2\rightarrow \alpha)$ where $\alpha$ is fresh
$\quad$return $(S\alpha, S \circ S_1 \circ S_2)$
There are other hard cases, but I will be accepting an answer if it is about at least this one.
EDIT:
In Damas' PhD thesis, the pages 74-82 are the completeness proof of algorithm W. After this proof there are two corollaries about the existence of principal type schemes. After that the thesis changes to subjects no related to my question.
