$\inferrule*{(\cdot,B)=\mathsf{split}(B,M^{\prime})\\\ \Delta;\Gamma\vdash
M^{\prime}:B\\\ \Delta;\Gamma,x:B\vdash
N^{\prime}:\delta(A)}{\Delta;\Gamma\vdash{\rm{\bf
let}}\;(x:B)=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}:\delta(A)}$

∎

##  Appendix B Proofs for Section 4.2

We again proceed by collecting auxiliary lemmas in Section B.1 before proving
each theorem from Section 4.2 in an individual subsection.

###  B.1. Auxiliary Lemmas

The following lemma states how solutions for constraints
$\mathfrak{U}(\Theta,\theta)$ look like. The lemma is somewhat specialised for
the specific places where we use it, by introducing an extra type context
$\Delta^{\prime}$ and an existential quantifier around
$\mathfrak{U}(\Theta,\theta)$.

###### Lemma 13.

Let $\Delta\vdash\theta:\Theta\Rightarrow\Theta$ and
$\Delta,\Delta^{\prime}\vdash\Gamma\ \mathbf{ok}$ and
$\mathsf{ftv}(\Theta)=\Xi,\tilde{a}$.

Then we have

$\begin{array}[]{c}(\Delta,\Delta^{\prime});\Xi;\Gamma;\delta\vdash\exists\tilde{a}.\mathfrak{U}(\Theta,\theta)\\\
\text{iff}\\\ \text{there exists }\theta^{\prime}\text{ such that
}\Delta,\Delta^{\prime}\vdash\theta^{\prime}:\Theta\Rightarrow\cdot\text{ and
}\delta={(\theta^{\prime}\circ\theta)}\mathord{\upharpoonright}_{\Xi}.\end{array}$

###### Proof.

By definition, the subconstraint $\mathfrak{U}(\theta)$ of
$\mathfrak{U}(\Theta,\theta)$ contains constraints of the form
$a\sim\theta(a)$ for all $a$ in $\Theta$. These constraints are satisfied by
exactly those substitutions $\delta$ refining $\theta$. In addition, the
${\mathord{\bullet}}{}$ subconstraints in $\mathfrak{U}(\Theta)$ are satisfied
iff the refinement respects the restrictions in $\Theta$. ∎

The next lemma states how _most general_ solutions of constraints
$\mathfrak{U}(\Theta,\theta)$ look like.

###### Lemma 14.

Let the following conditions hold:

  * •

$\Delta\vdash\theta:\Theta\Rightarrow\Theta$

  * •

$\mathsf{ftv}(\Theta)=\Xi,\tilde{a}$

  * •

$\Delta\vdash\Gamma\ \mathbf{ok}$

  * •

$\overline{b}\approx\mathsf{ftv}(\theta)-\Delta$

Then we have

$\begin{array}[]{c}\mathsf{mostgen}((\Delta,\Delta^{\prime}),\Xi,\Gamma,\exists\tilde{a}.\mathfrak{U}(\Theta,\theta),\Delta_{\mathrm{m}},\delta_{\mathrm{m}})\\\
\text{iff}\\\ \text{there exists
}\overline{c}\subseteq\Delta_{\mathrm{m}}\text{ s.t.
}\delta_{\mathrm{m}}={([\overline{b}\mapsto\overline{c}]\circ\theta)}\mathord{\upharpoonright}_{\Xi}\end{array}$

###### Proof.

Follows directly from Lemma 13 and the observation that the most general
solution of $\mathfrak{U}(\Theta,\theta)$ is the one that maps all flexible
variables in $\mathsf{ftv}(\theta)$ to fresh, pairwise disjoint rigid
variables. Observe that by assumption
$\Delta\vdash\theta:\Theta\Rightarrow\Theta$ and the fact that rigid variables
are considered monomorphic we have
$\Delta\vdash[\overline{b}\mapsto\overline{c}]\circ\theta:\Theta\Rightarrow\cdot$
as well. ∎

###### Lemma 15.

Let $C_{1}$, $C_{2}$, $\Delta,\Xi,\delta$ and $F$ be given and let the
following condition hold: for all $\Delta^{\prime},\delta^{\prime}$ we have
$(\Delta,\mathsf{rc}(F),\Delta^{\prime});(\Xi,\mathsf{fc}(F));\delta^{\prime}(\mathsf{tc}(F));\delta^{\prime}\vdash
C_{1}$ iff
$(\Delta,\mathsf{rc}(F),\Delta^{\prime});(\Xi,\mathsf{fc}(F));\delta^{\prime}(\mathsf{tc}(F));\delta^{\prime}\vdash
C_{2}$.

Then we have have $\Delta;\Xi;\cdot;\delta\vdash F[C_{1}]\text{ iff
}\Delta;\Xi;\cdot;\delta\vdash F[C_{2}]$.

###### Proof.

By induction on structure of $F$, observing that any judgement involving a
constraint with subconstraint $C_{1}$ can be replaced by a corresponding
judgement involving $C_{2}$ (and vice versa). ∎

###### Lemma 16 (Stack machine steps preserve well-formedness of states).

If $s\ \mathbf{ok}$ and $s\to s^{\prime}$ then $s^{\prime}\ \mathbf{ok}$.

###### Proof.

By case analysis over which stack machine rule was applied. ∎

###### Lemma 17 (Weakening $\mathsf{mostgen}$).

Let
$\mathsf{mostgen}(\Delta,\Xi,\Gamma,C,\Delta_{\mathrm{m}},\delta_{\mathrm{m}})$
and $(\Delta,\Xi,\Delta_{\mathrm{m}})\mathop{\\#}(\overline{a},\overline{b})$.
Then we have
$\mathsf{mostgen}(\Delta,(\Xi,\tilde{a}),\Gamma,C,(\Delta_{\mathrm{m}},\overline{b}),\delta_{\mathrm{m}}[\overline{a}\mapsto\overline{b}])$.

###### Proof.

By
$\mathsf{mostgen}(\Delta,\Xi,\Gamma,C,\Delta_{\mathrm{m}},\delta_{\mathrm{m}})$
we have $(\Delta,\Delta_{\mathrm{m}});\Xi;\Gamma;\delta_{\mathrm{m}}\vdash C$
and therefore $(\Delta,\Delta_{\mathrm{m}});\Xi;\Gamma\vdash C\ \mathbf{ok}$
(cf. Lemma 12). This means that none of the variables in $\overline{a}$ are
constrained in any way by $C$, meaning that the most general solution maps
them to pairwise disjoint variables, like $\overline{b}$. ∎

###### Lemma 18 (Refinement).

Let $\Xi\mathop{\\#}\Delta^{\prime}$. If $\Delta;\Xi;\Gamma;\delta\vdash C$
and
$\Delta^{\prime}\vdash\delta^{\prime}:\Delta\Rightarrow_{\mathord{\bullet}}\cdot$
then
$\Delta^{\prime};\Xi;\delta^{\prime}(\Gamma);\delta^{\prime}\circ\delta\vdash
C$.

###### Proof.

By structural induction on $C$, observing that for all
$a\in\Xi,R\in\\{{\mathord{\bullet}},\star\\}$ we have
$\Delta\vdash_{R}\delta(a)\ \mathbf{ok}$ iff
$\Delta^{\prime}\vdash_{R}\delta^{\prime}(\delta(a))\ \mathbf{ok}$. ∎

###### Lemma 19 (Substitution).

If $\Delta;(\Xi,a);\Gamma;\delta[a\mapsto A]\vdash C$ then
$\Delta;\Xi;\Gamma;\delta\vdash C[a/A]$.

###### Proof.

By structural induction on $C$. Observe that the substitution does not
interfere with generalisation: The variable $a$ is already in scope and
therefore not subject to generalisation by any let constraint within $C$. ∎

###  B.2. Proof of Theorem 3

See 3

###### Proof.

We carry out the proof by case analysis of the stack machine reduction rules.
Let $s$ be the state before, and $s^{\prime}$ the state after the step.

We focus on the let rules.

  * •

Case S-LetPolyPop: We have that $s$ is of the form
$(\forall\Delta::{}\exists\Xi::{}F::{\rm{\bf let}}_{\star}\;x=\sqcap
a.\Box\;{\rm{\bf
in}}\;C::\exists\tilde{a},\Theta_{0},\theta_{0},\mathsf{true})$ for some
$F,C$, and $\tilde{a}$ and assume that the following conditions imposed by
S-LetPolyPop hold:

$\begin{array}[t]{@{}l@{}}\widetilde{a^{\prime}};\>\widetilde{a^{\prime\prime}}=\mathsf{partition}((\tilde{b},a),\theta_{0},\Theta_{0})\\\
A=\theta_{0}(a)\\\ \overline{c}\>=\mathsf{ftv}(A)\cap\widetilde{a^{\prime}}\\\
B=\forall\overline{c}.A\\\ \Theta_{1}=\Theta_{0}-\widetilde{a^{\prime}}\\\
\theta_{1}={\theta_{0}}\mathord{\upharpoonright}_{\Theta_{1}}\end{array}$

We need to show

$\begin{array}[]{c}\Delta;\Xi;\cdot;\delta\vdash F::{\rm{\bf
let}}_{\star}\;x=\sqcap a.\Box\;{\rm{\bf
in}}\;C::\exists\tilde{a}[\mathsf{true}\wedge\mathfrak{U}(\Theta_{0},\theta_{0})]\\\
\;\text{ iff }\\\ \Delta;\Xi;\cdot;\delta\vdash
F::\exists{\widetilde{a^{\prime\prime}}}[{\rm{\bf def}}\;(x:B)\;{\rm{\bf
in}}\;C\wedge\mathfrak{U}(\Theta_{1},\theta_{1})],\end{array}$

which is equivalent to

$\begin{array}[]{c}\Delta;\Xi;\cdot;\delta\vdash F[C^{\prime}_{0}]\\\ \;\text{
iff }\\\ \Delta;\Xi;\cdot;\delta\vdash F[C^{\prime}_{1}]\end{array}$

if we define $C^{\prime}_{0}:={\rm{\bf let}}_{\star}\;x=\sqcap
a.\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0})\;{\rm{\bf in}}\;C$ and
$C^{\prime}_{1}:=\exists\widetilde{a^{\prime\prime}}.({\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;C)\wedge\mathfrak{U}(\Theta_{1},\theta_{1})$.

We can prove this equivalence directly using Lemma 15. In order to apply this
lemma, we need to show that the following holds: For all
$\hat{\Delta},\hat{\delta}$ we have
$(\Delta,\mathsf{rc}(F),\hat{\Delta});(\Xi,\mathsf{fc}(F));\hat{\delta}(\mathsf{tc}({F}));\hat{\delta}\vdash
C^{\prime}_{0}$ iff
$(\Delta,\mathsf{rc}(F),\hat{\Delta});(\Xi,\mathsf{fc}(F));\hat{\delta}(\mathsf{tc}({F}));\hat{\delta}\vdash
C^{\prime}_{1}$

To this end, suppose $\hat{\Delta}$, and $\hat{\delta}$ are given. Let
$\Delta^{\prime}\coloneqq\Delta,\mathsf{rc}(F),\hat{\Delta}$ and
$\Xi^{\prime}\coloneqq\Xi,\mathsf{fc}(F)$ and
$\Gamma^{\prime}\coloneqq\hat{\delta}(\mathsf{tc}(F))$.

    * $\Longrightarrow$

: We assume $\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash
C^{\prime}_{0}$ (1). The derivation of this must have the following form, for
some
$\Delta_{\mathrm{m}},\delta_{\mathrm{m}},\Delta_{\mathrm{o}},\overline{b},\delta^{\prime},A^{\prime}$:

$\inferrule{\mathsf{mostgen}(\Delta^{\prime},(\Xi^{\prime},a),\Gamma^{\prime},\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0}),\Delta_{\mathrm{m}},\delta_{\mathrm{m}})\\\
\\\
\Delta_{\mathrm{o}}=\mathsf{ftv}(\delta_{\mathrm{m}}(\Xi^{\prime}))-\Delta^{\prime}\\\
\overline{b}=\mathsf{ftv}(\delta_{\mathrm{m}}(a))-\Delta^{\prime},\Delta_{\mathrm{o}}\\\
\\\
\Delta^{\prime}\vdash\delta^{\prime}:\Delta_{\mathrm{o}}\Rightarrow_{\mathord{\bullet}}\cdot\\\
A^{\prime}=\delta^{\prime}(\delta_{\mathrm{m}}(a))\\\ \\\
(\Delta^{\prime},\tilde{b});(\Xi^{\prime},a);\Gamma^{\prime};\hat{\delta}[a\mapsto
A^{\prime}]\vdash\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0})\\\
\Delta^{\prime};\Xi^{\prime};(\Gamma^{\prime},x:\forall\overline{b}.A^{\prime});\hat{\delta}\vdash
C}{\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash{\rm{\bf
let}}_{\star}\;x=\sqcap
a.\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0})\;{\rm{\bf in}}\;C}$

