<figure><img src="image_18.png" /></figure>

# B Properties of the constraint language

This appendix establishes key properties of the constraint language. The first is the principality of shapes Theorem 3.2: any non-variable type $\tau$ admits a non-trivial principal shape $\zeta$.

The second is the canonicalization of satisfiability derivations $\phi \vdash C$, which enables a simple induction principal for reasoning about unicity. This canonical form for derivations is a crucial tool in our proof of soundness and completeness in §D.

## B.1 Principality of shapes

**THEOREM 3.2 (PRINCIPAL SHAPES).** Any non-variable type $\tau$ has a non-trivial principal shape $\zeta$.

*PROOF.* Let us assume $\tau$ is a non-variable type.

**Case** $\tau$ is a type constructor $c \bar{\tau}$.

c is a top-level type constructor of arity $n$, which in our setting may be the nullary 1, the binary arrow, the $n$-ary product, or a nominal record type. In all these cases, the shape of $\tau$ is $v\bar{\gamma}$. c $\bar{\gamma}$ where $\bar{\gamma}$ is a sequence of $n$ distinct type variables. This is clearly principal.

**Case** $\tau$ is a **polytype** $[\forall \bar{\alpha}. \tau]$.

We may assume w.l.o.g. that each variable of $\bar{\alpha}$ occurs free in $\tau$. Let $(\pi_i)_{i=1}^n$ be the sequence of shortest paths in $\tau$ that cannot be extended to reach a (polymorphic) variable in $\bar{\alpha}$, in lexicographic order and $\bar{\gamma}$ be a sequence $(\gamma_i)_{i=1}^n$ of distinct variables that do not appear in $\tau$. Let $\tau_0$ be $\tau[\pi_i := \gamma_i]_{i=1}^n$, i.e., the term $\tau$ where each path $\pi_i$ has been substituted by the variable $\gamma_i$. Let $\zeta$ be the shape $v\bar{\gamma}$. [$\forall \bar{\alpha}. \tau_0$]. We claim that $\zeta'$ is actually the principal shape of [$\forall \bar{\alpha}. \tau$].

By construction, $\tau$ is equal to $\zeta \bar{\tau}$ (1). where $\bar{\tau}$ is the sequence composed of $\tau_i$ equal to $\tau/\pi_i$ for $i$ ranging from 1 to $n$. Indeed, by definition, $\zeta \bar{\tau}$ is equal to $(\tau[\pi_i := \gamma_i]_{i=1}^n)[\gamma_i := \tau_i]$ which is obviously equal to $\tau$. The remaining of the proof checks that $\zeta'$ is minimal (2), that is, we assume that $\zeta'$ is another shape such that [$\forall \bar{\alpha}. \tau$] is equal to $\zeta' \bar{\tau}$ for some $\bar{\tau}'$ (3) and show that $\zeta \le \zeta'$ (4).

It follows from (3) that $\zeta'$ must be a polytype shape, i.e., of the form $v\bar{\gamma}$. [$\forall \bar{\beta}. \tau'$] and [$\forall \bar{\alpha}. \tau$] is equal to [$\forall \bar{\beta}. \tau'$] [$\bar{\gamma}' := \bar{\tau}'$] (5). We may assume w.l.o.g. that $\bar{\beta}$ and $\bar{\gamma}'$ are disjoint, that $\bar{\gamma}'$ does not contain useless variables, i.e., that they all appear in $\tau'$ and that they actually appear in lexicographic order. Now that never term contains useless variables, (5) implies that the sequences $\bar{\alpha}$ and $\bar{\beta}$ can be put in one-to-one correspondences. Besides, since they all ordered in the order of appearance in terms, they the correspondence respects the ordering. Hence, the substitution [$\bar{\beta} := \bar{\alpha}$] is a renaming. Therefore, we can assume w.l.o.g. that $\bar{\beta}$ is $\bar{\alpha}$, That is, (5) becomes that [$\forall \bar{\alpha}. \tau$] is equal to [$\forall \bar{\alpha}. \tau' [\bar{\gamma}' := \bar{\tau}']$], which given that variables $\bar{\alpha}$ appear in the same order in both terms, implies that $\tau$ is equal to $\tau' [\bar{\gamma}' := \bar{\tau}']$ (6).
Since $\bar{\tau}'$ does not contain any variable in $\bar{\alpha}$, every path $\pi_i$ is a path in $\tau'$. Thus, we may write $\tau'$ as $\tau'[\pi_i := \tau_i'']_{i=1}^n$ where $\tau_i''$ is $\tau'/\pi_i$. This is also equal to $(\tau'[\pi_i := \gamma_i]_{i=1}^n)[\gamma_i := \tau_i'']_{i=1}^n$, that is $\tau_0[\gamma_i := \tau_i'']_{i=1}^n$. In summary, we have $\tau'$ is equal to $\tau_0[\gamma_i := \tau_i'']_{i=1}^n$, which implies that $[\forall \bar{\alpha}. \tau']$ is equal to $[\forall \bar{\alpha}. \tau_0[\gamma_i := \tau_i'']_{i=1}^n]$, i.e., $[\forall \bar{\alpha}. \tau_0][\gamma_i := \tau_i'']_{i=1}^n$ (7). By **INST-SHAPE**, we have $\nu\bar{\gamma}. [\forall \bar{\alpha}. \tau_0] \preceq \nu\bar{\gamma}'. [\forall \bar{\alpha}. \tau_0][\gamma_i := \tau_i'']_{i=1}^n$, which, given (7), is exactly (4). □

## B.2 Canonicalization of satisfiability

They key result in this section is that our semantic derivations $\phi \vdash C$ can always be rewritten to only apply the rule **MATCH-CTX** at the very bottom of the derivation, rather than in the middle of derivations. This corresponds to explicitating the unique shapes of all suspended constraints (in some order that respects the dependency between suspended constraints), and then continuing with a syntax-directed proof of a fully-discharged constraint.

We did not impose this ordering in our definition of the semantics to make it more flexible and more declarative, but the inversion principle that it provides will be helpful when reasoning about the solver in §C.

We define in §A a formal judgment $C$ simple that says that $C$ does not contain any suspended match constraint, and extend it trivially to constraint contexts: $C$ simple. In particular, the erasure $[C]$ of a constraint (Definition 4.2) is always simple. We then introduce in §A a “canonical” semantic judgment $\phi \models C$ that enforces the structure we mentioned: its derivation starts by discharging suspended constraints, until eventually we reach a simple constraint $C$. Below we prove that any semantic derivation $\phi \vdash C$ can be turned into a canonical semantic derivation $\phi \models C$.

We can think of this result as controlling the amount of non-syntax-directness in our rules: we need some of it, but it suffices to have it only at the outside, and it contains a more standard derivation that is easy to reason about.

**Inversion.** When $C$ is simple, a derivation of $\phi \vdash C$ does not use the contextual rule (it is a derivation in $\phi \vdash_{\text{simple}} C$), so it enjoys the usual inversion principle on syntax-directed judgments; for example, if $\phi \vdash_{\text{simple}} C_1 \wedge C_2$ then by inversion $\phi \vdash_{\text{simple}} C_1$ and $\phi \vdash_{\text{simple}} C_2$, etc.

**Congruence.** Congruence does not hold in general in our system due to the contextual rule. For example, $C_1 \triangleq$ (match $\alpha$ with _ $\Rightarrow$ true) is unsatisfiable so we have $C_1 \equiv$ false, but for $C \triangleq$ ($\exists \alpha. \alpha = \text{int} \wedge \Box$) we have $C[C_1] \equiv$ true and $C[\text{false}] \equiv$ false. It holds simply for simple constraints.

**LEMMA B.1 (SIMPLE CONGRUENCE).** *Given simple constraints $C_1, C_2$ and simple context $C$. If $C_1 \vdash C_2$, then $C[C_1] \vdash C[C_2]$.*

**PROOF.** Induction on the derivation of $C$ simple. □

<figure><img src="image_19.png" /></figure>

**Composability.** The composability result below is an important test of our definition of the unicity condition $C[\tau!\zeta]$, which is in part engineered for this lemma to be simple to prove. In the past we used a definition of unicity that also required $C[\text{true}]$ to be satisfiable, which broke the composability property.

**LEMMA B.2 (COMPOSABILITY OF UNICITY).** *If $C_1[\tau!\zeta]$, then $C_2[C_1][\tau!\zeta]$.*

**PROOF.** Induction on the structure of $C_2$. □

**Case** □ immediate.
**Case** $\mathscr{C}_3 \wedge C$.

$\mathscr{C}_1[\tau!\zeta]$

$\mathscr{C}_3[\mathscr{C}_1][\tau!\zeta]$

For all $\phi, g$

$\phi \vdash [\mathscr{C}_3[\mathscr{C}_1][\tau = g]] \wedge [C]$

$\phi \vdash [\mathscr{C}_3[\mathscr{C}_1][\tau = g]]$

$\mathrm{shape}(g) = \zeta$

<figure><img src="image_20.png" /></figure>

$(\mathscr{C}_3[\mathscr{C}_1] \wedge C)[\tau!\zeta]$

Premise

By i.h.

Definition of $(\mathscr{C}_3[\mathscr{C}_1] \wedge C)[\tau!\zeta]$

$\Rightarrow I$

Simple inversion

$\Rightarrow E$ on $\mathscr{C}_3[\mathscr{C}_1][\tau!\zeta]$

Above

**Case** $C \wedge \mathscr{C}_3$.

Similar to the $\mathscr{C}_3 \wedge C$ case.

**Case** $\exists\alpha. \mathscr{C}_3$.

$\mathscr{C}_1[\tau!\zeta]$

$\mathscr{C}_3[\mathscr{C}_1][\tau!\zeta]$

For all $\phi, g$

$\phi \vdash \exists\alpha. [\mathscr{C}_3[\mathscr{C}_1][\tau = g]]$

$\phi[\alpha := g'] \vdash [\mathscr{C}_3[\mathscr{C}_1][\tau = g]]$

$\mathrm{shape}(g) = \zeta$

<figure><img src="image_21.png" /></figure>

$(\exists\alpha. \mathscr{C}_3[\mathscr{C}_1])[\tau!\zeta]$

Premise

By i.h.

Definition of $(\exists\alpha. \mathscr{C}_3[\mathscr{C}_1])[\tau!\zeta]$

$\Rightarrow I$

Simple inversion

$\Rightarrow E$ on $\mathscr{C}_3[\mathscr{C}_1][\tau!\zeta]$

Above

**Case** $\forall\alpha. \mathscr{C}_3$.

Similar to $\exists\alpha. \mathscr{C}_3$ case.

**Case** $\exists i^x. \mathscr{C}_3$.

Similar to $\exists\alpha. \mathscr{C}_3$ case.

**Case** let $x = \lambda\alpha. \mathscr{C}_3$ in C.

$\mathscr{C}_1[\tau!\zeta]$

$\mathscr{C}_3[\mathscr{C}_1][\tau!\zeta]$

For all $\phi, g$

$\phi \vdash \mathrm{let} x = \lambda\alpha. [\mathscr{C}_3[\mathscr{C}_1][\tau = g]] \in [C]$

$\phi \vdash \exists\alpha. [\mathscr{C}_3[\mathscr{C}_1][\tau = g]]$

$\phi[\alpha := g'] \vdash [\mathscr{C}_3[\mathscr{C}_1][\tau = g]]$

$\mathrm{shape}(g) = \zeta$

<figure><img src="image_22.png" /></figure>

$(\mathrm{let} x = \lambda\alpha. \mathscr{C}_3[\mathscr{C}_1] \in C)[\tau!\zeta]$

Premise

By i.h.

Definition of $(\mathrm{let} x \dots)[\tau!\zeta]$

$\Rightarrow I$

Simple inversion

Simple inversion

$\Rightarrow E$ on $\mathscr{C}_3[\mathscr{C}_1][\tau!\zeta]$

Above

**Case** let $x = \lambda\alpha. C$ in $\mathscr{C}_3$.

Similar to let $x = \lambda\alpha. \mathscr{C}_3$ in C case.

**Case** let $x \alpha [\bar{\alpha}] = \mathscr{C}_3$ in C.

Similar to let $x = \lambda\alpha. \mathscr{C}_3$ in C case.

**Case** let $x \alpha [\bar{\alpha}] = C$ in $\mathscr{C}_3$.

Similar to let $x = \lambda\alpha. C$ in $\mathscr{C}_3$ case.

LEMMA B.3 (INVERSION OF UNICITY).

(i) If $(\exists\alpha. \mathscr{C})[\tau!\zeta]$, then $\mathscr{C}[\tau!\zeta]$.

(ii) If $(\forall\alpha. \mathscr{C})[\tau!\zeta]$, then $\mathscr{C}[\tau!\zeta]$.

□
PROOF. The definition of $\mathscr{C}[\tau!\zeta]$ uses simple semantics on the erasure $\llbracket \mathscr{C} \rrbracket$, so these results are easily shown by simple inversion. $\square$

LEMMA B.4 (DECANONICALIZATION). If $\phi \Vdash C$, then $\phi \vdash C$.

PROOF. Induction on the given derivation $\phi \Vdash C$

$\square$

THEOREM B.5 (CANONICALIZATION). If $\phi \vdash C$, then $\phi \Vdash C$.

PROOF. We proceed by induction on $\phi \vdash C$ with the measure $\|C\|$.

**Case**

$$\underline{\phi \vdash true} \qquad \text{TRUE}$$

☐ $\phi \Vdash true$ immediate by CAN-BASE

**Case**

$$\frac{\phi(\tau_1) = \phi(\tau_2)}{\phi \vdash \tau_1 = \tau_2} \quad \text{UNIF}$$

Similar to the TRUE case.

**Case**

$$\frac{\phi \vdash C_1 \qquad \phi \vdash C_2}{\phi \vdash C_1 \wedge C_2} \qquad \text{CONJ}$$

$\phi \vdash C_1$ Premise

$\phi \vdash C_2$ Premise

$\phi \Vdash C_1$ By i.h.

$\phi \Vdash C_2$ By i.h.

By cases on $\phi \Vdash C_1, \phi \Vdash C_2$.

**Subcase**

$$\frac{\phi \vdash C_1 \qquad C_1 \text{ simple}}{\phi \Vdash C_1} \qquad \text{CAN-BASE}$$

$$\frac{\phi \vdash C_2 \qquad C_2 \text{ simple}}{\phi \Vdash C_2} \qquad \text{CAN-BASE}$$

☐ $\phi \Vdash C_1 \wedge C_2$ immediate by CAN-BASE

**Subcase**

$$\frac{\mathscr{C}[\tau!\zeta] \qquad \phi \Vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]}{\phi \Vdash \underbrace{\mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]}_{C_1}} \qquad \text{CAN-MATCH-CTX}$$

