Local type argument synthesis when type variable does not appear in arguments

Question

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?

Answer 1

As a prelude, there is some terminological confusion in your question. The issue is about a type variable occurring in a result type of a function. This is fairly minor. A more serious one is when you say "my implementation happily infers the types of the above two functions to be ...". What functions? Functions are terms like (in this case) $\tt fun(x:T)e$ but the rule you quote is actually about function application, i.e. it applies to terms like $\tt f(e)$. Either way, the two things you present are types not terms. What you seem to want to say is: given a function $\mathtt{f}\in\tt All(X)()\to X$, the expression $\tt f()$ seems to have the inferred type $\tt X$.

$\tt \sigma \in \bigwedge \overline{C} \Downarrow R$ implies that $\sigma$ is a map for all the variables in $\tt R$ or else it wouldn't even make sense. Maybe it doesn't make sense, but we see that in the rule you listed the constraint generation step produces a $\mathtt{\bar X}/V$ constraint and the substitution algorithm will thus produce a $\mathtt{\bar X}/V$ substitution which, by definition, has a mapping for each type variable in $\tt \bar X$. I assume your confusion is that you look at the minimal substitution generating algorithm $\sigma_{C\tt R}$ at the bottom of page 11, note that in your second case, for example, the constraint generation step produces an empty set of constraints and thus the "for each constraint" iterates over an empty set producing a substitution with no mappings which presumably would act as the identity. However, this would violate the definition of an $\mathtt{\bar X}/V$ substitution. The detail here is the definition of the empty constraint set. At the beginning of section 3.3 on page 9 it states:

The empty $\mathtt{\bar X}/V$ constraint set, written $\emptyset$, contains the trivial constraint $\tt Bot <: X_\mathit{i} <: Top$ for each variable $\mathtt{X}_i$.

Since the result type is covariant (in a top-level context), we'll get $\tt Bot$ in those cases. In particular, given that $\mathtt{f}\in\tt All(X)()\to X$, the expression $\tt f()$ will have the inferred type $\tt Bot$. The produced substitution $\sigma_{\emptyset\tt R}$ will map $\tt X$ to $\tt Bot$.