ve_rules][edit]

Promotion Rules ($S \Uparrow^V T$)
- For $\top$ and $\bot$: $$ \top \Uparrow^V \top \quad (\text{VU-Top}) $$ $$ \bot \Uparrow^V \bot \quad (\text{VU-Bot}) $$
- For type variable $X$:
  - If $X$ belongs to the set $V$ that needs to be eliminated, promote it to $\top$. $$ \frac{X \in V}{X \Uparrow^V \top} \quad (\text{VU-Var-1}) $$
  - If $X$ is not in $V$, it remains unchanged. $$ \frac{X \notin V}{X \Uparrow^V X} \quad (\text{VU-Var-2}) $$
- For function types:
  - Recursively demote its parameter types (contravariant position) and promote its return type (covariant position). $$ \frac{\overline{S} \Downarrow^V \overline{U} \quad T \Uparrow^V R \quad \overline{X} \notin V}{\forall\overline{X}.\overline{S} \to T \Uparrow^V \forall\overline{X}.\overline{U} \to R} \quad (\text{VU-Fun}) $$
Demotion Rules ($S \Downarrow^V T$)
- Handling of $\top$ and $\bot$ is consistent with promotion rules.
- For type variable $X$:
  - If $X$ belongs to $V$, demote it to $\bot$. $$ \frac{X \in V}{X \Downarrow^V \bot} \quad (\text{VD-Var-1}) $$
  - If $X$ is not in $V$, it remains unchanged.
- For function types:
  - Recursively promote its parameter types and demote its return type. $$ \frac{\overline{S} \Uparrow^V \overline{U} \quad T \Downarrow^V R \quad \overline{X} \notin V}{\forall\overline{X}.\overline{S} \to T \Downarrow^V \forall\overline{X}.\overline{U} \to R} \quad (\text{VD-Fun}) $$

This can be implemented very straightforwardly in MoonBit:

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
  }
}