# Constraint-based type inference for FreezeML

Frank Emrich<EMAIL_ADDRESS>,  Jan Stolarek<EMAIL_ADDRESS>Lodz University of TechnologyPoland ,  James Cheney<EMAIL_ADDRESS>The
Alan Turing InstituteUK and  Sam Lindley<EMAIL_ADDRESS>The University
of EdinburghUK

###### Abstract.

FreezeML is a new approach to first-class polymorphic type inference that
employs term annotations to control when and how polymorphic types are
instantiated and generalised. It conservatively extends Hindley-Milner type
inference and was first presented as an extension to Algorithm W. More modern
type inference techniques such as HM($X$) and OutsideIn($X$) employ
constraints to support features such as type classes, type families, rows, and
other extensions. We take the first step towards modernising FreezeML by
presenting a constraint-based type inference algorithm. We introduce a new
constraint language, inspired by the Pottier/Rémy presentation of HM($X$), in
order to allow FreezeML type inference problems to be expressed as
constraints. We present a deterministic stack machine for solving FreezeML
constraints and prove its termination and correctness.

first-class polymorphism, type inference, impredicative types, constraints

††ccs: Software and its engineering Polymorphism††ccs: Software and its
engineering Functional languages

##  1\. Introduction

Hindley-Milner type inference is well-studied, yet extending it to provide
full support for polymorphism (“first-class” polymorphism a la System F)
remains an active research topic—characterised in one recent paper as “a deep,
deep swamp” (Serrano et al., 2018). A term such as $\lambda f.f\>f$ , which
would be rejected by Hindley-Milner type inference, may be accepted by a type
system permitting first-class polymorphism, by assigning a sufficiently
polymorphic type to $f$, such as $\forall a.a\to a$. However, type inference
for System F is undecidable (Wells, 1994), meaning that some restrictions must
be imposed. Choosing $\forall a.a$ as the type for $f$ also allows the example
above to type-check, but no System F type can be given to the function that
subsumes both choices. A wide range of solutions has emerged to explore the
resulting design space, yielding systems that go beyond System F types, employ
elaborate heuristics that determine the system’s behaviour, require type
annotations for certain terms, or rely on additional syntax, or give up on
completeness or principal typing, to name a few (Le Botlan and Rémy, 2003;
Leijen, 2008; Russo and Vytiniotis, 2009; Serrano et al., 2018; Garrigue and
Rémy, 1999; Serrano et al., 2020; Vytiniotis et al., 2006).

Recently, Emrich et al. (2020) proposed a new approach called FreezeML that
has several desirable properties: it conservatively extends ML type inference,
allows expressing arbitrary System F types and computations, and retains
decidable, complete type inference. The key ingredient of FreezeML is the
“freezing” operation, an annotation on term-level variables that _blocks_
automatic instantiation of any quantifiers in that variable’s type. FreezeML
also includes let- and lambda-bindings with ascribed types (which are standard
in other systems). Unlike other approaches to first-class polymorphism that
err on the side of explicitness (Russo and Vytiniotis, 2009; Garrigue and
Rémy, 1999), FreezeML uses just System F types instead of introducing
different, incompatible sorts of polymorphic types.

Freezing enables the programmer to control when instantiation happens instead
of requiring the type inference algorithm to guess or employ some heuristic
that the programmer must then work around. For instance, suppose we have
defined functions $\mathsf{single}:\forall a.a\to\mathsf{List}\;a$, which
creates a singleton list, and $\mathsf{choose}:\forall a.a\to a\to a$, which
returns one of its arguments (for type inference purposes it does not matter
which). In FreezeML we can define $f_{1}\;()=\mathsf{single}\;\mathsf{choose}$
and $f_{2}\;()=\mathsf{single}\;\lceil{\mathsf{choose}}\rceil$. In the former
(following the usual ML convention) both $\mathsf{single}$ and
$\mathsf{choose}$ are fully instantiated before the body is generalised, hence
$f_{1}:\forall a.\mathsf{unit}\to\mathsf{List}\;(a\to a\to a)$. In the latter,
however, instantiation of $\mathsf{choose}$ is frozen, hence
$f_{2}:\mathsf{unit}\to\mathsf{List}\;(\forall a.a\to a\to a)$.

The original presentation of FreezeML type inference was given as an extension
to Algorithm W (Damas and Milner, 1982). Although Algorithm W is well-
understood, many modern type inference implementations, notably Haskell,
employ _constraint-based type inference_ (Pottier, 2014; Pottier and Rémy,
2005; Vytiniotis et al., 2011) instead in which type inference is split into
two stages, mediated by an intermediate logical language of _constraints_
(Odersky et al., 1999; Pottier and Rémy, 2005). In the first stage, programs
$M$ are translated to constraints $C$ such that $C$ is solvable if and only if
$M$ is typable, and the solutions to $C$ are the possible types of $M$. In the
second stage, the constraint $C$ is solved (or shown to be unsatisfiable),
without further reference to $M$. Adopting a constraint-based inference
strategy has several potential benefits over the traditional Algorithm
W-style, including separating the core logic of type inference from the
details of the surface language, leveraging already-known efficient techniques
for constraint solver implementation, and supporting extensions such as type
classes and families, subtyping, rows, units of measure, GADTs (Odersky et
al., 1999; Simonet and Pottier, 2007; Vytiniotis et al., 2011), etc.

One influential approach to constraint-based type inference is HM($X$)
(Odersky et al., 1999; Pottier and Rémy, 2005), that is, Hindley-Milner type
inference “parameterised over X”, where $X$ stands for a constraint domain
that can be used in types. For example, if $X$ is a theory of type equality,
one obtains standard Hindley-Milner type inference HM($=$); if $X$ is a theory
of row types one obtains row type inference; if $X$ is a theory of subtyping
one gets type inference with subtyping.

In this paper, we take a first step towards such a constraint-parametric
system, a version of FreezeML parameterised in a constraint domain $X$, in the
spirit of HM($X$). Specifically, we introduce a constraint language for
FreezeML, inspired by HM($X$), in which type expressions can include arbitrary
polymorphism, and which provides suitable constraints to encode type inference
for FreezeML programs. (We have not yet explored parameterising the system
over the constraint domain $X$, but even adapting FreezeML to a constraint-
based approach turns out to require surmounting significant technical
obstacles.) We also provide a deterministic stack machine for solving these
constraints (again inspired by the presentation of constraint solving for
HM($X$) by Pottier and Rémy). Full correctness proofs for both contributions
are included in an appendix.

Formulating a suitable constraint language for FreezeML and a (provably)
correct translation and sound and complete solver involves several subtleties.
Handling the freeze operator itself turns out to be straightforward by adding
a constraint that checks that the type of a variable exactly matches an
expected type. Unification of types needs to account for polymorphism
occurring anywhere in a type, and constraints need to be extended with
universal quantifiers as well, in order to deal with polymorphism in ascribed
types. We also add a “monomorphism constraint” to enforce FreezeML’s
requirement that certain types are required to be monomorphic. Finally, to
deal with FreezeML’s approach to the value restriction (in which let-bindings
of non-values are allowed but not generalised) we introduce an additional
constraint form to handle type inference of non-generalisable expressions.
However, the most challenging problem is to design a constraint language and
semantics that preserves the necessary invariants to ensure that FreezeML type
inference remains sound, complete, and principal: specifically, to ensure that
flexible type variables occurring in the inferred types of variables are
always monomorphic, which is necessary in FreezeML to avoid the need to “guess
polymorphism” when a polymorphic type is instantiated.

Like certain other systems (Leroy and Mauny, 1991; Vytiniotis et al., 2006;
Leijen, 2008), typing derivations in FreezeML require principal types to be
assigned to certain subterms. To the best of our knowledge, the inference
algorithm shown in this paper is the first one based on constraint solving for
such a type system, requiring similar principality conditions in the semantics
of the constraint language. Detailed proofs of correctness are provided in an
appendix.

We characterise these contributions as a first step towards a longer-term
goal: parameterising FreezeML type inference over other constraint domains X.
This is a natural next step for future work, and would enable experimentation
with combining FreezeML-style polymorphism with features found in other modern
type systems, such as Haskell’s type classes and families (and the numerous
libraries that rely on them), higher-kinded types, and GADTs (Vytiniotis et
al., 2011), row types as found in Links (Lindley and Cheney, 2012), Koka
(Leijen, 2014) or Rose (Morris and McKinna, 2019), units of measure as found
in F# (Kennedy, 2009) and some Haskell libraries (Gundry, 2015). To summarise,
in this paper we:

  * •

present background on FreezeML (Section 2);

  * •

introduce a constraint language inspired by Pottier and Rémy’s presentation of
HM($X$) and give a translation from FreezeML programs to constraints
representing type inference problems (Section 3);

  * •

present a stack machine for solving the constraints (again inspired by Pottier
and Rémy’s) and show that it is correct, deterministic, and terminating
(Section 4);

  * •

discuss extensions (Section 5), related and future work (Section 6), and
conclude (Section 7).

##  2\. FreezeML

In this section we summarise the syntax and typing rules of FreezeML. (We omit
the dynamic semantics, given by elaboration into System F (Emrich et al.,
2020), as it is not relevant to the current paper.)

##### Lists as sets.