$\phi \Vdash C_2$

$\phi \Vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ Premise

$\phi \vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ Lemma B.4
$\phi \vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}] \wedge C_2$ By CONJ

$\phi \Vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}] \wedge C_2$ By i.h.

$\mathscr{C}[\alpha!\zeta]$ Premise

$(\mathscr{C} \wedge C_2)[\alpha!\zeta]$ Lemma B.2

■ $\phi \Vdash \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]$ By CAN-MATCH-CTX

**Subcase**

$$ \phi \Vdash C_1 \frac{\mathscr{C}[\tau!\zeta] \qquad \phi \Vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]}{\phi \Vdash \underbrace{\mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]}_{C_2}}_{\text{CAN-MATCH-CTX}} $$

Symmetric to the above case.

**Case**

$$ \frac{\phi[\alpha := g] \vdash C}{\phi \vdash \exists \alpha. C} \text{ EXISTS} $$

$\phi[\alpha := g] \vdash C$ Premise

$\phi[\alpha := g] \Vdash C$ By i.h.

By cases on $\phi[\alpha := g] \Vdash C$.

**Subcase**

$$ \frac{\phi[\alpha := g] \vdash C \qquad C \text{ simple}}{\phi[\alpha := g] \Vdash C} \text{ CAN-BASE} $$

■ $\phi \Vdash \exists \alpha. C$ Immediate by CAN-BASE

**Subcase**

$$ \frac{\mathscr{C}[\tau!\zeta] \qquad \phi[\alpha := g] \Vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]}{\phi \Vdash \underbrace{\mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]}_{C}}_{\text{CAN-MATCH-CTX}} $$

$\phi[\alpha := g] \Vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ Premise

$\phi[\alpha := g] \vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ Lemma B.4

$\phi \vdash \exists \alpha. \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ By EXISTS

$\phi \Vdash \exists \alpha. \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ By i.h.

$\mathscr{C}[\tau!\zeta]$ Premise

$(\exists \alpha. \mathscr{C})[\tau!\zeta]$ Lemma B.2

■ $\phi \Vdash \exists \alpha. \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]$ By CAN-MATCH-CTX

**Case**

$$ \frac{\forall g, \phi[\alpha := g] \vdash C}{\phi \vdash \forall \alpha. C} \text{ FORALL} $$

Similar to the EXISTS case.
**Case**

$$ \mathfrak{S} = \phi(\lambda\alpha. C_1) \qquad \mathfrak{S} \neq \emptyset \\ \frac{\phi[x := \mathfrak{S}] \vdash C_2}{\phi \vdash \text{let } x = \lambda\alpha. C_1 \text{ in } C_2} \quad \text{LET} $$

$\phi[x := \mathfrak{S}] \models C_2$ By i.h.

By cases on $\phi[x := \mathfrak{S}] \models C_2$.

**Subcase**

$$ \frac{\phi[x := \mathfrak{S}] \vdash C_2 \qquad C_2 \text{ simple}}{\phi[x := \mathfrak{S}] \models C_2} \quad \text{CAN-BASE} $$

□ $\mathfrak{S} \models \text{let } x = \lambda\alpha. C_1 \text{ in } C_2$ Immediate by CAN-BASE

**Subcase**

$$ \frac{\mathcal{C}[\tau!\zeta] \qquad \phi[x := \mathfrak{S}] \models \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]}{\phi[x := \mathfrak{S}] \models \underbrace{\mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}]}_{C_2}} \quad \text{CAN-MATCH-CTX} $$

$\mathcal{C}[\tau!\zeta]$ Premise

(let $x = \lambda\alpha. C_1$ in $\mathcal{C}[\tau!\zeta]$ Lemma B.2)

$\phi[x := \mathfrak{S}] \models \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ Premise

$\phi[x := \mathfrak{S}] \vdash \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ Lemma B.4

$\phi \vdash \text{let } x = \lambda\alpha. C_1 \text{ in } \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ By LET

$\phi \models \text{let } x = \lambda\alpha. C_1 \text{ in } \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ By i.h.

<figure><img src="image_23.png" /></figure>

$\phi \models \text{let } x = \lambda\alpha. C_1 \text{ in } \mathcal{C}[\text{match } \tau \text{ with } \zeta]$

By CAN-MATCH-CTX

**Case**

$$ \frac{\phi(\tau) \in \phi(x)}{\phi \vdash x \tau} \quad \text{APP} $$

Similar to the TRUE case.

**Case**

$$ \mathfrak{R} = \phi(\lambda\alpha[\bar{\alpha}]. C_1) \qquad \mathfrak{R} \neq \emptyset \\ \frac{\phi[x := \mathfrak{R}] \vdash C_2}{\phi \vdash \text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } C_2} \quad \text{LETR} $$

Similar to the LET case.

**Case**

$$ \frac{(\phi(\tau), \_) \in \phi(x)}{\phi \vdash x \tau} \quad \text{APPR} $$

Similar to the APP case.

**Case**

$$ (\_\phi') \in \phi(x) \\ \frac{\phi[i := \phi'] \vdash C}{\phi \vdash \exists i^x. C} \quad \text{EXISTS-INST} $$

Similar to the EXISTS case.
**Case**

$$ \frac{\forall \tau \in \epsilon, \phi(\tau) = g}{\phi \vdash \epsilon} \text{ MULTI-UNIF} $$

Similar to the UNIF case.

**Case**

$$ \frac{\phi(i)(\alpha) = \phi(\tau)}{\phi \vdash i(\alpha) \leadsto \tau} \text{ INCR-INST} $$

Similar to the APP case.

□

**LEMMA B.6 (INVERSION OF SUSPENSION).** If $\phi \vdash \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]$ and $\mathscr{C}[\tau!\zeta]$, then
$\phi \vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$.

**PROOF.** We use canonicalization (Theorem B.5) to induct on $\phi \models \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]$ instead of
$\phi \vdash \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]$.

This simplifies the proof, but introduces a circular dependency between Theorem B.5 and Lemma B.6. However, this does not compromise the well-foundedness of induction, as the application of Lemma B.6 (via Corollary B.7) within the proof of Theorem B.5 is restricted to strictly smaller constraints.

**Case**

$$ \frac{\phi \vdash \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}] \qquad \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}] \text{ simple}}{\phi \models \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]} \text{ CAN-BASE} $$

The second premise is a contradiction.

**Case**

$$ \frac{\mathscr{C}'[\tau'!\zeta'] \qquad \phi \models \mathscr{C}'[\text{match } \tau' := \zeta' \text{ with } \bar{\chi}']}{\phi \models \underbrace{\mathscr{C}'[\text{match } \tau' \text{ with } \bar{\chi}']}_{\mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}]} \text{ CAN-MATCH-CTX}} $$

By cases on $\mathscr{C} = \mathscr{C}'$.

**Subcase** $\mathscr{C} = \mathscr{C}'$.

$$ \mathscr{C} = \mathscr{C}' \qquad \text{Premise} $$

$$ \tau' = \tau $$

$$ \zeta' = \zeta $$

$$ \bar{\chi}' = \bar{\chi} $$

$$ \blacksquare \quad \phi \models \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}] \quad \text{Premise} $$

**Subcase** $\mathscr{C} \neq \mathscr{C}'$.

$$ \mathscr{C}_2[\text{match } \tau \text{ with } \bar{\chi}, \text{ match } \tau' \text{ with } \bar{\chi}'] = \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}] \quad \text{For some 2-hole context } \mathscr{C}_2 \\ = \mathscr{C}'[\text{match } \tau' \text{ with } \bar{\chi}'] $$

$$ \phi \models \mathscr{C}_2[\text{match } \tau \text{ with } \bar{\chi}, \text{ match } \tau' := \zeta' \text{ with } \bar{\chi}'] \text{ Premise} $$

$$ \text{For all } \phi', g' \qquad \text{Defn. of } \mathscr{C}_2[\square, \text{ match } \tau' := \zeta' \text{ with } \bar{\chi}'] [\tau!\zeta] $$
$$ 
\begin{align*}
\phi' \vdash [\mathcal{C}_2[\tau = g', \text{match } \tau' := \zeta' \text{ with } \bar{\chi}')] &\Rightarrow I \\
\phi' \vdash [\mathcal{C}_2[\tau = g', \text{true}]] &\qquad \text{Lemma B.1}
\end{align*}
$$

$$ 
\begin{align*}
[\mathcal{C}_2[\tau = g', \text{true}]] &= [\mathcal{C}_2[\tau = g', [\text{match } \tau' \text{ with } \bar{\chi}]]] && \text{By definition} \\
&= [\mathcal{C}[\tau = g')] && \text{By definition} \\
\phi' \vdash [\mathcal{C}[\tau = g')] && \text{Above} \\
\text{shape}(g') = \zeta && \implies \text{E on } \mathcal{C}[\tau!\zeta] \\
\mathcal{C}_2[\square, \text{match } \tau' := \zeta' \text{ with } \bar{\chi}][\tau!\zeta] && \text{Above} \\
\phi \models \mathcal{C}_2[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \text{match } \tau' := \zeta' \text{ with } \bar{\chi}] && \text{By } \text{i.h.}
\end{align*}
$$

$$ \text{For all } \phi', g' \qquad \text{Defn. of } \mathcal{C}_2[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \square][\tau'!\zeta'] $$

$$ 
\begin{align*}
\phi' \vdash [\mathcal{C}_2[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \tau' = g')] &\Rightarrow I \\
\phi' \vdash [\mathcal{C}_2[\text{true}, \tau' = g]] &\qquad \text{Lemma B.1} \\
[\mathcal{C}_2[\text{true}, \tau' = g]] &= [\mathcal{C}_2[[\text{match } \tau \text{ with } \bar{\chi}], \tau' = g]] && \text{By definition} \\
&= [\mathcal{C}'[\tau' = g]] && \text{By definition} \\
\phi' \vdash [\mathcal{C}[\tau = g]] && \text{Above} \\
\mathcal{C}'[\tau'!\zeta'] && \text{Premise} \\
\text{shape}(g') = \zeta && \implies \text{E on } \mathcal{C}'[\tau'!\zeta'] \\
\mathcal{C}_2[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \square][\tau'!\zeta'] && \text{Above} \\
\phi \models \mathcal{C}_2[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \text{match } \tau' \text{ with } \bar{\chi}] && \text{By } \text{CAN-MATCH-CTX}
\end{align*}
$$

□

**COROLLARY B.7.** If $\mathcal{C}[\tau!\zeta]$, then $\phi(\lambda\alpha.\mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}]) = \phi(\lambda\alpha.\mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}])$. Similarly, $\phi(\lambda\alpha[\bar{\alpha}].\mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}]) = \phi(\lambda\alpha[\bar{\alpha}].\mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}])$.

**PROOF.** It is sufficient to show that $\phi[\alpha := g] \vdash \mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}]$ if and only if $\phi \vdash \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$.

**Case** $\Rightarrow$.

$$ 
\begin{array}{l@{\qquad}l}
\mathcal{C}[\tau!\zeta] & \text{Premise} \\
\phi[\alpha := g] \vdash \mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}] & \text{Premise} \\
\text{LEMMA B.6} & \text{Lemma B.6}
\end{array}
$$

**Case** $\Leftarrow$.

$$ 
\begin{array}{l@{\qquad}l}
\mathcal{C}[\tau!\zeta] & \text{Premise} \\
\phi[\alpha := g] \vdash \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}] & \text{Premise} \\
\text{LEMMA B.6} & \text{Lemma B.6}
\end{array}
$$

For $\phi(\lambda\alpha[\bar{\alpha}].\mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}]) = \phi(\lambda\alpha[\bar{\alpha}].\mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}])$, the proof is identical.

□

### C Properties of the constraint solver

The primary requirement of our constraint solver is correctness: a constraint C is satisfiable if and only if the solver terminates with a solution.

This section decomposes this requirement into three properties: preservation, progress, and termination—and provides proofs for each. Correctness then follows as a corollary of these results.
## C.1 Preservation

This section details the proof of *preservation* for the solver: if $C_1 \rightarrow C_2$, then $C_1 \equiv C_2$. Since rewriting may occur under arbitrary contexts, it suffices to check for each rule, that the equivalence $C_1 \equiv C_2$ holds under all contexts $\mathscr{C}$.