We can assume w.l.o.g. that the variables in $\Delta_{\mathrm{m}}$ are fresh.

By $s\ \mathbf{ok}$ and $s^{\prime}\ \mathbf{ok}$, we have
$\mathsf{ftv}(\Theta_{0})=(\Xi,a,\tilde{a})$ as well as idempotency of
$\theta_{0}$ and $\theta_{1}$.

Let $\Xi_{\mathrm{f}}\coloneqq\mathsf{ftv}(\theta_{0})-\Delta^{\prime}$, which
implies $\Xi_{\mathrm{f}}\subseteq\Theta$. By Lemma 14 there exists a
bijection $\delta_{\mathrm{r}}$ such that
$\Delta_{\mathrm{m}}\vdash\delta_{\mathrm{r}}:\Xi_{\mathrm{f}}\Rightarrow_{\mathord{\bullet}}\cdot$
and
$\delta_{\mathrm{m}}={(\delta_{\mathrm{r}}\circ\theta_{0})}\mathord{\upharpoonright}_{(\Xi^{\prime},a)}$
(2).

We observe
$\delta_{\mathrm{r}}(\widetilde{a^{\prime\prime}})\subseteq\Delta_{\mathrm{o}}$.
We can now define $\widehat{\delta^{\prime\prime}}$ such that for all
$b\in(\Xi^{\prime},\widetilde{a^{\prime\prime}})$ we have

$\widehat{\delta^{\prime\prime}}(b)=\begin{cases}\hat{\delta}(b)&\text{if
}b\in\Xi^{\prime}\\\ \delta^{\prime}(\delta_{\mathrm{r}}(b))&\text{if
}b\in\widetilde{a^{\prime\prime}}\end{cases}$

which yields
$\Delta^{\prime}\vdash\widehat{\delta^{\prime\prime}}:(\Xi^{\prime},\widetilde{a^{\prime\prime}})\Rightarrow_{\star}\cdot$
(3).

Next, we show $\delta_{\mathrm{r}}(\overline{c})=\overline{b}$ (4):

