To compute specific type parameters regarding $R$, there is another crucial operation: the change in polarity due to variable substitution.
The polarity of a type variable $X$ in another type expression $R$ describes how the type of the entire expression changes accordingly when the type of that variable becomes larger or smaller.

• Covariant: If $R$ is covariant in $X$, then “becoming larger” of $X$ (becoming a supertype) causes $R$ to also “become larger”. For example, in $T \to X$, $X$ is covariant. If $\mathbb{Z} \lt: \mathbb{R}$, then $T \to \mathbb{Z} \lt: T \to \mathbb{R}$.
• Contravariant: If $R$ is contravariant in $X$, then “becoming larger” of $X$ causes $R$ to “become smaller” (become a subtype). For example, in $X \to T$, $X$ is contravariant. If $\mathbb{Z} \lt: \mathbb{R}$, then $\mathbb{R} \to T \lt: \mathbb{Z} \to T$.
• Invariant: If $R$ is invariant in $X$, then $R$ remains unchanged only if $X$ remains unchanged. Any change results in incomparable outcomes. For example, in $X \to X$, $X$ is invariant.
• Constant: If $R$ is constant in $X$, then changes in $X$ do not affect the type of $R$. Constant types typically refer to those that do not contain variables, such as primitive types or concrete classes.

Currently, our consideration of polarity focuses primarily on function types,
and we only need to pay attention to the position of variables in function types (whether on the left or right of the arrow),
while also considering nested function structures. It is recommended that the reader pause here to think about the design of this algorithm.
Of course, you can also directly expand the code block below to view the specific implementation.

pub fn Type::variance(self : Type, va : Var) -> Variance {
  letrec go = (ty : Type, polarity : Bool) => {
    match ty {
      TyVar(v) if v == va => if polarity { Covariant } else { Contravariant }
      TyVar(_) | TyTop | TyBot => Constant
      TyFun(_, params, ret) => {
        let param_variance = params
          .map(p => go(p, !polarity))
          .fold(init=Constant, combine_variance)
        combine_variance(param_variance, go(ret, polarity))
      }
    }
  }
  and combine_variance = (v1 : Variance, v2 : Variance) => {
    match (v1, v2) {
      (Constant, v) | (v, Constant) => v
      (Covariant, Covariant) | (Contravariant, Contravariant) => v1
      (Covariant, Contravariant) | (Contravariant, Covariant) => Invariant
      (Invariant, _) | (_, Invariant) => Invariant
    }
  }

  go(self, true)
}

At this point, we have fully defined a completely executable algorithm consisting of three steps: “Variable Elimination,” “Constraint Generation,” and “Parameter Calculation.” But how do we ensure that the behavior of this concrete algorithm is entirely consistent with the non-constructive, declarative App-InfSpec specification?

The proof of their equivalence is distilled into a core proposition asserting:

1. If the most general substitution $\sigma_{CR}$ exists, then it is the optimal solution required by the specification.
2. If the most general substitution $\sigma_{CR}$ does not exist, then the optimal solution required by the specification also necessarily does not exist.

Proof Sketch:

• Part 1 (Correctness of the Algorithm): To prove that $\sigma_{CR}$ is optimal, we take an arbitrary other valid substitution $\sigma'$ satisfying the constraints and need to prove $\sigma_{CR}(R) \lt: \sigma'(R)$. Consider constructing a “chain of substitutions” from $\sigma_{CR}$ to $\sigma'$, where each step changes only one variable’s value. For example, $\sigma_0 = \sigma_{CR}$, $\sigma_1 = \sigma_0[X_1 \mapsto \sigma'(X_1)]$, …, $\sigma_n = \sigma'$. Next, we prove that at each step along this path, the resulting type is monotonically non-decreasing, i.e., $\sigma_{i-1}(R) \lt: \sigma_i(R)$. The proof of this step relies directly on the aforementioned polarity definitions. For instance, if $R$ is covariant in $X_i$, our algorithm selected the lower bound $S$, and $\sigma'(X_i)$ must be greater than or equal to $S$. Therefore, by the definition of covariance, the resulting type must “increase.” Similarly, the assertion holds in other cases. Ultimately, by transitivity, we conclude $\sigma_{CR}(R) \lt: \sigma'(R)$, proving the optimality of $\sigma_{CR}$.

• Part 2 (Completeness of Algorithm Failure): When the algorithm fails, it must be because the constraint interval $[S, T]$ for some invariant variable $X_i$ has $S \neq T$. We use proof by contradiction: assume that an optimal solution $\sigma$ still exists under these circumstances. Since $S \neq T$, we can always find another valid substitution $\sigma'$ such that $\sigma(X_i)$ differs from $\sigma'(X_i)$. However, because $R$ is invariant in $X_i$, $\sigma(R)$ and $\sigma'(R)$ become incomparable. This contradicts the assumption that “$\sigma$ is the optimal solution (i.e., it is smaller than all other solutions)”. Therefore, in this case, the optimal solution necessarily does not exist.