However, the introduction of suspended match constraints breaks congruence of equivalence. That is, it is no longer the case that $C_1 \equiv C_2$ implies $\mathscr{C}[C_1] \equiv \mathscr{C}[C_2]$. For instance, we have match $\alpha$ with $\bar{\chi} \equiv \text{false}$, yet $\mathscr{C}[\text{match } \alpha \text{ with } \bar{\chi}] \neq \mathscr{C}[\text{false}]$ for $\mathscr{C} := \square \wedge \alpha = \text{int}$.

As a result, we must prove *contextual equivalence* for each rewriting rule explicitly. This is both non-trivial and tedious. To simplify the task, we first present a series of auxiliary lemmas that recover contextual equivalence for many common cases. Whenever possible, we prefer to work with equivalences on *simple* constraints, as these retain the desired congruence properties that do not hold generally in our system.

**Definition C.1 (Contextual equivalence).** Two constraints $C_1$ and $C_2$ are contextually equivalence, written $C_1 \equiv_{\mathrm{ctx}} C_2$, iff:

$$C_1 \equiv_{\mathrm{ctx}} C_2 \triangleq \forall \mathscr{C}. \mathscr{C}[C_1] \equiv \mathscr{C}[C_2]$$

**COROLLARY C.2 (SIMPLE EQUIVALENCE IS CONGRUENT).** Given simple constraints $C_1, C_2$ and simple context $\mathscr{C}$. If $C_1 \equiv C_2$, then $\mathscr{C}[C_1] \equiv \mathscr{C}[C_2]$.

**PROOF.** Follows from Lemma B.1. □

<figure><img src="image_24.png" /></figure>

**LEMMA C.3 (SIMPLE EQUIVALENCE IS CONTEXTUAL).** For simple constraints $C_1, C_2$. If $C_1 \equiv C_2$, then $C_1 \equiv_{\mathrm{ctx}} C_2$.

**PROOF.** We proceed by induction on the number of suspended match constraints $n$ in $\mathscr{C}$.

**Case n is 0.** Follows from Corollary C.2.

**Case n is k + 1.**

**Subcase** $\Rightarrow$.

$\phi \vdash \mathscr{C}[C_1]$ Premise

$\phi \Vdash \mathscr{C}[C_1]$ Theorem B.5

$\mathscr{C}'[\tau!\zeta]$ Inversion of CAN-MATCH-CTX

$\phi \Vdash \mathscr{C}'[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ $''$

$\mathscr{C}[C_1] = \mathscr{C}'[\text{match } \tau := \zeta \text{ with } \bar{\chi}]$ $''$

$= \mathscr{C}_2[\text{match } \tau := \zeta \text{ with } \bar{\chi}, C_1]$ For some two-hole context $\mathscr{C}_2$

$\phi \vdash \mathscr{C}_2[\text{match } \tau := \zeta \text{ with } \bar{\chi}, C_2]$ By i.h.

For all $\phi'$, $\mathfrak{g}$ Defn of $\mathscr{C}'[\tau!\zeta]$

$\phi' \vdash [\mathscr{C}_2[\tau := \mathfrak{g}, C_2]]$ Premise

$\phi' \vdash [\mathscr{C}_2[\tau := \mathfrak{g}, C_1]]$ Corollary C.2

$\phi' \vdash [\mathscr{C}'[\tau := \mathfrak{g}]]$ Above

$\mathrm{shape}(\mathfrak{g}) = \zeta \qquad \Rightarrow \mathrm{E}$ on $\mathscr{C}'[\tau!\zeta]$

$\mathscr{C}_2[\square, C_2][\tau!\zeta]$ Above

∴ $\phi \vdash \mathscr{C}_2[\text{match } \tau \text{ with } \bar{\chi}, C_2]$ By MATCH-CTX

**Subcase** $\Leftarrow$.

Symmetric argument.

<figure><img src="image_25.png" /></figure>
**LEMMA C.4 (UNIFICATION IS SIMPLE).** For all unification problems U, U simple.

**PROOF.** By induction on the structure of U.

☐

**Definition C.5 (Context equivalence).** Two contexts $\mathcal{C}_1$ and $\mathcal{C}_2$ are equivalent with guard P, written $\mathcal{C}_1 \equiv_{\square}^{P} \mathcal{C}_2$ iff:

$$ \mathcal{C}_1 \equiv_{\square}^{P} \mathcal{C}_2 \triangleq \forall \bar{C}. P(\bar{C}) \implies \mathcal{C}_1[\bar{C}] \equiv_{\text{ctx}} \mathcal{C}_2[\bar{C}] $$

**Definition C.6 (Match-closed).** A predicate P on constraints is match-closed if, for all constraints $\bar{C}, \bar{C}'$, contexts $\mathcal{C}$, matches match $\tau$ with $\bar{\chi}$ and shapes $\zeta$,

$$ P(\bar{C}, \mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}], \bar{C}') \implies P(\bar{C}, \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}], \bar{C}') $$

**LEMMA C.7 (DETERMINES IS MATCH-CLOSED).** C determines $\bar{\beta}$ is match-closed. Similarly, $\vdash C$ determines $\bar{\beta}$ is matched closed.

**PROOF.** Follows from the definitions of $C$ determines $\bar{\beta}$, $\vdash C$ determines $\bar{\beta}$, and Lemma B.1. ☐

**LEMMA C.8 (SIMPLE CONTEXT EQUIVALENCE).** For any two simple contexts $\mathcal{C}_1, \mathcal{C}_2$ and a match-closed guard P. If the two contexts $\mathcal{C}_1$ and $\mathcal{C}_2$ are equivalent under any simple constraints satisfying P, then $\mathcal{C}_1 \equiv_{\square}^{P} \mathcal{C}_2$.

**PROOF.** Let us assume that $(\dagger)$ holds:

$$ \forall \mathcal{C}, \bar{C} \text{ simple. } P(\bar{C}) \implies \mathcal{C}[\mathcal{C}_1[\bar{C}]] \equiv \mathcal{C}[\mathcal{C}_2[\bar{C}]] $$

We proceed by induction on the number of suspended match constraints $n$ with the statement $Q(n) := \forall \bar{C}, \mathcal{C}. \#\text{match } \mathcal{C} + \#\text{match } \bar{C} = n \implies P(\bar{C}) \implies \mathcal{C}[\mathcal{C}_1[\bar{C}]] \equiv \mathcal{C}[\mathcal{C}_2[\bar{C}]]$.

**Case** $n$ is 0.

$$ \mathcal{C}, \bar{C} \text{ simple} \qquad \text{Premise } (n \text{ is 0}) \\ \blacksquare P(\bar{C}) \implies \mathcal{C}[\mathcal{C}_1][\bar{C}] \equiv \mathcal{C}[\mathcal{C}_2][\bar{C}] \quad \dagger $$

**Case** $n$ is $k+1$.

**Subcase** $\implies$.