We write $\tilde{X}$ for a (possibly empty) set $\\{X_{1},\dots,X_{n}\\}$ and
$\overline{X}$ for a (possibly empty) sequence $X_{1},\dots,X_{n}$. We
overload comma for use as a union / concatenation operator for sets and
sequences, writing $\tilde{X},\tilde{Y}$ for the set
$\\{X_{1},\dots,X_{m},Y_{1},\dots,Y_{n}\\}$ where
$\tilde{X}=\\{X_{1},\dots,X_{m}\\}$ and $\tilde{Y}=\\{Y_{1},\dots,Y_{n}\\}$,
and writing $\overline{X},\overline{Y}$ for the sequence
$X_{1},\dots,X_{m},Y_{1},\dots,Y_{n}$ where $\overline{X}=X_{1},\dots,X_{m}$
and $\tilde{Y}=Y_{1},\dots,Y_{n}$. Given $\overline{X}$, we may write
$\tilde{X}$ for the set containing the same elements. We sometimes indicate
that sets or sequences are required to be disjoint using the $\mathop{\\#}$
relation, e.g. $\Delta\mathop{\\#}\Delta^{\prime}$ means that $\Delta$ and
$\Delta^{\prime}$ are disjoint.

##### Types.

The syntax of types, instantiations, and contexts is as follows.

$\begin{array}[t]{@{}l@{}r@{~}c@{~}l@{}}\textrm{Type Variables}&a,b,c~{}\\\
\textrm{Type
Constructors}&D~{}&::=\hfil~{}&\mathord{\to}\mid\times\mid\mathsf{Int}\mid\dots\\\
\textrm{Types}&A,B~{}&::=\hfil~{}&a\mid D\,\overline{A}\mid\forall a.A\\\
\textrm{Monotypes}&S,T~{}&::=\hfil~{}&a\mid D\,\overline{S}\\\ \textrm{Guarded
Types}&G,H~{}&::=\hfil~{}&a\mid D\,\overline{A}\\\ \textrm{Type
Instantiation}&\delta~{}&::=\hfil~{}&\emptyset\mid\delta[a\mapsto A]\\\
\textrm{Type Contexts}&\Delta,\Xi~{}&::=\hfil~{}&\cdot\mid\Delta,a\\\
\textrm{Term Contexts}&\Gamma~{}&::=\hfil~{}&\cdot\mid\Gamma,x:A\\\
\end{array}$

Types are assembled from type variables ($a,b,c$) and type constructors ($D$).
Type constructors include at least functions ($\to$), products ($\times$), and
base types. FreezeML uses System F types ($A,B$), and the only syntactic form
for expressing type polymorphism is $\forall a.A$. A type is either a type
variable ($a$), a data types ($D\,\overline{A}$) with type constructor $D$ and
type arguments $\overline{A}$, or a polymorphic type $(\forall a.A$) that
binds type variable $a$ in type $A$. We consider types equal modulo alpha-
renaming, but not up to reordering of quantifiers or the addition/removal of
superfluous (i.e., unused) quantified variables. For example, the following
types are all different: $\forall a.\forall b.a\to b$, $\forall b.\forall
a.a\to b$, $\forall a.\forall b.\forall c.a\to b$. Monotypes ($S,T$) disallow
any polymorphism. Guarded types ($G,H$) disallow polymorphism at the top-
level. A type instantiation ($\delta$) maps type variables to types. Unlike
traditional presentations of ML, we explicitly track type variables in a type
context ($\Delta$). By convention we reserve $\Xi$ for flexible type contexts
which we will not need until we treat constraints in Section 3. Term contexts
($\Gamma$) ascribe types to term variables. Contexts are unordered and
duplicates are disallowed. As such, we will frequently take advantage of the
fact that a type context $\Delta$ is a set of type variables $\tilde{a}$ and
use both notations interchangeably. This means that we impose the same
disjointness conditions when writing $\Delta,\Delta^{\prime}$.

##### Typing judgements.

FreezeML typing judgements have the form $\Delta;\Gamma\vdash M:A$, stating
that term $M$ has type $A$ in type context $\Delta$ and term context $\Gamma$.
We assume standard well-formedness judgements for types and term contexts:
$\Delta\vdash A\ \mathbf{ok}$ and $\Delta\vdash\Gamma\ \mathbf{ok}$, which
state that only type variables in $\Delta$ can appear in $A$ and $\Gamma$
respectively. Moreover, the term well-formedness judgement
$\Delta;\Gamma\vdash M\ \mathbf{ok}$ states that all free term variables of
$M$ appear in $\Gamma$ and type annotations are well-formed. This judgement
also implements the scoping rules of FreezeML, where certain let bindings
bring type variables in scope such that they become available in type
annotations (Emrich et al., 2020). The scoping behaviour interacts with the
value restriction adopted by FreezeML, we therefore introduce
$\Delta;\Gamma\vdash M\ \mathbf{ok}$ formally when discussing let bindings
later in this section.

The typing rules are given in Fig. 1. As usual, in these rules we implicitly
assume that types and term contexts are well-formed with respect to the type
context and that the term is well-formed with respect to the type and term
context (i.e., $\Delta;\Gamma\vdash M\ \mathbf{ok}$). In the following running
examples, we assume that the function $\mathsf{id}$ is in scope and has type
$\forall a.a\to a$.

$\boxed{\Delta;\Gamma\vdash M:A}$

*[Lab=VarFrozen] x : A ∈Γ Δ; Γ ⊢⌈x⌉ : A

*[Lab=VarPlain] x : ∀¯a.H ∈Γ
Δ⊢δ: ~a ⇒_⋆⋅ Δ; Γ ⊢x : δ(H)

*[Lab=App] Δ; Γ ⊢M : A →B
Δ; Γ ⊢N : A Δ; Γ ⊢M N : B

*[Lab=LamPlain] Δ; (Γ, x : S) ⊢M : B Δ; Γ ⊢λx.M : S →B

*[Lab=LamAnn] Δ; (Γ, x : A) ⊢M : B Δ; Γ ⊢λ(x : A).M : A →B

*[Lab=LetPlain] ¯a = ftv(A’) - Δ

(Δ, ¯a, M, A’) ⇕A
(Δ, ~a); Γ⊢M : A’
Δ; (Γ, x : A) ⊢N : B
principal(Δ, Γ, M, ~a, A’) Δ; Γ ⊢let x = M in N : B

*[Lab=LetAnn] (~a, A’) = split(A, M)
(Δ, ~a); Γ ⊢M : A’
Δ; (Γ, x : A) ⊢N : B Δ; Γ ⊢let (x : A) = M in N : B

Figure 1. FreezeML Typing Rules.

##### Variables and instantiation.

A frozen variable ($\lceil{x}\rceil$) can only have the exact type as given by
the term environment $\Gamma$ (rule VarFrozen). This means meaning that the
_only_ type of $\lceil{\mathsf{id}}\rceil$ is $\forall a.a\to a$. In contrast,
plain variables ($x$) can be instantiated, as in algorithmic presentations of
ML (rule VarPlain). In fact, plain variables are the only terms in FreezeML
that eliminate polymorphic types. This means that if we have
$\Gamma(x)=\forall\overline{a}.H$, then the possible types of $x$ are all
results of instantiating all $\overline{a}$ in $H$, using arbitrarily
polymorphic types. Potential nested quantifiers inside $H$ are not
instantiated, however. As a result, for any well-formed $B$, the type $B\to B$
is a possible type of $\mathsf{id}$, whereas $\forall a.a\to a$ is not.

Formally, the VarPlain typing rule relies on an _instantiation_ $\delta$. Each
instantiation is parameterised by a _restriction_ 111Emrich et al. (2020)
called these _kinds_ , but we prefer to avoid potential confusion with other
uses of this overloaded term. $R$ which can be either monomorphic
(${\mathord{\bullet}}$) or polymorphic ($\star$), indicating whether type
variables may be substituted with monotypes or arbitrary types. The
instantiation judgement
$\Delta\vdash\delta:\Delta^{\prime}\Rightarrow_{R}\Delta^{\prime\prime}$
states that instantiation $\delta$ instantiates type variables in
$\Delta^{\prime}$ with types subject to restriction $R$ using the type context
$\Delta,\Delta^{\prime\prime}$. Variables in $\Delta$ are considered to be
mapped to themselves. This means that if $R$ is $\star$, then for all
$a\in\Delta^{\prime}$, $\delta(a)$ must be a well-formed type in context
$\Delta,\Delta^{\prime\prime}$, which may therefore be arbitrarily
polymorphic. Otherwise, if $R$ is ${\mathord{\bullet}}$, then each such
$\delta(a)$ must be a monomorphic type. Note that due to all variables
$b\in\Delta$ being mapped to themselves, $\delta(b)$ is always a (monomorphic)
well-formed type in context $\Delta,\Delta^{\prime\prime}$ for all such $b$.

Intuitively, the variables in $\Delta$ correspond to those appearing in the
surrounding context, whereas $\Delta^{\prime}$ corresponds to variables being
instantiated and $\Delta^{\prime\prime}$ contains new type variables appearing
in the instantiation. In VarPlain, the $\Delta^{\prime\prime}$ environment is
empty, but in the $\mathsf{principal}$ operation discussed below,
$\Delta^{\prime\prime}$ need not be empty. In order for this interpretation to
make sense the judgement has an implicit precondition that
$\Delta^{\prime}\\#\Delta$ and $\Delta^{\prime\prime}\\#\Delta$. It is defined
as follows.

$\boxed{\Delta\vdash\delta:\Delta^{\prime}\Rightarrow_{R}\Delta^{\prime\prime}}$
Δ⊢∅: ⋅⇒_R Δ’

Δ⊢δ: Δ’ ⇒_R Δ”
Δ, Δ” ⊢_R A ok Δ⊢δ[a ↦A] : (Δ’, a) ⇒_R Δ” We write $\Delta\vdash_{R}A\
\mathbf{ok}$ for the well-formedness judgement for types. It is standard
except for the presence of $R$; if $R$ is ${\mathord{\bullet}}$ then
$\Delta\vdash_{\mathord{\bullet}}A$ only holds if $A$ is a monotype $S$. In
other words, the judgement enforces the restriction $R$, where any well-formed
type satisfies the restriction $\star$. Therefore, the well-formedness
judgement $\Delta\vdash A\ \mathbf{ok}$ introduced earlier is a shorthand for
$\Delta\vdash_{\star}A\ \mathbf{ok}$.

##### Functions.

Function applications ($M\,N$) are standard and oblivious to polymorphism. The
parameter type $A$ of the function $M$ must exactly match that of the argument
$N$, where $A$ may be arbitrarily polymorphic. In particular,
$\lceil{id}\rceil\>3$ is ill-typed because $\lceil{id}\rceil$’s type $\forall
a.a\to a$ is not a function type. Conversely,
$\mathsf{id}\>\lceil{\mathsf{id}}\rceil$ has type $\forall b.b\to b$. The
first occurrence of $\mathsf{id}$ is instantiated, by picking the type
$\forall b.b\to b$ of $\lceil{\mathsf{id}}\rceil$ for the quantified type
variable. This showcases the impredicative nature of FreezeML, with alpha-
renaming performed for the sake of clarity.

Plain (i.e., unannotated) lambda abstractions ($\lambda x.M$) restrict the
domain to be monomorphic. This is a simple way to keep type inference
tractable, in line with other systems (Leijen, 2008; Serrano et al., 2018).
Annotated lambda abstractions ($\lambda(x:A).M$) allow the domain to be
polymorphic, at the cost of a type annotation. As a result, the example term
$\lambda f.f\>f$ given in the introduction is rejected in FreezeML, unless $f$
is annotated with an appropriate type. Writing $\lambda(f:\forall a.a\to
a).f\>f$ yields a function of type $(\forall a.a\to a)\to(B\to B)$ for any
well-formed $B$. The return types of both forms of lambda abstractions may be
arbitrarily polymorphic: both $\lambda(f:\forall a.a\to a).f\>\lceil{f}\rceil$
and $\lambda x.\lceil{\mathsf{id}}\rceil$ yield functions with polymorphic
return types.

##### Principality

The LetPlain rule has a _principality_ side condition that requires that the
type inferred for $x$ is a principal one. Terms cannot arbitrarily be
generalised in FreezeML while retaining typability. The term $\mathsf{id}$ has
type $A\to A$ for any type $A$, and in particular $a\to a$ for any type
variable $a$. However, it does not have type $\forall a.a\to a$. As in System
F, there is no direct relationship between the types $\forall a.a\to a$ and
$A\to A$ in FreezeML; generalisation only happens when a let-bound generalised
value is encountered, and instantiation only happens if triggered by a plain
variable occurrence.

The fact that FreezeML typing judgements carry type contexts specifying all
in-scope type variables makes it possible to characterise principal types
without universally quantifying additional type variables. Principal types are
always given in their context $\Delta;\Gamma$ and may use free type variables
not present in $\Delta$. For example, the principal types of term
$\mathsf{id}$ in the context $\Delta;\Gamma$ are exactly the types $b\to b$
for any $b\not\in\Delta$. This presentation is syntax-directed, in contrast to
declarative presentations of ML that allow generalisation at any point, and
would typically refer to the _type scheme_ $\forall a.a\to a$ (not to be
confused with the corresponding System F type) as the principal type of
$\mathsf{id}$.

We formalise the notion of principal type using the predicate
$\mathsf{principal}(\Delta,\Gamma,M,\Delta^{\prime},A^{\prime})$. It first
asserts that $A^{\prime}$ is a possible type of $M$ in the context
$\Delta,\Delta^{\prime};\Gamma$, where $\Delta^{\prime}$ includes all type
variables of $A^{\prime}$ not in $\Delta$. A minimality condition must also be
satisfied: any other possible type of $M$ can be obtained by instantiating the
variables in $\Delta^{\prime}$, possibly using some new type variables in
context $\Delta^{\prime\prime}$, but (crucially) _not_ instantiating any of
those in $\Delta$. Formally, a _principal type_ of $M$ in the context of
$\Delta$ and $\Gamma$ is any pair $(\Delta^{\prime},A^{\prime})$ such that
$\mathsf{principal}(\Delta,\Gamma,M,\Delta^{\prime},A^{\prime})$ holds. This
is unique up to safe renaming of the variables in $\Delta^{\prime}$ (that is,
avoiding already-known variables in $\Delta$) and the occurrence of
superfluous variables in $\Delta^{\prime}$ (i.e. variables not actually
occuring in $A^{\prime}$).222We could impose minimality of $\Delta^{\prime}$
and $\Delta^{\prime\prime}$ in the definition of $\mathsf{principal}$, but any
superfluous variables in either context simply have no effect. Given a
particular $A^{\prime}$ we can recover $\Delta^{\prime}$, so we say _the_
principal type to refer to a particular $A^{\prime}$ when $\Delta^{\prime}$ is
clear from context. principal(Δ, Γ, M, Δ’, A’) =Δ, Δ’; Γ⊢M : A’  and (for all
Δ”, A” ∣if  Δ, Δ”; Γ⊢M : A”then there exists  δ such that Δ⊢δ: Δ’ ⇒_⋆Δ”  and
δ(A’) = A” )

###### Remark 1 (Abuse of notation).

Notice that the definition of $\mathsf{principal}$ refers to typing
derivations in the “if” part of the condition. The reader may be concerned
about whether the typing judgement is well-defined given that it appears in a
negative position in the definition of $\mathsf{principal}$. As Emrich et al.
(2020) explain we can see that the definition is nevertheless well founded by
indexing by untyped terms or the height of derivation trees. Likewise, proofs
involving typing derivations are typically by induction on $M$ rather than by
rule induction. Although it is a slight abuse of notation, we prefer to
present the typing rules using inference rule notation for ease of comparison
with other systems. Formally however the rules in Figure 1 are implications
that happen to hold of the typing relation, not an inductive definition of it.
We refer to the extended version of Emrich et al. (2020) for the precise
definition.

##### Plain let bindings.

Following ML, FreezeML adopts a syntactic value restriction (Wright, 1995),
distinguishing two subcategories of terms.

$\begin{array}[t]{@{}l@{}r@{~}c@{~}l@{}}\textrm{Values}&\mathsf{Val}\ni
V,W~{}&::=\hfil~{}&\lceil{x}\rceil\mid x\mid\lambda
x.M\mid\lambda(x:A).M\mid{\rm{\bf let}}\;x=V\;{\rm{\bf in}}\;W\mid{\rm{\bf
let}}\;(x:A)=V\;{\rm{\bf in}}\;W\\\ \textrm{Guarded Values}&\mathsf{GVal}\ni
U~{}&::=\hfil~{}&\phantom{\lceil{x}\rceil\mid\;}x\mid\lambda
x.M\mid\lambda(x:A).M\mid{\rm{\bf let}}\;x=V\;{\rm{\bf in}}\;U\mid{\rm{\bf
let}}\;(x:A)=V\;{\rm{\bf in}}\;U\end{array}$

Values disallow applications. Guarded values disallow frozen variables, and
thus must have guarded type.333The only guarded value with a top-level
polymorphic type is a plain variable $x$ of type $\forall
a_{1},\dotsc,a_{n}.a_{i}$. This special case is handled gracefully by
FreezeML.

Plain let bindings (${\rm{\bf let}}\;x=M\;{\rm{\bf in}}\;N$) generalise –
subject to the value restriction – the principal type $A^{\prime}$ of $M$ and
ascribe it to $x$. Here, the predicate $\mathsf{principal}$ is used to
determine the type $A^{\prime}$, using fresh variables $\overline{a}$. Note
that the free type variable operator $\mathsf{ftv}$ returns a sequence rather
than a set when applied to a type, returning variables in the order of their
appearance. This reflects the fact that the order of quantifiers matters in
FreezeML.

If $M$ is a guarded value, the type $A$ of $x$ is then
$\forall\overline{a}.A^{\prime}$, performing the actual generalisation step.
This is achieved using the $\Updownarrow$ auxiliary judgement that enforces
the value restriction, which we return to shortly.

Generalising the principal type $A^{\prime}$ rather than an arbitrary type of
$M$ is necessary to ensure the existence of principal types in the overall
system (Emrich et al., 2020). First, recall that a principal type of an
expression $M$ with respect to $\Delta$ and $\Gamma$ is formally a _pair_
$(\Delta^{\prime},A^{\prime})$ such that
$\mathsf{principal}(\Delta,\Gamma,M,\Delta^{\prime},A^{\prime})$ hold.
Generalisation then quantifies the variables in $\Delta^{\prime}$ yielding a
type $\forall a_{1},\ldots,a_{n}.A$ where $a_{1},\ldots,a_{n}$ are in the
order in which the variables first appear in $A^{\prime}$. Now consider the
term

${\rm{\bf let}}\;f=\lambda x.x\;{\rm{\bf in}}\;\lceil{f}\rceil$

which is an example of FreezeML’s “explicit generalisation” operation
$\$V\equiv{\rm{\bf let}}\;f=V\;{\rm{\bf in}}\;\lceil{f}\rceil$ and allows
capturing the generalised principal type of a value. The principal type of
$\lambda x.x$ is $a\to a$ (provided $a\not\in\Delta$), and by generalising
this we obtain $\forall a.a\to a$ as the type of $f$, which then becomes the
type of the overall let term due to $f$ being frozen in its body. Note that
the type $\forall a.a\to a$ is _not_ the principal type of $\lambda x.x$
(formally: no pair $(\Delta^{\prime\prime},\forall a.a\to a)$ is a principal
type). If the typing rule permitted assigning other, non-principal, types to
$\lambda x.x$, such as $\mathsf{Int}\to\mathsf{Int}$, then generalisation
would have no effect. This would make $\mathsf{Int}\to\mathsf{Int}$ another
possible type of the overall let term (as freezing a variable with a guarded
or monomorphic type has no effect). However, this would mean that the overall
let term has no principal type. The two types $\mathsf{Int}\to\mathsf{Int}$
and $\forall a.a\to a$ don’t have a shared more general type in FreezeML, as
discussed earlier.

As mentioned before, the auxiliary judgement
$(\Delta,\overline{a},M,A^{\prime})\Updownarrow A$ enforces the value
restriction. Given $\Delta,\tilde{a}\vdash M:A^{\prime}$, the judgement
determines $A$ to be $\forall\overline{a}.A^{\prime}$ if $M$ is a guarded
value. Otherwise, $A$ is obtained from $A^{\prime}$ by instantiating all of
$\tilde{a}$ with _monotypes_.

$\boxed{(\Delta,\overline{a},M,A^{\prime})\Updownarrow A}$ M ∈GVal (Δ, ¯a, M,
A’) ⇕∀¯a. A’

Δ’ = ~a
Δ⊢δ: Δ’ ⇒_∙⋅
M ／∈GVal (Δ, ¯a, M, A’) ⇕δ(A’)

As is well-known, type inference for System F is undecidable, even with
nontrivial restrictions (Pfenning, 1993; Wells, 1994). The condition to
instantiate monomorphically is one of several design choices in FreezeML’s to
keep type inference decidable and tractable. Along with the monomorphic
restriction on the arguments to plain lambda abstractions, FreezeML ensures
that polymorphism can only ever appear in the term context if it was written
explicitly by a programmer in a type annotation or inferred as a principal
type of a plain let binding.

##### Annotated let bindings.

Annotated let bindings (${\rm{\bf let}}\;(x:A)=M\;{\rm{\bf in}}\;N$) also
generalise, subject to the value restriction, but ascribe the type $A$ to $x$.
The splitting operation $\mathsf{split}(A,M)$ enforces the value restriction
for annotated let terms. It decomposes $A$ into a collection of top-level
quantifiers and another type. The first component of the returned pair is
maximal if $M$ is a guarded value and empty otherwise due to the value
restriction. split(∀¯a.H, M) = {(~a, H)if
$M\in\mathsf{GVal}$(⋅,∀¯a.H)otherwise It is also important to note that in the
generalising case (i.e. when the let-bound expression is a guarded value $U$),
the top-level quantifiers in type annotations are in scope and can be used in
$U$ (e.g. in other type annotations). This is reflected in the
$\mathsf{split}$ operation which returns these variables in its first
argument. In contrast, in the non-generalising case where $M$ is not a guarded
value, these variables are not in scope in $M$. Since $M$’s type is not being
generalised, the only way it can end up with a polymorphic type is by
referencing (frozen) variables with polymorphic types.

Note that this scoping behaviour also needs to be reflected in the term well-
formedness judgement $\Delta;\Gamma\vdash M\ \mathbf{ok}$ mentioned earlier.
To this end, the well-formedness rule for annotated let bindings also uses the
$\mathsf{split}$ operation, as shown in Figure 2. The judgement
$\Delta;\Gamma\vdash M\ \mathbf{ok}$ only requires the presence of a binding
for all free term variables, but ignores the associated types. As a result,
the rules for unannotated lambda functions and let bindings add arbitrary
types $A$ to the the term context.

$\boxed{\Delta;\Gamma\vdash M\ \mathbf{ok}}$ x ∈Γ Δ;Γ⊢⌈x⌉ ok

x ∈Γ Δ;Γ⊢x ok

Δ;(Γ, x : A) ⊢M ok Δ;Γ⊢λx.M ok

Δ⊢A ok

Δ;(Γ, x : A) ⊢M ok Δ;Γ⊢λ(x : A).M ok

Δ;Γ⊢M ok

Δ;Γ⊢N ok Δ;Γ⊢M N ok

Δ;Γ⊢M ok
Δ;(Γ, x : A) ⊢N ok Δ;Γ⊢let x = M in N ok

Δ⊢A ok
(Δ’, A’) = split(A, M)
(Δ, Δ’);Γ⊢M ok
Δ;(Γ, x :A) ⊢N ok Δ;Γ⊢let (x : A) = M in N ok

Figure 2. Well-formedness of terms.

##  3\. Constraint language

In this section, we present the constraint language and a function for
generating typing constraints from terms. Following Pottier and Rémy (2005),
our constraint language uses both term variables and type variables. Following
Emrich et al. (2020), we distinguish rigid and flexible type variables. The
former arise in the object language from universal quantification. The latter
are used to represent unknown types.

The syntax and satisfiability judgement for constraints is given in Figure 3.
The judgement $\Delta;\Xi;\Gamma;\delta\vdash C$ states that in rigid type
context $\Delta$, flexible type context $\Xi$, term context $\Gamma$, using
instantiation $\delta$, the constraint $C$ is satisfied. Note that rigid and
flexible type contexts follow the same grammar, but we use the convention that
$\Delta$ is used for rigid variables, whereas $\Xi$ contains flexible ones.
Therefore, using both environments in the judgement allows us to distinguish
the flexible variables in scope from those that are rigid. In the judgement
$\Delta;\Xi;\Gamma;\delta\vdash C$ we implicitly assume that the term
environment $\Gamma$ is well-formed and contains no flexible variables
($\Delta\vdash\Gamma\ \mathbf{ok}$) and that type instantiations close over
the flexible type variables
($\Delta\vdash\delta:\Xi\Rightarrow_{\star}\cdot$).

To support composition of constraints we start with the always true constraint
($\mathsf{true}$) and conjunction ($C_{1}\wedge C_{2}$). The equality
constraint $A\sim B$ asserts that $A$ and $B$ are equivalent. The frozen
constraint $\lceil{x:A}\rceil$ asserts that $x$ has type $A$. The instance
constraint $x\preceq A$ asserts that top-level quantifiers of $x$’s type can
be instantiated to yield $A$. The universal constraint $\forall a.C$ binds
rigid type variable $a$ in $C$. The existential constraint $\exists a.C$ binds
flexible type variable $a$ in $C$. Monomorphism constraints
$\mathsf{mono}{}(a)$ assert that the flexible variable $a$ must only be
instantiated with monotypes. The definition constraint ${\rm{\bf
def}}\;(x:A)\;{\rm{\bf in}}\;C$ binds term variable $x$ in $C$. (It also
includes a side-constraint which we will return to shortly.) The polymorphic
let constraint ${\rm{\bf let}}_{\star}\;x=\sqcap a.C_{1}\;{\rm{\bf
in}}\;C_{2}$ and monomorphic let constraint ${\rm{\bf
let}}_{\mathord{\bullet}}\;x=\sqcap a.C_{1}\;{\rm{\bf in}}\;C_{2}$ are used to
bind $x$ in $C_{2}$, subject to the restrictions imposed on $a$ in $C_{1}$.
The two forms differ in how the type of $x$ is obtained from solving $C_{1}$
for $a$: either by generalisation $(\star)$ or monomorphic instantiation
$({\mathord{\bullet}}$). These constraints are somewhat involved, so we defer
a full explanation until we present the constraint-generation function.

We consider constraints equivalent modulo alpha-renaming of all binders, of
both type and term variables.

$\begin{array}[t]{@{}l@{}}\begin{array}[t]{@{}l@{\quad}r@{~}c@{~}l@{}}&C~{}&::=\hfil~{}&\mathsf{true}\mid
C\wedge C\mid A\sim B\mid\lceil{x:A}\rceil\mid x\preceq A\mid\forall
a.C\mid\exists a.C\mid\mathsf{mono}{}(a)\\\ &~{}&\mid\hfil~{}&{\rm{\bf
def}}\;(x:A)\;{\rm{\bf in}}\;C\mid{\rm{\bf let}}_{\star}\;x=\sqcap
a.C\;{\rm{\bf in}}\;C\mid{\rm{\bf let}}_{\mathord{\bullet}}\;x=\sqcap
a.C\;{\rm{\bf in}}\;C\\\ \end{array}\\\ \end{array}$

[Sem-True] Δ; Ξ; Γ; δ⊢true

[Sem-And] Δ; Ξ; Γ; δ⊢C_1
Δ; Ξ; Γ; δ⊢C_2
Δ; Ξ; Γ; δ⊢C_1 ∧C_2

[Sem-Equiv] (Δ, Ξ) ⊢_⋆A ok
(Δ, Ξ) ⊢_⋆B ok

δ(A) = δ(B) Δ; Ξ; Γ; δ⊢A ∼B
[Sem-Freeze] Γ(x) = δ(A) Δ; Ξ; Γ; δ⊢⌈x : A⌉

[Sem-Instance] Δ’ = ~a
Δ⊢δ’ : Δ’ ⇒_⋆⋅

Γ(x) = ∀¯a.H
δ’(H) = δ(A) Δ; Ξ; Γ; δ⊢x ⪯A
[Sem-Forall] (Δ, a); Ξ; Γ; δ⊢C Δ; Ξ; Γ; δ⊢∀a.C

[Sem-Exists] Δ; (Ξ, a ); Γ; δ[a ↦A] ⊢C Δ; Ξ; Γ; δ⊢∃a.C
[Sem-Mono] Δ⊢_∙δ(a) ok Δ; Ξ; Γ; δ⊢mono(a)

[Sem-Def] for all  a ∈ftv(A) - Δ ∣ Δ; Ξ; Γ; δ⊢mono(a)

Δ; Ξ; (Γ,x : δA); δ⊢C Δ; Ξ; Γ; δ⊢def (x : A) in C
[Sem-LetPoly] mostgen(Δ, (Ξ, a), Γ, C_1, Δ_m, δ_m)

Δ_o = ftv(δ_m(Ξ)) - Δ
¯b = ftv(δ_m(a)) - Δ, Δ_o

Δ⊢δ’ : Δ_o ⇒_∙⋅
A = δ’(δ_m(a))

(Δ, ~b); (Ξ, a); Γ; δ[a ↦A] ⊢C_1
Δ; Ξ; (Γ,x : ∀¯b. A); δ⊢C_2 Δ; Ξ; Γ; δ⊢let_⋆ x = ⊓a. C_1 in C_2

[Sem-LetMono] mostgen(Δ, (Ξ, a), Γ, C_1, Δ_m, δ_m)

Δ⊢δ’ : Δ_m ⇒_∙⋅
A = δ’(δ_m(a))

Δ; (Ξ, a); Γ; δ[a ↦A] ⊢C_1
Δ; Ξ; (Γ,x : A); δ⊢C_2 Δ; Ξ; Γ; δ⊢let_∙ x = ⊓a. C_1 in C_2

Figure 3. Satisfiability judgement for constraints.

###  3.1. Constraint generation

We now introduce the function $\llbracket M:A\rrbracket$, which translates a
term $M$ and type $A$ to a constraint. The only free type variables in the
resulting constraint are those appearing in $A$ and type annotations in $M$.
Assuming that $M$ is well-formed under $\Delta$ and $\Gamma$
($\Delta;\Gamma\vdash M\ \mathbf{ok}$) and that $A$ is well-formed under
$\Delta,\Xi$, the constraint $\llbracket M:A\rrbracket$ is well-formed under
$\Delta,\Xi$ and $\Gamma$ ($\Delta;\Xi;\Gamma\vdash\llbracket M:A\rrbracket\
\mathbf{ok}$). The latter judgement is given in Figure 4. Note that this
judgement ignores the types in $\Gamma$ and uses it to track bound term
variables, just like the well-formedness judgement on terms introduced in
Section 2.

Δ; Ξ; Γ⊢true ok

a ∈(Δ, Ξ) Δ; Ξ; Γ⊢mono(a) ok

Δ; Ξ; Γ⊢C_1 ok
Δ; Ξ; Γ⊢C_2 ok Δ; Ξ; Γ⊢C_1 ∧C_2 ok

Δ; (Ξ, a); Γ⊢C ok Δ; Ξ; Γ⊢∃a. C ok

(Δ, a); Ξ; Γ⊢C ok Δ; Ξ; Γ⊢∀a. C ok

(Δ, Ξ) ⊢A ok
(Δ, Ξ) ⊢B ok Δ; Ξ; Γ⊢A ∼B ok

x ∈Γ
(Δ, Ξ) ⊢A ok Δ; Ξ; Γ⊢x ⪯A ok

x ∈Γ
(Δ, Ξ) ⊢A ok Δ; Ξ; Γ⊢⌈x : A⌉ ok

(Δ, Ξ) ⊢A ok
Δ; Ξ; (Γ, x : A) ⊢C ok Δ; Ξ; Γ⊢def (x : A) in C ok

Δ; (Ξ, a); Γ⊢C_1 ok

Δ; Ξ; (Γ, x : A) ⊢C_2 ok Δ; Ξ; Γ⊢let_R x = ⊓a. C_1 in C_2 ok

Figure 4. Well-formedness of constraints.

If $\Xi$ is empty (i.e., $A$ contains no flexible variables) then this
constraint is satisfiable in context $\Delta;\Gamma$ if and only if $M$ has
type $A$ in context $\Delta;\Gamma$. However, if $A$ does contain flexible
variables, then the models of $\llbracket M:A\rrbracket$ are exactly those
that instantiate $A$ to valid types of $M$. We formalise these properties in
Section 3.4. Concretely, we perform type inference for $M$ by choosing $A$ to
be a single flexible variable.

$\begin{array}[]{@{}r@{~\;}c@{~\;}l@{}l@{}r@{}}\llbracket\lceil{x}\rceil:A\rrbracket~{}&=\hfil~{}&\lceil{x:A}\rceil&&\\\
\llbracket x:A\rrbracket~{}&=\hfil~{}&x\preceq A&&\\\ \llbracket
M\,N:A\rrbracket~{}&=\hfil~{}&\exists a_{1}.(\llbracket M:a_{1}\to
A\rrbracket\wedge\llbracket N:a_{1}\rrbracket)&&\\\ \llbracket\lambda
x.M:A\rrbracket~{}&=\hfil~{}&\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)&\\\
\llbracket\lambda(x:B).M:A\rrbracket~{}&=\hfil~{}&\exists a_{1}.B\to a_{1}\sim
A\wedge{\rm{\bf def}}\;(x:B)\;{\rm{\bf in}}\;\llbracket N:a_{1}\rrbracket&\\\
\llbracket{\rm{\bf let}}\;(x:\forall\overline{a}.H)=U\;{\rm{\bf
in}}\;N:A\rrbracket~{}&=\hfil~{}&(\forall\overline{a}.\llbracket
U:H\rrbracket)\;\wedge\;{\rm{\bf def}}\;(x:\forall\overline{a}.H)\;{\rm{\bf
in}}\;\llbracket N:A\rrbracket&\\\ \llbracket{\rm{\bf let}}\;(x:B)=M\;{\rm{\bf
in}}\;N:A\rrbracket~{}&=\hfil~{}&\llbracket M:B\rrbracket\;\wedge\;{\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;\llbracket N:A\rrbracket&\;\text{(if
$M\not\in\mathsf{GVal}$)}&\\\ \llbracket{\rm{\bf let}}\;x=U\;{\rm{\bf
in}}\;N:A\rrbracket~{}&=\hfil~{}&{\rm{\bf let}}_{\star}\;x=\sqcap a.\llbracket
U:a\rrbracket\;{\rm{\bf in}}\;\llbracket N:A\rrbracket&&\\\ \llbracket{\rm{\bf
let}}\;x=M\;{\rm{\bf in}}\;N:A\rrbracket~{}&=\hfil~{}&{\rm{\bf
let}}_{\mathord{\bullet}}\;x=\sqcap a.\llbracket M:a\rrbracket\;{\rm{\bf
in}}\;\llbracket N:A\rrbracket&\;\text{(if $M\not\in\mathsf{GVal}$)}&\\\
\end{array}$ Figure 5. Translation from terms to constraints.

The function $\llbracket-\rrbracket$ is defined in Figure 5.

Frozen variables and plain variables generate the corresponding atomic
constraints. An application generates an existential constraint that binds a
fresh flexible type variable for the argument type. A plain lambda abstraction
generates a constraint that binds fresh flexible type variables for argument
and return types and uses a definition constraint to bind the argument in the
constraints generated for the body of the lambda abstraction. An annotated
lambda abstraction generates a similar constraint to a plain lambda
abstraction, but the argument type is fixed by the type annotation. The
remaining four cases of $\llbracket-\rrbracket$ account for the four different
combinations arising from the two choices between plain or annotated and
between guarded value or not. An annotated let binding ${\rm{\bf
let}}\;(x:B)=M\;{\rm{\bf in}}\;N$ generates a conjunction of constraints: one
for $M$ and the other for $N$. Following the definition of $\mathsf{split}$ in
the LetAnn rule in Figure 1, if $M$ is a guarded value $U$ then its type can
be generalised to obtain $B$ as witnessed by the universal constraints. Notice
in particular that the quantified type variables introduced in the annotation
are in scope in $U$ in the sub-constraint $\forall\overline{a}.\llbracket
U:H\rrbracket$. Otherwise the types must match on the nose without any
generalisation, and in this case the quantified variables are not in scope in
$M$.

###  3.2. Def constraints

The side condition in the Sem-Def rule ensures that the argument type can only
be instantiated with a monomorphic type. In general, the side condition
preserves the invariant that no undetermined (or “guessed”) polymorphism
exists in the term context $\Gamma$. This is crucial to ensure the existence
of most general solutions for our constraint language. Consider the constraint
${\rm{\bf def}}\;(x:a)\;{\rm{\bf in}}\;x\preceq b\wedge c\sim(a\to b)$ with
free flexible variables $a,b,c$. Without the extra condition on def
constraints, different solutions could for instance include
$c\mapsto(\mathsf{Int}\to\mathsf{Int})$ or $c\mapsto((\forall
a.a)\to\mathsf{Int})$ for $c$. However, there is no more general solution
subsuming both. Note that the monomorphism condition on def constraints does
not impose the type annotation to be monomorphic itself, it only imposes
conditions on free flexible variables appearing within it. Consequently, the
constraint ${\rm{\bf def}}\;(x:(\forall a.a)\to b)\;{\rm{\bf
in}}\;\mathsf{true}$ is satisfiable as long as the flexible variable $b$ is
instantiated monomorphically. We cannot avoid the monomorphism condition
imposed on def constraints simply by using $\mathsf{mono}$ constraints. The
constraint $\mathsf{mono}(b){}\wedge{\rm{\bf def}}\;f(x:(\forall a.a)\to
b)\;{\rm{\bf in}}\;\mathsf{true}$ would be equivalent to the previous one in
terms of its solutions, even if we dropped the monomorphism condition built
into def constraints. However, this system would exhibit the same lack of most
general solutions for def constraints discussed earlier, showing that the
monomorphism condition needs to be imposed on def constraints directly.

###  3.3. Let constraints

Plain let bindings are translated to let constraints. A plain let binding of a
guarded value ${\rm{\bf let}}\;x=U\;{\rm{\bf in}}\;N$ generates a polymorphic
let constraint. In general, such a polymorphic let constraint ${\rm{\bf
let}}_{\star}\;x=\sqcap a.C_{1}\;{\rm{\bf in}}\;C_{2}$ binds the flexible
variable $a$ in $C_{1}$, much like an existential constraint. The type
assigned to $x$ in $C_{2}$ is then obtained by generalising type variables
appearing in the solution for $a$.

We make several observations motivating the overall semantics of let
constraints.

##### Need to generalise principal solution.

We first observe that let _constraints_ require a principality condition
similar to the one imposed on plain let _terms_. Consider the constraint $C$
defined as ${\rm{\bf let}}\;x=\sqcap a.\exists b.a\sim(b\to b)\;{\rm{\bf
in}}\;\lceil{x:c}\rceil$, appearing in a rigid context $\Delta$. It has a
single free type variable $c$ and we refer to its first subconstraint (i.e.,
$\exists b.a\sim(b\to b)$) as $C_{1}$ in the following. Allowing arbitrary
solutions for $a$ in $C_{1}$ to be generalised to yield the type for $x$ would
lead to the following pathological situation.

For any well-formed type $A$, $[a\mapsto(A\to A)]$ is a model of $C_{1}$. As
usual, we must not generalise any type variables already bound in the
surrounding scope, namely those variables in $\Delta$. However, we may
generalise fresh variables appearing in $A$. This means that if we choose
$[a\mapsto(\mathsf{Int}\to\mathsf{Int})]$ there is nothing to generalise and
we have $x:(\mathsf{Int}\to\mathsf{Int})$ in $C_{2}$ , whereas
$[a\mapsto(b^{\prime}\to b^{\prime})]$ for some fresh $b^{\prime}$ does allow
us to generalise, meaning that we have $x:(\forall b^{\prime}.b^{\prime}\to
b^{\prime})$ in $C_{2}$. Any solution of the overall constraint must use the
type of $x$ for $c$. This leads to a problem very similar to the one discussed
for let terms in Section 2: the two solutions
$[c\mapsto(\mathsf{Int}\to\mathsf{Int})]$ and $[c\mapsto(\forall
b^{\prime}.b^{\prime}\to b^{\prime})]$ of $C$ would have no shared most
general solution in our system.

We avoid this problem by demanding that only the most general solution for $a$
in $C_{1}$ must be generalised to yield the type for $x$ in $C_{2}$. In our
example, this means choosing $[a\mapsto(b^{\prime}\to b^{\prime})]$, where
$b^{\prime}$ is fresh, which means that in our example only $[c\mapsto(\forall
b^{\prime}.b^{\prime}\to b^{\prime})]$ is a valid solution of the overall let
constraint.

The rule Sem-LetPoly in Figure 3 enforces this using the premise
$\mathsf{mostgen}(\Delta,(\Xi,a),\Gamma,C_{1},\Delta_{\mathrm{m}},\delta_{\mathrm{m}})$,
which asserts that $\delta_{\mathrm{m}}$ is the most general model of $C_{1}$
in the context $\Delta;\Xi;\Gamma$. Here, $\Delta_{\mathrm{m}}$ contains fresh
variables that are used in place of flexible type variables for which no
further substitution/solution is currently known. Note that this premise (and
subsequently, $\delta_{\mathrm{m}}$) is independent from the ambient
instantiation $\delta$; the latter does not appear as an argument. The
predicate $\mathsf{mostgen}$ is defined as follows, stating that
$\delta_{\mathrm{m}}$ is a model of $C_{1}$ and every other one can be
obtained by refining $\delta_{\mathrm{m}}$ by composition.

$\begin{array}[t]{@{}l@{}}\mathsf{mostgen}(\Delta,\Xi,\Gamma,C,\Delta_{\mathrm{m}},\delta_{\mathrm{m}})=\\\
\qquad(\Delta,\Delta_{\mathrm{m}});\Xi;\Gamma;\delta_{\mathrm{m}}\vdash
C\;\text{ and }\\\ \qquad\begin{array}[t]{@{}l@{}}(\text{for all
}\Delta^{\prime\prime},\delta^{\prime\prime}\mid\begin{array}[t]{@{}l@{}}\text{if
}(\Delta,\Delta^{\prime\prime});\Xi;\Gamma;\delta^{\prime\prime}\vdash C\\\
\text{then there exists }\delta^{\prime}\text{ such that }\\\
\;\Delta\vdash\delta^{\prime}:\Delta_{\mathrm{m}}\Rightarrow_{\star}\Delta^{\prime\prime}\text{
and }\delta^{\prime}\circ\delta_{\mathrm{m}}=\delta^{\prime\prime})\\\
\end{array}\\\ \end{array}\end{array}$

The rule Sem-LetPoly then defines two subsets444In general,
$\Delta_{\mathrm{m}}$ may contain useless variables not appearing in the
codomain of $\delta_{\mathrm{m}}$. Otherwise, if all variables in
$\Delta_{\mathrm{m}}$ appear in the range of $\delta_{\mathrm{m}}$, then
$\Delta_{\mathrm{m}}$ and $\overline{b}$ denote a partitioning of
$\Delta_{\mathrm{m}}$.  of $\Delta_{\mathrm{m}}$: The variables in
$\Delta_{\mathrm{o}}$ are those appearing in the range of
$\delta_{\mathrm{m}}$ restricted to $\Xi$ (i.e., not considering the mapping
for $a$ in $\delta_{\mathrm{m}}$). This means that the variables in
$\Delta_{\mathrm{o}}$ are related to the _outer_ context, namely by being part
of the instantiations of the variables $\Xi$ in the surrounding scope.

The rule then determines the variables $\overline{b}$ to be generalised as the
flexible ones appearing freely in $\delta_{\mathrm{m}}(a)$ (i.e., the most
general solution for $a$) and disregarding the variables from
$\Delta_{\mathrm{o}}$, as the latter variables are related to the outer scope
$\Xi$.

##### Safe interaction with outer scope

We have discussed that the rule Sem-LetPoly forces solutions for constraints
of the form ${\rm{\bf let}}_{\star}\;x=\sqcap a.C_{1}\;{\rm{\bf in}}\;C_{2}$
to use the most general solution for $a$ in $C_{1}$ – using fresh rigid
variables $\Delta_{\mathrm{m}}$ – and quantifying over variables
$\overline{b}\subseteq\Delta_{\mathrm{m}}$ to obtain the type for $x$ in
$C_{2}$.

We now show how flexible variables from the outer scope that appear in $C_{1}$
may influence the type of $x$ and how we prevent this from introducing
undetermined polymorphism in the term context. Consider the constraint
$\exists a.{\rm{\bf let}}_{\star}\;x=\sqcap b.a\sim b\;{\rm{\bf in}}\;C_{2}$
appearing in rigid context $\Delta$. The semantics of $\exists$ constraints
(cf. Sem-Exists in Figure 3) necessitates choosing a type $B$ for $a$ such
that $\Delta\vdash B\ \mathbf{ok}$. The first subconstraint of the let
constraint then equates $a$ and $b$, making any kind of generalisation
impossible when determining the type of $x$ (i.e., the type of $x$ is just $B$
without further quantification). However, this means that the choice of $B$
influences the polymorphism of $x$, meaning that the constraint above may
introduce undetermined polymorphism in the term context if arbitrarily
polymorphic types were permitted for $a$. Thus we must restrict the possible
choices for $B$. The rule Sem-LetPoly does so by imposing a relationship
between the most general solution $\delta_{\mathrm{m}}(a)$ for $a$ and the
type $A$ actually chosen as the instantiation of $a$. In our example above,
each most general solution $\delta_{\mathrm{m}}$ of $C_{1}$ has the form
$[a\mapsto c,b\mapsto c]$, where $c\in\Delta_{\mathrm{m}}$. Therefore, we have
$\Delta_{\mathrm{o}}=c$ and $\overline{b}$ is empty. The rule Sem-LetPoly then
imposes that the actual type $A$ for $a$ results from monomorphically
instantiating all non-generalisable variables in $\delta_{\mathrm{m}}(a)$
(namely, $\Delta_{\mathrm{o}}$). In the example above, this means that $a$
(and therefore also $b$) must be instantiated with a monotype. Observe that in
general, $\delta^{\prime}(\delta_{\mathrm{m}}(a))$ may not be a feasible
choice for $A$ for any well-formed monomorphic instantiation
$\delta^{\prime}$. Consider the constraint:

$\exists a.a\sim(\mathsf{Int}\to\mathsf{Int})\wedge\left({\rm{\bf
let}}_{\star}\;x=\sqcap b.\exists c.a\sim b\wedge a\sim(c\to c)\;{\rm{\bf
in}}\;C_{2}\right)$

Here, $\delta^{\prime}(\delta_{\mathrm{m}}(a))$ may yield any type of the form
$S\to S$ (recall that $S$ denotes monotypes). However, the premise
$(\Delta,\tilde{b});(\Xi,a);\Gamma;\delta[a\mapsto A]\vdash C_{1}$ of Sem-
LetPoly forces $A$ to be compatible with any prior choices made by the ambient
instantiation $\delta$. In our examples, this ensures that
$A=(\mathsf{Int}\to\mathsf{Int})$.

##### Monomorphic let constraints

To accommodate the value restriction, the function $\llbracket-\rrbracket$
translates a plain let binding of a term $M$ that is not a guarded value,
${\rm{\bf let}}\;x=M\;{\rm{\bf in}}\;N$, to a monomorphic let constraint of
the form ${\rm{\bf let}}_{\mathord{\bullet}}\;x=\sqcap a.C_{1}\;{\rm{\bf
in}}\;C_{2}$. The only difference between a polymorphic let constraint and a
monomorphic one is that all variables that would be generalised by the former
are instantiated monomorphically by the latter.

The rule Sem-LetMono in Figure 3 achieves this by instantiating all of
$\Delta_{\mathrm{m}}$ monomorphically to obtain $A$ from
$\delta_{\mathrm{m}}(a)$. An equivalent, yet slightly more verbose version of
Sem-LetMono highlighting the symmetry between Sem-LetPoly and Sem-LetMono
could define $\Delta_{\mathrm{o}}$ and $\overline{b}$ just like the former
rule, and then impose
$\Delta\vdash\delta^{\prime}:(\Delta_{\mathrm{o}},\overline{b})\Rightarrow_{\mathord{\bullet}}\cdot$.
Observe that the variables in
$\Delta_{\mathrm{m}}-(\Delta_{\mathrm{o}},\overline{b})$ are irrelevant in
Sem-LetPoly.

###  3.4. Metatheory

We can now formalise the relationship between terms and the constraints
obtained from them. Firstly, if $M$ has type $A$, then $\llbracket
M:a\rrbracket$ is satisfiable by a substitution that maps $a$ to $A$.

###### Theorem 1 (Constraint generation is sound with respect to the typing
judgement).

Let $\Delta;\Gamma\vdash M:A$ and $a\mathop{\\#}\Delta$. Then
$\Delta;a;\Gamma;[a\mapsto A]\vdash\llbracket M:a\rrbracket$ holds.

Secondly, if a constraint $\llbracket M:a\rrbracket$ is satisfied using an
instantiation $\delta$, then $\delta(a)$ is a valid type for $M$.

###### Theorem 2 (Constraint generation is complete with respect to the typing
judgement).

If $\Delta;\Gamma\vdash M\ \mathbf{ok}$ and
$\Delta;a;\Gamma;\delta\vdash\llbracket M:a\rrbracket$, then
$\Delta;\Gamma\vdash M:\delta(a)$.

Both properties are proved by structural induction on $M$; proof details are
provided in the appendix (see supplementary material).

##  4\. Constraint solving

We present a stack machine for solving constraints in our language, similar to
the HM($X$) solver by Pottier and Rémy (2005). Our machine is defined in terms
of a transition relation on states of the form $(F,\Theta,\theta,C)$,
consisting of a _stack_ $F$, a _restriction context_ $\Theta$, a _type
substitution_ $\theta$, and an _in-progress constraint_ $C$, each of which we
elaborate on below.

##### Stacks

In a state $(F,\Theta,\theta,C)$, $C$ denotes the constraint to be solved
next.

The stack $F$ denotes the context in which $C$ appears, containing bindings
for type variables (rigid and flexible) and term variables that may appear in
$C$. Further, the stack indicates how to continue after $C$ has been solved.
Our stack machine operates on closed states, meaning that the stack contains
bindings for all free variables of $C$.

Formally, stacks are built from stack frames as follows.

$\begin{array}[t]{@{}l@{}}\begin{array}[t]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Frames}&f~{}&::=\hfil~{}&\Box\wedge
C\mid\forall\;a\mid\exists\;a\mid{\rm{\bf let}}_{R}\;x=\sqcap
a.\Box\;\mathsf{in}\;C\mid{\rm{\bf def}}\;(x:A)\\\
\textrm{Stacks}&F~{}&::=\hfil~{}&\cdot\mid F::f\end{array}\\\ \end{array}$

The different forms of stack frames directly correspond to those constraints
with at least one sub-constraint. The overall stack can then be seen as a
constraint with a hole in which $C$ is plugged. We use holes $\Box$ in frames
for constraints with two sub-constraints and store the second sub-constraint
to which we must return after solving the first one.

##### Restriction Contexts and Type Substitutions

The components $\Theta$ and $\theta$ of a state $(F,\Theta,\theta,C)$ encode
the _unification context_. Their syntax is defined as follows.

$\begin{array}[t]{@{}l@{}}\begin{array}[t]{@{}l@{\quad}r@{~}c@{~}l@{}}\textrm{Restriction
Contexts}&\Theta~{}&::=\hfil~{}&\cdot\mid\Theta,a:R\\\ \textrm{Type
Substitutions}&\theta~{}&::=\hfil~{}&\emptyset\mid\theta[a\mapsto A]\\\
\textrm{States}&s~{}&::=\hfil~{}&(F,\Theta,\theta,C)\end{array}\\\
\end{array}$

The restriction context $\Theta$ contains exactly the flexible variables bound
by the stack $F$ and stores the restriction imposed on each such variable.
Again, restrictions $R$ determine which types a flexible variable may be
unified or instantiated with: monomorphic only (${\mathord{\bullet}}$) or
arbitrary polymorphic types ($\star$).

Type substitutions $\theta$ are similar to type instantiations $\delta$.
However, they apply only to flexible variables, their codomain may contain
flexible variables, and must respect the restriction imposed on each
individual variable in the domain. Note that this is in contrast to
instantiations, where
$\Delta\vdash\delta:\Delta^{\prime}\Rightarrow_{R}\Delta^{\prime\prime}$ fixes
a single restriction $R$ for all variables in the domain of $\delta$.

To this end, we formalise what it means for a type $A$ to obey a restriction
$R$ using the judgement $\Delta;\Theta\vdash_{R}A\ \mathbf{ok}$, shown in
Figure 6. Rigid variables are monomorphic. Flexible variables have their
restriction determined by the restriction context. The restriction of a data
type is determined inductively. A universally quantified type is polymorphic.
Every monomorphic type is also a polymorphic type. Observe that the well-
formedness judgement $\Delta\vdash_{R}A\ \mathbf{ok}$ used in Section 3 can
now be considered as a shorthand for $\Delta;\cdot\vdash_{R}A\ \mathbf{ok}$.

We can now formally state what it means for a substitution $\theta$ to be
well-formed, mapping flexible variables in $\Theta^{\prime}$ to well-formed
types over variables from $\Delta,\Theta$ via the judgement
$\Delta\vdash\theta:\Theta^{\prime}\Rightarrow\Theta$, which is also shown in
Figure 6. As for substitutions, we additionally require that
$\Theta\mathop{\\#}\Delta$ and $\Theta^{\prime}\mathop{\\#}\Delta$ (however,
$\Theta$ and $\Theta^{\prime}$ need not be disjoint). In summary, this means
that in any solver state, the substitution $\theta$ contains the current
knowledge about unification variables, respecting the restrictions imposed by
$\Theta$.

$\boxed{\Delta;\Theta\vdash_{R}A\ \mathbf{ok}}$ *a ∈Δ Δ;Θ⊢_∙a

*a : R ∈Θ Δ;Θ⊢_R a

*arity(D) = n

Δ;Θ⊢_R A_1 ok

⋯

Δ;Θ⊢_R A_n ok Δ;Θ⊢_R D ¯A ok

*(Δ, a); Θ⊢_R A ok Δ; Θ⊢_⋆∀a.A ok

*Δ; Θ⊢_∙A ok Δ; Θ⊢_⋆A ok

$\boxed{\Delta\vdash\theta:\Theta^{\prime}\Rightarrow\Theta}$ Δ⊢∅: ⋅⇒Θ

Δ⊢θ: Θ’ ⇒Θ
Δ;Θ⊢_R A ok Δ⊢θ[a ↦A] : (Θ’, a : R) ⇒Θ

Figure 6. Well-formedness of types and substitutions.

We write $\mathsf{bv}(F)$ and $\mathsf{btv}(F)$ for the term variables and
type variables (flexible or rigid) bound by $F$, respectively. Moreover, we
write $\mathsf{rc}(F)$, $\mathsf{fc}(F)$, and $\mathsf{tc}(F)$ for the rigid
context, flexible context, and term context synthesised from a stack $F$,
respectively. The latter operators consider $\forall$ frames
($\mathsf{rc}(F)$), let and $\exists$ frames ($\mathsf{fc}(F)$), and def
frames ($\mathsf{tc}(F)$), as shown in Figure 7.

$\begin{array}[]{cc}\mathsf{rc}(F)=\begin{cases}\cdot&\text{if
}F=\cdot\\\\[2.0pt] \mathsf{rc}(F^{\prime}),a&\text{if }F=F^{\prime}::\forall
a\\\ \mathsf{rc}(F^{\prime})&\text{otherwise
}(F=F^{\prime}::\\_)\end{cases}\par&\mathsf{fc}(F)=\begin{cases}\cdot&\text{if
}F=\cdot\\\ \mathsf{fc}(F^{\prime}),a&\text{if }\begin{aligned}
&F=F^{\prime}::\exists a\;\text{ or }\\\ &F=F^{\prime}::{\rm{\bf
let}}_{R}\;x=\sqcap a.\Box\;{\rm{\bf in}}\;C_{2}\end{aligned}\\\
\mathsf{fc}(F^{\prime})&\text{otherwise }(F=F^{\prime}::\\_)\\\
\end{cases}\\\\[30.00005pt]
\lx@intercol\hfil\mathsf{tc}(F)=\begin{cases}\cdot&\text{if }F=\cdot\\\
\mathsf{tc}(F^{\prime}),(x:A)&\text{if }F=F^{\prime}::{\rm{\bf def}}\;(x:A)\\\
\mathsf{tc}(F^{\prime})&\text{otherwise }(F=F^{\prime}::\\_)\\\
\end{cases}\hfil\lx@intercol\end{array}$ Figure 7. Extracting components from
stacks.

In order for a state $(F,\Theta,\theta,C)$ to be well-formed
($\vdash(F,\Theta,\theta,C)\ \mathbf{ok}$), we require that
$\mathsf{rc}(F)\vdash\theta:\Theta\Rightarrow\Theta$, that $\theta$ is
idempotent, that $C$ is well-formed
($\mathsf{rc}(F);\mathsf{fc}(F);\mathsf{tc}(F)\vdash C\ \mathbf{ok}$), and
that $F$ is well-formed with respect to $\Theta$ ($\Theta\vdash F\
\mathbf{ok}$). The latter judgement is defined in Figure 8. In addition to
basic well-formedness conditions on the involved types and constraints, the
judgement $\Theta\vdash F\ \mathbf{ok}$ imposes the following invariants: all
type and term variables bound by $F$ are pairwise disjoint and all free type
variables appearing in annotations on def constraints are monomorphic.
Moreover, $\Theta$ must contain exactly the flexible variables bound by $F$.

###### Remark 2 (Idempotent substitutions).

Our requirement that $\theta$ be idempotent (i.e. $\theta\circ\theta=\theta$)
concretely means that each binding $a\mapsto A$ in $\theta$ either maps $a$ to
itself (an “undetermined variable”) or to a type $A$ whose flexible variables
are all undetermined. This has some helpful consequences, for example in the
definition of $\mathsf{partition}$, discussed later (Remark 3).

To check the well-formedness of constraints embedded in stack frames, the
corresponding rules of $\Theta\vdash F\ \mathbf{ok}$ in Figure 8 synthesise
term contexts from the stack under consideration. As with earlier well-
formedness judgements, the judgement $\Theta\vdash F\ \mathbf{ok}$ checks that
all term variables are in scope, but ignores the associated types.

$\boxed{\Theta\vdash F\ \mathbf{ok}}$

⋅⊢⋅ ok

rc(F); Θ; tc(F) ⊢C ok
Θ⊢F ok Θ⊢F :: □∧C ok
Θ⊢F ok
a ／∈btv(F) Θ⊢F :: ∀ a ok

Θ⊢F ok
a ／∈btv(F) (Θ, a : R) ⊢F :: ∃ a ok
for all  a ∈ftv(A) - rc(F) ∣(a : ∙) ∈Θ

x ／∈bv(F)
Θ⊢F ok Θ⊢F :: def (x : A) ok

rc(F); Θ; (tc(F), x : A) ⊢C ok

x ／∈bv(F)
Θ⊢F ok
(Θ, a : R) ⊢F :: let_R’ x = ⊓a.□ in C ok

Figure 8. Stack well-formedness.

###  4.1. Stack Machine Rules

$(F,\Theta,\theta,A\sim
B)$$(F,\Theta^{\prime},\theta^{\prime}\circ\theta,\mathsf{true}){\;\footnotesize\color[rgb]{0.3515625,0.3515625,0.3515625}\definecolor[named]{pgfstrokecolor}{rgb}{0.3515625,0.3515625,0.3515625}\text{where}(\Theta^{\prime},\theta^{\prime})=\mathcal{U}(\mathsf{rc}(F),\Theta,\theta
A,\theta
B)}$$\rightarrow$$(\text{{S-Eq}})$$(F,\Theta,\theta,\lceil{x:A}\rceil)$$(F,\Theta,\theta,\mathsf{tc}(F)(x)\sim
A)$$\rightarrow$$(\text{{S-Freeze}})$$(F,\Theta,\theta,x\preceq
A)$$(F,\Theta,\theta,\exists\overline{a}.H\sim
A){\;\footnotesize\color[rgb]{0.3515625,0.3515625,0.3515625}\definecolor[named]{pgfstrokecolor}{rgb}{0.3515625,0.3515625,0.3515625}\text{where
}\forall\overline{a}.H=\mathsf{tc}(F)(x)\quad\tilde{a}\mathop{\\#}\mathsf{btv}(F)}$$\rightarrow$$(\text{{S-Inst}})$$(F,\Theta,\theta,\mathsf{mono}(a))$$(F,\Theta^{\prime},\theta,\mathsf{true})$$\rightarrow$$(\text{{S-Mono}})$where
$\begin{array}[t]{@{}l@{}}\begin{array}[t]{@{}l}\overline{b}=\mathsf{ftv}(\theta(a))-\mathsf{rc}(F)\quad\Theta^{\prime}=(\Theta-\tilde{b})\cup\widetilde{b:{\mathord{\bullet}}}\quad\Theta^{\prime}\vdash_{{\mathord{\bullet}}}\theta(a)\
\mathbf{ok}\end{array}\end{array}$ $(F,\Theta,\theta,C_{1}\wedge
C_{2})$$(F::\Box\wedge
C_{2},\Theta,\theta,C_{1})$$\rightarrow$$(\text{{S-ConjPush}})$$(F::\Box\wedge
C_{2},\Theta,\theta,\mathsf{true})$$(F,\Theta,\theta,C_{2})$$\rightarrow$$(\text{{S-ConjPop}})$$(F,\Theta,\theta,\exists
a.\,C)$$(F::\exists a,(\Theta,a:\star),\theta[a\mapsto
a],C)$$\rightarrow$$(\text{{S-ExistsPush}})$$(F::f::\exists\overline{a},\Theta,\theta,\mathsf{true})$$(F::\exists\tilde{c}::f,\Theta^{\prime},{\theta}\mathord{\upharpoonright}_{\Theta^{\prime}},\mathsf{true})$$\rightarrow$$(\text{{S-ExistsLower}})$where
$\begin{array}[t]{@{}l@{}}\text{$f$ is neither a ${\rm{\bf let}}$ or $\exists$
frame}\quad\tilde{b};\>\tilde{c}=\mathsf{partition}(\tilde{a},\theta,\Theta)\quad\Theta^{\prime}=\Theta-\tilde{b}\quad|\tilde{a}|>0\end{array}$
$(F,\Theta,\theta,\forall
a.C)$$(F::\forall\;a,\Theta,\theta,C)$$\rightarrow$$(\text{{S-ForallPush}})$$(F::\forall\;a,\Theta,\theta,\mathsf{true})$$(F,\Theta,\theta,\mathsf{true}){\;\footnotesize\color[rgb]{0.3515625,0.3515625,0.3515625}\definecolor[named]{pgfstrokecolor}{rgb}{0.3515625,0.3515625,0.3515625}\text{where
}a\not\in\mathsf{ftv}(\theta(\Theta))}$$\rightarrow$$(\text{{S-ForallPop}})$$(F,\Theta,\theta,{\rm{\bf
def}}\;(x:A)\;{\rm{\bf in}}\;C)$$(F::{\rm{\bf
def}}\;(x:A),\Theta^{\prime},\theta,C)$$\rightarrow$$(\text{{S-DefPush}})$where
$\begin{array}[t]{@{}l@{}}\begin{array}[t]{@{}l}\overline{b}=\mathsf{ftv}(\theta(A))-\mathsf{rc}(F)\quad\Theta^{\prime}=(\Theta-\tilde{b})\cup\widetilde{b:{\mathord{\bullet}}}\quad\text{for
all
}a\in\mathsf{ftv}(A)\mid\Theta^{\prime}\vdash_{{\mathord{\bullet}}}\theta(a)\
\mathbf{ok}\end{array}\end{array}$ $(F::{\rm{\bf
def}}\;(x:A),\Theta,\theta,\mathsf{true})$$(F,\Theta,\theta,\mathsf{true})$$\rightarrow$$(\text{{S-DefPop}})$$(F,\Theta,\theta,{\rm{\bf
let}}_{R}\;x=\sqcap b.C_{1}\;{\rm{\bf in}}\;C_{2})$$(F::{\rm{\bf
let}}_{R}\;x=\sqcap b.\Box\;{\rm{\bf
in}}\;C_{2},(\Theta,b:\star),\theta[b\mapsto
b],C_{1})$$\rightarrow$$(\text{{S-LetPush}})$$(F::{\rm{\bf
let}}_{\star}\;x=\sqcap b.\Box\;{\rm{\bf
in}}\;C::\exists\overline{a},\Theta,\theta,\mathsf{true})$$(F::\exists\widetilde{a^{\prime\prime}},\Theta^{\prime},{\theta}\mathord{\upharpoonright}_{\Theta^{\prime}},{\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;C)$$\rightarrow$$(\text{{S-LetPolyPop}})$where
$\begin{array}[t]{@{}l@{}}\widetilde{a^{\prime}};\>\widetilde{a^{\prime\prime}}=\mathsf{partition}((\tilde{a},b),\theta,\Theta)\quad
A=\theta(b)\quad\overline{c}\>=\mathsf{ftv}(A)\cap\widetilde{a^{\prime}}\quad\Theta^{\prime}=\Theta-\widetilde{a^{\prime}}\quad
B=\forall\overline{c}.A\end{array}$ $(F::{\rm{\bf
let}}_{\mathord{\bullet}}\;x=\sqcap b.\Box\;{\rm{\bf
in}}\;C::\exists\overline{a},\Theta,\theta,\mathsf{true})$$(F::\exists(\tilde{c},\widetilde{a^{\prime\prime}}),\Theta^{\prime},{\theta}\mathord{\upharpoonright}_{\Theta^{\prime}},{\rm{\bf
def}}\;(x:A)\;{\rm{\bf in}}\;C)$$\rightarrow$$(\text{{S-LetMonoPop}})$where
$\begin{array}[t]{@{}l@{}}\widetilde{a^{\prime}};\>\widetilde{a^{\prime\prime}}=\mathsf{partition}((\tilde{a},b),\theta,\Theta)\quad
A=\theta(b)\quad\overline{c}=\mathsf{ftv}(A)\cap\widetilde{a^{\prime}}\quad\Theta^{\prime}=\Theta-(\widetilde{a^{\prime}}-\tilde{c})\end{array}$
Figure 9. Constraint solving rules.

We now introduce the rules of the constraint solver itself (Figure 9). These
rules are deterministic in the sense that at most one rule applies at any
point. Moreover, after each step the resulting state is unique up to the names
of binders added to the stack and the order of adjacent existential frames in
the frame (e.g., a step may yield either $F::\exists a::\exists b::\dots$ or
$F::\exists b::\exists a::\dots$). A constraint is satisfiable in a given
context if the machine reaches a state of the form
$(\forall\Delta::\exists\Xi,\Theta,\theta,\mathsf{true})$ from an initial
configuration built from $C$ and the context. From such a final configuration
we can also read off a most general solution for the constraint. If the
constraint is unsatisfiable, the machine gets stuck before reaching such a
final state. We formalise the properties of the solver in Section 4.2.

##### Unification

The rule S-Eq in Figure 9 handles equality constraints of the form $A\sim B$.
We apply $\theta$ to both types as this may refine the types prior to invoking
the unification procedure $\mathcal{U}$. It remains unchanged as compared to
the original type inference system for FreezeML based on Algorithm W (Emrich
et al., 2020).

$\begin{array}[]{c
c}\begin{array}[t]{@{}l@{}}\mathcal{U}(\Delta,\Theta,a,a)=\\\
\quad\text{return}\;(\Theta,\theta_{\mathrm{id}})\vskip 12.0pt plus 4.0pt
minus 4.0pt\\\ \mathcal{U}(\Delta,\Theta,D\,\overline{A},D\,\overline{B})=\\\
\quad\begin{array}[t]{@{}l@{}}\text{let}\;(\Theta_{1},\theta_{1})=(\Theta,\theta_{\mathrm{id}})\\\
\text{let}\;n=\mathsf{arity}(D)\\\ \text{for }i\in 1\ldots n\\\
\quad\text{let}\;(\Theta_{i+1},\theta_{i+1})=\\\
\qquad\begin{array}[t]{@{}l@{}}\text{let}\;(\Theta^{\prime},\theta^{\prime})=\mathcal{U}(\Delta,\Theta_{i},\theta_{i}(A_{i}),\theta_{i}(B_{i}))\\\
\text{return}\;(\Theta^{\prime},\theta^{\prime}\circ\theta_{i})\\\
\end{array}\\\ \text{return}\;(\Theta_{n+1},\theta_{n+1})\\\
\end{array}\par\end{array}\par&\qquad\begin{array}[t]{@{}l@{}}\mathcal{U}(\Delta,(\Theta,a:R),a,A)=\\\
\mathcal{U}(\Delta,(\Theta,a:R),A,a)=\\\
\quad\begin{array}[t]{@{}l@{}}\text{let}\;\Theta_{1}=\mathsf{demote}(R,\Theta,\mathsf{ftv}(A)-\Delta)\\\
\text{assert}\;\Delta,\Theta_{1}\vdash_{R}A\ \mathbf{ok}\\\
\text{return}\;(\Theta_{1},\theta_{\mathrm{id}}[a\mapsto A])\\\
\end{array}\vskip 12.0pt plus 4.0pt minus 4.0pt\\\
\mathcal{U}(\Delta,\Theta,\forall a.A,\forall b.B)=\\\
\quad\begin{array}[t]{@{}l@{}}\text{assume fresh}\;c\\\
\text{let}\;(\Theta_{1},\theta^{\prime})=\mathcal{U}((\Delta,c),\Theta,A[c/a],B[c/b])\\\
\text{assert}\;c\notin\mathsf{ftv}(\theta^{\prime})\\\
\text{return}\;(\Theta_{1},\theta^{\prime})\\\
\end{array}\end{array}\end{array}$

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{demote}(\star,\Theta,\Delta)~{}&=\hfil~{}&\Theta\\\
\mathsf{demote}({\mathord{\bullet}},\cdot,\Delta)~{}&=\hfil~{}&\cdot\\\
\mathsf{demote}({\mathord{\bullet}},(\Theta,a:R),\Delta)~{}&=\hfil~{}&\mathsf{demote}({\mathord{\bullet}},\Theta,\Delta),a:{\mathord{\bullet}}\quad(a\in\Delta)\\\
\mathsf{demote}({\mathord{\bullet}},(\Theta,a:R),\Delta)~{}&=\hfil~{}&\mathsf{demote}({\mathord{\bullet}},\Theta,\Delta),a:R\quad(a\not\in\Delta)\\\
\end{array}$

Figure 10. Unification algorithm.

The unification algorithm is largely standard, supporting unification of
polymorphic types without reordering of quantifiers or the removal/addition of
unneeded quantifiers, as per FreezeML’s notion of type equality. It returns
updated versions of the restriction context and substitution, named
$\Theta^{\prime}$ and $\theta^{\prime}$. The algorithm is sound, complete, and
yields most general unifiers (Emrich et al., 2020, Theorem 4 and 5).

One notable feature is the unification algorithm’s treatment of restrictions.
The restriction context $\Theta^{\prime}$ returned by the algorithm contains
the same flexible variables as the original $\Theta$, but some variables
therein may have been demoted from a polymorphic restriction to a monomorphic
one. Unifying a flexible, monomorphic variable $a$ with a type $A$ only
succeeds if making all free flexible variables in $A$ monomorphic makes $A$
itself monomorphic. Therefore, assuming
$a:{\mathord{\bullet}},b:\star\in\Theta$, unifying $a$ with $b\to b$ yields
$(b:{\mathord{\bullet}})\in\Theta^{\prime}$, whereas unification of $a$ with
$\forall c.c\to c)$ fails.

The unification algorithm is shown in Figure 10. On each invocation, the first
applicable clause is used; $\theta_{\mathrm{id}}$ denotes the identity
substitution on $\Theta$.

##### Basic constraints.

The rules for constraints $\lceil{x:A}\rceil$ and $x\preceq A$ yield
corresponding equality constraints. For instantiation constraints, the solver
instantiates all top-level quantifiers $\overline{a}$ of $x$’s type by
existentially quantifying them. Note that the rule imposes picking variables
$\overline{a}$ that are fresh with respect to the bound type variables (rigid
and flexible) of $F$. In both rules, $\mathsf{tc}(F)$ denotes the term context
synthesised from all ${\rm{\bf def}}$ constraints in $F$.

A monomorphism constraint $\mathsf{mono}{}(a)$ is handled by demoting all
flexible variables in $\theta(a)$. The step fails if doing so does not make
$\theta(a)$ a monomorphic type. Note that demoting the involved restrictions
means that later unification steps cannot make $a$ polymorphic — even if, say,
$\theta(a)=a$ holds at the time of applying S-Mono, recording
$(a:{\mathord{\bullet}})$ in $\Theta^{\prime}$ ensures that it stays
monomorphic.

The rules S-ConjPush and S-ConjPop handle conjunctions. When encountering
$C_{1}\wedge C_{2}$, the first rule pushes a corresponding frame on the stack.
Once $C_{1}$ is solved and the state’s in-progress constraint becomes
$\mathsf{true}$, the latter rule pops this frame from the stack and continues
solving $C_{2}$.

##### Binding of type variables.

When encountering $\exists a.C$ or $\forall a.C$, a corresponding frame is
added by the rules S-ExistsPush and S-ForallPush, respectively.

In general, once the in-progress constraint in a state becomes $\mathsf{true}$
and the topmost stack frame binds a flexible variable $a$, the binding frame
is either moved downwards in the stack, generalised when handling ${\rm{\bf
let}}$ constraints, or dropped if no variable further down in the stack
depends on $a$. Note that lowering binders of flexible variables in the stack
this way effectively increases the syntactic scope of the bound variable as it
moves outwards in the constraint representing the stack. The rule
S-ExistsLower implements part of this lowering mechanism; it acts on stacks of
the form $F::f::\exists\overline{a}$, a shorthand for $F::f::\exists
a_{0}::\dots::\exists a_{n}$. The rule requires that $f$ is neither a let
frame (whose rules treat adjacent existentials directly) or another
existential frame (to make the rule deterministic by making $\overline{a}$
exhaustive). It uses the helper function $\mathsf{partition}$, which returns a
tuple and is defined as follows.

$\mathsf{partition}(\Xi,\theta,\Theta)=\Xi^{\prime};\Xi^{\prime\prime}\text{
where }\Xi^{\prime},\Xi^{\prime\prime}=\Xi\text{ and }\text{for all
}a\in\Xi:a\in\Xi^{\prime\prime}\text{ iff
}a\in\mathsf{ftv}({\theta}\mathord{\upharpoonright}_{(\mathsf{ftv}(\Theta)-\Xi)})$

It partitions $\Xi$ into two sets $\Xi^{\prime}$ and $\Xi^{\prime\prime}$ such
that the latter contains exactly those variables appearing in the range of
$\theta$ restricted to the flexible variables bound further down in the stack
(i.e., $\theta$ restricted to $\mathsf{ftv}(\Theta)-\Xi$). This formalises the
notion that no variable further down in the stack depends on a variable in
$\Xi^{\prime}$. Therefore, the bindings for $\Xi^{\prime}$ can simply be
removed altogether; the bindings for $\Xi^{\prime\prime}$ must be kept and are
lowered within the stack.

###### Remark 3 (Idempotence and $\mathsf{partition}$).

If we did not require substitutions to be idempotent, the existing definitions
would break in subtle ways (or need to be made more complicated). For
example,. let $a,b,c\in\Theta$ and $\Xi=\\{a,b\\}$ and $\theta=[a\mapsto
a,b\mapsto a,c\mapsto b]$. Note that this $\theta$ is not idempotent since
$\theta(\theta(c)))=a\neq b=\theta(c)$. The definition of
$\mathsf{partition}(\Xi,\theta,\Theta)$ would then yield
$\Xi^{\prime}=\\{a\\}$ and $\Xi^{\prime\prime}=\\{b\\}$, even though $c$
depends on both variables.

When popping a frame $\forall a$ from the stack, the rule S-ForallPop checks
that $a$ does not escape its scope by still being present in the range of
$\theta$. Note that together with the lowering of existentials mentioned
before, removing the unneeded variables $\tilde{b}$ in S-ExistsLower is not
simply an optimisation, but necessary for completeness. Consider the state
$(F::\forall a::\exists b,\Theta,\theta,\mathsf{true})$ where $\theta(b)=a$.
If this variable was lowered by S-ExistsLower – yielding a new state
$(F::\exists b::\forall a,\Theta,\theta,\mathsf{true})$ – instead of being
removed, this would cause S-ForallPop to erroneously detect an escaping
quantifier.

##### Binding of term variables

Similarly to the other *Push rules, S-DefPush moves a constraint ${\rm{\bf
def}}\;(x:A)\;{\rm{\bf in}}\;C$ to the stack and makes $C$ the next in-
progress constraint. However, it also forces all flexible variables found in
$\theta(A)$ to be monomorphic and checks that doing so does not make the
substitution ill-formed. This ill-formedness would arise if the substitution
maps one of the type variables to be monomorphised to a polymorphic type. The
monomorphisation is crucial in order to maintain the invariant that the term
context does not contain unknown polymorphism in the form of unrestricted
(i.e., polymorphic) unification variables. Note that the checks performed by
S-DefPush are equivalent to adding
$\bigwedge_{a\in\mathsf{ftv}(A)-\mathsf{rc}(F)}\;\mathsf{mono}(a)$ as a
conjunct to $C$, but doing so may create an ill-formed intermediate state
before failing when solving one of the $\mathsf{mono}{}$ constraints. The rule
S-DefPop is the counterpart of S-DefPush and simply pops the ${\rm{\bf def}}$
frame.

S-LetPush handles constraints ${\rm{\bf let}}_{R}\;x=\sqcap b.C_{1}\;{\rm{\bf
in}}\;C_{2}$ by adding a stack frame and bringing $b$ into scope while solving
$C_{1}$. Once $C_{1}$ has been solved, the rules S-LetPolyPop and S-LetMonoPop
handle the different semantics of ${\rm{\bf let}}_{{\mathord{\bullet}}}$ and
${\rm{\bf let}}_{\star}$ regarding how they determine the type of $x$. We
first consider the former rule. Note that the rule is applicable with zero or
more existential frames on top of the let frame, binding $\tilde{a}$, followed
by the actual let frame. These existential frames are either the result of
existential constraints at the top-level of the original constraint $C_{1}$
(the first subconstraint of the ${\rm{\bf let}}$ constraint under
consideration), or were lowered while solving $C_{1}$.

Similarly to S-ExistsLower, the variables $\tilde{a}$ and $b$ are partitioned
by the $\mathsf{partition}$ function into $\widetilde{a^{\prime}}$ and
$\widetilde{a^{\prime\prime}}$. Note that we include $b$ here because
${\rm{\bf let}}_{R}\;x=\sqcap b.C_{1}\;{\rm{\bf in}}\;C_{2}$ binds $b$
existentially in $C_{1}$. By definition of $\mathsf{partition}$, we again have
that no unification variable bound below the ${\rm{\bf let}}$ frame depends on
any of the variables in $\widetilde{a^{\prime}}$ (as indicated by $a$ not
appearing in the image of $\theta$ restricted to the variables bound in the
lower frames). Similarly to S-ExistsLower, the variables
$\widetilde{a^{\prime\prime}}$ must be preserved and are lowered in the stack.
Note that $\widetilde{a^{\prime\prime}}$ may or may not contain $b$.

The type $A$ for $x$ is then determined by generalising $\theta(b)$. The
variables $\overline{c}$ to be generalised are obtained from taking those free
type variables of $\theta(b)$ that also appear in $\widetilde{a^{\prime}}$.
Recall that $\mathsf{ftv}$ applied to a type yields an ordered sequence, and
we assume that the ordering is preserved under intersection.

By definition, $\widetilde{a^{\prime}}$ contains those variables from
$\tilde{a},b$ that do not appear in the codomain of $\theta$ restricted to the
variables from lower stack frames (i.e. no such variable from a lower stack
frame directly depends on a variable in $\widetilde{a^{\prime}}$).
Nevertheless, there may be variables $a\in\widetilde{a^{\prime}}$ such that
$\theta(a)=B$ where $B$ contains (or is) a variable from a lower frame (i.e.
from $\Theta-\tilde{a},b$), meaning that $a$ must not be generalised. However,
due to the idempotency of $\theta$, we have that $\theta(a)=a$ for all
$a\in\theta(b)$. In other words, intersecting $\widetilde{a^{\prime}}$ with
the free type variables of $\theta(b)$ evokes that $\overline{c}$ only
contains “undetermined” variables mapped to themselves that are not referenced
by lower stack frames, either.

Note that rewriting the let frame to a def constraint also evokes that solving
the latter monomorphises any flexible variables in $A$ that were not
generalised. This reflects the monomorphic instantiation imposed in the
semantics of ${\rm{\bf let}}_{\star}$ constraints (cf. $\delta^{\prime}$ in
Sem-PolyPop in Figure 3).

The only difference between S-LetPolyPop and S-LetMonoPop is that while the
latter rule also determines the variables $\tilde{c}$, it does not generalise
them. This means that the resulting type $A$ assigned to $x$ contains the
unification variables $\tilde{c}$ freely. Therefore, these variables must kept
in scope and are existentially quantified further down in stack after the rule
is applied.

###  4.2. Metatheory

Our goal is to state a preservation property along the lines that stepping
from state $s_{0}$ to $s_{1}$ implies that some representation of $s_{0}$ as a
constraint is equivalent to $s_{1}$’s constraint representation. To this end,
we first define how to represent the unification context, comprising $\Theta$
and $\theta$, as a constraint. Given $\Theta$ and $\theta$, we define:

$\begin{array}[]{r@{\;\;} c@{\;\;}
l}\mathfrak{U}(\Theta)&=&\bigwedge_{(a\,:\,{\mathord{\bullet}})\in\Theta}\;\mathsf{mono}(a)\\\\[6.0pt]
\mathfrak{U}(\theta)&=&\bigwedge_{a\in\mathsf{ftv}(\Theta)}\;a\sim\theta(a)\\\\[6.0pt]
\mathfrak{U}(\Theta,\theta)&=&\mathfrak{U}(\Theta)\wedge\mathfrak{U}(\theta)\end{array}$

Using $\mathfrak{U}$, we may now represent a state $(F,\Theta,\theta,C)$ as
$F[C\wedge\mathfrak{U}(\Theta,\theta)]$, where the $F[-]$ operator plugs a
constraint into the stack’s innermost hole:

$\begin{array}[t]{@{}l@{}}\begin{array}[t]{@{}r@{\quad}c@{\quad}l@{\quad}r@{}}\cdot[C]&=&C\\\
(F::\Box\wedge C_{2})[C_{1}]&=&F[C_{1}\wedge C_{2}]\\\
(F::\forall\;a)[C]&=&F[\forall a.C]\\\ (F::\exists\;a)[C]&=&F[\exists a.C]\\\
(F::{\rm{\bf let}}_{R}\,x=\sqcap
a.\Box\;\mathsf{in}\;C_{2})[C_{1}]&=&F[{\rm{\bf let}}_{R}\,x=\sqcap
a.C_{1}\;{\rm{\bf in}}\;C_{2}]\\\ (F::{\rm{\bf def}}\;(x:A))[C]&=&F[{\rm{\bf
def}}\;(x:A)\;{\rm{\bf in}}\;C]\par\end{array}\end{array}$

Note that if the state is closed (i.e., $F$ binds all variables free in $C$)
the resulting constraint $F[C]$ is closed, too. In order to reason about
constraints that are satisfied by non-empty instantiations, we assume that
there are some rigid and flexible contexts $\Delta$ and $\Xi$ quantified by
the bottom-most stack frames that remain unchanged by the step. Therefore, we
consider the satisfiability of constraints before and after the step by an
instantiation $\delta$ with $\Delta\vdash\delta:\Xi\Rightarrow_{\star}\cdot$.

###### Theorem 3 (Preservation).

If $(\forall\Delta::\exists\Xi::F_{0},\Theta_{0},\theta_{0},C_{0})\
\mathbf{ok}$ and

$(\forall\Delta::\exists\Xi::F_{0},\Theta_{0},\theta_{0},C_{0})\to(\forall\Delta::\exists\Xi::F_{1},\Theta_{1},\theta_{1},C_{1})$

then

$\Delta;\Xi;\cdot;\delta\vdash
F_{0}[C_{0}\wedge\mathfrak{U}(\Theta_{0},\theta_{0})]\;\text{ iff
}\;\Delta;\Xi;\cdot;\delta\vdash
F_{1}[C_{1}\wedge\mathfrak{U}(\Theta_{1},\theta_{1})]$

This preservation property is inspired by a similar one holding for HM($X$)
(Pottier and Rémy, 2005, Lemma 10.6.9).

The following progress property states that given a well-formed, non-final
state whose representation as a formula is satisfiable, the stack machine can
take a step.

###### Theorem 4 (Progress).

Let $(F,\Theta,\theta,C)\ \mathbf{ok}$ and
$F[C]\neq\forall\Delta.\exists\Xi.\mathsf{true}$ for all $\Delta,\Xi$.
Further, let $\cdot;\cdot;\cdot;\emptyset\vdash
F[C\wedge\mathfrak{U}(\Theta,\theta)]$. Then there exists a state $s_{1}$ such
that $(F,\Theta,\Gamma,\theta,C)\to s_{1}$.

Termination is another crucial property.

###### Theorem 5 (Termination).

The constraint solver terminates on all inputs.

The proof relies on the existence of a well-ordering $<$ on states such that
$s\to s^{\prime}$ implies $s^{\prime}<s$. We observe that the well-ordering
cannot simply be defined based on the syntactic size of the in-progress
constraint of each state before and after the step, even when plugging the
constraint into each state’s stack. For example, the rule S-Inst in Figure 9
may introduce an arbitrary number of nested existential constraints. Other
rules such as S-ExistsLower may simply reorder stack frames. Therefore, given
a state $(F,\Theta,\theta,C)$, the well-ordering not only takes the size of
$F[C]$ and $C$ into account but also the number of instantiation constraints
in $C$ and the position of the right-most existential frame in $F$.

We use the syntax ${\rm{\bf def}}\;\Gamma\;{\rm{\bf in}}\;C$ to denote a
series of nested def constraints with $C$ as the innermost constraint, where
each def constraints performs a binding from $\Gamma$. We now state the
overall correctness of the solver as follows: A constraint $C$ is satisfiable
in context $\Delta;\Xi;\Gamma$ using instantiation $\delta$ if and only if the
solver reaches a final state from the input constraint
$\forall\Delta.\exists\Xi.{\rm{\bf def}}\;\Gamma\;{\rm{\bf in}}\;C$ and
$\delta$ is a refinement of the substitution $\theta$ returned by the solver.
Here, a “refinement” of $\theta$ is simply a composition with $\theta$.

###### Theorem 6 (Correctness of constraint solver).

Let $\Delta\vdash\Gamma\ \mathbf{ok}$ and $\Delta;\Xi;\Gamma\vdash C\
\mathbf{ok}$. Then we have

$\begin{array}[t]{@{}l@{}}\Delta;\Xi;\Gamma;\delta\vdash C\\\ \text{iff}\\\
\text{there exist }\Theta,\theta^{\prime},\theta,\Xi^{\prime}\text{ s.t.\ }\\\
\begin{array}[]{cl}&(\cdot,\cdot,\emptyset,\forall\Delta.\,\exists\Xi.\,{\rm{\bf
def}}\;\Gamma\;{\rm{\bf
in}}\;C)\to^{*}(\forall\Delta::\exists\;(\Xi,\Xi^{\prime}),\Theta,\theta,\mathsf{true})\text{
and }\\\ &\Delta\vdash\theta^{\prime}:\Theta\Rightarrow\cdot\text{ and }\\\
&{(\theta^{\prime}\circ\theta)}\mathord{\upharpoonright}_{\Xi}=\delta.\end{array}\end{array}$

Even though $\theta^{\prime}$ acts like an instantiation (its codomain only
contains rigid variables), it is crucial for it to be a substitution, meaning
that it respects the individual restrictions in $\Theta$. An instantiation
$\delta^{\prime}$ in place of $\theta^{\prime}$ may violate the restrictions
in $\Theta$ and introduce polymorphism in places where the type system
prohibits it, which would make the right-to-left direction of the theorem
invalid. Also note the domain of $\theta$ is $(\Xi,\Xi^{\prime})$, whereas
that of $\delta$ is $\Xi$. Thus, we restrict $\theta$ to $\Xi$ when relating
it to $\delta$.

Observe that Theorem 6 also states that our solver finds most general
solutions: The instantiation $\theta$ returned by the solver is independent
from $\delta$. Together with the deterministic nature of our solver, this
means that any such $\delta$ can be obtained from $\theta$.

For the purposes of type-checking, we may now relate the correctness of the
solver to constraints resulting from the translation function
$\llbracket-\rrbracket$ introduced in Section 3.1. If the solver succeeds on
the translation of some term $M$ in some context $\Delta;\Gamma$, then the
term is well-typed in context $\Delta;\Gamma$ for any well-formed refinement
of $\theta(a)$, where $a$ is the placeholder variable used for the type of
$M$.

###### Theorem 7 (Constraint-based typechecking is sound).

Let $\Delta\vdash\Gamma$ and $\Delta;\Gamma\vdash M\ \mathbf{ok}$ and
$a\mathop{\\#}\Delta$. If
$(\cdot,\cdot,\emptyset,\allowbreak\forall\Delta.\,\exists a.\,{\rm{\bf
def}}\;\Gamma\;{\rm{\bf in}}\;\allowbreak\llbracket M:a\rrbracket)$ $\to^{*}$
$(\forall\Delta::\exists\;(a,\tilde{b}),\Theta,\theta,\allowbreak\mathsf{true})$
and $\Delta\vdash\theta^{\prime}:\Theta\Rightarrow\cdot$ then
$\Delta;\Gamma\vdash M:(\theta^{\prime}\circ\theta)(a)$.

Conversely, if $M$ has type $A$, then $A$ can be obtained from instantiating
$\theta(a)$.

###### Theorem 8 (Constraint-based typechecking is complete and most general).

Let $a\mathop{\\#}\Delta$. If $\Delta;\Gamma\vdash M:A$ then there exist
$\Xi,\Theta,\theta$, $\delta$ such that
$(\cdot,\cdot,\emptyset,\forall\Delta\,.\exists a\,.{\rm{\bf
def}}\;\Gamma\;{\rm{\bf in}}\;\llbracket
M:a\rrbracket)\to^{*}(\forall\Delta::\exists\;\Xi,\Theta,\theta,\mathsf{true})$
and $A=\delta(\theta(a))$.

###### Remark 4 ($\mathsf{mono}{}(-)$ constraints).

The constraint $\mathsf{mono}{}(a)$ constrains a type variable to be
instantiated only with a monotype. Such constraints are not produced during
constraint generation and appear in the constraint solving rules only in the
rule S-Mono which solves them immediately by checking the current
instantiation of $a$ and constraining the free variables of $a$ to be
monomorphic. Moreover, because ${\rm{\bf def}}\;(x:A)\;{\rm{\bf in}}\;C$
constraints also require $A$ to be monomorphic, we considerd leaving out the
$\mathsf{mono}{}(a)$ constraint form altogether and considering it syntactic
sugar for ${\rm{\bf def}}\;(x:a)\;{\rm{\bf in}}\;\mathsf{true}$. The main
reason we have not done this is to simplify the presentation, particularly in
the statement and proof of the above results, in order to ensure a simple
translation of monomorphism information latent in $\Theta$ back into explicit
constraints.

An alternative design we considered would be to attach monomorphism
restrictions to existential quantifiers, and drop the monomorphism requirement
on ${\rm{\bf def}}$ constraints. However, we were not able to find a way to
make this work that retains most general solutions for ${\rm{\bf def}}$
constraints, as illustrated in Section 3.2.

##  5\. Discussion

In this section we discuss two extensions: using ranks for efficiency and
unordered quantification. We also compare our approach more directly to
Pottier and Rémy’s presentation of HM($X$).

###  5.1. Using Ranks

In our solver, the lowering of existential frames in the stack as well as
generalisation are controlled by the free type variables in the image of the
substitution $\theta$ in the state under consideration. Both mechanisms depend
on the $\mathsf{partition}$ function. A more efficient implementation
associates a _rank_ with each unification variable (Rémy, 1992; Kuan and
MacQueen, 2007), which can then be used instead of checking what free type
variables appear in certain types in the context.

Implementing ranks for our solver requires a similar mechanism to the one
described for the HM($X$) solver by Pottier and Rémy (2005); ranks are
orthogonal to the support for first-class polymorphism in our system.

We briefly outline how to adapt their mechanism to implement the escape check
our solver performs for $\forall$ quantifiers. To this end we associate a rank
with each flexible _and_ rigid variable $b$ in a given state $s$, denoted
$\mathsf{rank}(b)$. We define $\mathsf{rank}(s)$ as the number of let frames
plus the number of $\forall$ frames appearing in $F$. When the solver
encounters a binder for type variable $b$ in state $s$, the variable’s rank is
then initialised to be $\mathsf{rank}(s)$. When the unifier detects that some
flexible variable $a$ should be substituted with some type $A$, then the ranks
of all variables in $A$ are updated to be no larger than $\mathsf{rank}(a)$.
The escape check in the rule S-ForallPop, applied to state $s=(F::\forall
b,\Theta,\theta,\mathsf{true})$, can then be performed by checking that
$\mathsf{rank}(b)=\mathsf{rank}(s)$ holds. To partition the variables in $\Xi$
using ranks in the rules S-LetPolyPop and S-LetPolyPop in Figure 9 we use the
following modified version of the function $\mathsf{partition}$:

$\mathsf{partition^{\prime}}(\Xi,s)=\Xi^{\prime};\Xi^{\prime\prime}\text{
where }\Xi^{\prime},\Xi^{\prime\prime}=\Xi\text{ and }(\text{for all
}a\in\Xi\mid a\in\Xi^{\prime\prime}\text{ iff
}a\in\mathsf{rank}(a)<\mathsf{rank}(s))$

##### Eschewing existential frames.

To avoid the need for (inefficiently) lowering existential frames in the stack
by swapping with one non-existential frame at a time (as for example in
S-ExistsLower), we may optimise the solver further by not carrying individual
existential frames in the stack at all. Instead, each state $s$ contains
$\mathsf{rank}(s)$ sets of type variables of that rank. We may then remove the
rule S-ExistsLower altogether; in S-Let*Pop the variables
$\widetilde{a^{\prime}}$ are determined by taking exactly those of rank
$\mathsf{rank}(s)$ (the set $\widetilde{a^{\prime\prime}}$ isn’t needed
anymore in this setting).

###  5.2. Unordered FreezeML

So far we have considered a syntactic equational theory on types that equates
quantified types up to alpha-equivalence only and does not allow for any
reordering of quantifiers or the removal/addition of unused ones. This is in
line with the original presentation of FreezeML (Emrich et al., 2020).

However, this is not a fundamental requirement of the system. We may define
_Unordered FreezeML_ , a variant of FreezeML where quantifiers are unordered,
by redefining equality of types to allow $\forall ab.a\to b=\forall ba.a\to
b=\forall abc.a\to b$ and consider $\mathsf{ftv}$ to return sets of variables
rather than sequences. The typing rules of Unordered FreezeML can than be
obtained from Figure 1 by replacing every occurrence of $\overline{a}$ by
$\tilde{a}$. Likewise, type inference for Unordered FreezeML can be performed
using a stack machine using the same rules as shown in Figure 9. The only
change is to replace the unification algorithm $\mathcal{U}$ with an
alternative one ignoring the order of quantifiers as well as unnecessary ones.
This is of course not trivial because unification can no longer assume that
when it encounters a $\forall$ on one side of an equation, the other side must
be a $\forall$ binding the same (modulo alpha-equivalence) variable.
Unification must be modified to handle the case where one side $\forall$-binds
an unused variable (e.g. $\forall a.int\sim int$) or where bindings must be
reordered (e.g. $\forall a,b,c.a\to b\to c\sim\forall a,b,c.c\to b\to a$). The
point is that this complexity seems to be confined to unification and the rest
of the system is unchanged.

###  5.3. Comparison with HM($X$) solver by Pottier and Rémy

The solver presented in this section is inspired by the one presented by
Pottier and Rémy (2005) for HM($X$), adding support for first-class
polymorphism in the style of FreezeML.

Additional notable differences include the following:

  * •

In the HM($X$) solver, configurations carry a collection $U$ of unification
constraints. It can be interpreted as a conjunction built from a subset of the
constraint language with additional well-formedness restrictions. This means
that when extending the constraint language, the definition of constraint
permitted in $U$ can be adapted accordingly.

Our solver represents the unifier context with two separate components
$\Theta$ and $\theta$. This is mostly for the purpose of making the system
more similar to the original type inference algorithm of FreezeML. Our system
already provides a mechanism for representing the unification context as a
constraint, in the form of $\mathfrak{U}(\Theta,\theta)$, defined in Section
4.2 for the purposes of our meta-theory. It would be straightforward to define
unification contexts in our solver in terms of $\mathfrak{U}(\Theta,\theta)$
(or a more structured representation thereof using multi-equations) instead of
$\Theta$ and $\theta$.

  * •

The solver presented by Pottier and Rémy supports recursive types by allowing
the solver state to contain constraints of the form $a\sim A$, where $A\neq a$
and $a\in\mathsf{ftv}(A)$. In our system, a corresponding state with
$\theta(a)=A$ for the same $A$ would be ill-formed, as we require $\theta$ to
be idempotent.

We consider support for recursive types as orthogonal to the issue of
supporting first-class polymorphism, but our reliance on the idempotency of
$\theta$ would require adding explicit $\mu$ types for handling recursive
types.

  * •

The HM($X$) solver implements several optimisations, for example mechanisms to
reduce the number of type variables present in states. Similar optimisations
could be performed by our solver, but we eschew them for the sake of brevity,
including the usage of ranks described in Section 5.1.

  * •

In the HM($X$) solver, def constraints and term variables efficiently handle
sharing the work of type inference for let-generalized values, but they are
not strictly necessary: def constraints can be eliminated by a form of
constraint inlining. Doing so would not change the results of type inference
but would be disastrous for performance. In constrast, our system uses term
variables as a means of keeping first-class polymorphism tractable. Term
variables are used as placeholders for polymorphic types that we may
instantiate, which is why we require that the polymorphism in these types is
always fully determined. Flexible type variables can also become bound to
arbitrarily polymorphic types (e.g. during type inference for
$id~{}\lceil{id}\rceil$) but the quantifiers occurring in these types are
never instantiated during constraint solving, they can only be unified with
other quantifiers. By ensuring that all polymorphism in the term context is
fully known, we guarantee that we do not instantiate unknown polymorphism. On
the other hand, it does not appear possible to eliminate def constraints via
substitution or to define let constraints in terms of def, as in Pottier and
Rémy work.

###### Remark 5 (Itches we haven’t been able to scratch yet).

An alternative system without term variables in the constraint language should
be possible, in which case instantiation of quantifiers occuring in types
bound to type variables would need to take place. This would require an
additional mechanism to guarantee that the polymorphism of those type
variables that could be instantiated in this version is fixed. We haven’t
adopted this alternative design as we consider the current design that uses
term variables to be closer to Pottier and Rémy’s work and the original
version of FreezeML.

It also may be possible to recover the property that let and def constraints
canbe “expanded away”. One possibility (suggested by a reviewer) is to seek a
suitable adjustment of the notion of constraint inlining that accounts for
frozen constraints, perhaps by generalizing them to permit a local type
constraint ($\lceil{x:[C]A}\rceil$). As discussed in 6, allowing for full
constrained types in our setting poses challenges, and may also encounter
similar issues to those encountered in equational reasoning about FreezeML
terms, which was considered briefly by Emrich et al. (2020). This general
issue deserves further investigation.

Further discussion of these two issues, which are interrelated, is in an
appendix.

##  6\. Related Work

Constraint-based type inference for Hindley-Milner and related systems has a
long history (Wand, 1987). Some of the most relevant systems include qualified
types (Jones, 1994), HM($X$) (Odersky et al., 1999), OutsideIn($X$)
(Vytiniotis et al., 2011), and GI (Serrano et al., 2018) which present
increasingly sophisticated techniques for solving (generalisations of)
constraints generated from ML or Haskell-like programs. Our work differs in
building on HM($X$) as presented by Pottier and Rémy (2005), while adapting it
to support first-class polymorphism based on the FreezeML approach. On the
other hand, constraint-based FreezeML does not so far support constraint
solving parameterised by an arbitrary constraint domain $X$, and extending it
to support this is a natural but nontrivial next step. In particular, FreezeML
uses exactly System F types, rather than the type schemes with constraint
components of the form $\forall\overline{a}.C\Rightarrow A$ found in HM($X$).
We have compared our constraint solver to the HM($X$) solver by Pottier and
Rémy in Section 5.3.

FreezeML is also related to PolyML as explained by Emrich et al. (2020).
Unlike FreezeML, PolyML uses two different sorts of polymorphic types: ML-like
type schemes and first-class polymorphic types. The latter may only be
introduced with explicit type annotations. As a result, the conditions to pick
most general solutions in the semantics of certain constraints in our language
are not necessary in PolyML.

The type system of GI (Serrano et al., 2018) uses carefully crafted rules for
$n$-ary function applications, determining when arguments’ types may be
generalised or instantiated. It does not perform let generalisation. Its type
inference system is built on constraint solving, using a different approach
towards restricting polymorphism. It syntactically distinguishes three sorts
of unification variables, which may only be instantiated with monomorphic,
guarded, or fully polymorphic types. While our solver determines the order of
constraint solving using a stack, their system allows individual rules to be
blocked until progress has been made elsewhere, for example waiting until a
fully polymorphic variable has been substituted with a more concrete type.

QuickLook (Serrano et al., 2020) combines Hindley-Milner style type inference
with bidirectional type inference in a subtle way, and when typechecking
applications of polymorphically typed variables, performs a “quick look” at
all of the arguments; this amounts to a sound but shallow analysis whether
there is a unique type instantiation (possibly involving polymorphism). If
there is a unique type instantiation then that instantiation is chosen,
otherwise quantified variables are instantiated with monomorphic flexible
variables. Type inference for QuickLook follows a two-stage approach: all
first-class polymorphism is resolved at constraint generation time, and the
actual constraint solver does not have to find solutions for polymorphic type
variables. Consequently, their constraint language and solver are completely
standard and oblivious to first-class polymorphism. Thus, QuickLook requires
only small modifications to existing Haskell-style type inference, including
extensions such as qualified types and GADTs, but (like other recent proposals
such as GI) does not support let-bound polymorphism nor come with a formal
completeness result. In an appendix the authors discuss approaches to
supporting let generalisation; one is to use let constraints in the style of
Pottier and Rémy, and that is what we do.

Some aspects of our solver are reminiscent of the approach taken in Type
Inference in Context by Gundry et al. (2010), though their approach performs
type inference as a traversal of source language terms rather than introducing
an intermediate constraint language. We are interested in adapting their
approach to FreezeML type inference, particularly leveraging the insight that
type inference monotonically increases knowledge about possible solutions
(reflected in the structure of their contexts).

Returning to the motivation for this work mentioned in the introduction, it is
a natural to ask what obstacles remain to generalizing our system to handle an
arbitrary constraint domain (the “$X$” in HM($X$)). The immediate obstacle is
how to handle constrained or qualified types $C\Rightarrow A$ which are
considered equivalent up to reordering constraints $C$. Such types need not
induce, and depending on the theory $X$ such types may have equivalent forms
with different numbers of quantified types. Adopting the unordered
quantification approach in Section 5.2 could help with this, but we leave this
and the investigation of generalizing to a “FreezeML$(X)$” to future work.

##  7\. Conclusions

Emrich et al. (2020) recently introduced FreezeML, a new approach to ML-style
type inference that supports the full power of System F polymorphism using
type and term annotations to control instantiation and generalisation of
polymorphic types. Their initial type inference algorithm was a
straightforward extension of Algorithm W. We have introduced Constraint
FreezeML, an alternative constraint-based presentation of FreezeML type
inference, opening up many possibilities for extending FreezeML in the future.
We extended the constraint language of HM($X$) with suitable constraints,
equipped with a semantics and translation from FreezeML programs to
constraints that encode type inference problems, and presented a
deterministic, terminating state machine for solving the constraints. Several
potential next steps are opened by this work, including generalising to
support arbitrary constraint domains (the “$X$” in HM($X$)), implementing the
solver efficiently using ranks, and considering recursive types and higher
kinds.

###### Acknowledgements.

This work was supported by ERC Consolidator Grant Skye (grant number 682315)
and by an ISCF Metrology Fellowship grant provided by the UK government’s
Department for Business, Energy and Industrial Strategy (BEIS). Lindley is
supported by UKRI Future Leaders Fellowship “Effect Handler Oriented
Programming” (MR/T043830/1).

## References

  * (1)
  * Cooper et al. (2006) Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. 2006\.  Links: Web Programming Without Tiers. In _Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures_ _(Lecture Notes in Computer Science, Vol. 4709)_ , Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.). Springer, 266–296.  https://doi.org/10.1007/978-3-540-74792-5_12
  * Damas and Milner (1982) Luís Damas and Robin Milner. 1982.  Principal Type-Schemes for Functional Programs. In _POPL_. ACM Press, 207–212.
  * Emrich et al. (2020) Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates. 2020.  FreezeML: Complete and Easy Type Inference for First-class Polymorphism. In _PLDI_. ACM, 423–437.  Extended version available at https://doi.org/10.48550/arXiv.2004.00396.
  * Garrigue and Rémy (1999) Jacques Garrigue and Didier Rémy. 1999.  Semi-Explicit First-Class Polymorphism for ML.  _Inf. Comput._ 155, 1-2 (1999), 134–169.
  * Gundry (2015) Adam Gundry. 2015\.  A typechecker plugin for units of measure: domain-specific constraint solving in GHC Haskell. In _Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015_ , Ben Lippmeier (Ed.). ACM, 11–22.  https://doi.org/10.1145/2804302.2804305
  * Gundry et al. (2010) Adam Gundry, Conor McBride, and James McKinna. 2010\.  Type Inference in Context. In _MSFP@ICFP_. ACM, 43–54.
  * Jones (1994) Mark P. Jones. 1994\.  A Theory of Qualified Types.  _Sci. Comput. Program._ 22, 3 (1994), 231–256.  https://doi.org/10.1016/0167-6423(94)00005-0
  * Kennedy (2009) Andrew Kennedy. 2009\.  Types for Units-of-Measure: Theory and Practice. In _CEFP_ _(Lecture Notes in Computer Science, Vol. 6299)_. Springer, 268–305.
  * Kuan and MacQueen (2007) George Kuan and David MacQueen. 2007.  Efficient type inference using ranked type variables. In _ML_. ACM, 3–14.
  * Le Botlan and Rémy (2003) Didier Le Botlan and Didier Rémy. 2003.  ML${}^{\mbox{F}}$: raising ML to the power of System F. In _ICFP_. ACM, 27–38.
  * Leijen (2008) Daan Leijen. 2008\.  HMF: simple type inference for first-class polymorphism. In _ICFP_. ACM, 283–294.
  * Leijen (2014) Daan Leijen. 2014\.  Koka: Programming with Row Polymorphic Effect Types. In _MSFP_ _(EPTCS, Vol. 153)_. 100–126.
  * Leroy and Mauny (1991) Xavier Leroy and Michel Mauny. 1991.  Dynamics in ML. In _FPCA_. Springer, 406–426.
  * Lindley and Cheney (2012) Sam Lindley and James Cheney. 2012.  Row-based effect types for database integration. In _TLDI_. ACM, 91–102.
  * McBride and Paterson (2008) Conor McBride and Ross Paterson. 2008.  Applicative programming with effects.  _J. Funct. Program._ 18, 1 (2008), 1–13.  https://doi.org/10.1017/S0956796807006326
  * Morris and McKinna (2019) J. Garrett Morris and James McKinna. 2019.  Abstracting extensible data types: or, rows by any other name.  _Proc. ACM Program. Lang._ 3, POPL (2019), 12:1–12:28.
  * Odersky et al. (1999) Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999\.  Type Inference with Constrained Types.  _Theory Pract. Object Syst._ 5, 1 (1999), 35–55.
  * Pfenning (1993) Frank Pfenning. 1993\.  On the Undecidability of Partial Polymorphic Type Reconstruction.  _Fundam. Inform._ 19, 1/2 (1993), 185–199.
  * Pottier (2014) François Pottier. 2014\.  Hindley-Milner Elaboration in Applicative Style: Functional Pearl. In _ICFP_. ACM, 203–212.
  * Pottier and Rémy (2005) François Pottier and Didier Rémy. 2005.  _The Essence of ML Type Inference_.  MIT Press, Chapter 10, 389–489.
  * Rémy (1992) Didier Rémy. 1992\.  _Extension of ML Type System with a Sorted Equational Theory on Types_.  Technical Report RR-1766. Institut National de Recherche en Informatique et en Automatique.
  * Russo and Vytiniotis (2009) Claudio V. Russo and Dimitrios Vytiniotis. 2009.  QML: Explicit First-class Polymorphism for ML. In _ML_. ACM, 3–14.
  * Serrano et al. (2020) Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020.  A quick look at impredicativity.  _Proc. ACM Program. Lang._ 4, ICFP (2020), 89:1–89:29.  https://doi.org/10.1145/3408971
  * Serrano et al. (2018) Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018\.  Guarded impredicative polymorphism. In _PLDI_. ACM, 783–796.
  * Simonet and Pottier (2007) Vincent Simonet and François Pottier. 2007.  A constraint-based approach to guarded algebraic data types.  _ACM Trans. Program. Lang. Syst._ 29, 1 (2007), 1\.  https://doi.org/10.1145/1180475.1180476
  * Vytiniotis et al. (2011) Dimitrios Vytiniotis, Simon L. Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011.  OutsideIn(X): Modular type inference with local assumptions.  _J. Funct. Program._ 21, 4-5 (2011), 333–412.
  * Vytiniotis et al. (2006) Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. 2006.  Boxy types: inference for higher-rank types and impredicativity. In _ICFP_. ACM, 251–262.
  * Wand (1987) Mitchell Wand. 1987\.  A simple algorithm and proof for type inference.  _Fundamenta Informaticae_ (1987).
  * Wells (1994) J. B. Wells. 1994\.  Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable. In _LICS_. IEEE Computer Society, 176–185.
  * Wright (1995) Andrew K. Wright. 1995\.  Simple Imperative Polymorphism.  _LISP Symb. Comput._ 8, 4 (1995), 343–355.

##  Appendix A Proofs for Section 3.4

The proofs of Theorems 1 and 2 proceed via mutual induction on the structure
of the term $M$. Both proofs use the following lemma, but only on subterms of
the term $M$ in question.

###### Lemma 9.

Let $\Delta^{\prime}=\mathsf{ftv}(A)-\Delta$ and $\Delta;\Gamma\vdash M\
\mathbf{ok}$. Then $\mathsf{principal}(\Delta,\Gamma,M,\Delta^{\prime},A)$ iff
$\mathsf{mostgen}(\Delta,\allowbreak(a),\allowbreak\Gamma,\allowbreak\llbracket
M:a\rrbracket,\Delta^{\prime},[a\mapsto A])$.

The proof of Lemma 9 in turn uses both theorems directly.

We proceed by collecting auxiliary lemmas (including Lemma 9) in Section A.1.
The two subsequent subsections contain the proofs of Theorem 1, Theorem 2,
respectively.

###  A.1. Auxiliary Lemmas

###### Lemma 10.

Let $M\in\mathsf{GVal}$ and
$\mathsf{principal}(\Delta,\Gamma,M,\Delta^{\prime},A)$. Then $A$ is a guarded
type.

###### Proof.

The only way for $A$ to be a top-level polymorphic type of a guarded value $M$
is if $M$ is a plain (i.e, not frozen) variable $x$ of type $\forall
a_{0},\dotsc,a_{n}.a_{i}$. However, the _principal_ type of $x$ is $a$ for
some fresh polymorphic variable $a\in\Delta^{\prime}$, which is a guarded
type. ∎

###### Lemma 11 (Well-formedness of constraint translation).

Let $\Delta;\Gamma\vdash M\ \mathbf{ok}$ and $(\Delta,\Xi)\vdash A\
\mathbf{ok}$. Then $\Delta;\Xi;\Gamma\vdash\llbracket M:A\rrbracket\
\mathbf{ok}$ holds.

###### Proof.

By induction on structure of $M$. We observe that the only free type variables
of $\llbracket M:A\rrbracket$ are those appearing freely in $A$ and in type
annotations appearing in $M$. By $\Delta;\Gamma\vdash M:A$ we have that all
such free type variables in the annotations in $M$ are rigid variables from
$\Delta$. Hence, the only free unification variables of $\llbracket
M:A\rrbracket$ are those in $A$.

∎

###### Lemma 12 (Satisfiability implies well-formedness).

If $\Delta;\Xi;\Gamma;\delta\vdash C$ then $\Delta;\Xi;\Gamma\vdash C\
\mathbf{ok}$.

###### Proof.

We observe that the rules Sem-Equiv, Sem-Freeze, Sem-Inst Sem-Def all
(explicitly or implicitly) require the types found in the constraint under
consideration to be well-formed in the context $\Delta;\Xi$. The rule Sem-Mono
imposes $a\in(\Delta,\Xi)$. Finally, the rules Sem-Freeze, Sem-Inst require
$x\in\Gamma$. ∎

See the note at the beginning of Appendix A, for an explanation of the
dependencies between Theorem 1, Theorem 2 and Lemma 9.

See 9

###### Proof.

Recall the definitons of $\mathsf{principal}$ and $\mathsf{mostgen}$:

$\displaystyle\mathsf{principal}(\Delta,\Gamma,M,\Delta^{\prime},A)=$ (1)
$\displaystyle\qquad\Delta,\Delta^{\prime};\Gamma\vdash M:A\;\text{ and }$ (2)
$\displaystyle\begin{aligned} \qquad(\text{for all
}\Delta^{\prime\prime},A^{\prime\prime}\mid\begin{array}[t]{@{}l@{}}\text{if
}\Delta,\Delta^{\prime\prime};\Gamma\vdash M:A^{\prime\prime}\\\ \text{then
there exists }\delta\text{ such that }\\\
\;\Delta\vdash\delta:\Delta^{\prime}\Rightarrow_{\star}\Delta^{\prime\prime}\text{
and }\delta(A)=A^{\prime\prime})\end{array}\end{aligned}$

$\displaystyle\mathsf{mostgen}(\Delta,a,\Gamma,\delta,\llbracket
M:a\rrbracket,\Delta^{\prime},[a\mapsto A])=$ (3)
$\displaystyle\qquad(\Delta,\Delta^{\prime});a;\Gamma;[a\mapsto
A]\vdash\llbracket M:a\rrbracket\;\text{ and }\;$ (4)
$\displaystyle\qquad\begin{aligned} (\text{for all
}\Delta^{\prime\prime},\delta^{\prime\prime}\mid\begin{array}[t]{@{}l@{}}\text{if
}(\Delta,\Delta^{\prime\prime});a;\Gamma;\delta^{\prime\prime}\vdash\llbracket
M:a\rrbracket\\\ \text{then there exists }\delta\text{ such that }\\\
\;\Delta\vdash\delta:\Delta^{\prime}\Rightarrow_{\star}\Delta^{\prime\prime}\text{
and }\delta^{\prime\prime}=\delta\circ[a\mapsto A])\\\ \end{array}\\\
\end{aligned}$

  * $\mathbf{\Rightarrow}$

We apply Theorem 1 to $(\ref{proof:principal-vs-mostgen:principal-part-one})$,
immediately yielding the desired property $(\ref{proof:principal-vs-
mostgen:mostgen-part-one})$.

To show $(\ref{proof:principal-vs-mostgen:mostgen-part-two})$, we assume
$(\Delta,\Delta^{\prime\prime});a;\Gamma;\delta^{\prime\prime}\vdash\llbracket
M:a\rrbracket$, which implies that $\delta^{\prime\prime}=[a\mapsto
A^{\prime\prime}]$ for some $A^{\prime\prime}$.

By Theorem 2 this gives us $(\Delta,\Delta^{\prime\prime});\Gamma\vdash
M:A^{\prime\prime}$. According to $(\ref{proof:principal-vs-mostgen:principal-
part-two})$, there exists a $\delta$ with the desired properties.

  * $\mathbf{\Leftarrow}$

We apply Theorem 2 to (3), which gives us satisfaction of property
$(\ref{proof:principal-vs-mostgen:principal-part-one})$.

To show (4), we assume $\Delta,\Delta^{\prime\prime};\Gamma\vdash
M:A^{\prime\prime}$. Theorem 1 then gives us
$(\Delta,\Delta^{\prime\prime});a;\Gamma;[a\mapsto
A^{\prime\prime}]\vdash\llbracket M:a\rrbracket$. According to
$(\ref{proof:principal-vs-mostgen:mostgen-part-two})$ there exists an
appropriate $\delta$.

∎

###  A.2. Proof of Theorem 1

See 1

###### Proof.

By structural induction on $M$, focusing on the let cases.

Case ${\rm{\bf let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$, where
$M^{\prime}\in\mathsf{GVal}$:

The derivation of $\Delta;\Gamma\vdash M:A$ has the following form, for some
$B,B^{\prime},\overline{a}$.

$\inferrule{\overline{a}=\mathsf{ftv}(B^{\prime})-\Delta\\\
(\Delta,\overline{a},M^{\prime},B^{\prime})\Updownarrow B\\\
(\Delta,\tilde{a});\Gamma\vdash M^{\prime}:B^{\prime}\\\
\Delta;\Gamma,x:B\vdash N:A\\\
\mathsf{principal}(\Delta,\Gamma,M^{\prime},\tilde{a},B^{\prime})}{\Delta;\Gamma\vdash{\rm{\bf
let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N:A}$

By $M^{\prime}\in\mathsf{GVal}$ we have $B=\forall\overline{a}.B^{\prime}$ and
$\llbracket M:a\rrbracket={\rm{\bf let}}_{\star}\;x=\sqcap b.\llbracket
M^{\prime}:b\rrbracket\;{\rm{\bf in}}\;\llbracket N^{\prime}:a\rrbracket$. We
assume w.l.o.g. that $b\mathop{\\#}(\Delta,\tilde{a})$. By induction we have
$(\Delta,\tilde{a});b;\Gamma;[b\mapsto B^{\prime}]\vdash\llbracket
M^{\prime}:b\rrbracket$ and $\Delta;a;(\Gamma,x:B);[a\mapsto
A]\vdash\llbracket N^{\prime}:a\rrbracket$. We can weaken the former to
$(\Delta,\tilde{a});(a,b);\Gamma;[a\mapsto A,b\mapsto
B^{\prime}]\vdash\llbracket M^{\prime}:b\rrbracket$. By Lemma 9,
$\mathsf{principal}(\Delta,\Gamma,M^{\prime},\tilde{a},B^{\prime})$ implies
$\mathsf{mostgen}(\Delta,b,\Gamma,\llbracket
M^{\prime}:b\rrbracket,\tilde{a},[b\mapsto B^{\prime}])$. According to Lemma
17 we can weaken this to $\mathsf{mostgen}(\Delta,(a,b),\Gamma,\llbracket
M^{\prime}:b\rrbracket,(\tilde{a},c),[a\mapsto c,b\mapsto B^{\prime}])$ for
some fresh $c$.

Let $\Delta_{\mathrm{o}}\coloneqq c$ and
$\delta^{\prime}\coloneqq[c\mapsto\mathsf{unit}]$ and
$\delta_{\mathrm{m}}=[a\mapsto c,b\mapsto B^{\prime}]$. Due to
$c\not\in\mathsf{ftv}(B^{\prime})$ we have
$\delta^{\prime}(\delta(b))=\delta(B^{\prime})=B^{\prime}$.

We can then derive the following

$\inferrule{\mathsf{mostgen}(\Delta,(a,b),\Gamma,\llbracket
M^{\prime}:b\rrbracket,(\tilde{a},c),\delta_{\mathrm{m}})\\\ \\\
\Delta_{\mathrm{o}}=\mathsf{ftv}(\delta_{\mathrm{m}}(a))-\Delta\\\
\overline{a}=\mathsf{ftv}(\delta_{\mathrm{m}}(b))-\Delta,\Delta_{\mathrm{o}}\\\
\\\
\Delta\vdash\delta^{\prime}:\Delta_{\mathrm{o}}\Rightarrow_{\mathord{\bullet}}\cdot\\\
B^{\prime}=\delta^{\prime}(\delta_{\mathrm{m}}(b))\\\ \\\
(\Delta,\tilde{a});(a,b);\Gamma;\delta[a\mapsto A,b\mapsto
B^{\prime}]\vdash\llbracket M^{\prime}:b\rrbracket\\\
\Delta;a;(\Gamma,x:B);\delta\vdash\llbracket
N^{\prime}:a\rrbracket}{\Delta;a;\Gamma;[a\mapsto A]\vdash{\rm{\bf
let}}_{\star}\;x=\sqcap b.\llbracket M^{\prime}:b\rrbracket\;{\rm{\bf
in}}\;\llbracket N^{\prime}:a\rrbracket}$

Case ${\rm{\bf let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$, where
$M^{\prime}\not\in\mathsf{GVal}$:

We have a derivation of the same shape as in the previous case. However, by
$M^{\prime}\not\in\mathsf{GVal}$ we have $B=\delta(B^{\prime})$ and
$\llbracket M:a\rrbracket={\rm{\bf let}}_{\mathord{\bullet}}\;x=\sqcap
b.\llbracket M^{\prime}:b\rrbracket\;{\rm{\bf in}}\;\llbracket
N^{\prime}:a\rrbracket$, for some $\delta$ such that
$\Delta\vdash\delta:\tilde{a}\Rightarrow_{\mathord{\bullet}}\cdot$.

Let $\Delta_{\mathrm{o}}$ and $\delta_{\mathrm{m}}$ as in the previous case
and extend $\delta$ to $\delta^{\prime}$ by setting $\delta^{\prime}(a)=c$.
This implies
$B=\delta(B^{\prime})=\delta^{\prime}(B^{\prime})=\delta(\delta_{\mathrm{m}}(b))$.

We also extend $\delta$ to $\delta^{\prime\prime}$ by setting
$\delta^{\prime\prime}(a^{\prime})=a^{\prime}$ for all $a^{\prime}\in\Delta$.

Using similar reasoning as in the previous case we get
$\mathsf{mostgen}(\Delta,(a,b),\Gamma,\llbracket
M^{\prime}:b\rrbracket,(\tilde{a},c),\delta_{\mathrm{m}})$,
$\Delta;a;(\Gamma,x:B);[a\mapsto A]\vdash\llbracket N^{\prime}:a\rrbracket$,
and $(\Delta,\tilde{a});a;\Gamma;[a\mapsto A,b\mapsto
B^{\prime}]\vdash\llbracket M^{\prime}:b\rrbracket$. Applying Lemma 18 to the
latter using $\delta^{\prime\prime}$ yields
$\Delta;(a,b);\delta^{\prime\prime}(\Gamma);[a\mapsto\delta^{\prime\prime}(A),b\mapsto\delta^{\prime\prime}(B^{\prime})]\vdash\llbracket
M^{\prime}:b\rrbracket$, which is equivalent to $\Delta;(a,b);\Gamma;[a\mapsto
A,b\mapsto B]\vdash\llbracket M^{\prime}:b\rrbracket$,

We can then derive the following

$\inferrule{\mathsf{mostgen}(\Delta,(a,b),\Gamma,\llbracket
M^{\prime}:b\rrbracket,(\tilde{a},c),\delta_{\mathrm{m}})\\\ \\\
\Delta\vdash\delta^{\prime}:(\tilde{a},c)\Rightarrow_{\mathord{\bullet}}\cdot\\\
B=\delta^{\prime}(\delta_{\mathrm{m}}(a))\\\ \\\
\Delta;(a,b);\Gamma;\delta[b\mapsto B]\vdash\llbracket
M^{\prime}:b\rrbracket\\\ \Delta;a;(\Gamma,x:B);\delta\vdash\llbracket
N^{\prime}:a\rrbracket}{\Delta;a;\Gamma;[a\mapsto A]\vdash{\rm{\bf
let}}_{\mathord{\bullet}}\;x=\sqcap b.\llbracket
M^{\prime}:b\rrbracket\;{\rm{\bf in}}\;\llbracket N^{\prime}:a\rrbracket}$

Case ${\rm{\bf let}}(x:B)=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$, where
$M^{\prime}\in\mathsf{GVal}$::

Let $\overline{a}$, $H$ such that $B=\forall\overline{a}.H$.

The derivation of $\Delta;\Gamma\vdash M^{\prime}:A$ has the following form,
for some $\Delta^{\prime},A^{\prime}$:

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

By $M^{\prime}\in\mathsf{GVal}$, we have $\Delta^{\prime}=\tilde{a}$,
$B^{\prime}=H$ and $\llbracket M:A\rrbracket=(\forall\overline{a}.\llbracket
M^{\prime}:H\rrbracket)\wedge{\rm{\bf def}}\;(x:B)\;{\rm{\bf in}}\;\llbracket
N^{\prime}:A\rrbracket$. Let $b$ be fresh. By induction, we have
$(\Delta,\Delta^{\prime});b;\Gamma;[b\mapsto B^{\prime}]\vdash\llbracket
M^{\prime}:b\rrbracket$ and $\Delta;a;(\Gamma,x:B);[a\mapsto
A]\vdash\llbracket N^{\prime}:A\rrbracket$. By Lemma 19 we can substitute the
former to $(\Delta,\Delta^{\prime});\cdot;\Gamma;\emptyset\vdash\llbracket
M^{\prime}:H\rrbracket$.

Recall that an implicit precondition of $\Delta;(\Gamma,x:B)\vdash
N^{\prime}:A$ we have $\Delta\vdash\Gamma\ \mathbf{ok}$, which implies
$\Delta\vdash B\ \mathbf{ok}$. Therefore, we have that
$\mathsf{ftv}(B)-\Delta$ is empty and $B[a/A]=B$.

We can now derive the desired judgement.

$\inferrule*{\inferrule*{\inferrule*{(\Delta,\Delta^{\prime});a;\Gamma;[a\mapsto
A]\vdash\llbracket M^{\prime}:H\rrbracket}{\vdots}}{\Delta;a;\Gamma;[a\mapsto
A]\vdash(\forall\overline{a}.\llbracket M^{\prime}:H\rrbracket)}\\\
\inferrule*{\text{for all
}a\in\mathsf{ftv}(B)-\Delta\;\mid\;\Delta;\Xi;\Gamma;\delta\vdash\mathsf{mono}(a)\\\
\\\ \Delta;\Xi;(\Gamma,x:B[a/A]);\delta\vdash C}{\Delta;a;\Gamma;[a\mapsto
A]\vdash{\rm{\bf def}}\;(x:B)\;{\rm{\bf in}}\;\llbracket
N^{\prime}:A\rrbracket}}{\Delta;a;\Gamma;[a\mapsto
A]\vdash(\forall\overline{a}.\llbracket M^{\prime}:H\rrbracket)\wedge{\rm{\bf
def}}\;(x:B)\;{\rm{\bf in}}\;\llbracket N^{\prime}:A\rrbracket}$

Case ${\rm{\bf let}}(x:A)=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$, where
$M^{\prime}\not\in\mathsf{GVal}$::

Analogous to previous case, with $\Delta^{\prime}=\emptyset$, $B^{\prime}=B$.

∎

###  A.3. Proof of Theorem 2

See 2

###### Proof.

We prove the following, slightly more general property by induction on $M$: If
$\Delta;\Gamma\vdash M\ \mathbf{ok}$ and $\Delta;\Xi\vdash A\ \mathbf{ok}$ and
$\Delta;\Xi;\Gamma;\delta\vdash\llbracket M:A\rrbracket$, then
$\Delta;\Gamma\vdash M:\delta(A)$.

Note that by the implicit preconditions of
$\Delta;\Xi;\Gamma;\delta\vdash\llbracket M:A\rrbracket$ we have
$\Delta\mathop{\\#}\Xi$, $\Delta\vdash\Gamma\ \mathbf{ok}$, and
$\Delta\vdash\delta:\Xi\Rightarrow_{\star}\cdot$. The latter implies
$\Delta\vdash\delta(A)\ \mathbf{ok}$.

We focus on the let cases.

Case ${\rm{\bf let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$,
$M^{\prime}\in\mathsf{GVal}$::

We have $\Delta;\Xi;\Gamma;\delta\vdash{\rm{\bf let}}_{\star}\;x=\sqcap
b.\llbracket M^{\prime}:b\rrbracket\;{\rm{\bf in}}\;\llbracket
N^{\prime}:A\rrbracket$. The derivation of this has the following form for
some
$B,\overline{a},\Delta_{\mathrm{m}},\Delta_{\mathrm{o}},\delta_{\mathrm{m}}$
and $\delta^{\prime}$:

$\inferrule{\mathsf{mostgen}(\Delta,(\Xi,b),\Gamma,\llbracket
M^{\prime}:b\rrbracket,\Delta_{\mathrm{m}},\delta_{\mathrm{m}})\\\ \\\
\Delta_{\mathrm{o}}=\mathsf{ftv}(\delta_{\mathrm{m}}(\Xi))-\Delta\\\
\overline{a}=\mathsf{ftv}(\delta_{\mathrm{m}}(b))-\Delta,\Delta_{\mathrm{o}}\\\
\\\
\Delta\vdash\delta^{\prime}:\Delta_{\mathrm{o}}\Rightarrow_{\mathord{\bullet}}\cdot\\\
B=\delta^{\prime}(\delta_{\mathrm{m}}(b))\\\ \\\
(\Delta,\tilde{a});(\Xi,b);\Gamma;\delta[b\mapsto B]\vdash\llbracket
M^{\prime}:b\rrbracket\\\
\Delta;\Xi;(\Gamma,x:\forall\overline{a}.B);\delta\vdash\llbracket
N^{\prime}:A\rrbracket}{\Delta;\Xi;\Gamma;\delta\vdash{\rm{\bf
let}}_{\star}\;x=\sqcap b.\llbracket M^{\prime}:b\rrbracket\;{\rm{\bf
in}}\;\llbracket N^{\prime}:A\rrbracket}$

By induction, this gives us $(\Delta,\tilde{a});\Gamma\vdash M^{\prime}:B$ and
$\Delta;(\Gamma,x:\forall\overline{a}.B)\vdash N^{\prime}:\delta(A)$. By
$M^{\prime}\in\mathsf{GVal}$, we have $\Delta\vdash M^{\prime}$ and
$\Delta\vdash\Gamma$. According to Lemma 11 this implies
$\Delta;b;\Gamma\vdash\llbracket M^{\prime}:b\rrbracket\ \mathbf{ok}$ (i.e.,
$b$ is the only free flexible variable of $\llbracket
M^{\prime}:b\rrbracket$). This means that $\llbracket M^{\prime}:b\rrbracket$
leaves all variables of $\Xi$ entirely unconstrained. Therefore, we have that
$\delta_{\mathrm{m}}$ maps all $a\in\Xi$ to pairwise different variables $c$
from $\Delta_{\mathrm{m}}$ and $c\not\in\mathsf{ftv}(\delta_{\mathrm{m}}(b))$
for all such $c$. This implies
$\overline{a}=\mathsf{ftv}(\delta_{\mathrm{m}}(b))-\Delta,\Delta_{\mathrm{o}}=\mathsf{ftv}(\delta_{\mathrm{m}}(b))-\Delta,\Delta_{\mathrm{o}}$
(i.e., removing $\Delta_{\mathrm{o}}$ from the subtracted context has no
effect) and $B=\delta_{\mathrm{m}}(b)$ (i.e., applying $\delta^{\prime}$ to
$\delta_{\mathrm{m}}(b)$ has no effect).

Consequently, we may strengthen
$\mathsf{mostgen}(\Delta,(\Xi,b),\Gamma,\llbracket
M^{\prime}:b\rrbracket,\Delta_{\mathrm{m}},\delta_{\mathrm{m}})$ to
$\mathsf{mostgen}(\Delta,b,\Gamma,\llbracket
M^{\prime}:b\rrbracket,\tilde{a},[b\mapsto\delta_{\mathrm{m}}(b)])$. We may
then apply Lemma 9 to the latter, yielding
$\mathsf{principal}(\Delta,\Gamma,M^{\prime},\tilde{a},B)$. Finally, Lemma 10
shows us that $B$ is a guarded type, and we may refer to it as $H$.

We can therefore derive the desired property $\Delta;\Gamma\vdash{\rm{\bf
let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}:\delta(A)$ as follows:

$\inferrule*{\overline{a}=\mathsf{ftv}(H)-\Delta\\\
(\Delta,\overline{a},M^{\prime},H)\Updownarrow\forall\overline{a}.H\\\
(\Delta,\tilde{a});\Gamma\vdash M^{\prime}:H\\\
\Delta;(\Gamma,x:\forall\overline{a}.H)\vdash N^{\prime}:\delta(A)\\\ \\\
\mathsf{principal}(\Delta,\Gamma,M^{\prime},\tilde{a},H)}{\Delta;\Gamma\vdash{\rm{\bf
let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}:\delta(A)}$

Case ${\rm{\bf let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$ if
$M^{\prime}\not\in\mathsf{GVal}$::

This case is largely analogous to the previous one.

This time we have a derivation of the form:

$\inferrule{\mathsf{mostgen}(\Delta,(\Xi,a),\Gamma,\llbracket
M^{\prime}:b\rrbracket,\Delta_{\mathrm{m}},\delta_{\mathrm{m}})\\\ \\\
\Delta\vdash\delta^{\prime}:\Delta_{\mathrm{m}}\Rightarrow_{\mathord{\bullet}}\cdot\\\
B=\delta^{\prime}(\delta_{\mathrm{m}}(b))\\\ \\\
\Delta;(\Xi,a);\Gamma;\delta[b\mapsto B]\vdash\llbracket
M^{\prime}:b\rrbracket\\\ \Delta;\Xi;(\Gamma,x:B);\delta\vdash\llbracket
N^{\prime}:A\rrbracket}{\Delta;\Theta;\Gamma;\delta\vdash{\rm{\bf
let}}_{\mathord{\bullet}}\;x=\sqcap b.\llbracket
M^{\prime}:b\rrbracket\;{\rm{\bf in}}\;\llbracket N^{\prime}:A\rrbracket}$

Let $A^{\prime}\coloneqq\delta_{\mathrm{m}}(b)$ and
$\overline{a}\coloneqq\mathsf{ftv}(A^{\prime})-\Delta$. By
$\mathsf{mostgen}(\Delta,(\Xi,a),\Gamma,\llbracket
M^{\prime}:b\rrbracket,\Delta_{\mathrm{m}},\delta_{\mathrm{m}})$ we have
$(\Delta,\Delta_{\mathrm{m}});(\Xi,a);\Gamma;\delta_{\mathrm{m}}\vdash\llbracket
M^{\prime}:b\rrbracket$. By induction, this implies
$(\Delta,\Delta_{\mathrm{m}});\Gamma\vdash M^{\prime}:A^{\prime}$, which we
can strengthen to $(\Delta,\tilde{a});\Gamma\vdash M^{\prime}:A^{\prime}$

We obtain $\Delta;(\Gamma,x:B)\vdash\delta(A)$ directly by applying the
induction hypothesis to $\Delta;\Xi;(\Gamma,x:B);\delta\vdash\llbracket
N^{\prime}:A\rrbracket$. Likewise, we obtain
$\mathsf{principal}(\Delta,\Gamma,M^{\prime},\tilde{a},A^{\prime})$ using the
same reasoning as in the previous case.

Finally, we observe that
$\Delta\vdash{\delta^{\prime}}\mathord{\upharpoonright}_{\tilde{a}}:\tilde{a}\Rightarrow\cdot$
holds and
$B={\delta^{\prime}}\mathord{\upharpoonright}_{\tilde{a}}(A^{\prime})$.
Therefore, we have $(\Delta,\overline{a},M,A^{\prime})\Updownarrow B$

Thus, we can derive the following:

$\inferrule*{\overline{a}=\mathsf{ftv}(A^{\prime})-\Delta\\\
(\Delta,\overline{a},M,A^{\prime})\Updownarrow B\\\
\Delta,\tilde{a};\Gamma\vdash M:A^{\prime}\\\ \Delta;\Gamma,x:A\vdash
N:\delta(A)\\\
\mathsf{principal}(\Delta,\Gamma,M,\tilde{a},A^{\prime})}{\Delta;\Gamma\vdash{\rm{\bf
let}}\;x=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}:\delta(A)}$

Case ${\rm{\bf let}}\;(x:B)=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$ if
$M^{\prime}\in\mathsf{GVal}$::

Let $\overline{b}$ and $H$ such that $B=\forall\overline{b}.H$.

We then have $\Delta;\Xi;\Gamma;\delta\vdash(\forall\overline{b}.\llbracket
M^{\prime}:H\rrbracket)\;\wedge\;{\rm{\bf def}}\;(x:B)\;{\rm{\bf
in}}\;\llbracket N^{\prime}:A\rrbracket$. The derivation tree of this contains
derivations for $(\Delta,\tilde{b});\Xi;\Gamma;\delta\vdash\llbracket
M^{\prime}:H\rrbracket$ and
$\Delta;\Xi;(\Gamma,x:\delta(B));\delta\vdash\llbracket
N^{\prime}:A\rrbracket$.

By $\Delta;\Gamma\vdash M\ \mathbf{ok}$ we have $\Delta\vdash B$ (i.e., $B$
contains no flexible variables). Therefore, $\delta(B)=B$ and $\delta(H)=H$.
By induction, this then gives us $(\Delta,\tilde{a});\Gamma\vdash
M^{\prime}:H$ and $\Delta;(\Gamma,x:B)\vdash N^{\prime}:\delta(A)$.

Hence, we can derive

$\inferrule*{(\tilde{a},H)=\mathsf{split}(B,M^{\prime})\\\
(\Delta,\tilde{a});\Gamma\vdash M^{\prime}:H\\\ \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)}$

Case ${\rm{\bf let}}\;(x:B)=M^{\prime}\;{\rm{\bf in}}\;N^{\prime}$ if
$M^{\prime}\not\in\mathsf{GVal}$:

This case is similar to the previous one: We have
$\Delta;\Xi;\Gamma;\delta\vdash\llbracket
M^{\prime}:B\rrbracket)\;\wedge\;{\rm{\bf def}}\;(x:B)\;{\rm{\bf
in}}\;\llbracket N^{\prime}:A\rrbracket$ this time and $\delta(B)=B$ due to
$\Delta;\Gamma\vdash M\ \mathbf{ok}$.

We get $\Delta;\Gamma\vdash M^{\prime}:B$ and $\Delta;(\Gamma,x:B)\vdash
N^{\prime}:\delta(A)$ by induction and can derive