$\begin{array}[]{r c
l}\delta_{\mathrm{r}}(\overline{c})&=&\delta_{\mathrm{r}}(\mathsf{ftv}(\theta_{0}(a))\cap\widetilde{a^{\prime}})\\\
&=&\delta_{\mathrm{r}}(\mathsf{ftv}(\theta_{0}(a))-\Xi^{\prime}-\widetilde{a^{\prime\prime}}-\Delta^{\prime})\\\
&&\;\text{(by
$\mathsf{ftv}(\theta_{0}(a))\subseteq\Delta^{\prime},\Xi^{\prime},\widetilde{a^{\prime}},\widetilde{a^{\prime\prime}}$)}\\\
&=&\delta_{\mathrm{r}}(\mathsf{ftv}(\theta_{0}(a))-\mathsf{ftv}(\theta_{0}(\Xi^{\prime}))-\widetilde{a^{\prime\prime}}-\Delta^{\prime})\\\
&&\;(\text{by $\theta_{0}(b)=b$ for all $b\in\mathsf{ftv}(\theta(a))$ and
$\widetilde{a^{\prime}}\mathop{\\#}\mathsf{ftv}(\theta(\Xi^{\prime}))\subseteq\Delta^{\prime},\Xi^{\prime},\widetilde{a^{\prime\prime}}$})\\\
&=&\delta_{\mathrm{r}}(\mathsf{ftv}(\theta_{0}(a))-\mathsf{ftv}(\theta_{0}(\Xi^{\prime}))-\Delta^{\prime})\\\
&&\;(\text{by
}\widetilde{a^{\prime\prime}}\subseteq\mathsf{ftv}(\theta_{0}(\Xi^{\prime})))\\\
&=&\mathsf{ftv}(\delta_{\mathrm{m}}(a))-\mathsf{ftv}(\delta_{\mathrm{m}}(\Xi^{\prime}))-\Delta^{\prime}\\\
&&\;(\text{by (\ref*{proof:subject-reduction-statement:let-poly:rsubst-r-
composition})})\\\
&=&\mathsf{ftv}(\delta_{\mathrm{m}}(a))-\Delta^{\prime},\Delta_{\mathrm{o}}\\\
&=&\overline{b}\end{array}$

We now show
$\widehat{\delta^{\prime\prime}}(c)=\delta^{\prime}(\delta_{\mathrm{r}}(c))$
for all
$c\in\mathsf{ftv}(\theta_{0}(a))\cap(\Xi^{\prime},\widetilde{a^{\prime\prime}})$
(5). First, we observe that for all such $c\in\widetilde{a^{\prime\prime}}$
this holds by definition of $\widehat{\delta^{\prime\prime}}$. Next, by
$(\Delta^{\prime},\tilde{b});(\Xi^{\prime},a);\Gamma^{\prime};\widehat{\delta^{\prime}}\vdash\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0})$
(see derivation of ($\Longrightarrow$ ‣ • ‣ B.2)) and Lemma 13 we have that
there exists $\delta_{\mathrm{s}}$ such that
$(\Delta^{\prime},\tilde{b})\vdash\delta_{\mathrm{s}}:(\Xi^{\prime},a,\tilde{a})\Rightarrow_{\star}\cdot$
and
$\widehat{\delta^{\prime}}={(\delta_{\mathrm{s}}\circ\theta_{0})}\mathord{\upharpoonright}_{(\Xi^{\prime},a)}$
(6). We have $\theta_{0}(b)=b$ for all $b\in\mathsf{ftv}(\theta_{0})$ and
therefore $\delta_{\mathrm{s}}(b)=\widehat{\delta^{\prime}}(b)$ (7) for any
such $b$. Using this, we observe

$\begin{array}[]{r c l l}&&\widehat{\delta^{\prime}}(a)\\\
&=&\delta_{\mathrm{s}}(\theta_{0}((a))&\text{(by (\ref*{proof:subject-
reduction-statement:let-poly:rsubst-s-comp}))}\\\ &=&A^{\prime}&\text{(by
def.\ of $\widehat{\delta^{\prime}}$)}\\\
&=&\delta^{\prime}(\delta_{\mathrm{m}}(a))&\text{(by def.\ of
$A^{\prime}$)}\\\
&=&\delta^{\prime}(\delta_{\mathrm{r}}(\theta_{0}(a)))&\text{(by
(\ref*{proof:subject-reduction-statement:let-poly:rsubst-r-composition}))}\\\
\end{array}$

This implies that for all $b\in\mathsf{ftv}(\theta_{0}(a))\cap\Xi^{\prime}$ we
have
$\delta^{\prime}(\delta_{\mathrm{r}}(b))=\delta_{\mathrm{s}}(b)\stackrel{{\scriptstyle(\ref*{proof:subject-
reduction-statement:let-poly:rsubst-s-vs-hat-
rsubst-p})}}{{=}}\widehat{\delta^{\prime}}(b)=\widehat{\delta^{\prime\prime}}(b)$
and therefore ($\Longrightarrow$ ‣ • ‣ B.2) holds.

We now show that $\widehat{\delta^{\prime\prime}}(B)$ is alpha-equivalent to
$\forall\tilde{b}.A^{\prime}$:

$\begin{array}[]{rcl}\widehat{\delta^{\prime\prime}}(B)&=&\widehat{\delta^{\prime\prime}}(\forall\overline{c}.\theta_{0}(a))\\\
&=&\forall\overline{c}.\widehat{\delta^{\prime\prime}}(\theta_{0}(a))\\\
&&\;(\text{due to }(\ref*{proof:subject-reduction-statement:let-poly:hat-
theta-pp-
wf}),\overline{c}\mathop{\\#}\Xi^{\prime},\widetilde{a^{\prime\prime}}\text{
and }\overline{c}\mathop{\\#}\Delta^{\prime},\Delta_{\mathrm{m}})\\\
&=&\forall\overline{b}.\left(\widehat{\delta^{\prime\prime}}(\theta_{0}(a))[\overline{c}\mapsto\overline{b}]\right)\\\
&&\;(\text{due to (\ref*{proof:subject-reduction-statement:let-poly:omany-c-
vs-omany-b}), $\overline{c}\mathop{\\#}\overline{b}$})\\\
&=&\forall\overline{b}.\delta^{\prime}(\delta_{\mathrm{r}}(\theta_{0}(a)))\\\
&&\;(\text{due to (\ref*{proof:subject-reduction-statement:let-poly:rsubst-r-
composition}), (\ref*{proof:subject-reduction-statement:let-poly:hat-rsubst-
pp-on-Xi-p}), $\widehat{\delta^{\prime\prime}}(b)=b$ for all
$b\in\overline{b}$})\\\
&=&\forall\overline{b}.\delta^{\prime}(\delta_{\mathrm{m}}(a))\\\
&=&\forall\overline{b}.A^{\prime}\end{array}$

This means that by
$\Delta^{\prime};\Xi^{\prime};(\Gamma^{\prime},x:\forall\overline{b}.A^{\prime});\hat{\delta}\vdash
C$ (see derivation of ($\Longrightarrow$ ‣ • ‣ B.2)) we also have
$\Delta^{\prime};\Xi^{\prime};(\Gamma^{\prime},x:\widehat{\delta^{\prime\prime}}(B));\hat{\delta}\vdash
C$, which we can weaken to
$\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});(\Gamma^{\prime},x:\widehat{\delta^{\prime\prime}}(B));\widehat{\delta^{\prime\prime}}\vdash
C$ (8).

We now show that for all $b\in\mathsf{ftv}(B)-\Delta^{\prime}$ we have
$\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash\mathsf{mono}(b)$
(9): We have
$\mathsf{ftv}(B)-\Delta^{\prime}=\mathsf{ftv}(\forall\overline{c}.\theta_{0}(a))-\Delta^{\prime}\subseteq\Xi,\widetilde{a^{\prime\prime}}$.
By ($\Longrightarrow$ ‣ • ‣ B.2) we have
$\widehat{\delta^{\prime\prime}}(b)=\delta^{\prime}(\delta_{\mathrm{r}}(b))$
for any such $b$. By
$\Delta^{\prime}\vdash\delta^{\prime}:\Delta_{\mathrm{o}}\Rightarrow_{\mathord{\bullet}}\cdot$
and $\delta_{\mathrm{r}}$ being a bijection on variables, we have
$\Delta^{\prime}\vdash_{\mathord{\bullet}}\widehat{\delta^{\prime\prime}}(b)\
\mathbf{ok}$.

We now show
$\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash\mathfrak{U}(\Theta_{1},\theta_{1})$
(10): Recall that per ($\Longrightarrow$ ‣ • ‣ B.2), we have
$\widehat{\delta^{\prime}}={(\delta_{\mathrm{s}}\circ\theta_{0})}\mathord{\upharpoonright}_{(\Xi^{\prime},a)}$,
where $\widehat{\delta^{\prime}}$ and $\widehat{\delta^{\prime\prime}}$
coincide on $\Xi^{\prime}$. Further, $\theta_{0}(b)=b$ for all
$b\in\widetilde{a^{\prime\prime}}$. We can therefore apply Lemma 13 to
$\widehat{\delta^{\prime\prime}}$ to obtain ($\Longrightarrow$ ‣ • ‣ B.2).

Using ($\Longrightarrow$ ‣ • ‣ B.2), ($\Longrightarrow$ ‣ • ‣ B.2), and
($\Longrightarrow$ ‣ • ‣ B.2) we can now derive
$\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash
C^{\prime}_{1}$ as follows:

$\inferrule*{\inferrule*{\inferrule*{\inferrule*{\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});(\Gamma^{\prime},x:\widehat{\delta^{\prime\prime}}B);\widehat{\delta^{\prime\prime}}\vdash
C\\\ \text{for all
}b\in\mathsf{ftv}(B)-\Delta^{\prime}\;\mid\;\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash\mathsf{mono}(b)}{\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash{\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;C\\\ }\\\
\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash\mathfrak{U}(\Theta_{1},\theta_{1})}{\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash({\rm{\bf
def}}\;(x:B)\;{\rm{\bf
in}}\;C)\wedge\mathfrak{U}(\Theta_{1},\theta_{1})}}{\vdots}}{\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash\exists\widetilde{a^{\prime\prime}}.({\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;C)\wedge\mathfrak{U}(\Theta_{1},\theta_{1})}$

    * $\Longleftarrow$

: We assume $\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash
C^{\prime}_{1}$ (11). The derivation of this must have the following form for
some $\widehat{\delta^{\prime\prime}}$:

$\inferrule{\inferrule{\inferrule{\inferrule{\inferrule{\vdots}{\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});(\Gamma^{\prime},x:\widehat{\delta^{\prime\prime}}B);\widehat{\delta^{\prime\prime}}\vdash
C}\\\ \\\ \text{for all
}b\in\mathsf{ftv}(B)-\Delta^{\prime}\;\mid\;\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash\mathsf{mono}(b)}{\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash{\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;C\\\ }\\\
\inferrule{\vdots}{\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash\mathfrak{U}(\Theta_{1},\theta_{1})}}{\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash({\rm{\bf
def}}\;(x:B)\;{\rm{\bf
in}}\;C)\wedge\mathfrak{U}(\Theta_{1},\theta_{1})}}{\vdots}}{\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash\exists\widetilde{a^{\prime\prime}}.({\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;C)\wedge\mathfrak{U}(\Theta_{1},\theta_{1})}$

This immedately gives us
$\Delta^{\prime}\vdash\widehat{\delta^{\prime\prime}}:(\Xi^{\prime},\widetilde{a^{\prime\prime}})\Rightarrow_{\star}\cdot$
(12).

Let $\Xi_{\mathrm{f}}$ be defined as in the $\Rightarrow$ case and let
$\delta_{\mathrm{r}}$ be a bijection from $\Xi_{\mathrm{f}}$ to fresh
variables. Further, let
$\Delta_{\mathrm{m}}\coloneqq\mathsf{ftv}(\delta_{\mathrm{r}})$ and
$\delta_{\mathrm{m}}\coloneqq{(\delta_{\mathrm{r}}\circ\theta_{0})}\mathord{\upharpoonright}_{(\Xi^{\prime},a)}$.
By Lemma 14 we then have
$\mathsf{mostgen}(\Delta^{\prime},(\Xi^{\prime},a),\allowbreak\Gamma^{\prime},\allowbreak\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0}),\allowbreak\Delta_{\mathrm{m}},\delta_{\mathrm{m}})$.
We may now define $\Delta_{\mathrm{o}}$ and $\overline{b}$ as in the
$\Rightarrow$ case, making each of them a subset of $\Delta_{\mathrm{m}}$.

We now define $\delta^{\prime}$ for all $b\in\Delta_{\mathrm{o}}$ as follows:

$\delta^{\prime}(b)=\begin{cases}\widehat{\delta^{\prime\prime}}(\delta_{\mathrm{r}}^{-1}(b))&\text{if
}\delta_{\mathrm{r}}^{-1}(b)\in\mathsf{ftv}(\theta(a))-\widetilde{a^{\prime}}-\Delta^{\prime}\\\
\mathsf{unit}&\text{otherwise}\end{cases}$

We have $\widetilde{a^{\prime}}\subseteq\overline{c}$ and therefore
$\mathsf{ftv}(B)=\mathsf{ftv}(\forall\tilde{c}.\theta(a))=\mathsf{ftv}(\theta(a))-\widetilde{a^{\prime}}$.
Thus, by the definition above and the second premise of the derivation of
$\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash{\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;C$, we have
$\Delta^{\prime}\vdash\delta^{\prime}:\Delta_{\mathrm{o}}\Rightarrow_{\mathord{\bullet}}\cdot$.

The definition of $\delta^{\prime}$ immedately yields
$\widehat{\delta^{\prime\prime}}(c)=\delta^{\prime}(\delta_{\mathrm{r}}(c))$
for all
$c\in\mathsf{ftv}(\theta_{0}(a))\cap(\Xi^{\prime},\widetilde{a^{\prime\prime}})$.
(which we called ($\Longrightarrow$ ‣ • ‣ B.2) in the $\Rightarrow$
direction). We define
$A^{\prime}\coloneqq\delta^{\prime}(\delta_{\mathrm{m}}(a))$. Together with
($\Longleftarrow$ ‣ • ‣ B.2), we can use the same reasoning as in the
$\Rightarrow$ case to obtain $\overline{b}=\delta_{\mathrm{r}}(\overline{c})$
and the alpha-equivalence of and $\widehat{\delta^{\prime\prime}}(B)$ and
$\forall\overline{b}.A^{\prime}$.

Hence,
$\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});(\Gamma^{\prime},x:\widehat{\delta^{\prime\prime}}B);\widehat{\delta^{\prime\prime}}\vdash
C$ (see derivation of ($\Longleftarrow$ ‣ • ‣ B.2)) is equivalent to
$\Delta^{\prime};\allowbreak(\Xi^{\prime},\widetilde{a^{\prime\prime}});\allowbreak(\Gamma^{\prime},x:\forall\overline{b}.A^{\prime});\allowbreak\widehat{\delta^{\prime\prime}}\vdash
C$. We have $\Delta^{\prime}\vdash\forall\overline{b}.A^{\prime}\ \mathbf{ok}$
and $(\Delta,\mathsf{rc}(F));\Xi^{\prime};(\mathsf{tc}(F),x:\bot)\vdash C\
\mathbf{ok}$ which means we can weaken it to
$\Delta^{\prime};\Xi^{\prime};(\Gamma^{\prime},x:\forall\overline{b}.A^{\prime});\hat{\delta}\vdash
C$.

Next, we define $\widehat{\delta^{\prime}}\coloneqq\hat{\delta}[a\mapsto
A^{\prime}]$ as in the $\Rightarrow$ case and show that
$(\Delta^{\prime},\tilde{b});(\Xi^{\prime},a);\Gamma^{\prime};\widehat{\delta^{\prime}}\vdash\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\allowbreak\theta_{0})$
(13) holds. To this end, we wish to apply Lemma 13 to
$\Delta^{\prime};(\Xi^{\prime},\widetilde{a^{\prime\prime}});\Gamma^{\prime};\widehat{\delta^{\prime\prime}}\vdash\mathfrak{U}(\Theta_{1},\theta_{1})$
(see derivation of ($\Longleftarrow$ ‣ • ‣ B.2)), which gives us the existence
of $\theta^{\prime}_{1}$ such that
$\Delta^{\prime}\vdash\theta^{\prime}_{1}:\Theta_{1}\Rightarrow\cdot$ and
$\widehat{\delta^{\prime\prime}}=\theta^{\prime}_{1}\circ\theta_{1}$ (14). We
now show that the necessary preconditions of the lemma are satisfied.

Recall that
$\mathsf{ftv}(\Theta_{1})=\mathsf{ftv}(\Theta_{0})-\widetilde{a^{\prime}}$ and
$\tilde{c}\subseteq\widetilde{a^{\prime}}$. We now define
$\theta^{\prime}_{0}$ as an extension of $\theta^{\prime}_{1}$ by setting
$\theta^{\prime}_{0}(c)=\delta_{\mathrm{r}}(c)$ for all $c\in\tilde{c}$, and
$\theta^{\prime}_{0}(c)=\mathsf{unit}$ for all
$c\in\widetilde{a^{\prime}}-\tilde{c}$. This implies
$\Delta^{\prime},\tilde{b}\vdash\theta^{\prime}_{0}:\Theta_{0}\Rightarrow\cdot$.
We now show that
$\widehat{\delta^{\prime}}={(\theta^{\prime}_{0}\circ\theta_{0})}\mathord{\upharpoonright}_{(\Xi^{\prime},a)}$
(15). For all $b\in\Xi^{\prime}$ we immediately get
$\theta^{\prime}_{0}(\theta_{0}(b))=\widehat{\delta^{\prime\prime}}(b)$ by
$\Xi^{\prime}\subseteq\mathsf{ftv}(\Theta_{1})$ and ($\Longleftarrow$ ‣ • ‣
B.2).

It remains to show that
$\theta^{\prime}_{0}(\theta_{0}(a))=\widehat{\delta^{\prime}}(a)\stackrel{{\scriptstyle\text{def.\
}}}{{=}}A^{\prime}$. By definition of $A^{\prime}$ and $\delta_{\mathrm{m}}$
we have
$A^{\prime}=\delta^{\prime}(\delta_{\mathrm{m}}(a))=\delta^{\prime}(\delta_{\mathrm{r}}(\theta_{0}(a))$.
Therefore, it sufficies to show that for all
$b\in\mathsf{ftv}(\theta_{0}(a))-\Delta^{\prime}$ we have
$\theta^{\prime}_{0}(b)=\delta^{\prime}(\delta_{\mathrm{r}}(b))$. If
$b\in(\Xi^{\prime},\widetilde{a^{\prime\prime}})$ we have
$\theta^{\prime}_{0}(b)=\theta^{\prime}_{1}(b)$. By
$b\in\mathsf{ftv}(\theta_{0})$ we have $\theta_{0}(b)=b$, which means that
($\Longleftarrow$ ‣ • ‣ B.2) imposes
$\theta^{\prime}_{1}(b)=\widehat{\delta^{\prime\prime}}(b)$. By definition of
$\delta^{\prime}$ we then have
$\theta^{\prime}_{0}(b)=\theta^{\prime}_{1}(b)=\widehat{\delta^{\prime\prime}}(b)=\widehat{\delta^{\prime\prime}}(\delta^{-1}_{\mathrm{r}}(\delta_{\mathrm{r}}(b)))=\delta^{\prime}(\delta_{\mathrm{r}}(b))$.
Otherwise, if $b\in\widetilde{a^{\prime}}$, we have
$\delta_{\mathrm{r}}(b)\not\in\Delta_{\mathrm{o}}$ and therefore
$\theta^{\prime}_{0}(b)=\delta_{\mathrm{r}}(b)=\delta^{\prime}(\delta_{\mathrm{r}}(b))$.
Finally, having shown ($\Longleftarrow$ ‣ • ‣ B.2) we may apply Lemma 13 to
obtain ($\Longleftarrow$ ‣ • ‣ B.2).

In conclusion, we can now derive
$\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash
C^{\prime}_{1}$ as follows:

$\inferrule{\mathsf{mostgen}(\Delta^{\prime},(\Xi^{\prime},a),\Gamma^{\prime},\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0}),\Delta_{\mathrm{m}},\delta_{\mathrm{m}})\\\
\\\
\Delta_{\mathrm{o}}=\mathsf{ftv}(\delta_{\mathrm{m}}(\Xi^{\prime}))-\Delta^{\prime}\\\
\overline{b}=\mathsf{ftv}(\delta_{\mathrm{m}}(a))-\Delta^{\prime},\Delta_{\mathrm{o}}\\\
\\\
\Delta^{\prime}\vdash\delta^{\prime}:\Delta_{\mathrm{o}}\Rightarrow_{\mathord{\bullet}}\cdot\\\
A^{\prime}=\delta^{\prime}(\delta_{\mathrm{m}}(a))\\\ \\\
(\Delta^{\prime},\tilde{b});(\Xi^{\prime},a);\Gamma^{\prime};\hat{\delta}[a\mapsto
A^{\prime}]\vdash\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0})\\\
\Delta^{\prime};\Xi^{\prime};(\Gamma^{\prime},x:\forall\overline{b}.A^{\prime});\hat{\delta}\vdash
C}{\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\hat{\delta}\vdash{\rm{\bf
let}}_{\star}\;x=\sqcap
a.\exists\tilde{a}.\mathfrak{U}(\Theta_{0},\theta_{0})\;{\rm{\bf in}}\;C}$