$$ \begin{array}{l@{\qquad}l} P(\bar{C}) & \text{Premise} \\ \phi \vdash \mathcal{C}[\mathcal{C}_1][\bar{C}] & \text{Premise} \\ \phi \models \mathcal{C}[\mathcal{C}_1][\bar{C}] & \text{Theorem B.5} \\ \phi \models \mathcal{C}'[\text{match } \tau := \zeta \text{ with } \bar{\chi}] & \text{Inversion of CAN-MATCH-CTX} \\ \mathcal{C}'[\tau!\zeta] & \text{"} \end{array} $$

$$ \mathcal{C}[\mathcal{C}_1][\bar{C}] = \mathcal{C}'[\text{match } \tau \text{ with } \bar{\chi}] \quad \text{"} $$

Cases on $\mathcal{C}, \bar{C}$.

**Subsubcase** $\mathcal{C}$ contains $\mathcal{C}'$'s hole.

$$ \mathcal{C}[\mathcal{C}_1][\bar{C}] = \mathcal{C}_3[\text{match } \tau \text{ with } \bar{\chi}, \mathcal{C}_1[\bar{C}]] \quad \text{For some 2-hole context } \mathcal{C}_3 $$

$$ \phi \models \mathcal{C}_3[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \mathcal{C}_1[\bar{C}]] $$

$$ k = \#\text{match } \mathcal{C}_3[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \mathcal{C}_1[\bar{C}]] $$

$$ \phi \vdash \mathcal{C}_3[\text{match } \tau := \zeta \text{ with } \bar{\chi}, \mathcal{C}_2[\bar{C}]] \quad \text{By i.h.} $$
For all $\phi', g$

$$ \phi' \vdash [C_3[\tau = g, C_2[\bar{C}]]] \quad \text{Premise} $$

$$ \phi' \vdash [C_3[\tau = g, C_1[\bar{C}]]] \quad \text{†} $$

$$ \text{shape}(g) = \zeta \quad \Rightarrow \quad \text{E on } C'[\tau!\zeta] $$

$$ C_3[\square, C_2[\bar{C}]][\tau!\zeta] \quad \text{Above} $$

<figure><img src="image_26.png" /></figure>

$$ \phi \vdash C_3[\text{match } \tau \text{ with } \bar{\chi}, C_2[\bar{C}]] \quad \text{By } \textit{MATCH-CTX} $$

**Subsubcase** $C_i$ contains $C'$'s hole.

Similar argument to the above case, but relies on the match-closure of P.

**Subcase** $\Leftarrow$.

Symmetric argument.

□

**LEMMA C.9 (SIMPLE LET EQUIVALENCE).** *Given simple constraints $C_1, C_2$ and a simple context $C$. Suppose that*

$$ \forall \phi, \phi', \bar{C} \text{ simple. } \phi'(x) = \phi(\lambda \alpha[\bar{\alpha}]. C[\bar{C}]) \Rightarrow \phi' \vdash C_1 \iff \phi' \vdash C_2 $$

Then, for any context $C'$ that does not re-bind $x$, we have:

$$ \text{let } x \ \alpha \ [\bar{\alpha}] = C[\bar{\alpha}] \text{ in } C'[C_1] \equiv_P \text{ let } x \ \alpha \ [\bar{\alpha}] = C[\bar{\alpha}] \text{ in } C'[C_2] $$

for any match-closed guard P on the holes.

**PROOF.** Let us pose $\mathfrak{R} = \phi(\lambda\alpha[\bar{\alpha}]. C[\bar{C}])$ and let us assume (†):

$$ \forall \phi, \phi', \bar{C}. \phi'(x) = \mathfrak{R} \Rightarrow \phi' \vdash C_1 \iff \phi' \vdash C_2 $$

We proceed by induction on the number of suspended match constraints in $C'', C', \bar{C}$ with the statement $P(n) := \forall C'', C', \bar{C}. \#\text{match } C'', C', \bar{C} = n \Rightarrow C''[\text{let } x \ \alpha \ [\bar{\alpha}] = C[\bar{C}] \text{ in } C'[C_1]] \equiv C''[\text{let } x \ \alpha \ [\bar{\alpha}] = C[\bar{C}] \text{ in } C'[C_2]].$

**Case** $n$ is 0.

Thus $C'', C', \bar{C}$ are simple. It suffices to show the equivalence on the let-constraint directly and use congruence of equivalence for simple constraints (Lemma C.3) to establish the result.

We proceed by induction on the structure of $C'$ with the statement (‡):

$$ \forall \phi, \phi'. \phi'(x) = \mathfrak{R} \Rightarrow \phi' \vdash C'[C_1] \iff \phi' \vdash C'[C_2] $$

This holds due to the compositionality of simple equivalence using $\dagger$ as a base case.

**Subcase** $\Rightarrow$.

$$ \phi \vdash \text{let } x \ \alpha \ [\bar{\alpha}] = C[\bar{C}] \text{ in } C'[C_1] \quad \text{Premise} $$

$$ \phi[x := \mathfrak{R}] \vdash C'[C_1] \quad \text{''} $$

$$ \phi[x := \mathfrak{R}] \vdash C'[C_2] \quad \text{‡} $$

$$ \phi \vdash \text{let } x \ \alpha \ [\bar{\alpha}] = C[\bar{C}] \text{ in } C'[C_2] \quad \text{By } \textit{LETR} $$

**Subcase** $\Leftarrow$.

Symmetric argument.

**Case** $n$ is $k+1$.

Analogous to the inductive step in Lemma C.8.

□

**LEMMA C.10.** If $C[\tau!\zeta]$, then $C[\tau!\zeta]$.
PROOF. Case

$$ \frac{\tau \notin \mathcal{V}}{\vdash \mathcal{C}[\tau! \text{ shape}(\tau)]} \text{ S-UNI-TYPE} $$

$\tau \notin \mathcal{V}$ Premise

$\tau = \text{shape}(\tau) \bar{\tau}$ For some $\bar{\tau}$

For all $\phi, g$

Defn. of $\mathcal{C}[\tau! \text{ shape}(\tau)]$

$\phi \vdash [\mathcal{C}[\tau = g]]$ Premise

$\phi_1 \vdash \tau = g$ Inversion of $[\mathcal{C}_1]$

$g = \phi_1(\tau)$ Simple inversion

$= \text{shape}(\tau) \phi_1(\bar{\tau})$

$\text{ shape}(g) = \text{shape}(\tau)$

Applying shape to both sides

Case

$$ \frac{\alpha \# \text{bv}(\mathcal{C}_2)}{\vdash \mathcal{C}_1[\alpha = \tau = \epsilon \wedge \mathcal{C}_2[-]] [\alpha! \text{ shape}(\tau)]} \text{ S-UNI-VAR} $$

$\alpha \# \text{bv}(\mathcal{C}_2)$ Premise

$\tau = \text{shape}(\tau) \bar{\tau}$ For some $\bar{\tau}$

For all $\phi, g$

Defn. of $\mathcal{C}[\alpha! \text{ shape}(\tau)]$

$\phi \vdash [\mathcal{C}_1[\alpha = \text{shape}(\tau) \bar{\tau} = \epsilon \wedge \mathcal{C}_2[\alpha = g]]]$ Premise

$\phi_1 \vdash \alpha = \text{shape}(\tau) \bar{\tau} = \epsilon$ Inversion of $[\mathcal{C}_1]$

$\phi_2 \vdash \alpha = g$ Inversion of $[\mathcal{C}_2]$

$g = \phi_2(\alpha)$ Simple inversion

$= \phi_1(\alpha)$

$= \text{shape}(\tau) \phi_1(\bar{\tau})$

$\text{ shape}(g) = \text{shape}(\tau)$

Applying shape to both sides

Case

$$ \frac{\vdash \text{ let } x \alpha [\bar{\alpha}] = \mathcal{C}_1[\text{true}] \text{ in } \mathcal{C}_2[i^x(\alpha') \to \gamma \wedge -][\gamma!\zeta]}{\alpha' \in \alpha, \bar{\alpha} \quad x \# \text{bv}(\mathcal{C}_2) \quad \alpha' \# \text{bv}(\mathcal{C}_1)} \text{ S-UNI-BACKPROP} $$

$$ \vdash \text{ let } x \alpha [\bar{\alpha}] = \mathcal{C}_1[-] \text{ in } \mathcal{C}_2[i^x(\alpha') \to \gamma][\alpha'!\zeta] \text{ S-UNI-BACKPROP} $$

$\alpha' \in \alpha, \bar{\alpha}$ Premise

$x \# \text{bv}(\mathcal{C}_2)$ ”

$\alpha' \# \text{bv}(\mathcal{C}_1)$ ”

$\vdash \text{ let } x \alpha [\bar{\alpha}] = \mathcal{C}_1[\text{true}] \text{ in } \mathcal{C}_2[i^x(\alpha') \to \gamma \wedge -][\gamma!\zeta]$ ”

$\text{ let } x \alpha [\bar{\alpha}] = \mathcal{C}_1[\text{true}] \text{ in } \mathcal{C}_2[i^x(\alpha') \to \gamma \wedge -][\gamma!\zeta]$ By i.h.

For all $\phi, g$

Defn. of ... $[\alpha! \text{ shape}(\tau)]$

$\phi \vdash [\text{let } x \alpha [\bar{\alpha}] = \mathcal{C}_1[\alpha' = g] \text{ in } \mathcal{C}_2[i^x(\alpha') \to \gamma]]$ Premise

Let $\mathfrak{R} = \phi(\lambda\alpha[\bar{\alpha}]. [\mathcal{C}_1[\alpha' = g]])$.

Let $\phi_1 = \phi[x := \mathfrak{R}]$.

$\phi'(\alpha') = g$ For any $(\cdot, \phi') \in \phi_1(x)$

$\phi_2 \vdash i^x(\alpha') \to \gamma$ Inversion of $[\mathcal{C}_2]$

$\phi_2(i^x)(\alpha') = \phi_2(\gamma)$ Simple inversion
$$\phi_2(i^x) \in \phi_2(x)$$

$$\phi_2(i^x)(\alpha') = \mathfrak{g} \\ = \phi_2(\gamma)$$

$$\phi_1 \vdash [\mathcal{C}_2[i^x(\alpha') \rightsquigarrow \gamma \wedge \gamma = \mathfrak{g}]]$$

$$\phi \vdash [\text{let } x \ \alpha \ [\bar{\alpha}] = \mathcal{C}_1[\alpha' = \mathfrak{g}] \text{ in } \mathcal{C}_2[i^x(\alpha') \rightsquigarrow \gamma \wedge \gamma = \mathfrak{g}]]$$

$$\phi \vdash \text{let } x \ \alpha \ [\bar{\alpha}] = \mathcal{C}_1[\text{true}] \text{ in } \mathcal{C}_2[i^x(\alpha') \rightsquigarrow \gamma \wedge \gamma = \mathfrak{g}]$$

<figure><img src="image_27.png" /></figure>

shape(g) = $\zeta$

Since $\exists i^x. \in \mathcal{C}_2$, $\phi_2$ extends $\phi_1$

Above

''

Entailment for $\lfloor \mathcal{C}_2 \rfloor$

By LETR

Simple congruence

$\implies E \text{ on } \dots [\gamma!\zeta]$

□

**LEMMA C.11.** If $\mathcal{C}$ is normalized, then $\mathcal{C}[\tau!\zeta]$ if and only $\vdash \mathcal{C}[\tau!\zeta]$.

**PROOF.**

**Case** $\implies$.

Let us assume $\mathcal{C}[\tau!\zeta]$ and $\mathcal{C}$ is normalized.

Given $\mathcal{C}$ is normalized, every constraint in $\mathcal{C}$ is of the form:

$$R ::= \bar{\bar{\epsilon}} \wedge \overline{\text{match } \alpha \text{ with } \bar{\chi} \wedge \exists \overline{i^x}. i^x(\beta) \rightsquigarrow \gamma \wedge \text{let } x \ \delta \ [\bar{\delta}] = R_1 \text{ in } R_2}$$

By assumptions, we have $\forall \phi, g. \phi \vdash [\mathcal{C}][\alpha = g] \implies \text{shape}(g) = \zeta$. Hence $\lfloor \mathcal{C} \rfloor$ contains $\lfloor R \rfloor$ where:

$$\lfloor R \rfloor ::= \bar{\bar{\epsilon}} \wedge \exists \overline{i^x}. \overline{i^x}(\beta) \rightsquigarrow \gamma \wedge \text{let } x \ \delta \ [\bar{\delta}] = \lfloor R_1 \rfloor \text{ in } \lfloor R_2 \rfloor$$

w.l.o.g. all constraints that may determine the shape of $\alpha$ are located with the regional binder (following the S-EXISTS-LOWER and S-LET-CONJLEFT rules). There are two cases:

**Subcase** $\alpha = \tau = \epsilon \in \bar{\bar{\epsilon}}$. Apply S-UNI-VAR.

**Subcase** Otherwise.

Since $\mathcal{C}$ is normalized, it must be that case that no equality constraint determines the shape of $\alpha$. Since any such equality would normalize to $\alpha = \tau = \epsilon$, contradicting our assumption that $\mathcal{C}$ is normalized.

By elimination on the structure of $R$, the only constraints that could determine the shape of $\alpha$ are incremental instantiation constraints that copy $\alpha$. So there exists a partial instantiation constraint $i^x(\alpha) \rightsquigarrow \gamma$ such that $\mathcal{C}'[i^x(\alpha) \rightsquigarrow \gamma] = \mathcal{C}[\text{true}]$ and $\mathcal{C}'[\gamma!\zeta]$.

By induction, we have $\vdash \mathcal{C}'[\gamma!\zeta]$. From S-UNI-BACKPROP, we have $\vdash \mathcal{C}[\alpha!\zeta]$.

**Case** $\iff$. Follows from Lemma C.10.

□

**LEMMA C.12 (UNIFICATION PRESERVATION).** If $U_1 \to U_2$, then $U_1 \equiv U_2$

**PROOF.** By induction on the given derivation $U_1 \to U_2$. See Pottier and Rémy [2005] for more details.

□

**THEOREM 5.7 (PRESERVATION).** If $C_1 \to C_2$, then $C_1 \equiv C_2$.

**PROOF.** We proceed by induction on the given derivation. It suffices to show that for each individual rule $R (C_1 \to_R C_2)$, that $C_1 \equiv_{\text{ctx}} C_2$.
**Case**

$$ \begin{array}{ccc} U_1 & \rightarrow & U_2 \\ \cline{3-3} U_2 & & \end{array} \quad \text{S-UNIF} $$

$U_1 \rightarrow U_2$ Premise

$U_1 \equiv U_2$ Lemma C.12

$U_1, U_2$ simple Lemma C.4

$\text{ contra } U_1 \equiv \text{ctx } U_2$ Lemma C.3

**Case**

$$ \frac{ (\exists \alpha. C_1) \land C_2 \qquad \alpha \# C_2 }{ \exists \alpha. C_1 \land C_2 } \rightarrow \text{S-EXISTS-CONJ} $$

$\alpha \# C_2$ Premise

Sufficient to show equivalence for simple constraints. Lemma C.8

Suppose $C_1, C_2$ simple. Premise

**Subcase** $\Rightarrow$ .

For all $\phi$

$\phi \vdash (\exists \alpha. C_1) \land C_2$ Premise

$\phi[\alpha := g] \vdash C_1$ Simple inversion

$\phi \vdash C_2$ Simple inversion

$\phi[\alpha := g] \vdash C_2$ $\alpha \# C_2$

$\phi[\alpha := g] \vdash C_1 \land C_2$ By CONJ

$\text{ contra } \phi \vdash \exists \alpha. C_1 \land C_2$ By EXISTS

**Subcase** $\Leftarrow$ .

Symmetric argument.

**Case** S-LET, S-TRUE, S-FALSE, S-LET-EXISTSRIGHT, S-LET-CONJLEFT, S-LET-CONJRIGHT, S-INST-NAME, S-EXISTS-EXISTS-INST, S-EXISTS-INST-CONJ, S-EXISTS-INST-LET, S-EXISTS-INST-SOLVE, S-ALL-CONJ.

Similar argument to the S-EXISTS-CONJ case.

**Case**

$$ \frac{ \text{let } x \ \alpha \ [\bar{\alpha}] = \exists \beta. C_1 \text{ in } C_2 \qquad \beta \ \# \ \alpha, \bar{\alpha}, C_2 }{ \text{let } x \ \alpha \ [\bar{\alpha}, \beta] = C_1 \text{ in } C_2 } \rightarrow \text{S-LET-EXISTSLEFT} $$

If we have $\phi \vdash \text{let } x \ \alpha \ [\bar{\alpha}] = \exists \beta. C_1$ in $C_2$, then for each instance $(i^x := \phi'_i) \in \phi$ we have $\phi'_i \vdash \exists \beta. C_1$. By simple inversion, we have $\phi'_i \vdash \exists \beta. C_1$ if and only if $\phi'_i [\beta := g_i] \vdash C_1$ for some $g_i$, and so our derivation

$$ \phi[\overline{i^x := \phi'_i}] \vdash \text{let } x \ \alpha \ [\bar{\alpha}] = \exists \beta. C_1 \text{ in } C_2 $$

corresponds to exactly one derivation

$$ \phi[\overline{i^x := \phi'_i [\beta := g_i]}] \vdash \text{let } x \ \alpha \ [\bar{\alpha}, \beta] = C_1 \text{ in } C_2 $$
**Case**

$$ \frac{\mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}] \quad \vdash \quad \mathscr{C}[\tau!\zeta]}{\mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]} \rightarrow_{\text{S-MATCH-CTX}} \text{S-MATCH-CTX} $$

Premise

$\mathscr{C}[\tau!\zeta]$ Lemma C.10

Sufficient to show equivalences between constraints. Lemma B.2

**Subcase** $\Rightarrow$.

For all $\phi$

$\phi \vdash \mathscr{C}[\text{match } \alpha \text{ with } \bar{\chi}]$ Premise

■ $\phi \vdash \mathscr{C}[\text{match } \alpha := \text{shape}(\tau) \text{ with } \bar{\chi}]$ Lemma B.6

**Subcase** $\Leftarrow$.

For all $\phi$

$\phi \vdash \mathscr{C}[\text{match } \alpha := \text{shape}(\tau) \text{ with } \bar{\chi}]$ Premise

■ $\phi \vdash \mathscr{C}[\text{match } \alpha \text{ with } \bar{\chi}]$ By MATCH-CTX

**Case**

$$ \frac{\text{let } x \ \alpha \ [\bar{\alpha}] = C \text{ in } \mathscr{C}[x \ \tau] \qquad \gamma \ # \ \tau \qquad x \ # \ \text{bv}(\mathscr{C})}{\text{let } x \ \alpha \ [\bar{\alpha}] = C \text{ in } \mathscr{C}[\exists \gamma, i^x. \gamma = \tau \land i(\alpha) \to \gamma]} \rightarrow_{\text{S-LET-APP}} $$

$\gamma \ # \ \tau$ Premise

$x \ # \ \text{bv}(\mathscr{C})$ Premise

Sufficient to show a simple equivalence between $x \tau$ and $\exists \gamma, i^x. \gamma = \tau \land i(\alpha) \to \gamma$. Lemma C.9

Suppose $\phi'(x) = \phi(\lambda\alpha[\bar{\alpha}].C)$. Premise

**Subcase** $\Rightarrow$.

$\phi' \vdash x \ \tau$ Premise

$(\phi'(\tau), \phi_1) \in \phi'(x)$ Simple inversion

$\phi'(\tau) = \phi_1(\alpha)$ Defn. of $\phi(\lambda\alpha[\bar{\alpha}].C)$

$\phi'[\gamma := \phi'(\tau), i := \phi_1] \vdash i(\alpha) \to \gamma$ By INCR-INST

$\phi'[\gamma := \phi'(\tau), i := \phi_1] \vdash \gamma = \tau$ By UNIF

■ $\phi' \vdash \exists \gamma, i^x. \gamma = \tau \land i(\alpha) \to \gamma$ By EXISTS, EXISTS-INST and CONJ

**Subcase** $\Leftarrow$.

Symmetric argument.

**Case**

$$ \frac{\text{let } x \ \alpha \ [\bar{\alpha}] = C \text{ in } \mathscr{C}[i^x(\alpha') \to \gamma] \qquad \alpha' \in \alpha, \bar{\alpha} \qquad \neg\text{cyclic}(C) \qquad \bar{\beta}' \ # \alpha', \gamma, \bar{\beta} \qquad x \ # \ \text{bv}(\mathscr{C})}{\text{let } x \ \alpha \ [\bar{\alpha}] = C \text{ in } \mathscr{C}[\exists \bar{\beta}'. \gamma = \zeta \bar{\beta}' \land i^x(\bar{\beta}) \to \bar{\beta}'] \rightarrow_{\text{S-INST-COPY}} \text{S-INST-COPY}} $$

$x \ # \ \text{bv}(\mathscr{C})$ Premise

$\bar{\beta}' \ # \alpha', \gamma, \bar{\beta}$ Premise

Sufficient to show equivalence between $i^x(\alpha') \to \gamma$ and $\exists \bar{\beta}'. \gamma = \zeta \bar{\beta}' \land i^x(\bar{\beta}) \to \bar{\beta}'$. Lemma C.9

Suppose $\phi'(x) = \phi(\lambda\alpha[\bar{\alpha}].C)$. Premise
**Subcase** $\Rightarrow$.

$\phi' \vdash i^x(\alpha') \Rightarrow \gamma$
$(g, \phi_1) \in \phi'(x)$
$\exists i^x \in \mathscr{C}$
Premise

$\phi'(i) = \phi_1$

$\phi'(\gamma) = \phi(i)(\alpha')$ 
= $\phi_1(\alpha')$ 
Simple inversion 
Above

$\phi_1 \vdash C' \wedge \alpha' = \zeta \bar{\beta} = \epsilon$ 
Above

$\phi_1 \vdash \alpha' = \zeta \bar{\beta} = \epsilon$ 
Simple inversion

$\phi_1(\alpha') = \zeta \phi_1(\bar{\beta})$ 
"

$\phi'(\gamma) = \zeta \phi_1(\bar{\beta})$ 
Above

$\phi'[\bar{\beta}' := \phi_1(\bar{\beta})] \vdash \gamma = \zeta \bar{\beta}'$ 
By UNIF

$\phi'[\bar{\beta}' := \phi_1(\bar{\beta})] \vdash i^x(\bar{\beta}) \Rightarrow \bar{\beta}'$ 
By INCR-INST

<figure><img src="image_28.png" /></figure>

$\phi' \vdash \exists \bar{\beta}'. \gamma = \zeta \bar{\beta}' \wedge i^x(\bar{\beta}) \Rightarrow \bar{\beta}'$ 
By EXISTS and CONJ

**Subcase** $\Leftarrow$.

Symmetric argument.

**Case**

$\frac{i(\alpha) \Rightarrow \gamma_1 \wedge i(\alpha) \Rightarrow \gamma_2}{i(\alpha) \Rightarrow \gamma_1 \wedge \gamma_1 = \gamma_2}$ 
S-INST-UNIF

Sufficient to show equivalence between $i(\alpha) \Rightarrow \gamma_1 \wedge i(\alpha) \Rightarrow \gamma_2$ and $i(\alpha) \Rightarrow \gamma_1 \wedge \gamma_1 = \gamma_2$. Lemma C.8

**Subcase** $\Rightarrow$.

$\phi \vdash i(\alpha) \Rightarrow \gamma_1 \wedge i(\alpha) \Rightarrow \gamma_2$ 
Premise
$\phi \vdash i(\alpha) \Rightarrow \gamma_1$ 
Simple inversion
$\phi \vdash i(\alpha) \Rightarrow \gamma_2$ 
"

$\phi(\gamma_1) = \phi(i)(\alpha)$ 
"

$\phi(\gamma_2) = \phi(i)(\alpha)$ 
" 
$\phi(\gamma_1) = \phi(\gamma_2)$ 
Above

<figure><img src="image_29.png" /></figure>

$\phi \vdash i(\alpha) \Rightarrow \gamma_1 \wedge \gamma_1 = \gamma_2$ 
By CONJ

**Subcase** $\Leftarrow$.

Symmetric argument.

**Case**

$\frac{\text{let } x \ \alpha \ [\bar{\alpha}] = \bar{\epsilon} \wedge C \text{ in } \mathscr{C}[i^x(\alpha') \Rightarrow \gamma] \\ \forall \alpha'. \exists \alpha, \bar{\alpha}. \bar{\epsilon} \equiv \text{true} \qquad \alpha' \in \alpha, \bar{\alpha} \qquad \alpha' \# C \qquad i(\alpha') \# \text{insts}(\mathscr{C}) \qquad x \# \text{bv}(\mathscr{C})}{\text{let } x \ \alpha \ [\bar{\alpha}] = \bar{\epsilon} \wedge C \text{ in } \mathscr{C}[\text{true}]}$ 
S-INST-POLY

$\forall \alpha'. \exists \alpha, \bar{\alpha}. \bar{\epsilon} \equiv \text{true}$ 
Premise

$\alpha' \# C$ 
Premise

$i(\alpha') \# \text{insts}(\mathscr{C})$ 
Premise

$x \# \text{bv}(\mathscr{C})$ 
Premise

Sufficient to show equivalence between $i^x(\alpha') \Rightarrow \gamma$ and true. Lemma C.9

Suppose $\phi'(x) = \phi(\lambda\alpha[\bar{\alpha}, \alpha'|. \bar{\epsilon} \wedge C)$. Premise
**Subcase** $\implies$.

$\phi' \vdash i^x(\alpha') \rightsquigarrow \gamma$ Premise

■ $\phi' \vdash \text{true}$ By TRUE

**Subcase** $\iff$.

$\phi' \vdash \text{true}$ Premise
$(g, \phi_1) \in \phi'(x)$ $\mathscr{C} = \mathscr{C}_1[\exists i^x. \mathscr{C}_2]$ \\
$\phi'(i) = \phi_1$ $''$

By cases on $\phi_1(\alpha')$.

**Subsubcase** $\phi_1(\alpha') = \phi'(\gamma)$.

$\phi_1(\alpha') = \phi'(\gamma)$ Premise

■ $\phi' \vdash i^x(\alpha') \rightsquigarrow \gamma$ By INCR-INST

**Subsubcase** $\phi_1(\alpha') \neq \phi'(\gamma)$.

Let $\phi_2 = \phi_1[\alpha' := \phi'(\gamma)]$.

$\phi_1 \vdash \bar{\epsilon} \wedge C$ By definition

$\phi_1 \vdash \bar{\epsilon}$ Simple inversion

$\phi_2 \vdash \bar{\epsilon}$ $\alpha'$ is polymorphic

$\phi_2 \vdash C$ $\alpha' \# C$

$\phi_2 \vdash \bar{\epsilon} \wedge C$ By CONJ

$(g, \phi_2) \in \phi(x)$ By definition
Suppose $\phi_3 \vdash \mathscr{C}_2[\text{true}]$. Considering entailment on $\exists i^x$.

$\phi_3(i) = \phi_1$ $''$
$\phi_3[i := \phi_2] \vdash \mathscr{C}_2[\text{true}]$ $i(\alpha') \# \text{insts}(\mathscr{C}_2)$

$\mathscr{D} :: \phi_3 \vdash \mathscr{C}_2[\text{true}]$ By EXISTS-INST

$\mathscr{D}$ is a derivation that satisfies $\phi_1(\alpha') = \phi'(\gamma)$.

■ So this case degenerates to the former case.

**Case**

$\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[i^x(\beta) \rightsquigarrow \gamma] \quad \beta \notin \alpha, \bar{\alpha} \quad x, \beta \# \text{bv}(\mathscr{C}) \xrightarrow{\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[\beta = \gamma]} \text{S-INST-MONO}$

$\beta \# \alpha, \bar{\alpha}$ Premise

$x, \beta \# \text{bv}(\mathscr{C})$ Premise

Sufficient to show equivalence between $i^x(\beta) \rightsquigarrow \gamma$ and $\beta = \gamma$. Lemma C.9

Suppose $\phi'(x) = \phi(\lambda\alpha[\bar{\alpha}].C)$. Premise

**Subcase** $\implies$.

$\phi' \vdash i^x(\beta) \rightsquigarrow \gamma$ Premise

$(\lhd \phi_1) \in \phi(C)$ $\exists i^x. \in \mathscr{C}$

$\phi'(i) = \phi_1$ $''$

$\phi'(\gamma) = \phi_1(\beta)$ Simple inversion

$\phi_1(\beta) = \phi(\beta)$ $\beta \# \alpha, \bar{\alpha}$

$\phi'(\beta) = \phi(\beta)$ $\beta \# \text{bv}(\mathscr{C})$

$\phi'(\gamma) = \phi'(\beta)$ Above

$\phi' \vdash \gamma = \beta$ By UNIF
**Subcase** ⇐.

Symmetric argument.

**Case**

$$ \frac{\text{let } x \ \alpha \ [\bar{\alpha}] = \bar{\epsilon} \ \text{in } C \qquad x \ #C \qquad \exists \alpha, \bar{\alpha}. \bar{\epsilon} \equiv \text{true}}{C} \rightarrow \text{S-LET-SOLVE} $$

x #C Premise

$\exists \alpha, \bar{\alpha}. \bar{\epsilon} \equiv \text{true}$

Sufficient to show equivalence for simple constraints. Lemma C.8

Suppose C simple. Premise

**Subcase** ⇐.

For all $\phi$

$\phi \vdash \text{let } x \ \alpha \ [\bar{\alpha}] = \bar{\epsilon} \ \text{in } C$ Premise

$\phi \vdash \exists \alpha, \bar{\alpha}. \bar{\epsilon}$ Simple inversion

$\phi[x := \phi(\lambda\alpha[\bar{\alpha}].\bar{\epsilon})] \vdash C$ "

<figure><img src="image_30.png" /></figure>

$\phi \vdash C$ x #C

**Subcase** ⇐.

For all $\phi$

$\phi \vdash C$ Premise

$\phi[x := \phi(\lambda\alpha[\bar{\alpha}].\bar{\epsilon})] \vdash C$ x #C

$\phi \vdash \exists \alpha, \bar{\alpha}. \bar{\epsilon}$

<figure><img src="image_31.png" /></figure>

$\phi \vdash \text{let } x \ \alpha \ [\bar{\alpha}] = \bar{\epsilon} \ \text{in } C$ By LETR

**Case**

$$ \frac{\text{let } x \ \alpha \ [\bar{\alpha}, \bar{\beta}] = C_1 \ \text{in } C_2 \qquad \exists \alpha, \bar{\alpha}. C_1 \ \text{determines } \bar{\beta}}{\exists \bar{\beta}. \text{let } x \ \alpha \ [\bar{\alpha}] = C_1 \ \text{in } C_2} \rightarrow \text{S-EXISTS-LOWER} $$

$\exists \alpha, \bar{\alpha}. C_1$ determines $\bar{\beta}$ Premise

Sufficient to show equivalence for simple constraints. Lemma C.8 and Lemma C.7

Suppose $C_1, C_2$ simple. Premise

**Subcase** ⇐.

$\phi \vdash \text{let } x \ \alpha \ [\bar{\alpha}, \bar{\beta}] = C_1 \ \text{in } C_2$ Premise

$\phi \vdash \exists \alpha, \bar{\alpha}, \bar{\beta}. C_1$ Simple inversion

$\phi[x := \phi(\lambda\alpha[\bar{\alpha}, \bar{\beta}].C_1)] \vdash C_2$ "

$\phi[\alpha := \mathfrak{g}, \bar{\alpha} := \bar{\mathfrak{g}}, \bar{\beta} := \bar{\mathfrak{g}}'] \vdash C_1$ "

$\phi[\bar{\beta} := \bar{\mathfrak{g}}'] \vdash \exists \alpha, \bar{\alpha}. C_1$ By EXISTS

Sufficient to show $\phi[x := \phi(\lambda\alpha[\bar{\alpha}, \bar{\beta}].C_1)] = \phi[\bar{\beta} := \bar{\mathfrak{g}}](\lambda\alpha[\bar{\alpha}].C_1)$.

**Subsubcase** ⇐.

$\phi[\alpha := \mathfrak{g}_1, \bar{\alpha} := \bar{\mathfrak{g}}_1, \bar{\beta} := \bar{\mathfrak{g}}_2] \vdash C_1$ Premise

$\phi[\bar{\beta} := \bar{\mathfrak{g}}_2] \vdash \exists \alpha, \bar{\alpha}. C_1$ By EXISTS

$\bar{\mathfrak{g}}_2 = \bar{\mathfrak{g}}'$ By definition of determines

$\text{■} \quad \phi[\bar{\beta} := \bar{\mathfrak{g}}', \alpha := \mathfrak{g}_1, \bar{\alpha} := \bar{\mathfrak{g}}_1] \vdash C_1$ Above

**Subsubcase** ⇐.

Symmetric argument.
**Subcase** ⇐.

Symmetric argument.

**Case** S-COMPRESS, S-GC, S-EXISTS-ALL, S-ALL-ESCAPE, S-ALL-RIGID, S-ALL-SOLVE.

Similar argument. Use Lemma C.8. The simple equivalences are standard, see Pottier and Rémy [2005].

☐

## C.2 Progress

LEMMA C.13 (UNIFICATION PROGRESS). If unification problem $U$ cannot take a step $U \rightarrow U'$, then either:

(i) $U$ is solved.

(ii) $U$ is false.

**PROOF.** This is a standard result. See Pottier and Rémy [2005]. ☐

☐

THEOREM C.14 (PROGRESS). If constraint $C$ cannot take a step $C \rightarrow C'$, then either:

(1) $C$ is solved.

(2) $C$ is stuck, it is either: (a) false; (b) $\hat{C}[x \tau]$ where $x \# \hat{C}$; (c) $\hat{C}[i^x(\alpha) \rightarrow \gamma]$ where $x \# \hat{C}$ and $i(\alpha) \# \text{insts}(\hat{C})$; (d) for every match constraint $\hat{C}$ [match $\alpha$ with $\bar{\chi}$] in $C$, $\hat{C}[\alpha!\zeta]$ does not hold for any $\zeta$. Here, $\hat{C}$ is a normal context, i.e., such that no other rewrites can be applied.

**PROOF.** We proceed by induction on the structure of $C$. We focus on suspended match constraints, conjunctions, and let rules.

**Case** match $\tau$ with $\bar{\chi}$. We have two cases:

**Subcase** $\tau$ is a non-variable type. Apply S-MATCH-CTX using S-UNI-TYPE

**Subcase** $\tau$ is a type variable $\alpha$.

We have $\square[\alpha \nparallel]$. It suffices that every match constraint in a context-reachable position $\hat{C}$ [match $\alpha'$ with $\bar{\chi}$] satisfies $\hat{C}[\alpha' \nparallel]$. By the definition of constraint contexts, there is only one such $\hat{C}$, namely $\square$, for which we already have $\square[\alpha \nparallel]$. Hence match $\tau$ with $\bar{\chi}$ is stuck.

**Case** $C_1 \land C_2$. We begin by inducting on $C_1$ and $C_2$. Then we consider cases:

**Subcase** $C_1$ (or $C_2$) take a step. Apply congruence rewriting rule.

**Subcase** $C_1$ (or $C_2$) is true. Apply S-TRUE.

**Subcase** $C_1$ (or $C_2$) is false. Apply S-FALSE.

**Subcase** $C_1$ (or $C_2$) begins with $\exists$. Apply S-EXISTS-CONJ.

**Subcase** $C_1, C_2$ are solved.

We either apply the above $\exists$ case, or both $C_1$ and $C_2$ are solved multi-equations $\bar{\epsilon}_1, \bar{\epsilon}_2$. We perform cases on this:

**Subsubcase** $\bar{\epsilon}_1$ and $\bar{\epsilon}_2$ are mergable. Apply U-MERGE.

**Subsubcase** cyclic($\bar{\epsilon}_1, \bar{\epsilon}_2$). Apply U-CYCLE.

**Subsubcase** Otherwise. The conjunction $\bar{\epsilon}_1 \land \bar{\epsilon}_2$ is solved.

**Subcase** $C_1$ and $C_2$ are stuck (and not false).

w.l.o.g., consider cases $C_1$.

**Subsubcase** $\hat{C}_1[x \tau]$. We have $x \# \text{bv}(\hat{C}_1)$.

$\hat{C}_1[x \tau] \land C_2$ is stuck as we do not bind $x$ in $\hat{C}_1 \land C_2$.

**Subsubcase** $\hat{C}_1[i^x(\alpha) \rightarrow \gamma]$. We have $x \# \text{bv}(\hat{C}_1)$ and $i(\alpha) \# \text{insts}(\hat{C}_1)$.
If $i(\alpha) \in \text{insts}(C_2)$ and $i \# \text{bv}(\hat{C}_1)$, then apply **S-INST-UNIFY**. It must be the case that we can apply **S-INST-UNIFY**, otherwise, we could lift these instantiation constraints using **S-EXISTS-LOWER** and **S-LET-CONJLEFT**, contradicting that $\hat{C}_1$ is stuck.

Otherwise, $x \# \text{bv}(\hat{C}_1 \wedge C_2)$, thus $\hat{C}_1[i^x(\alpha) \to \gamma]$ is stuck.

**Subsubcase** $\hat{C}_1[\text{match } \alpha' \text{ with } \bar{\chi}]$. We have $\mathcal{C}_1[\alpha' \nparallel]$. Consider a match constraint match $\alpha'$ with $\bar{\chi}$ in $C_1$.

If $\vdash [\hat{C}_1[-] \wedge C_2][\alpha'!\zeta]$. Then we can apply **S-MATCH-CTX**.

Otherwise $\vdash' [\hat{C}_1[-] \wedge C_2][\alpha'!\zeta]$. We have Lemma C.11, so we are stuck and $(\mathcal{C}_1 \wedge C_2)[\alpha' \nparallel]$.

**Case** let $x \alpha [\bar{\alpha}] = C_1$ in $C_2$. We begin by inducting on $C_1$ and $C_2$. Then we consider cases:

**Subcase** $C_1$ (or $C_2$) take a step. Apply congruence rewriting rule.

**Subcase** $C_1$ (or $C_2$) is false. Apply **S-FALSE**.

**Subcase** $C_1$ begins with $\exists$. Apply **S-LET-EXISTSLEFT**

**Subcase** $C_2$ begins with $\exists$. Apply **S-LET-EXISTSRIGHT**

**Subcase** $C_2$ begins with $\wedge$ with $x \# \text{ from conjunct}$. Apply **S-LET-CONJRIGHT**.

**Subcase** $C_1$ begins with $\wedge$ with $\alpha, \bar{\alpha} \# \text{ from conjunct}$. Try apply **S-LET-CONJLEFT**

**Subcase** $C_2$ begins with $\exists i^{x'}, x \neq x'$. Apply **S-EXISTS-INST-LET**

**Subcase** $\alpha' \in \bar{\alpha}$ is determined by $C_1$. Apply **S-EXISTS-LOWER**

**Subcase** $C_2$ is solved.

Thus $C_2$ must be true (due to above cases).

**Subsubcase** $C_1$ is solved. Thus $C_1$ must be $\bar{\epsilon}$.

There are two cases:

* $\exists \alpha, \bar{\alpha}. \bar{\epsilon} \equiv \text{true}$. Apply **S-LET-SOLVE**.

* $\exists \alpha, \bar{\alpha}. \bar{\epsilon} \neq \text{true}$. It must be the case there is some $\beta$ that dominates a $\alpha'$ in $\alpha, \bar{\alpha}$ in $\bar{\epsilon}$. Hence $\exists \alpha, \bar{\alpha} \setminus \alpha'$. $\bar{\epsilon}$ determines $\alpha'$. So we can apply **S-EXISTS-LOWER**.

**Subsubcase** $C_1$ is stuck.

The constraint let $x \alpha [\bar{\alpha}] = C_1$ in $C_2$ remains stuck, since no additional term variable bindings occur for the scope of $C_1$, ruling out the instantiation cases. Additionally, we cannot apply backpropagation since $C_2$ is true.

**Subcase** $C_2$ is stuck.

**Subsubcase** $\hat{C}[x \tau]$. We have $x \# \text{bv}(\hat{C})$.

Apply **S-LET-APPR**.

**Subsubcase** $\hat{C}[i^x(\alpha') \to \gamma]$. We have $x \# \text{bv}(\hat{C})$ or $i(\alpha') \# \text{insts}(\hat{C})$.

* $\alpha' \in \alpha, \bar{\alpha}$.

We can either apply **S-INST-COPY** or **S-COMPRESS** if a multi-equation involving $\alpha'$ occurs in $C_1$.

Otherwise, we consider cases where $C_1$ is solved or stuck.

If $C_1$ is solved, then it must be of the form $\bar{\epsilon}$. There are two cases:

- $\exists \alpha, \bar{\alpha}. \bar{\epsilon} \equiv \text{true}$. As $\alpha'$ does not appear in the head position of any multi-equation in $\bar{\epsilon}$, it must be polymorphic. Thus $\forall \alpha'. \exists \alpha, \bar{\alpha} \setminus \alpha'$. $\bar{\epsilon} \equiv \text{true}$. So we can apply **S-INST-POLY**.

- $\exists \alpha, \bar{\alpha}. \bar{\epsilon} \neq \text{true}$. Apply **S-EXISTS-LOWER** (using the same logic as above).

If $C_1$ is stuck, then neither stuck case regarding instantiations in $C_1$ is fixed, so in these cases the constraint remains stuck. If $C_1$ is stuck with $\hat{C}'[\text{match } \beta \text{ with } \bar{\chi}']$. Then either backpropagation (via **S-UNI-BACKPROP** and **S-MATCH-CTX**) applies with an equation in $\hat{C}$, or the entire constraint is stuck (by Lemma C.11).

* $\alpha' \notin \alpha, \bar{\alpha}$. Apply **S-INST-MONO**.

**Subsubcase** For any $\hat{C}[\text{match } \alpha' \text{ with } \bar{\chi}]$. We have $\hat{C}[\alpha' \nparallel]$.
Either let $x \alpha [\bar{\alpha}] = C_1$ in $C_2$ can progress with an instantiation constraint (in the above case) to discharge the match constraint or let $x \alpha [\bar{\alpha}] = C_1$ in $C_2$ is stuck.

☐

### C.3 Termination

This section presents a proof of termination for our solver. Most rewrite rules, in both unification and constraint solving, are *destructive*—that is, they eliminate or modify the structure of a constraint in a way that prevents the rule from begin applied again. Consequently, to establish termination, it suffices to consider only those rules that are not inherently destructive.

**LEMMA C.15 (UNIFICATION TERMINATION).** *The unifier terminates on all inputs.*

**PROOF.** Let every shape $\zeta$ have an integer weight defined by $\mathrm{sw}(\zeta) \triangleq 4 + 2 \times |\zeta|$, where $|\zeta|$ is the arity of the shape $\zeta$. The weight of a type $\mathrm{tw}(\tau)$ is defined by:

$$
\begin{align*}
\mathrm{tw}(\alpha) &\triangleq 1 \\
\mathrm{tw}(\zeta \bar{\tau}) &\triangleq \mathrm{iw}(\zeta \bar{\tau}) - 2 \\
\mathrm{iw}(\alpha) &\triangleq 0 \\
\mathrm{iw}(\zeta \bar{\tau}) &\triangleq \mathrm{sw}(\zeta) + \mathrm{iw}(\bar{\tau}) \\
\mathrm{iw}(\bar{\tau}) &\triangleq \sum_{i=1}^{n} \mathrm{iw}(\tau_i)
\end{align*}
$$

The helper $\mathrm{iw}(\tau)$ computes the “internal” weight of $\tau$; in the common case of shallow types it is just the weight of its head shape.

We define the weight of a multi-equation as the sum of the weights of its members. The weight of a unification problem $\mathrm{uw}(U)$ is defined as the sum of the weights of its multi-equations.

In $U \rightarrow U'$, the rules U-DECOMP and U-NAME are not obviously destructive, as they may introduce new constraints that are structurally larger than the constraint being rewritten.

However, we show that this is not problematic: in both cases, the unification weight $\mathrm{uw}(U)$ strictly decreases. The remaining rules are obviously destructive and either maintain or decrease the unification weight.

#### Case

$$ \frac{\underset{\zeta \bar{\alpha} = \epsilon}{\zeta \bar{\alpha} = \zeta \bar{\beta}} = \epsilon}{\underset{\zeta \bar{\alpha} = \epsilon \wedge \bar{\alpha} = \bar{\beta}}{\zeta \bar{\alpha} = \epsilon \wedge \bar{\alpha} = \beta}} \rightarrow \text{U-DECOMP} $$

We have:

$$
\begin{align*}
(+) \quad \mathrm{uw}(\zeta \bar{\alpha} = \zeta \bar{\beta} = \epsilon) &= \mathrm{tw}(\zeta \bar{\alpha}) + \mathrm{tw}(\zeta \bar{\beta}) + \mathrm{tw}(\epsilon) \\
(-) \quad \mathrm{uw}(\zeta \bar{\alpha} = \epsilon \wedge \bar{\alpha} = \bar{\beta}) &= \mathrm{tw}(\zeta \bar{\alpha}) + \mathrm{tw}(\epsilon) + \mathrm{tw}(\bar{\alpha}) + \mathrm{tw}(\bar{\beta}) \\
&= \frac{\mathrm{tw}(\zeta \bar{\beta}) - \mathrm{tw}(\bar{\alpha}) - \mathrm{tw}(\bar{\beta})}{(\mathrm{sw}(\zeta) + 0 - 2) - 2|\zeta|} \\
&= \frac{(2 + 2|\zeta|) - 2|\zeta|}{2} = 2
\end{align*}
$$

Hence $\mathrm{uw}(\zeta \bar{\alpha} = \zeta \bar{\beta} = \epsilon) > \mathrm{uw}(\zeta \bar{\alpha} = \epsilon \wedge \bar{\alpha} = \bar{\beta})$.
Case

$$ \frac{\zeta(\bar{\tau}, \tau_i, \bar{\tau}') = \epsilon \qquad \alpha \# \bar{\tau}, \bar{\tau}', \epsilon \qquad \tau_i \notin \mathcal{V} \qquad \exists \alpha. \zeta(\bar{\tau}, \alpha, \bar{\tau}') = \epsilon \wedge \alpha = \tau_i}{\text{U-NAME}} $$

Given $\tau_i \notin \mathcal{V}$, by Theorem 3.2, $\tau_i = \zeta' \bar{\tau}''$ for some shape $\zeta'$ and types $\bar{\tau}''$. So we have:

$$ \begin{align*} (+) \quad \text{uw } (\zeta(\bar{\tau}, \tau_i, \bar{\tau}') = \epsilon) &= \text{sw } (\zeta) + \text{iw } (\bar{\tau}) + \text{iw } (\tau_i) + \text{iw } (\bar{\tau}') - 2 + \text{uw } (\epsilon) \\ (-) \quad \text{uw } (\exists \alpha. \alpha = \tau_i \wedge \zeta(\bar{\tau}, \alpha, \bar{\tau}') = \epsilon) &= \text{sw } (\zeta) + \text{iw } (\bar{\tau}) + 0 + \text{iw } (\bar{\tau}') - 2 + \text{uw } (\epsilon) + 1 + \text{tw } (\tau_i) \\ &= \text{iw } (\tau_i) - \text{iw } (\alpha) - \text{tw } (\tau_i) - 1 \\ &= \text{iw } (\tau_i) - 0 - (\text{iw } (\tau_i) - 2) - 1 \\ &= \mathbf{1} \end{align*} $$

$$ \text{Hence } \text{uw } (\zeta(\bar{\tau}, \tau_i, \bar{\tau}') = \epsilon) > \text{uw } (\exists \alpha. \zeta(\bar{\tau}, \alpha, \bar{\tau}') = \epsilon \wedge \alpha = \tau_i). $$

□

**THEOREM 5.6 (TERMINATION).** *The constraint solver terminates on all inputs.*

*PROOF.* The difficulty for termination comes from the “suspended match discharge” rule S-MATCH-CTX which can make arbitrary sub-constraints appear in the non-suspended part of the constraint; and from the instantiation rules that copy/duplicate existing structure in another part of the constraint, increasing its total size.

As we argued before, the other rewrite rules are *destructive*, they strictly simplify the constraint towards a normal form and can only be applied finitely many times when taken together. The fragment without discharge rules and incremental instantiation is also extremely similar to the constraint language of Pottier and Rémy [2005], so their termination proof applies directly.

*Discharge rules.* The discharge rules strictly decrease the number of occurrences of suspended match constraint (if we also count nested suspended constraints), and no rewriting rule introduces new suspended match constraints. So these discharge rules can only be applied finitely many times. To prove termination of constraint solving, it thus suffices to prove that rewriting sequences that do not contain one of the discharge rules (those that occur in-between two discharge rules) are always finite.

*Starting instantiations.* By a similar argument, the number of non-incremental instantiations $x \tau$ decreases strictly on S-LET-APPR when an incremental instantiation starts, and is preserved by other non-discharge rules. The rule S-LET-APPR can thus only occur finitely many times in non-discharging sequences, and it suffices to prove that all rewriting sequences that are non-discharging and do not contain S-LET-APPR are finite.

*Other instantiation rules.* Among other instantiation rules, the rule of concern is S-INST-COPY, which is not destructive: it introduces new instantiation constraints and structurally increases the size of the constraint.

Intuitively, S-INST-COPY should not endanger termination because the amount of copying it can perform for a given instantiation is bounded by the size of the types in the constraint C it is copying from. (C could have cyclic equations with infinite unfoldings, but S-INST-COPY forbids copying in that case.) The difficulty is that rewrites to C can be interleaved with instantiation rules, so that the equations that are being copied can grow strictly during instantiation.

To control this, we perform a structural induction: to prove that (let $x \alpha$ $[\bar{a}]$ = $C_1$ in $C_2$) does not contain infinite non-discharging non-instance-starting rewrite rules, we can assume that the result holds for the strictly smaller constraint $C_1$, and then prove termination of the incremental instantiations of $x$ in $C_2$. (The notion of structural size used here is preserved by non-discharging rewrite rules, as they do not affect the let-structure of the constraint.)
Assuming that $C_1$ has no infinite rewriting sequence, it suffices to prove that only finitely many
rewrites in the rest of the constraint (namely $C_2$) can occur between each rewrite of $C_1$.

We define a weight that captures the contribution of types within $C_1$ to the partial instances
in $C_2$:

$$
\mathrm{tw}(\zeta \bar{\tau}) \triangleq 2 \times \mathrm{sw}(\zeta) + \sum_{i=1}^{n} \mathrm{tw}(\tau_i)
$$

$$
\mathrm{tw}(\alpha) \triangleq \begin{cases} \sup \{\mathrm{tw}(\tau) : \alpha = \tau \in C_1\} & \text{if } C_1 \text{ is acyclic} \\ 0 & \text{otherwise} \end{cases}
$$

The weight of a incremental instantiation cw ($i^x(\alpha) \rightsquigarrow \tau$) is defined as the sum of tw ($\tau$) and tw ($\alpha$). The weight of other constraints is given using the measure uw defined in the proof of Lemma C.15.

Case

$$
\frac{
  \begin{array}{@{}c@{\quad}c@{}}
    \begin{array}{@{}c@{}} \text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C} [i^x(\alpha') \rightsquigarrow \gamma] \\
    \phantom{\text{let } } C = C' \wedge \alpha' = \zeta \bar{\beta} = \epsilon
  \end{array}
  &
  \begin{array}{@{}c@{}} \text{\textbf{a}} \alpha' \in \alpha, \bar{\alpha} \quad \neg\text{cyclic}(C) \quad \bar{\beta}' \# \alpha', \gamma, \bar{\beta} \quad \text{x} \# \text{bv}(\mathscr{C}) \\
    \text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C} [\exists \bar{\beta}'. \gamma = \zeta \bar{\beta}' \wedge i^x(\bar{\beta}) \rightsquigarrow \bar{\beta}']
  \end{array}
\end{array}
\right\}
\xrightarrow{\text{S-INST-COPY}}
$$

We aim to show that the weight of the rewritten constraint $\exists \bar{\beta}'. \gamma = \zeta \bar{\beta}' \wedge i^x(\bar{\beta}) \rightsquigarrow \bar{\beta}'$ is strictly less than the original $i^x(\alpha') \rightsquigarrow \gamma$.

$$
\mathrm{cw}(i^x(\alpha') \rightsquigarrow \gamma) = 1 + \mathrm{tw}(\alpha)
$$

$$
\geq 1 + 2 \times \mathrm{sw}(\zeta) + \sum_{i=1}^{n} \mathrm{tw}(\beta_i)
$$

$$
\mathrm{cw}(\exists \bar{\beta}'. \gamma = \zeta \bar{\beta}' \wedge i^x(\bar{\beta}) \rightsquigarrow \bar{\beta}') = 1 + \mathrm{sw}(\zeta) + \sum_{i=1}^{n} \mathrm{tw}(\beta_i) + |\bar{\beta}'|
$$

To ensure a strict decrease, it suffices to show that sw (ζ) > |β̃'|. Given that |β̃'| = |ζ|, and by the definition of sw (ζ), this inequality holds. Therefore, the weight strictly decreases under S-INST-COPY.

Thus the constraint solver terminates.

☐

C.4 Correctness

LEMMA C.16. Given non-simple C constraint. If every match constraint $\mathscr{C}$ [match $\tau$ with $\bar{\chi}$] = C satisfies $\mathscr{C}$ [$\tau \nparallel$], then C is unsatisfiable.

PROOF. By contradiction, inverting on the canonical derivation of C.

☐

LEMMA C.17 (SCOPE PRESERVATION). For all $C_1, C_2$, if $C_1 \rightarrow C_2$, then $fv(C_1) \supseteq fv(C_2)$.

PROOF. By induction on $C_1 \rightarrow C_2$.

☐

COROLLARY C.18. For the closed-term-variable constraint C, C is satisfiable if and only if $C \to^* \hat{C}$ and $\hat{C}$ is a solved form equivalent to C.

PROOF. We show each direction individually:

Case $\Rightarrow$.

By transfinite induction on the well-ordering of constraints whose existence is shown in Theo-
rem 5.6.

We have C is satisfiable. By Theorem C.14, we have three cases:

**Subcase** *C is solved*. We have $C \to^* C$ and $C \equiv C$ by reflexivity. So we are done.
**Subcase** *C* is *stuck*. Given *C* is a closed-term-variable constraint, it must be the case that either *C* is false or ᶜ*[match *τ* with *χ*] and ᶜ*[*τ* ≠ *χ*].

If C is false, this contradicts our assumption that C is satisfiable. Similarly, by Lemma C.16, if C is ᶜ'[match τ with χ], then this also contradicts the satisfiability of C.

**Subcase** $C \to C'$.

By Theorem 5.7, we have $C \equiv C'$, thus $C'$ is satisfiable. Additionally, by Lemma C.17, we have $fv(C') = \emptyset$. So by induction, we have $C' \to^* \hat{C}$ and $\hat{C}$ is a solved form equivalent to $C'$. By transitivity of equivalence, we therefore have $\hat{C} \equiv C$, as required.

**Case** ⇐.

By induction on the rewriting $C \to^* \hat{C}$.

**Subcase**

$$ \hat{C} \underset{\sim}{\longrightarrow}^* C \xrightarrow{\text{ZERO-STEP}} $$

We have $C = \hat{C}$ by inversion. All solved forms are satisfiable, thus C is satisfiable.

**Subcase**

$$ \frac{C \to C' \qquad C' \to^* \hat{C}}{C \to^* \hat{C}} \xrightarrow{\text{ONE-STEP}} $$

By induction, we have $C'$ is satisfiable. By Theorem 5.7, $C \equiv C'$, hence C is satisfiable.

☐

# D Properties of OmniML

This section states and proves the two central metatheoretic properties of OmniML. The first is the *soundness and completeness* of the constraint generator [[*e* : *α*]] with respect to the OmniML typing rules. The second is the existence of *principal types*, which follows as a consequence of soundness and completeness: every closed well-typed term *e* admits a most general type.

Throughout this section, we restrict our attention to *closed terms*. This is because the typing context Γ can contain bindings to terms whose type is “guessed”. When we generate constraints for a term *e* under a context Γ, we encode the type schemes in Γ as part of the constraint itself using let-constraints. However, these schemes are treated as known within the constraint! As a result, we assume terms are closed from the outside to avoid Γ leaking any guessed type information.

## D.1 Simple syntax-directed system

As a first step towards proving soundness and completeness of constraint generation, we first present a variant of the OmniML type system for *simple terms*. For this system, the syntax tree completely determines the derivation tree.

We use the standard technique of removing the INST and GEN rules, and always apply instantiations in VAR (VAR-SD) and always generalize at let-bindings (LET-SD). We can show that this system is sound and complete with respect to the declarative rules.

**THEOREM D.1 (SOUNDNESS OF THE SYNTAX DIRECTED RULES).** *Given the simple term e. If Γ ⊢<sup>sd</sup> simple e : τ then we also have Γ ⊢<sub>simple</sub> e : τ*.*

**PROOF.** Induction on the given derivation.

☐

**THEOREM D.2 (COMPLETENESS OF THE SYNTAX DIRECTED RULES).** *Given the simple term e. If Γ ⊢<sub>simple</sub> e : σ, then Γ ⊢<sub>simple</sub> e : τ for any instance τ of σ.*

**PROOF.** Induction on the given derivation.

☐
**Inversion.** On a simple syntax-directed derivation $\Gamma \vdash_{\text{simple}}^{\text{sd}} e : \tau$, we have the usual inversion principle:

**LEMMA D.3 (SIMPLE INVERSION).**

(i) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} x : \tau$, then $x : \forall \bar{\alpha}. \tau' \in \Gamma$ and $\tau = \tau'[\bar{\alpha} := \bar{\tau}]$.

(ii) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} \lambda x. e : \tau$, then $\Gamma, x : \tau_1 \vdash_{\text{simple}}^{\text{sd}} e : \tau_2$ and $\tau = \tau_1 \to \tau_2$.

(iii) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} e_1 e_2 : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e_1 : \tau' \to \tau$ and $\Gamma \vdash_{\text{simple}}^{\text{sd}} e_2 : \tau'$.

(iv) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} () : \tau$, then $\tau = 1$.

(v) If $\Gamma \vdash_{\text{simple}}^{\text{sd}}$ let $x = e_1$ in $e_2 : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e_1 : \tau'$, $\bar{\alpha} \# \text{fv}(\Gamma)$, and $\Gamma, x : \forall \bar{\alpha}. \tau' \vdash_{\text{simple}}^{\text{sd}} e_2 : \tau$.

(vi) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} (e : \exists \bar{\alpha}. \tau') : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e : \tau'[\bar{\alpha} := \bar{\tau}]$ and $\tau = \tau'[\bar{\alpha} := \bar{\tau}]$.

(vii) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} (e_1, \dots, e_n) : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e_i : \tau_i$ for all $1 \le i \le n$ and $\tau = \prod_{i=1}^n \tau_i$.

(viii) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} e.j^n : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e : \prod_{i=1}^n \tau_i$ and $\tau = \tau_j$, with $n \ge j$.

(ix) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} [e : \exists \bar{\alpha}. \forall \bar{\beta}. \tau'] : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e : \tau[\bar{\alpha} := \bar{\tau}], \bar{\beta} \# \Gamma$ and $\tau = [\forall \bar{\beta}. \tau'][\bar{\alpha} := \bar{\tau}]$.

(x) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} \langle e : \exists \bar{\alpha}. \sigma \rangle : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e : [\sigma][\bar{\alpha} := \bar{\tau}]$ and $\sigma[\bar{\alpha} := \bar{\tau}] \le \tau$.

(xi) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} \Box$ with $\bar{e} : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e_i : \tau'_i$ for all $1 \le i \le n$.

(xii) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} T.\{\ell = e\} : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e_i : \tau_i$ and $T.\ell \le \tau \to \tau_i$ for $1 \le i \le n$ and $\text{dom}(T.\Omega) = \bar{e}$.

(xiii) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} \{\ell = e\} : \tau$, then $\ell \triangleright T$ and $\Gamma \vdash_{\text{simple}}^{\text{sd}} T.\{\overline{\ell = e}\} : \tau$.

(xiv) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} e.T.\ell : \tau$, then $\Gamma \vdash_{\text{simple}}^{\text{sd}} e : \tau', T.\ell \le \tau' \to \tau$.

(xv) If $\Gamma \vdash_{\text{simple}}^{\text{sd}} e.\ell : \tau$, then $\ell \triangleright T$ and $\Gamma \vdash_{\text{simple}}^{\text{sd}} e.T.\ell : \tau$.

## D.2 Canonicalization of typability

Our system satisfies a similar canonicalization theorem to constraint satisfiability.

**LEMMA D.4 (COMPOSABILITY OF UNICITY).**

(i) If $\mathscr{E}_1[\Box \triangleleft \zeta | \bar{e}]$, then $\mathscr{E}_2[\mathscr{E}_1][\Box \triangleleft \zeta | \bar{e}]$.

(ii) If $\mathscr{E}_1[e \triangleright \zeta]$, then $\mathscr{E}_2[\mathscr{E}_1][e \triangleright \zeta]$.

**PROOF.** By induction on $\mathscr{E}_2$. $\square$

**LEMMA D.5 (DECANONICALIZATION).** If $\vdash e : \tau$, then $\emptyset \vdash e : \tau$.

**PROOF.** By induction on the given derivation $\vdash e : \tau$. $\square$

**THEOREM D.6 (CANONICALIZATION).** If $\vdash e : \sigma$, then $\vdash e : \tau$ for any instance $\tau$ of $\sigma$.

**PROOF.** By induction on the following measure of $e$:

$$ \|e\| \triangleq \langle \#\text{implicit } e, |e| \rangle $$

where $\langle \dots \rangle$ denotes a lexicographically ordered pair, and

(1) $\#\text{implicit } e$ is the number of implicit constructs in $e$ i.e., overloaded tuple projections $e.j$, implicit non-unique field projections $e.\ell$, implicit non-unique records $\{\ell = e\}$, polytype instantiations $\langle e \rangle$ and polytype boxing $[e]$.

(2) the last component $|e|$ is a structural measure of terms i.e., a application $e_1 e_2$ is larger than the two terms $e_1, e_2$.

This measure is analogous to the measure $\|C\|$ for constraints. $\square$
### D.3 Unifiers

A substitution $\vartheta$ is an idempotent function from type variables to types. The (finite) domain of $\vartheta$ is the set of type variables such that $\vartheta(\alpha) \neq \alpha$ for any $\alpha \in \text{dom } \vartheta$, while the codomain consists of the free type variables of its range. We use the notation $[\bar{\alpha} := \bar{\tau}]$ for the substitution $\vartheta$ with domain $\bar{\alpha}$ and $\vartheta(\bar{\alpha}) = \bar{\tau}$.

The constraint induced by a substitution $\vartheta$, written $\exists\vartheta$, is $\exists\bar{\beta}. \bar{\alpha} = \bar{\tau}$ where $\bar{\beta} = \text{rng } \vartheta, \bar{\alpha} = \text{dom } \vartheta$ and $\vartheta(\bar{\alpha}) = \bar{\tau}$.

**Definition D.7 (Unifier).** A substitution $\vartheta$ is a unifier of $C$ if $\exists\vartheta$ entails $C$. A unifier $\vartheta$ of $C$ is most general when $\exists\vartheta$ is equivalent to $C$.

**LEMMA D.8 (SIMPLE INVERSION OF UNIFIERS).**

* If $\vartheta$ is a unifier of $\tau_1 = \tau_2$, then $\vartheta(\tau_1) = \vartheta(\tau_2)$.

* For simple $C_1, C_2$, if $\vartheta$ is a unifier of $C_1 \wedge C_2$, then $\vartheta$ is a unifier of $C_1$ and $C_2$.

* For simple $C$, if $\vartheta$ is a unifier of $\exists\alpha.C$, then $\vartheta[\alpha := \tau]$ is a unifier of $C$ for some $\tau$.

* For simple $C$, if $\vartheta$ is a unifier of $\forall\alpha.C$, then $\vartheta$ is a unifier of $C$.

**PROOF.** Follows by simple inversion. $\square$

**LEMMA D.9.** If $\vartheta$ unifies $\exists\alpha.C$, then there exists a unifier $\vartheta'$ that extends $\vartheta$ with $\alpha$, where $\vartheta'$ is most general unifier of $\exists\vartheta \wedge C$.

Then $\lambda\alpha.C$ is equivalent to $\lambda\alpha.\sigma \le \alpha$ under $\vartheta$, where $\sigma = \forall\bar{\beta}.\vartheta'(\alpha)$ and $\bar{\beta} = \text{fv}(\vartheta'(\alpha)) \setminus \text{rang } \vartheta$. We write this equivalent constraint abstraction as $[\lambda\alpha.C]_\vartheta$.

**PROOF.** See Pottier and Rémy [2005]. $\square$

**LEMMA D.10 (LET INVERSION OF UNIFIERS).** For simple $C_1, C_2$. If $\vartheta$ unifies let $x = \lambda\alpha.C_1$ in $C_2$, then $\vartheta$ unifies $\exists\alpha.C_1$ and $\vartheta$ unifies let $x = [\lambda\alpha.C_1]_\vartheta$ in $C_2$

**PROOF.** Follows from Lemma D.9 and simple inversion. $\square$

**LEMMA D.11.** For two substitutions $\vartheta, \vartheta'$. If $\exists\vartheta \vdash \exists\vartheta'$, there exists $\vartheta''$ such that $\vartheta = \vartheta'' \circ \vartheta'$.

**PROOF.** Standard result, follows from definition of $\exists\vartheta$. $\square$

### D.4 Soundness and completeness of constraint generation

**LEMMA D.12.** For any term context $\mathscr{C}$, term $e$, $[\mathscr{C}[\Box : \tau] : \tau']$ $[[e : \tau]] = [\mathscr{C}[e] : \tau']$.

**PROOF.** By induction on the structure of $\mathscr{C}$. $\square$

**LEMMA D.13.** For any term $e$, $[e : \tau]] = [e] : \tau$.

**PROOF.** By induction on $e$. $\square$

**LEMMA D.14 (SIMPLE SOUNDNESS AND COMPLETENESS).** For simple terms $e$. $\vartheta(\Gamma) \vdash_{\text{simple}} e : \vartheta(\tau)$ if and only if $\vartheta$ is a unifier of $[\Gamma \vdash e : \tau]$.

**PROOF.** By induction on $e$ simple. $\square$

**THEOREM D.15 (SOUNDNESS AND COMPLETENESS).** $\vdash e : \vartheta(\alpha)$ if and only if $\vartheta$ is a unifier of $[e : \alpha]$

**PROOF.** By induction on the number $n$ of implicit terms in $e$. $\square$
**Case n is 0.**

<figure><img src="image_32.png" /></figure>

**Case n is k + 1.**

**Subcase** $\Rightarrow$.

**Subsubcase**

<figure><img src="image_33.png" /></figure>

**Subsubcase** CAN-POLY-I, CAN-USE-I, CAN-RCD-I, CAN-RCD-PROJ-I.

Similar arguments.
**Subcase** ⇐.

**Subsubcase**

$$ \frac{\mathscr{C}[\alpha_1 ! v\bar{\gamma} . \Pi_{i=1}^n \bar{\gamma}]}{\vartheta \text{ unifies } \mathscr{C}[\text{match } \alpha_1 \text{ with } \Pi \gamma_j \Rightarrow \beta = \gamma]} \stackrel{\text{CAN-MATCH-CTX}}{\underbrace{\mathscr{C}[\text{match } \alpha_1 \text{ with } \Pi \gamma_j \Rightarrow \beta = \gamma]}}_{[e:\alpha]} $$

$$ [[e : \tau]] = \text{let } \Gamma \text{ in } [[\mathscr{C}[e.j] : \alpha]] \text{ Premise} $$

$$ \mathscr{C} = \text{let } \Gamma \text{ in } [[\mathscr{C}[\Box : \beta] : \alpha][\exists \alpha. [[e : \alpha] \wedge \Box]] \text{ Premise} $$

$$ \vartheta \text{ unifies } \mathscr{C}[\text{match } \alpha_1 := v\bar{\gamma} . \Pi_{i=1}^n \bar{\gamma} \text{ with } \dots] \text{ Premise} $$

$$ \vartheta \text{ unifies } [[\mathscr{C}[e.j^n] : \alpha]] \qquad \text{Above (See } \Rightarrow \text{ direction)} $$

$$ \Vdash \mathscr{C}[e.j^n] : \vartheta(\alpha) \qquad \text{By } i.h. $$

$$ \Gamma' \vdash \mathscr{C}[\Box \text{ with } (e : g)] : \tau' \qquad \text{Premise} $$

$$ \Gamma' = \emptyset \qquad \mathscr{C}[\Box \text{ with } (e : g)] \text{ is closed} \qquad \text{Lemma D.5} $$

$$ \Vdash \mathscr{C}[\Box \text{ with } (e : g)] : \tau' \qquad \text{By } i.h. $$

$$ [\alpha := \tau'] \text{ unifies } [[\mathscr{C}[\Box \text{ with } (e : g)] : \alpha]] \qquad \text{By definition} $$

$$ \phi[\alpha := \phi(\tau')] \vdash [[\mathscr{C}[\Box \text{ with } (e : g)] : \alpha]] \qquad \text{By definition} $$

$$ \mathscr{C}[\alpha_1 ! v\bar{\gamma} . \Pi_{i=1}^n \bar{\gamma}] \qquad \text{Premise} $$

$$ \text{shape}(g) = v\bar{\gamma} . \Pi_{i=1}^n \bar{\gamma} \qquad \Rightarrow \text{E} $$

$$ \mathscr{C}[e \triangleright v\bar{\gamma} . \Pi_{i=1}^n \bar{\gamma}] \qquad \text{Above} $$

$$ \Vdash \mathscr{C}[e.j] : \vartheta(\alpha) \qquad \text{By CAN-PROJ-I} $$

**Subsubcase** $[e]$, $\langle e \rangle$, $\{\overline{\ell = e}\}$, $e.\ell$.

Similar arguments.

□

## D.5 Principal types

**THEOREM 4.12 (PRINCIPAL TYPES).** For any well-typed closed OmniML term $e$, there exists a type $\tau$ such that: (i) $\vdash e : \tau$. (ii) For any other typing $\vdash e : \tau'$, then $\tau' = \theta(\tau)$ for some substitution $\theta$.

**PROOF.** Let $e$ be an arbitrary closed well-typed term; that is, there exists a type $\tau$ such that $\vdash e : \tau$. By Theorem D.15, the constraint $[[e : \alpha]]$ is satisfiable (specifically under the unifier $\alpha = \tau$). By Corollary C.18, there exists a solved constraint $\hat{C}$ such that $\hat{C} \equiv [[e : \alpha]]$. From $\hat{C}$, we extract a unifier $\vartheta$. Since $\hat{C} \equiv \exists \vartheta$, it follows that $\vartheta$ is most general.

We claim that $\vartheta(\alpha)$ is the principal type of $e$. This amounts to showing:

(i) $\vdash e : \vartheta(\alpha)$

(ii) For any other typing $\vdash e : \tau'$, then $\tau' = \theta(\vartheta(\alpha))$ for some $\theta$.

Since $\vartheta$ is a unifier of $[[e : \alpha]]$, it follows immediately from Theorem D.15 that $\vdash e : \vartheta(\alpha)$, proving (i). For (ii), suppose $\vdash e : \tau'$ for some $\tau'$. Then by Theorem D.15 again, there exists a unifier $\vartheta'$ of $[[e : \alpha]]$ such that $\vartheta'(\alpha) = \tau'$. Since $\vartheta$ is most general, we have $\exists \vartheta' \vdash \exists \vartheta$, and by Lemma D.11, this implies the existence of a substitution $\vartheta''$ such that $\vartheta' = \vartheta'' \circ \vartheta$. Hence, $\tau' = \vartheta'(\alpha) = \vartheta''(\vartheta(\alpha))$, witnessing that $\tau'$ is an instance of $\vartheta(\alpha)$, as required (ii). □
CONTENTS

<table><tr><td>Abstract</td><td>1</td></tr><tr><td>1 Introduction</td><td>1</td></tr><tr><td>2 Overview</td><td>3</td></tr><tr><td>3 The OmniML calculus</td><td>13</td></tr><tr><td>4 Constraints</td><td>19</td></tr><tr><td>5 Constraint solving</td><td>26</td></tr><tr><td>6 Implementation</td><td>34</td></tr><tr><td>7 Related work</td><td>35</td></tr><tr><td>8 Conclusions</td><td>39</td></tr><tr><td>References</td><td>39</td></tr><tr><td>A Full technical reference</td><td>43</td></tr><tr><td>B Properties of the constraint language</td><td>54</td></tr><tr><td>C Properties of the constraint solver</td><td>61</td></tr><tr><td>D Properties of OmniML</td><td>77</td></tr><tr><td>Contents</td><td>82</td></tr></table>