Rather than treating type parameter inference as a search problem of “finding and verifying the optimal solution” among infinite possibilities,
we reframe it as a problem of “solving for unknown boundaries” similar to solving algebraic equations.
Instead of guessing what the type parameters $\overline{X}$ might be,
we derive the conditions $\overline{X}$ must satisfy by analyzing the subtyping relation itself.

Observing that our rules contain subtyping constraints, consider the general case $S \lt: T$,
which inherently implies constraints on its components (including unknown variables).
If $X$ is an unknown variable in $T$, the structure of $S$ necessarily restricts the possible forms of $X$.
Our algorithm transforms this implicit structural restriction into a set of explicit assertions about $X$’s bounds.

However, before systematically extracting these constraints, we must first address a preliminary yet critical challenge related to variable scoping.
If not handled properly, the constraints we generate may themselves be ill-formed.
This challenge motivates the algorithm’s first concrete step: variable elimination.

pub fn Type::promotion(self : Type, v : Set[Var]) -> Type {
  match self {
    TyFun(xs, ss, t) => {
      let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
      let us = ss.map(s => s.demotion(vP))
      let r = t.promotion(vP)
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyTop
    _ => self
  }
}

pub fn Type::demotion(self : Type, v : Set[Var]) -> Type {
  match self {
    TyFun(xs, ss, t) => {
      let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
      let us = ss.map(s => s.promotion(vP))
      let r = t.demotion(vP)
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyBot
    _ => self
  }
}

Constraint generation is the core engine of the local type parameter synthesis algorithm.
After ensuring scoping safety through variable elimination,
this step’s mission is to transform a subtyping judgment—for example,
$S \lt: T$ where $S$ or $T$ contains undetermined type parameters $\overline{X}$—into a set of explicit constraints on these unknowns $\overline{X}$.
We now formally define the structure of constraints in code:

• Constraint: In this system, each constraint takes the form $S_i \lt: X_i \lt: T_i$, specifying both a lower bound $S_i$ and an upper bound $T_i$ for a single unknown type variable $X_i$.

• Constraint Set: A constraint set $C$ is a finite mapping (implementable as a Hash Map in code) from a group of unknown variables $\overline{X}$ to their corresponding constraints. A key invariant is that the bounds ($S_i$, $T_i$) in any constraint must not contain any pending unknown variables (i.e., variables in $\overline{X}$) or any local variables to be eliminated (i.e., variables in $V$). The empty constraint set ($\emptyset$) represents the least restrictive constraint, equivalent to $\bot \lt: X_i \lt: \top$ for each $X_i$.

• Constraint set intersection ($\wedge$) is defined as the intersection of two constraint sets $C$ and $D$, obtained by merging constraints for the same variable. The new lower bound is the least upper bound (join, $\vee$) of the original lower bounds, while the new upper bound is the greatest lower bound (meet, $\wedge$) of the original upper bounds.

struct Constraints(Map[Var, Subtype])

pub fn Constraints::empty() -> Constraints {
  Constraints(Map([]))
}

fn Constraints::items(self : Constraints) -> Map[Var, Subtype] {
  let Constraints(items) = self
  items
}

pub fn Constraints::meet(
  self : Constraints,
  other : Constraints,
) -> Constraints {
  Constraints(
    union_with(self.items(), other.items(), (l, r) => {
      let { l: l1, r: r1 } = l
      let { l: l2, r: r2 } = r
      { l: l1 & l2, r: r1 | r2 }
    }),
  )
}

pub fn meets(c : Array[Constraints]) -> Constraints {
  c.iter().fold(init=Constraints::empty(), Constraints::meet)
}

The constraint generation process is formalized as a derivation relation $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$, meaning: given a set of variables $V$ to avoid, the (weakest) constraint set $C$ on unknown variables $\overline{X}$ required for $S \lt: T$ to hold, where $C$ is the output of this relation.

The algorithm is defined by recursive rules, with key rules as follows (note: we always assume $\overline{X} \cap V = \emptyset$):

• Trivial Cases: When the upper bound of the subtyping relation is $\top$ or the lower bound is $\bot$, the relation holds unconditionally, thus generating an empty constraint set $\emptyset$.
• Upper Bound Constraint: When judging $Y \lt: S$ (where $Y \in \overline{X}$ is an unknown variable and $S$ is a known type), the algorithm generates an upper bound constraint for $Y$.
  $$ \frac{Y \in \overline{X} \quad S \Downarrow^V T \quad \text{FV}(S) \cap \overline{X} = \emptyset}{V \vdash_{\overline{X}} Y \lt: S \Rightarrow \{ \bot \lt: Y \lt: T \}} \quad (\text{CG-Upper}) $$
  Note that the variable elimination operation ($S \Downarrow^V T$) ensures the upper bound $T$ is well-formed.
• Lower Bound Constraint: Dually, when judging $S \lt: Y$, the algorithm generates a lower bound constraint for $Y$.
  $$ \frac{Y \in \overline{X} \quad S \Uparrow^V T \quad \text{FV}(S) \cap \overline{X} = \emptyset}{V \vdash_{\overline{X}} S \lt: Y \Rightarrow \{ T \lt: Y \lt: \top \}} \quad (\text{CG-Lower}) $$
• Function Type: When comparing function types, the algorithm recursively processes parameter and return types, then merges the resulting sub-constraint sets.
  $$ \frac{V \cup \{\overline{Y}\} \vdash_{\overline{X}} \overline{T} \lt: \overline{R} \Rightarrow \overline{C} \quad V \cup \{\overline{Y}\} \vdash_{\overline{X}} S \lt: U \Rightarrow D}{V \vdash_{\overline{X}} \forall \overline{Y}.\overline{R} \to S \lt: \forall \overline{Y}.\overline{T} \to U \Rightarrow (\bigwedge \overline{C}) \wedge D} \quad (\text{CG-Fun}) $$
  Here, constraints are accumulated through intersection ($\wedge$) of sub-constraint sets.

/// Pre-condition: xs and v are disjoint sets of variables.
pub fn Subtype::generate(
  self : Subtype,
  xs : Array[Var],
  v : Set[Var],
) -> Constraints raise {
  match (self.l, self.r) {
    (_, TyTop) | (TyBot, _) => Constraints::empty()
    (TyVar(y1), TyVar(y2)) if y1 == y2 && !xs.contains(y1) =>
      Constraints::empty()
    (TyVar(y), s) if xs.contains(y) => {
      let t = s.demotion(v)
      Constraints(Map::from_array([(y, { l: TyBot, r: t })]))
    }
    (s, TyVar(y)) if xs.contains(y) => {
      let t = s.promotion(v)
      Constraints(Map::from_array([(y, { l: t, r: TyTop })]))
    }
    (TyFun(ys1, r, s), TyFun(ys2, t, u)) if ys1 == ys2 => {
      let vy = v.union(Set::from_array(ys1))
      let cs = t.zip(r).map(tr => { l: tr.0, r: tr.1 }.generate(xs, vy))
        |> meets()
      cs.meet({ l: s, r: u }.generate(xs, vy))
    }
    _ => raise ConstraintGenerationError
  }
}

A crucial observation is that in any invocation $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$, the unknown variables $\overline{X}$ appear only on one side of $S$ or $T$. This makes the entire process a matching-modulo-subtyping problem rather than a full unification problem, ensuring the algorithm’s simplicity and determinism.