∎

###  B.3. Proof of Theorem 4

See 4

###### Proof.

Let $s:=(F,\Theta,\theta,C)$. By assumption, we have
$\cdot;\cdot;\cdot;\emptyset\vdash F[C\wedge\mathfrak{U}(\Theta,\theta)]$ (1).

We first assume $C\neq\mathsf{true}$ and show that one of the rules in Figure
9 is applicable.

  * •

Case $C_{1}\wedge C_{2}$: Rule S-ConjPush is applicable.

  * •

Case $A\sim B$: The left-hand-side of S-Eq matches. The derivation of (B.3)
must contain a subderivation of the form

$\inferrule{\delta^{\prime}(A)=\delta^{\prime}(B)}{\Delta^{\prime};\Xi^{\prime};\Gamma^{\prime};\delta^{\prime}\vdash
A\sim B}$

for some $\Delta^{\prime},\Xi^{\prime},\Gamma^{\prime},\delta^{\prime}$.

Since we are using the same unification algorithm as in (Emrich et al., 2020),
we can then use (Emrich et al., 2020, Theorem 5) to show that unification
succeeds.

  * •

Case $\lceil{x:A}\rceil$: The left-hand-side of S-Inst matches. By (B.3) we
have $x\in\mathsf{tc}(F)$, meaning that the rule succeeds.

  * •

Case $x\preceq A$: Rule S-Freeze is applicable (using the same argument to
show $x\in\mathsf{tc}(F)$ as in the previous case).

  * •

Case $\exists a.C^{\prime}$: Rule S-ExistsPush is applicable.

  * •

Case $\forall a.C^{\prime}$: Rule S-ForallPush is applicable.

  * •

Case ${\rm{\bf def}}\;(x:A)\;{\rm{\bf in}}\;C^{\prime}$: The left-hand-side of
S-DefPush matches.

The derivation of (B.3) must contain a sub-derivation of the form

