I am implementing the techniques described in the classic Local Type Inference paper. Specifically, I am implementing the type argument synthesis algorithm from section 3.
My algorithm seems to mostly work, but it doesn’t seem to produce reasonable results when a quantified type variable appears in the result of a function, but not in its arguments. For context, I’ve reproduced the $\text{App-InfAlg}$ rule here:
$$ \dfrac{\begin{align}\tt\Gamma \vdash f \in All(\overline{X}) \overline{T} \rightarrow R \qquad &\tt \Gamma \vdash \overline{e} \in \overline{S} \qquad \lvert\overline{X}\rvert > 0\\ \tt\emptyset \vdash_\overline{X}\overline{S} <: \overline{T} \Rightarrow \overline{C}&\qquad\tt \sigma \in \bigwedge \overline{C} \Downarrow R \end{align}} {\tt\Gamma \vdash f(\overline{e}) \in \sigma R \Rightarrow f[\sigma \overline{X}](\overline{e})} (\text{App-InfAlg}) $$
The most important piece here is the $\tt\emptyset \vdash_\overline{X}\overline{S} <: \overline{T} \Rightarrow \overline{C}$ premise, which invokes the constraint generation algorithm. Importantly, though, it only generates constraints using $\tt\overline{S}$ and $\tt\overline{T}$, which correspond to the argument types (that is, the types to the left of the arrow). This is problematic for types like this, which include type variables that only appear in the result:
$$ \tt All(X, Y)(X) \rightarrow Y $$
Or, even more simply:
$$ \tt All(X)() \rightarrow X $$
In this case, my implementation happily infers the type of the above two functions to be $\tt Y$ and $\tt X$, respectively, which are clearly not valid types, since they are type variables that have escaped their scope!
My guess is that my implementation is wrong, and the algorithm accounts for this case. In that situation, I would expect the algorithm to either reject the applications or infer $\tt Bot$ as the result type. However, I don’t see how this could possibly be accounted for, since the algorithmic inference rule only uses $\tt R$ for the purposes of turning the constraints $\overline{C}$ into the substitution set $\sigma$.
How does the algorithm handle this situation?