$\inferrule{(\text{for all
}a\in\mathsf{ftv}(A)-(\mathsf{rc}(F),\Delta^{\prime})\mid(\mathsf{rc}(F),\Delta^{\prime});\mathsf{fc}(F);\delta(\mathsf{tc}(F));\delta\vdash\mathsf{mono}(a)\\\
\\\
(\mathsf{rc}(F),\Delta^{\prime});\mathsf{fc}(F);(\delta(\mathsf{tc}(F)),x:\delta
A);\delta\vdash
C^{\prime}}{(\mathsf{rc}(F),\Delta^{\prime});\mathsf{fc}(F);\delta(\mathsf{tc}(F));\delta\vdash{\rm{\bf
def}}\;(x:A)\;{\rm{\bf in}}\;C^{\prime}}$

for some $\delta$, where $C^{\prime}=C\wedge\mathfrak{U}(\Theta,\theta)$ and
$\mathsf{ftv}(\Theta)=\Xi$. Note that by $s\ \mathbf{ok}$ we have
$\mathsf{ftv}(A)\subseteq(\mathsf{rc}(F),\mathsf{fc}(F))$.

According to Lemma 13, we have $\delta=\theta^{\prime}\circ\theta$ for some
$\theta^{\prime}$ with
$(\mathsf{rc}(F),\Delta^{\prime})\vdash\theta^{\prime}:\Theta\Rightarrow\cdot$.
Therefore, the monomorphism conditions imposed by S-DefPush are satisfied.

  * •

Case $\mathsf{mono}(a)$: Analogous to def case; the sub-derivation for
$\mathsf{mono}(a)$ implies that the monomorphism conditions imposed by S-Mono
are satisifed, making the rule applicable.

  * •

Case ${\rm{\bf let}}_{R}\;x=\sqcap a.C_{1}\;{\rm{\bf in}}\;C_{2}$: Rule
S-LetPush is applicable.

We now conside the case that $C$ is $\mathsf{true}$. Due the assumption about
the shape of $F[C]$, we know that $F$ is neither emtpy nor of the shape
$\forall\Delta::\exists\overline{a}$ for any $\overline{a}$.

We perform a case analysis on the topmost stack frame of $F$:

  * •

Case $\Box\wedge C_{2}$: Rule S-ConjPop is applicable.

  * •

Case ${\rm{\bf def}}\;(x:A)$: Rule S-DefPop is applicable.

  * •

Case ${\rm{\bf let}}_{R}\;x=\sqcap a.C_{1}\;{\rm{\bf in}}\;C_{2}$: Rule
S-LetPolyPop or S-LetMonoPop is applicable, where the sequence $\overline{a}$
mentioned in the rule’s definition is empty. None of the respective rule’s
side conditions can fail.

  * •

Case $\forall a$: Let $F^{\prime}$ be defined such that $F=F^{\prime}::\forall
a$. By assumption $s\ \mathbf{ok}$ we have that the variables in $\Theta$ are
exactly the variables bound by $\exists$ or ${\rm{\bf let}}$ frames in
$F^{\prime}$. Suppose there exists $b\in\mathsf{ftv}(\Theta)$ such that
$a\in\mathsf{ftv}(\theta(b))$, which would cause the rule to fail. Then there
exists a frame $f$ in $F^{\prime}$ that binds $b$. Let $F_{p}$ be the
(possibly empty) prefix of $F^{\prime}$ up to, but not including, frame $f$
and let $F_{s}$ be the (possibly empty) suffix from there (i.e.,
$F^{\prime}=F_{p}::{}f::F_{s}$).

We distinguish two sub-cases further:

    1. (1)

If $f=\exists b$ then the derivation of (B.3) must contain a sub-derivation of
the following form:

$\inferrule{(\mathsf{rc}(F_{p}),\Delta^{\prime});(\mathsf{fc}(F_{p}),b);\delta(\mathsf{tc}(F_{p}));\delta[b\mapsto
A]\vdash
C^{\prime}}{(\mathsf{rc}(F_{p}),\Delta^{\prime});\mathsf{fc}(F_{p});\delta(\mathsf{tc}(F_{p}));\delta\vdash\exists
b.C^{\prime}}$

for some $A$, $\delta$, and $\Delta^{\prime}$, where
$C^{\prime}=F_{s}[C\wedge\mathfrak{U}(\Theta,\theta)]$.

Note that
$(\mathsf{rc}(F_{p}),\Delta^{\prime});(\mathsf{fc}(F_{p}),b);\delta(\mathsf{tc}(F_{p}));\delta[b\mapsto
A]\vdash C^{\prime}$ implies $(\mathsf{rc}(F_{p}),\Delta^{\prime})\vdash A\
\mathbf{ok}$ (2). Further, as $F_{s}$ contains the frame $\forall a$, we have
$a\not\in\mathsf{rc}(F_{p}),\Delta^{\prime}$ (3).

Likewise, there existis a subderivation showing
$(\mathsf{rc}(F),\Delta^{\prime\prime});\mathsf{fc}(F);\delta^{\prime\prime}(\mathsf{tc}(F));\delta^{\prime\prime}\vdash\mathfrak{U}(\Theta,\theta)$
for some $\Delta^{\prime\prime}$ and $\delta^{\prime\prime}$, where
$\Delta^{\prime\prime}\supseteq\Delta^{\prime}$ and $\delta^{\prime\prime}$ is
an extension of $\delta[b\mapsto A]$. By Lemma 13 we have that there exists
$\theta^{\prime}$ such that
$\mathsf{rc}(F),\Delta^{\prime\prime}\vdash\theta^{\prime}:\Theta\Rightarrow\cdot$
and $\delta^{\prime\prime}=(\theta^{\prime}\circ\theta)$. Because
$\delta^{\prime\prime}$ is an extension of $\delta[b\mapsto A]$, this implies
$A=\theta^{\prime}(\theta(b))$.

By $a\in\mathsf{rc}(F)$ we have $\theta^{\prime}(a)=a$. Due to assumption
$a\in\mathsf{ftv}(\theta(b))$ we then have $a\in\mathsf{ftv}(A)$ However, we
have $a\not\in\mathsf{btv}(F_{p}),\Delta^{\prime}$ (1) and
$\mathsf{rc}(F_{p}),\Delta^{\prime}\vdash A\ \mathbf{ok}$ (1), yielding the
contradiction $a\not\in\mathsf{ftv}(A)$.

    2. (2)

If $f$ is of the the form ${\rm{\bf let}}_{\star}\;x=\sqcap b.C_{1}\;{\rm{\bf
in}}\;C_{2}$ then the derivation of (B.3) must contain a sub-derivation of the
following form:

$\inferrule{\dots\\\ \\\
(\mathsf{rc}(F_{p}),\Delta^{\prime},\tilde{a});(\mathsf{fc}(F_{p}),b);\delta(\mathsf{tc}(F_{p}));\delta[b\mapsto
A]\vdash C_{1}\\\
}{(\mathsf{rc}(F_{p}),\Delta^{\prime});\mathsf{fc}(F_{p});\delta(\mathsf{tc}(F_{p}));\delta\vdash{\rm{\bf
let}}_{\star}\;x=\sqcap b.C_{1}\;{\rm{\bf in}}\;C_{2}}$

for some $A,\Delta^{\prime},\tilde{a}$ and $\delta$, where
$C_{1}=F_{s}[C\wedge\mathfrak{U}(\Theta,\theta)]$. We have
$(\mathsf{rc}(F_{p}),\Delta^{\prime},\tilde{a})\vdash A\ \mathbf{ok}$ and
$a\not\in\mathsf{rc}(F_{p}),\Delta^{\prime},\tilde{a}$ and may therefore
obtain the same contradiction as in the previous case $f=\exists b$.

    3. (3)

The case ${\rm{\bf let}}_{\mathord{\bullet}}\;x=\sqcap b.C_{1}\;{\rm{\bf
in}}\;C_{2}$ is analogous.

  * •

Case $\exists{a}$: If the topmost stack frames of $F$ have the shape ${\rm{\bf
let}}_{R}x=\sqcap a.\Box\;{\rm{\bf in}}\;C^{\prime}::\exists\overline{b}$,
then S-LetPolyPop or S-LetMonoPop is applicable, as discussed before.
Otherwise, due to our assumption about the shape of $F[C]$, there exists a
frame $f$ in $F$ that isn’t an $\exists$ frame and we can apply S-ExistsLower,
which always succeeds.

∎

###  B.4. Proof of Theorem 5

###### Lemma 20 (Well-Ordering on States).

There exists a strict well-ordering $<$ on the set $\mathsf{St}$ of stack
machine states such that for all $s,s^{\prime}\in\mathsf{St}$ with $s\to
s^{\prime}$ we have $s^{\prime}<s$.

###### Proof.

First, we define the size of a constraint $C$, denoted $|C|$, s.t.

$\begin{array}[]{r c l}|\mathsf{true}|&=&0\\\ |\mathsf{mono}(a)|&=&1\\\ |A\sim
B|&=&1\\\ |\lceil{x:A}\rceil|&=&2\\\ |x\preceq A|&=&2\\\ |\exists
a.C|&=&1+|C|\\\ |\forall a.C|&=&1+|C|\\\ |{\rm{\bf def}}\;(x:A)\;{\rm{\bf
in}}\;C|&=&1+|C|\\\ |C_{1}\wedge C_{2}|&=&1+|C_{1}|+|C_{2}|\\\ |{\rm{\bf
let}}_{R}\;x=\sqcap a.C_{1}\;{\rm{\bf in}}\;C_{2}|&=&3+|C_{1}|+|C_{2}|\\\
\end{array}$

Next, we define $\mathsf{insts}(C)$ to be the number of instantiation
(sub-)constraints in $C$.

We now define the function $|\cdot|$ that maps states to elements of
$\mathbb{N}_{0}\times\mathbb{N}_{0}\times\mathbb{N}_{0}\times\mathbb{N}_{0}$:

$\begin{array}[]{r c
l}|(f_{0}::\dots::f_{n},\Theta,\theta,C)|=(\mathsf{insts}(C),\>|F[C]|,\>|C|,\>\max\\{i\mid
0\leq i\leq n,\text{ $f_{i}$ is an $\exists$ frame }\\})\end{array}$

We observe that the lexicographic ordering $<_{\mathit{lex}}$ on tuples from
$\mathbb{N}_{0}\times\mathbb{N}_{0}\times\mathbb{N}_{0}\times\mathbb{N}_{0}$
constitutes a well-ordering on such tuples and we will show below that for
each step $s\to s^{\prime}$ we have that $|s^{\prime}|<_{\mathit{lex}}|s|$
holds. However, the function $|\cdot|$ on states is surjective, which implies
that defining $s^{\prime}<s$ iff $|s^{\prime}|<_{\mathit{lex}}|s|$ would _not_
yield a total order on states. Hence, let $<_{\mathit{ord}}$ be some arbitrary
strict well-order on states. We then define

$s^{\prime}<s\;\;\text{iff}\;\;|s^{\prime}|<_{\mathit{lex}}|s|\text{ or
}|s^{\prime}|=|s|\text{ and }s^{\prime}<_{\mathit{ord}}s$

which is indeed a well-ordering.

It remains to show that each step of the stack machine produces a smaller
state w.r.t. $|\cdot|$. Hence, assume $s\to s^{\prime}$, where
$s=(F,\Theta,\theta,C)$ and
$s^{\prime}=(F^{\prime},\Theta^{\prime},\theta^{\prime},C^{\prime})$.

  * •

If the step is the result of applying the rule S-Eq, S-Freeze, or S-Mono, then
we have $F=F^{\prime}$ and $|C^{\prime}|<|C|$, yielding
$|s^{\prime}|<_{\mathit{lex}}|s|$ via the second component of the tuples.

  * •

If the step is the result of applying S-Inst, we have
$\mathsf{insts}(C^{\prime})=\mathsf{insts}(C)-1$ and we have
$|s^{\prime}|<_{\mathit{lex}}|s|$ via the first component of the tuples.

  * •

If the step is the result of applying the rule S-ConjPop, S-ForallPop, or
S-DefPop, we have $\mathsf{insts}(C)=\mathsf{insts}(C^{\prime})$ and
$|F^{\prime}[C^{\prime}]|<|F[C]|$, yielding $|s^{\prime}|<_{\mathit{lex}}|s|$
via the second component of the tuple.

  * •

If the step is the result of applying the rule S-ConjPush, S-ExistsPush,
S-ForallPush, S-DefPush, or S-LetPush, we have
$\mathsf{insts}(C)=\mathsf{insts}(C^{\prime})$ and
$F[C]=F^{\prime}[C^{\prime}]$, but $|C^{\prime}|<|C|$, yielding
$|s^{\prime}|<_{\mathit{lex}}|s|$ via the third component of the tuples.

  * •

If S-ExistsLower got applied, let $\tilde{c}$ and $\tilde{a}$ be defined as in
the rule, $F=f_{0}::\dots f_{n}$, and $l=|\tilde{a}|$. Note that the rule
imposes $l>0$ and we have $C=C^{\prime}=\mathsf{true}$.

We observe that $\tilde{c}$ is a subset of $\tilde{a}$. If
$|\tilde{a}|>|\tilde{c}|$ , we have $|F^{\prime}[C^{\prime}]|<|F[C]|$ because
the set of frames of $F^{\prime}$ is a strict subset of the frames in $F$. We
then obtain $|s^{\prime}|<_{\mathit{lex}}|s|$ immediately via the second
component of the tuples (the first component remains unchanged). Otherwise, we
have that the two sets are equal. In that case we have
$|F[C]|=|F^{\prime}[C^{\prime}]|$ (as there is merely a reordering of stack
frames happening) and $|C|=|C^{\prime}|=0$. The resulting stack $F^{\prime}$
is of the form $f^{\prime}_{0}::\dots f^{\prime}_{n}$, where
$f^{\prime}_{n}=f_{n-l}$ (not an $\exists$ frame), and $f^{\prime}_{n-1}$ is
an $\exists$ frame.

Together, we have $|s|=(\mathsf{insts}(C),|F[C]|,0,n)$, and
$|s^{\prime}|=(\mathsf{insts}(C^{\prime}),|F[C]|,0,n-1)$, and
$\mathsf{insts}(C)=\mathsf{insts}(C^{\prime})$, yielding
$|s^{\prime}|<_{\mathit{lex}}|s|$.

  * •

If rule S-LetPolyPop was applied, we use the following reasoning: $F$ is of
the form $F_{0}::\mathsf{let}_{\star}\,x=\sqcap
c.\Box\,\mathsf{in}\,\hat{C}::\exists\tilde{a}$ and $C$ is $\mathsf{true}$.
This yields

$\begin{array}[]{rcl}|F[C]|&=&|F_{0}[{\rm{\bf let}}_{\star}\;x=\sqcap
c.\exists\tilde{a}.\mathsf{true}\;{\rm{\bf in}}\;\hat{C}]|\\\ &=&|{\rm{\bf
let}}_{\star}\;x=\sqcap c.\mathsf{true}\;{\rm{\bf
in}}\;\mathsf{true}|+|\exists{\tilde{a}.\mathsf{true}}|+|\hat{C}|+|F_{0}[\mathsf{true}]|\\\
&=&3+|\tilde{a}|+|\hat{C}|+|F_{0}[\mathsf{true}]|,\end{array}$

Let $\widetilde{a^{\prime\prime}}$ be defined as in the rule. We have

$|F^{\prime}[C^{\prime}]|=|F_{0}[\exists\widetilde{a^{\prime\prime}}.{\rm{\bf
def}}\;(x:A)\;{\rm{\bf
in}}\;\hat{C}]=1+|\widetilde{a^{\prime\prime}}|+|\hat{C}|+|F_{0}[\mathsf{true}]|$

Proving $F^{\prime}[C^{\prime}]<F[C]$ is therefore equivalent to proving

$\begin{array}[]{c
l}&1+|\widetilde{a^{\prime\prime}}|+|\hat{C}|+|F_{0}[\mathsf{true}]|<3+|\tilde{a}|+|\hat{C}|+|F_{0}[\mathsf{true}]|\\\
\text{equiv. }&\widetilde{a^{\prime\prime}}<2+\tilde{a}.\end{array}$

We observe that $\widetilde{a^{\prime\prime}}$ is a strict subset of
$(\tilde{a},c)$ and hence $|\widetilde{a^{\prime\prime}}|<|\tilde{a}|+2$,
meaning that the inequality above holds.

We have $\mathsf{insts}(C)=\mathsf{insts}(C^{\prime})$, and therefore
$|s^{\prime}|<_{\mathit{lex}}|s|$ via the second component of the tuples.

  * •

The reasoning for rule S-LetMonoPop is analogous to the previous case. The
only change is that we need to observe that
$(\tilde{c},\widetilde{a^{\prime\prime}})$ is a subset of $(\tilde{a},c)$.

∎

See 5

###### Proof.

Follows immediately from Lemma 20, which guarantees the absence of infinite
sequences of steps. ∎

###  B.5. Proof of Theorem 6

The following lemma is a slight variation of Theorem 6; we use it in the proof
of the latter.

###### Lemma 21.

Let $(\forall\Delta::{}\exists\tilde{a}::{}F,\Theta,\theta,C)\ \mathbf{ok}$.
Then we have

$\begin{array}[t]{@{}l@{}}\Delta;\tilde{a};\cdot;\delta\vdash
F[C\wedge\mathfrak{U}(\Theta,\theta)]\\\ \text{iff}\\\ \text{there exist
}\Theta^{\prime},\theta^{\prime\prime},\theta^{\prime},\tilde{b}\text{ s.t.\
}\\\
\begin{array}[]{cl}&(\forall\Delta::{}\exists\tilde{a}::{}F,\Theta,\theta,C)\to^{*}(\forall\Delta::\exists\;(\tilde{a},\tilde{b}),\Theta^{\prime},\theta^{\prime},\mathsf{true})\text{
and }\\\
&\Delta\vdash\theta^{\prime\prime}:\Theta^{\prime}\Rightarrow\cdot\text{ and
}\\\
&{(\theta^{\prime\prime}\circ\theta^{\prime})}\mathord{\upharpoonright}_{\tilde{a}}=\delta\end{array}\end{array}$

###### Proof.

We show each direction individually:

  * $\Longrightarrow$

By transfinite induction on the well-ordering $<$ on stack machine states $s$
whose existence is shown in Lemma 20. Hence, we assume that the left-to-right
direction of the lemma holds for all $s^{\prime}$ on the left of the $\to^{*}$
s.t. $s^{\prime}<s$ and show that the left-to-right direction holds for $s$ on
the left of $\to^{*}$, too.

To this end, let
$s=(\forall\Delta::{}\exists\tilde{a}::{}F,\Theta,\theta,F,C)$ and we assume
$s\ \mathbf{ok}$ (1) and $\Delta;\tilde{a};\cdot;\delta\vdash
F[C\wedge\mathfrak{U}(\Theta,\theta)]$ (2).

We first consider the case that $s$ is already a final state in the senses of
this lemma, meaning that $F$ is of the shape $\exists\tilde{b}$ for some
$\tilde{b}$ and $C$ is $\mathsf{true}$. Further, we have
$\theta=\theta^{\prime}$ and $\Theta=\Theta^{\prime}$, where
$\mathsf{ftv}(\Theta)=\tilde{a},\tilde{b}$.

This makes ($\Longrightarrow$ ‣ B.5) equivalent to
$\Delta;\tilde{a};\cdot;\delta\vdash\exists\tilde{b}.\mathfrak{U}(\Theta,\theta)$.
Applying Lemma 13 then gives us the existence of an appropriate
$\theta^{\prime\prime}$.

We now consider the case where $s$ is not a final state, i.e., we don’t have
$F[C]=\exists\tilde{b}.\mathsf{true}$ for any $\tilde{b}$. We observe that
($\Longrightarrow$ ‣ B.5) implies
$;\cdot;\cdot;\emptyset\vdash\forall\Delta::\exists\tilde{a}::F[C\wedge\mathfrak{U}(\Theta,\theta)]$.
This allows us to apply Theorem 4, showing that the machine can take a step
from $s$ to a new state $s_{1}$. We now show that $s_{1}$ is of the form
$(\forall\Delta::{}\exists\tilde{a}::{}F_{1},\Theta_{1},\theta_{1},C_{1})$ for
some $F_{1},\Theta_{1},\theta_{1}$, and $C_{1}$:

If $F$ is empty, then $C$ must not be $\mathsf{true}$. All stack machine rules
applicable in this case preserve all existing stack frames. Otherwise, if $F$
is not empty, we observe that the only rules of the stack machine that may
replace more than the topmost stack frame are S-ExistsLower, S-LetMonoPop, and
S-LetPolyPop.

If S-ExistsLower was applied, we observe that the only way for the variables
$\tilde{a}$ in the definition of the rule S-ExistsLower not to be disjoint
from the variables $\tilde{a}$ in the statement of this lemma is if the stack
of $s$ is of the form $\forall\Delta::\exists\tilde{a}::\exists\tilde{b}$ for
some $\tilde{b}$, which violates the assumption about the shape of $F[C]$
above. Therefore, if S-ExistsLower was applied, the bottom-most frames
$\forall\Delta::\exists\tilde{a}$ of $s$ remained unchanged. If S-LetPolyPop
or S-LetMonoPop was applied, then $F$ must contain a ${\rm{\bf let}}$ frame
and any stack frames below that in $s$ (in particular, the frames
$\forall\Delta::\exists\tilde{a}$) remain unchanged.

Therefore, the $\forall\Delta::{}\exists\tilde{a}$ frames at the bottom of
$s$’s stack are preserved by any rule possibly turning $s$ into $s_{1}$. Using
($\Longrightarrow$ ‣ B.5) and the fact that the lower stack frames of $s_{1}$
are $\forall\Delta::\exists\tilde{a}$, we may apply Theorem 3 to the step
$s\to s_{1}$, which gives us

    * (2)

$\Delta;\tilde{a};\cdot;\delta\vdash
F[C\wedge\mathfrak{U}(\Theta,\theta)]\;\text{ iff
}\;\Delta;\tilde{a};\cdot;\delta\vdash
F_{1}[C_{1}\wedge\mathfrak{U}(\Theta_{1},\theta_{1})]$

By Lemma 20, we further have $s_{1}<s$ (3) and by Lemma 16 $s_{1}\
\mathbf{ok}$ (4).

Combining ($\Longrightarrow$ ‣ B.5) with ((2)) gives us
$\Delta;\tilde{a};\cdot;\delta\vdash
F_{1}[C_{1}\wedge\mathfrak{U}(\Theta_{1},\theta_{1})]$. This, together with
($\Longrightarrow$ ‣ B.5) and ($\Longrightarrow$ ‣ B.5) allows us to apply the
induction hypothesis to $s_{1}$. This gives us the existence of
$\Theta^{\prime},\theta^{\prime\prime},\theta^{\prime},\tilde{a}$ s.t.

    * (4)

$(\forall\Delta::{}\exists\tilde{a}::{}F_{1},\Theta_{1},\theta_{1},C_{1})\to^{*}(\forall\Delta::\exists\;(\tilde{a},\tilde{b}),\Theta^{\prime},\theta^{\prime},\mathsf{true})$

    * (4)

$\Delta\vdash\theta^{\prime\prime}:\Theta^{\prime}\Rightarrow\cdot$

    * (4)

${(\theta^{\prime\prime}\circ\theta^{\prime})}\mathord{\upharpoonright}_{\tilde{a}}=\delta$.

The step $s\to s_{1}$ extends ((4)) to
$(\forall\Delta::{}\exists\tilde{a}::{}F,\Theta,\theta,C)\to^{*}(\forall\Delta::\exists\;(\tilde{a},\tilde{b}),\Theta^{\prime},\theta^{\prime},\mathsf{true})$
and ((4)) as well as ((4)) show us that $\theta^{\prime\prime}$ has the
desired properties.

  * $\Longleftarrow$

Let $s$ be the state
$(\forall\Delta::{}\exists\tilde{a}::{}F,\Theta,\theta,C)$. We prove this
direction by induction on the length $n$ of the sequence
$s\to^{n}(\forall\Delta::\exists\;(\tilde{a},\tilde{b}),\Theta^{\prime},\theta^{\prime},\mathsf{true})$.
By assumption, we also have
$\Delta\vdash\theta^{\prime\prime}:\Theta^{\prime}\Rightarrow\cdot$ (5) and
${(\theta^{\prime\prime}\circ\theta^{\prime})}\mathord{\upharpoonright}_{\tilde{a}}=\delta$
(6).

If $n=0$ we have $\Theta=\Theta^{\prime}$, $\theta=\theta^{\prime}$,
$C=\mathsf{true}$, and $F=\exists\tilde{b}$. The property to prove simplifies
to
$\Delta;\tilde{a};\cdot;\delta\vdash\exists\tilde{b}.\mathfrak{U}(\Theta,\theta)$.
This follows directly from applying Lemma 13 to ($\Longleftarrow$ ‣ B.5) and
($\Longleftarrow$ ‣ B.5).

In the inductive step there exists some $s_{1}$ s.t.

$s\to
s_{1}\to^{*}(\forall\Delta::{}\exists(\tilde{a},\tilde{b}),\Theta^{\prime},\theta^{\prime},\mathsf{true})$

We now assume that $F[C]$ is not of the form $\exists\tilde{c}.\mathsf{true}$
for any $\tilde{c}$ (otherwise, $s$ would already be a final state in the
sense of this lemma and we finish the proof directly using the $n=0$ case
above).

Therefore, using the same reasoning as in the $\Longrightarrow$ direction, we
know that $s_{1}$ is of the form
$(\forall\Delta::{}\exists\tilde{a}::{}F_{1},\Theta_{1},\theta_{1},C_{1})$ for
some $F_{1},\Theta_{1},\theta_{1}$, and $C_{1}$. According to Lemma 16, we
have $s_{1}\ \mathbf{ok}$. We can therefore apply Theorem 3 to this single
step, yielding

    * (6)

$\Delta;\tilde{a};\cdot;\delta\vdash
F[C\wedge\mathfrak{U}(\Theta,\theta)]\;\text{ iff
}\;\Delta;\tilde{a};\cdot;\delta\vdash
F_{1}[C_{1}\wedge\mathfrak{U}(\Theta_{1},\theta_{1})]$

We apply the induction hypothesis to the sequence
$s_{1}\to^{*}(\forall\Delta::{}\exists(\tilde{a},\tilde{b}),\Theta^{\prime},\theta^{\prime},\mathsf{true})$,
yielding $\Delta;\widetilde{a};\cdot;\delta\vdash
F_{1}[C_{1}\wedge\mathfrak{U}(\Theta_{1},\theta_{1})]$ By ((6)), this gives us
the desired property $\Delta;\widetilde{a};\cdot;\delta\vdash
F[C\wedge\mathfrak{U}(\Theta,\theta)]$.

∎

See 6

###### Proof.

Let $\overline{a}$ be an arbitrary ordering of the variables in $\Xi$.
Further, let $\theta_{\mathrm{a}}:=[\overline{a}\mapsto\overline{a}]$ and
$\Theta_{\mathrm{a}}:=(\widetilde{a:\star})$. We have

$(\cdot,\cdot,\emptyset,\forall\Delta.\exists\tilde{a}.{\rm{\bf
def}}\;\Gamma\;{\rm{\bf
in}}\;C)\;\to^{*}\;(\forall\Delta::\exists\tilde{a},\Theta_{\mathrm{a}},\theta_{\mathrm{a}},{\rm{\bf
def}}\;\Gamma\;{\rm{\bf in}}\;C)$

after $|\Delta|$ applications of the rule S-ForallPush and $|\tilde{a}|$
applications of S-ExistsPush. Let the former state be defined as $s$, the
latter one as $s^{\prime}$. Here, due to $\Delta;\Theta;\Gamma\vdash C\
\mathbf{ok}$, we have $s^{\prime}\ \mathbf{ok}$.

Therefore, for all $\hat{\Theta},\hat{\theta},\tilde{b}$ we have

$\begin{array}[]{r c
l}s^{\prime}&\to^{*}&(\forall\Delta::\exists\;(\tilde{a},\tilde{b}),\hat{\Theta},\hat{\theta},\mathsf{true})\\\
\lx@intercol\hfil\text{iff}\hfil\lx@intercol\\\
s&\to^{*}&(\forall\Delta::\exists\;(\tilde{a},\tilde{b}),\hat{\Theta},\hat{\theta},\mathsf{true})\\\
\end{array}$

Now, let $F$ be the empty stack. We then have

$\begin{array}[]{r r@{} l@{} l@{} l@{}}&\Delta;\Xi;\Gamma;\delta&\vdash&C\\\
\;\text{ iff }&\Delta;\Xi;\cdot;\delta&\vdash&({\rm{\bf
def}}\;\Gamma\;{\rm{\bf in}}\;C)&\text{(by $\Delta\vdash\Gamma$: all mono.
conditions satisfied)}\\\ \;\text{ iff
}&\Delta;\Xi\,;\cdot;\delta&\vdash&({\rm{\bf def}}\;\Gamma\;{\rm{\bf
in}}\;C)\wedge\mathfrak{U}(\Theta_{\mathrm{a}},\theta_{\mathrm{a}})&\text{($\mathfrak{U}(\Theta_{\mathrm{a}},\theta_{\mathrm{a}})$
is equivalent to $\mathsf{true}$)}\\\ \;\text{ iff
}&\Delta;\Xi\,;\cdot;\delta&\vdash&F[({\rm{\bf def}}\;\Gamma\;{\rm{\bf
in}}\;C)\wedge\mathfrak{U}(\Theta_{\mathrm{a}},\theta_{\mathrm{a}})]&\text{($F$
is empty)}\\\ \end{array}$

Using this, the equivalence to prove then follows directly from Lemma 21. ∎

###  B.6. Proof of Theorem 7

See 7

###### Proof.

Suppose $(\cdot,\cdot,\emptyset,\forall\Delta.\exists a.{\rm{\bf
def}}\;\Gamma\;{\rm{\bf in}}\;\llbracket M:a\rrbracket)$ $\to^{*}$
$(\forall\Delta::\exists\;(a,\tilde{b}),\Theta,\theta,\allowbreak\mathsf{true})$
and $\Delta\vdash\theta^{\prime}:\Theta\Rightarrow\cdot$. Let $s$ refer to the
first state of the sequence above and $s^{\prime}$ to its last state.

We apply Lemma 11, which gives us $\Delta;a;\Gamma\vdash\llbracket
M:a\rrbracket\ \mathbf{ok}$. We therefore have $\vdash s\ \mathbf{ok}$. By
Lemma 16 we then have $\vdash s^{\prime}\ \mathbf{ok}$, too, which implies
$\Delta\vdash\Theta\Rightarrow\cdot$ and $\mathsf{ftv}(\Theta)=\tilde{b},a$.

We can therefore define $\delta$ as
$\theta^{\prime}\circ{\theta}\mathord{\upharpoonright}_{\\{a\\}}$. This allows
us to apply Theorem 6. We instantiate the right-to-left direction of the
theorem such that we need to show that the following properties hold:

  * (0)

$(\cdot,\cdot,\emptyset,\forall\Delta.\,\exists a.\,{\rm{\bf
def}}\>\Gamma\>{\rm{\bf
in}}\>C)\to^{*}(\forall\Delta::\exists\;(a,\tilde{b}),\Theta,\theta,\mathsf{true})$

  * (0)

$\Delta\vdash\theta^{\prime}:\Theta\Rightarrow\cdot$

  * (0)

${(\theta^{\prime}\circ\theta)}\mathord{\upharpoonright}_{a}=\delta$

The first two properties follow immediately by assumption, the third one holds
by definition of $\delta$. Therefore, the right-to-left direction of Theorem 6
gives us $\Delta;a;\Gamma;\delta\vdash\llbracket M:a\rrbracket$. Theorem 2
then immediately yields $\Delta;\Gamma\vdash M:\delta(a)$. By definition of
$\delta$ this is equivalent to the property to show.

∎

###  B.7. Proof of Theorem 8

See 8

###### Proof.

We assume $\Delta;\Gamma\vdash M:A$, which implies $\Delta\vdash\Gamma$ and
$\Delta;\Gamma\vdash M\ \mathbf{ok}$. This means that Theorem 1 gives us
$\Delta;a;\Gamma;[a\mapsto A]\vdash\llbracket M:a\rrbracket$.

We apply the left-to-right direction of Theorem 6 (using $\llbracket
M:a\rrbracket$ for $C$ and $[a\mapsto A]$ for $\delta$ in the theorem’s
statement) which gives us the existence of
$\Theta,\theta,\theta^{\prime},\tilde{c}$ s.t.

  * (0)

$(\cdot,\cdot,\emptyset,\forall\Delta.\exists a.{\rm{\bf
def}}\;\Gamma\;{\rm{\bf in}}\;\llbracket
M:a\rrbracket)\to^{*}(\forall\Delta::\exists(a,\tilde{c}),\Theta,\theta,\mathsf{true})$

  * (0)

$\Delta\vdash\theta^{\prime}:\Theta\Rightarrow\cdot$

  * (0)

${(\theta^{\prime}\circ\theta)}\mathord{\upharpoonright}_{\\{a\\}}=[a\mapsto
A]$

Clearly, we have
$(\theta^{\prime}\circ{\theta}\mathord{\upharpoonright}_{\\{a\\}})(a)=(\theta^{\prime}\circ\theta)(a)=[a\mapsto
A](a)=A,$ which is the second property we need to show. By choosing
$\Xi=(a,\tilde{c})$, property ((0)) becomes the first property that we needed
to show.

∎

##  Appendix C Further discussion of Let and Def constraints

As mentioned in the paper, our treatment of let and def constraints differs
from Pottier and Rémy (2005) in some ways, and in particular, lacks the nice
property that let constraints can be defined in terms of def constraints,
which can in turn be eliminated by a form of inlining. We have investigated
alternative designs, and not found one that has these properties and works
otherwise. In this appendix we outline the results of this exploration of the
design space. We use without further explanation notation from Pottier and
Rémy (2005).

###  C.1. Def constraints

In (Pottier and Rémy, 2005), qualified types $\sigma$ are of the form
$\forall\overline{X}[C].T$, where $T$ does not contain further quantifiers or
constraints.

Due to the existence of constraints in types in their system, the only
difference between Let constraints (using their syntax: of the form ${\rm{\bf
let}}\;x:\forall\overline{X}[C_{1}].T\;{\rm{\bf in}}\;C_{2}$) and Def
constraints (of the form ${\rm{\bf
def}}\;x:\forall\overline{X}[C_{1}].T\;{\rm{\bf in}}\;C_{2}$) is that the
former imposes satisfaction of the constraint $C_{1}$. This is expressed by
the following equivalence in (Pottier and Rémy, 2005): we have that

${\rm{\bf let}}\;x:\forall\overline{X}[C_{1}].T\;{\rm{\bf in}}\;C_{2}$

is equivalent to

$\exists\overline{X}.C_{1}\;\;\wedge\;\;{\rm{\bf
def}}\;x:\forall\overline{X}[C_{1}].T\;{\rm{\bf in}}\;C_{2}.$

####  C.1.1. Substituting def away in HM(X)

As stated in (Pottier and Rémy, 2005), their def constraints can be
substituted away. Concretely, in their work, the constraint ${\rm{\bf
def}}\;(x:\forall\overline{X}[C_{1}].T)\;{\rm{\bf in}}\;C_{2}$ is equivalent
to $C^{\prime}$, where $C^{\prime}$ results from $C_{2}$ by replacing all
$x\preceq T^{\prime}$ with $\exists\overline{X}.C_{1}\wedge T\leq T^{\prime}$.
Here, $\leq$ is their subtyping relation, and we may just use $\sim$ for the
purposes of this discussion.

####  C.1.2. Can we substitute def away?

We initially did not think this could be possible, however, this is not
entirely clear. In our system, consider the constraint ${\rm{\bf
def}}\;(x:\forall\overline{a}.H)\;{\rm{\bf in}}\;C_{2}$.

Straightforwardly adapting the equivalence from (Pottier and Rémy, 2005) would
yield a constraint $C^{\prime}$ that results from $C_{2}$ by replacing all
$x\preceq A$ with $\exists\overline{a}.H\sim A$ and all $\lceil{x:A}\rceil$
with $\forall\overline{a}.H\sim A$.

In our system, we then have that ${\rm{\bf
def}}\;(x:\forall\overline{a}.H)\;{\rm{\bf in}}\;C_{2}$ entails $C^{\prime}$,
but not the other direction.

To understand why, consider ${\rm{\bf def}}\;(x:a)\;{\rm{\bf
in}}\;x\preceq\forall b.(b\to b)$, where $a$ is some flexible variable. Its
substituted version $C^{\prime}$ is simply $a\sim\forall b.(b\to b)$, which is
clearly satisfiable, whereas the original constraint is not, as we need to
pick the polymorphic type $\forall b.b\to b$ for $a$, which def constraints
prohibit (due to the monomorphism premise in Sem-Def Figure 4).

####  C.1.3. What about redefining def?

One may now reasonably ask “is there a _different_ notion of def constraints
for which the reverse direction of the entailment holds” (which would mean
that a def constraint is indeed equivalent to the substituted version)? After
all, it’s the monomorphism restriction that is preventing the reverse
direction from holding.

One option we have considered is to try defining the semantics of def
constraints in terms of the substitution rule directly. Concretely, consider
the following, alternative version of the rule Sem-Def from Figure 3:

$\inferrule[\text{{Sem-Def-Alt}}]{\Delta;\Xi;\Gamma;\delta\vdash C[x\preceq
A\leadsto\exists\overline{a}.H\sim
A][\lceil{x:A}\rceil\leadsto\forall\overline{a}.H\sim
A]}{\Delta;\Xi;\Gamma;\delta\vdash{\rm{\bf
def}}\;(x:\forall\overline{a}.H)\;{\rm{\bf in}}\;C}$

We use $\leadsto$ here to indicate that _all_ subconstraints of $C$ of the
forms $x\preceq A$ and $\lceil{x:A}\rceil$ are replaced.

We conjecture that this yields a constraint language that still has most
general solutions and we could adapt the solver to behave accordingly. The
reason is that we still only _instantiate_ those variables $\overline{a}$ that
were explicitly given in the def constraint. If the remaining type $H$
contains flexible variables $a$ that are instantiated with polymorphic types
(which this version of def constraints would allow), those quantifiers could
never be instantiated. This is observable in the earlier example ${\rm{\bf
def}}\;(x:a)\;{\rm{\bf in}}\;x\preceq\forall b.(b\to b)$, which would now be
_defined_ to hold if $a\sim\forall b.(b\to b)$ holds, and therefore permits
the solution $a\mapsto(\forall b.b\to b)$ without being able to instantiate
$b$.

However, there are several issues with this, which is why we have not adopted
this idea in the paper.

  1. (1)

It appears rather un-intuitive that with this updated semantics, the _only_
solution for the constraint ${\rm{\bf def}}\;(x:a)\;{\rm{\bf
in}}\;x\preceq\forall b.(b\to b)$ is the one where we pick $a\mapsto(\forall
b.b\to b)$. When just seeing the constraint, we would expect $a\mapsto(\forall
b.b)$ to work, too.

  2. (2)

Similarly, consider the following two constraints:

$\begin{array}[]{rcll}C_{1}&:=&&{\rm{\bf def}}(x:\forall a.a\to a)\;{\rm{\bf
in}}\;x\preceq c\\\ C_{2}&:=&\exists b.b\sim(\forall a.a\to
a)\;\;\wedge&{\rm{\bf def}}(x:b)\;{\rm{\bf in}}\;x\preceq c\\\ \end{array}$

If we use the new version of let constraints (i.e., Sem-Def-Alt), we then have
that the solution for $C_{1}$ requires $c\mapsto d\to d$ for any type $d$,
whereas the solution for $C_{2}$ requires $c\mapsto(\forall a.a\to a)$. This
seems very un-intuitive.

Using our original semantics for def constraints (i.e., Sem-Def from Figure
3), we get the same solution for $C_{1}$ and $C_{2}$ is unsatisfiable.

  3. (3)

The rule Sem-Def-Alt would make def constraints more permissive than
unannotated $\lambda$ terms in FreezeML. If we used Sem-Def-Alt, we would be
able to conclude that the term $\lambda x.\lambda(f:(\forall
b.b)\to\mathsf{Int}).f\;\lceil{x}\rceil$ is well-typed, because the constraint
generated from it would now be satisfiable. However, this term is not accepted
by the FreezeML typing rules.

On the other hand, this problem could be mitigated by generating appropriate
$\mathsf{mono}{}$ constraints: We would change Figure 5 such that

$\llbracket\lambda x.M:A\rrbracket=\exists a_{1},a_{2}.(a_{1}\to a_{2}\sim
A\wedge{\rm{\bf def}}\;(x:a_{1})\;{\rm{\bf in}}\;\llbracket
M:a_{2}\rrbracket\wedge\mathsf{mono}{}(a_{1}))$

Instead of following the approach in C.1.3, one may think that we should make
instantiation constraints $A\preceq B$ part of the constraint language (rather
than being syntactic sugar for something else, as in (Pottier and Rémy,
2005)). Given a constraint ${\rm{\bf def}}(x:A)\;{\rm{\bf in}}\;C_{2}$, we
could then substitute all $x\preceq B$ in $C_{2}$ with $A\preceq B$ (and
substitute all $\lceil{x:B}\rceil$ as in C.1.2, meaning with $A\sim B$).

The problem with these constraints is that we need to ensure that the
polymorphism on the left-hand-side is already known: Without any restrictions,
the constraint $a\preceq\mathsf{Int}\to\mathsf{Int}$ would have no most
general solution, as both $a\mapsto(\forall b.b\to b)$ and
$a\mapsto\mathsf{Int}\to\mathsf{Int}$ are feasible.

However, term variables are _the very mechanism_ we use in our constraint
language to ensure that the polymorphism on the left-hand-side of an
instantiation constraint is fully determined! Therefore, using such
constraints would not simplify the treatment of instantiation.

###  C.2. Let constraints

Just using the semantics of let constraints, we can observe the following
properties

  1. (1)

If $\Delta;\Xi;\Gamma;\delta\vdash{\rm{\bf let}}_{\mathord{\bullet}}\;x=\sqcap
a.C_{1}\;{\rm{\bf in}}\;C_{2}$ holds, then for all
$\Delta_{\mathrm{m}},\delta_{\mathrm{m}}$ such that
$\mathsf{mostgen}(\Delta,(\Xi,a),\allowbreak\Gamma,\allowbreak
C_{1},\Delta_{\mathrm{m}},\allowbreak\delta_{\mathrm{m}})$ we have
$\Delta;\Xi;\Gamma;\delta\vdash\exists\Delta_{\mathrm{m}}.{\rm{\bf
def}}(x:\delta_{\mathrm{m}}(a))\;{\rm{\bf in}}\;C_{2}$.

  2. (2)

If $\Delta;\Xi;\Gamma;\delta\vdash{\rm{\bf let}}_{\mathord{\bullet}}\;x=\sqcap
a.C_{1}\;{\rm{\bf in}}\;C_{2}$ holds, then for all
$\Delta_{\mathrm{m}},\delta_{\mathrm{m}},\Delta_{\mathrm{o}},\overline{b}$
such that

$\begin{array}[t]{@{}l@{}}\mathsf{mostgen}(\Delta,(\Xi,a),\allowbreak\Gamma,\allowbreak
C_{1},\Delta_{\mathrm{m}},\allowbreak\delta_{\mathrm{m}})\\\
\Delta_{\mathrm{o}}=\mathsf{ftv}(\delta_{\mathrm{m}}(\Xi))-\Delta\\\
\overline{b}=\mathsf{ftv}(\delta_{\mathrm{m}}(a))-\Delta,\Delta_{\mathrm{o}}\\\
\\\ \end{array}$

we have $\Delta;\Xi;\Gamma;\delta\vdash\exists\Delta_{\mathrm{o}}.{\rm{\bf
def}}(x:\forall\overline{b}.\delta_{\mathrm{m}}(a))\;{\rm{\bf in}}\;C_{2}$.

Note that most general types are only unique up to the names of the freshly
introduced variables, which is why we need to universally quantify over
$\delta_{\mathrm{m}}$ and $\Delta_{\mathrm{m}}$ here. The extra conditions in
(2) defining $\Delta_{\mathrm{o}}$ and $\overline{b}$ are identical to those
in Sem-Let-Poly.

The properties stated in (1) and (2) are not equivalences between let and def
constraints, but only entailments.

It would probably be possible to state some form of equivalence, but that
doesn’t seem helpful: Because we don’t have constraints in types, a constraint
${\rm{\bf def}}\;(x:A)\;{\rm{\bf in}}\;C_{2}$ with an arbitrary type $A$
entails any constraint ${\rm{\bf let}}_{R}\;x=\sqcap a.C_{1}\;{\rm{\bf
in}}\;C_{2}$ where $C_{1}$ (a constraint pulled out of thin air) has a most
general solution that is somehow related to $A$.

Given the entailments stated in in (1) and (2), we could apply the
substitution of def constraints discussed in point C.1.2 in the previous
section C.1 to relate def constraints to constraints without def constraints.
Recall that these are also just entailments, not equivalences.

So far in this section, we have related constraints ${\rm{\bf let}}\;x=\sqcap
a.C_{1}\;{\rm{\bf in}}\;C_{2}$ to other constraints that effectively require
us to solve $C_{1}$ first (because we refer to
$\mathsf{mostgen}(\dots,C_{1},\dots)$ in the expansion). Would it be possible
to relate let constraints to other constraints without solving $C_{1}$ first?
In (Garrigue and Rémy, 1999) this is possible, by using constraints in types.

First, we observe that due to the impredicative nature of our system, we
cannot deal with instantiation constraints as in (Garrigue and Rémy, 1999)
(which we discussed Section C.1.1). Concretely, given a constraint ${\rm{\bf
let}}_{R}\;x=\sqcap a.C_{1}\;{\rm{\bf in}}\;C_{2}$, we cannot simply replace
all $x\preceq A$ occuring in $C_{2}$ with $\exists a.C_{1}\wedge a\sim A$.
While this may work for examples where generalisation occurs, like ${\rm{\bf
let}}_{\star}\;x=\sqcap a.\exists b.a\sim b\to b\;{\rm{\bf
in}}\;x\preceq\mathsf{Int}\to\mathsf{Int}$, it doesn’t work in cases such as
${\rm{\bf let}}_{R}\;x=\sqcap a.a\sim(\forall b.b\to b)\;{\rm{\bf
in}}\;x\preceq\mathsf{Int}\to\mathsf{Int}$ (irrespective of the choice of
$R$), because the scheme above would yield $\exists a.a\sim(\forall b.b\to
b)\wedge a\sim(\mathsf{Int}\to\mathsf{Int})$, which is unsatisfiable.

When considering ${\rm{\bf let}}_{\star}$ constraints, we observe that we
would need some form of explicit generalisation constraints to substitute away
freeze constraints under a generalising let constraint.

Consider the example ${\rm{\bf let}}_{\star}\;x=\sqcap a.\exists b.a\sim b\to
b\;{\rm{\bf in}}\;\lceil{x:\forall b.b\to b}\rceil$. Here, we cannot
substitute away $\lceil{x:\forall b.b\to b}\rceil$ with $\exists a.\exists
b.a\sim b\to b\;\wedge\;a\sim\forall b.b\to b$ (as discussed for handling
freeze constraints under ${\rm{\bf def}}$ in C.1.2).

Instead, we would need some kind of generalisation constraint $\sqcap a.C:A$
that generalises the type for $a$ in $C$ and asserts that the generalised
solution for $a$ is equal to $A$. However, we would have to generalise not any
type but the most general type: Otherwise, $\sqcap a.\exists b.a\sim b\to b:c$
would have the two solutions $c\mapsto(\mathsf{Int}\to\mathsf{Int})$ and
$c\mapsto\forall b.b\to b$, depending on what type we chose for $b$ prior to
generalising. This is the same reason why let terms and constraints have
principality conditions in our system.

Therefore, we would need to push the $\mathsf{mostgen}$ logic from let
constraints into the semantics of such generalisation constraints, too.