# A. Appendix

In this Appendix, we present full definitions of the language and type systems we have described, together with complete proofs of all results.

## A.1 The language of polymorphic variants

### A.1.1 Syntax

We assume that there exist a countable set $\mathcal{X}$ of expression variables, ranged over by $x, y, z, \dots$, a set $\mathcal{C}$ of constants, ranged over by $c$, and a set $\mathcal{L}$ of tags, ranged over by `tag`.

**Definition A.1 (Expressions).** An expression $e$ is a term inductively generated by the following grammar:

$$e ::= x \mid c \mid \lambda x.e \mid e e \mid (e, e) \mid \text{'tag}(e) \mid \text{match } e \text{ with } (p_i \to e_i)_{i \in I}$$

where $p$ ranges over the set $\mathcal{P}$ of patterns, defined below. We write $\mathcal{E}$ to denote the set of all expressions.

We define $fv(e)$ to be the set of expression variables occurring free in the expression $e$, and we say that $e$ is closed if and only if $fv(e)$ is empty.

As customary, we consider expressions up to $\alpha$-renaming of the variables bound by abstractions and by patterns.

**Definition A.2 (Patterns).** A pattern $p$ is a term inductively generated by the following grammar:

$$p ::= \_ | x | c | (p, p) | \text{'tag}(p) | p \& p | p | p$$

such that

* in a pair pattern $(p_1, p_2)$ or an intersection pattern $p_1 \& p_2$, $capt(p_1) \cap capt(p_2) = \emptyset$;

* in a union pattern $p_1|p_2$, $capt(p_1) = capt(p_2)$,

where $capt(p)$ denotes the set of expression variables occurring as sub-terms in a pattern $p$ (called the capture variables of $p$).

We write $\mathcal{P}$ to denote the set of all patterns.

### A.1.2 Semantics

**Definition A.3 (Values).** A value $v$ is a closed expression inductively generated by the following grammar.

$$v ::= c \mid \lambda x.e \mid (v, v) \mid \text{'tag}(v)$$

**Definition A.4 (Expression substitution).** An expression substitution $\zeta$ is a partial mapping of expression variables to values. We write $[v_i/x_i \mid i \in I]$ for the substitution which replaces free occurrences of $x_i$ with $v_i$, for each $i \in I$. We write $e_\zeta$ for the application of the substitution to an expression $e$. We write $\zeta_1 \cup \zeta_2$ for the union of disjoint substitutions.

**Definition A.5 (Semantics of pattern matching).** We write $v/p$ for the result of matching a value $v$ against a pattern $p$. We have either $v/p = \zeta$, where $\zeta$ is a substitution defined on the variables in $capt(p)$, or $v/p = \Omega$. In the former case, we say that $v$ matches $p$ (or that $p$ accepts $v$); in the latter, we say that matching fails.

The definition of $v/p$ is given inductively in Figure 6.

**Definition A.6 (Evaluation contexts).** Let the symbol $[]$ denote a hole. An evaluation context $E$ is a term inductively generated by the following grammar.

$$E ::= [] | E e | v E | (E, e) | (v, E) \mid \text{'tag}(E) \mid \text{match } E \text{ with } (p_i \to e_i)_{i \in I}$$

We write $E[e]$ for the expression obtained by replacing the hole in $E$ with the expression $e$.

**Definition A.7 (Reduction).** The reduction relation $\rightsquigarrow$ between expressions is given by the rules in Figure 7.

## A.2 Typing variants with kinding constraints

### A.2.1 Definition of the $\mathbb{K}$ type system

We assume that there exists a countable set $\mathcal{V}$ of type variables, ranged over by $\alpha, \beta, \gamma, \dots$. We also consider a finite set $\mathcal{B}$ of basic types, ranged over by $b$, and a function $b(\cdot)$ from constants to basic types.

**Definition A.8 (Types).** A type $\tau$ is a term inductively generated by the following grammar.

$$\tau ::= \alpha \mid b \mid \tau \to \tau \mid \tau \times \tau$$
References

V. Benzaken, G. Castagna, and A. Frisch. CDuce: an XML-centric general-purpose language. In *ACM SIGPLAN International Conference on Functional Programming (ICFP)*, pages 51–63, 2003.

M. Blume, U. A. Acar, and W. Chae. Exception handlers as extensible cases. In *Proceedings of the 6th Asian Symposium on Programming Languages and Systems (APLAS)*, LNCS, pages 273–289. Springer, 2008.

M. Bonsangue, J. Rot, D. Ancona, F. de Boer, and J. Rutten. A coalgebraic foundation for coinductive union types. In *Automata, Languages, and Programming - 41st International Colloquium (ICALP)*, volume 8573 of *Lecture Notes in Computer Science*, pages 62–73. Springer, 2014.

G. Castagna and Z. Xu. Set-theoretic foundation of parametric polymorphism and subtyping. In *ACM SIGPLAN International Conference on Functional Programming (ICFP)*, pages 94–106, 2011.

G. Castagna, K. Nguyễn, Z. Xu, H. Im, S. Lenglet, and L. Padovani. Polymorphic functions with set-theoretic types. part 1: Syntax, semantics, and evaluation. In *ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)*, pages 5–17, 2014.

G. Castagna, K. Nguyễn, Z. Xu, and P. Abate. Polymorphic functions with set-theoretic types. part 2: Local type inference and type reconstruction. In *ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)*, pages 289–302, 2015.

CDuce. http://www.cduce.org.

[CAML-LIST 1]. Polymorphic variant difference. https://goo.gl/W1PgdY, May 2007. OCaml mailing list post.

[CAML-LIST 2]. Variant filtering. https://goo.gl/d7DQhU, Feb. 2000. OCaml mailing list post.

[CAML-LIST 3]. Polymorphic variant typing. https://goo.gl/0054v1, Feb. 2005. OCaml mailing list post.

[CAML-LIST 4]. Getting rid of impossible polymorphic variant tags from inferred types. https://goo.gl/ELougz, Mar. 2004. OCaml mailing list post.

R. Davies. *Practical Refinement-Type Checking*. PhD thesis, Carnegie Mellon University, May 2005.

J. Dunfield. *A Unified System of Type Refinements*. PhD thesis, Carnegie Mellon University, Aug. 2007.

A. Frisch, G. Castagna, and V. Benzaken. Semantic Subtyping. In *LICS '02, 17th Annual IEEE Symposium on Logic in Computer Science*, pages 137–146. IEEE Computer Society Press, 2002.

A. Frisch, G. Castagna, and V. Benzaken. Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. *Journal of the ACM*, 55(4):1–67, 2008.

J. Garrigue. Programming with polymorphic variants. In *ACM SIGPLAN Workshop on ML*, 1998. Informal proceedings.

J. Garrigue. Simple type inference for structural polymorphism. In *International Workshop on Foundations of Object-Oriented Languages (FOOL)*, 2002. Informal proceedings.

J. Garrigue. Typing deep pattern-matching in presence of polymorphic variants. In *JSSST Workshop on Programming and Programming Languages*, 2004.

J. Garrigue. A certified implementation of ML with structural polymorphism and recursive types. *Mathematical Structures in Computer Science*, 25:867–891, 2015.

L. Maranget. Warnings for pattern matching. *Journal of Functional Programming*, 17(3):387–421, 2007.

V. Nicollet. Do variant types in OCaml suck? http://goo.gl/F00wal, Mar. 2011. Blog post.

D. J. Pearce. Sound and complete flow typing with unions, intersections and negations. In *International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)*, pages 335–354, Jan. 2013.

T. Petrucciani. A set-theoretic type system for polymorphic variants in ML. Master's thesis, Università degli studi di Genova, 2015.

B. Pierce. *Programming with Intersection Types and Bounded Polymorphism*. PhD thesis, Carnegie Mellon University, December 1991. Available as School of Computer Science technical report CMU-CS-91-205.

F. Pottier and D. Rémy. The essence of ML type inference. In B. C. Pierce, editor, *Advanced Topics in Types and Programming Languages*, chapter 10, pages 389–489. MIT Press, 2005.

J. C. Reynolds. *Algol-like Languages*, chapter Design of the Programming Language Forsythe, pages 173–233. Birkhäuser, Boston, MA, 1997. ISBN 978-1-4612-4118-8. Peter W. O'Hearn and Robert D. Tennent (eds.).

S. Tobin-Hochstadt and M. Felleisen. The design and implementation of typed scheme. In *ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)*, pages 395–406, 2008.

S. Tobin-Hochstadt and M. Felleisen. Logical types for untyped languages. In *ACM SIGPLAN International Conference on Functional Programming (ICFP)*, pages 117–128, 2010.

T. Wegrzanowski. Variant types in OCaml suck. http://goo.gl/bY0bMA, May 2006. Blog post.
$v/\_ = []$

$v/x = [v/x]$

$$v/c = \begin{cases} [] & \text{if } v = c \\ \Omega & \text{otherwise} \end{cases}$$

$$v/(p_1, p_2) = \begin{cases} \zeta_1 \cup \zeta_2 & \text{if } v = (v_1, v_2) \text{ and } \forall i. v_i / p_i = \zeta_i \\ \Omega & \text{otherwise} \end{cases}$$

$$v/\text{'tag}(p_1) = \begin{cases} \zeta_1 & \text{if } v = \text{'tag}(v_1) \text{ and } v_1 / p_1 = \zeta_1 \\ \Omega & \text{otherwise} \end{cases}$$

$$v/p_1 \& p_2 = \begin{cases} \zeta_1 \cup \zeta_2 & \text{if } \forall i. v/p_i = \zeta_i \\ \Omega & \text{otherwise} \end{cases}$$

$$v/p_1 | p_2 = \begin{cases} v/p_1 & \text{if } v/p_1 \neq \Omega \\ v/p_2 & \text{otherwise} \end{cases}$$

<caption>**Figure 6.** Semantics of pattern matching.</caption>

$$\begin{array}{l@{\qquad}l}
\text{R-Appl} & \frac{v/p_j = \zeta \quad \forall i < j. v/p_i = \Omega}{\text{match } v \text{ with } (p_i \to e_i)_{i \in I} \rightsquigarrow e_j \zeta} \quad j \in I} \\
& \\
& \text{R-Ctx} \quad \frac{e \rightsquigarrow e'}{E[e] \rightsquigarrow E[e']}
\end{array}$$

<caption>**Figure 7.** Small-step reduction relation.</caption>

**Definition A.9 (Kinds).** A kind $\kappa$ is either the unconstrained kind “•” or a constrained kind, that is, a triple $(L, U, T)$ where:

* $L$ is a finite set of tags {`tag1, ..., `tagn}};

* $U$ is either a finite set of tags or the set $\mathcal{L}$ of all tags;

* $T$ is a finite set of pairs of a tag and a type, written {`tag1: $\tau_1$, ..., `tagn: $\tau_n$} (its domain dom($T$) is the set of tags occurring in it);

and where the following conditions hold:

* $L \subseteq U$, $L \subseteq \text{dom}(T)$, and, if $U \neq \mathcal{L}$, $U \subseteq \text{dom}(T)$;

* tags in $L$ have a single type in $T$, that is, if `tag $\in L$, whenever both `tag: $\tau_1 \in T$ and `tag: $\tau_2 \in T$, we have $\tau_1 = \tau_2$.

**Definition A.10 (Kind entailment).** The entailment relation $\vdash$ between constrained kinds is defined as

$$(L, U, T) \vdash (L', U', T') \iff L \supseteq L' \wedge U \subseteq U' \wedge T \supseteq T.$$

**Definition A.11 (Kinding environments).** A kinding environment $K$ is a partial mapping from type variables to kinds. We write kinding environments as $K = \{\alpha_1 :: \kappa_1, ..., \alpha_n :: \kappa_n\}$. We write $K, K'$ for the updating of the kinding environment $K$ with the new bindings in $K'$. It is defined as follows.

$$(K, K')(\alpha) = \begin{cases} K'(\alpha) & \text{if } \alpha \in \text{dom}(K') \\ K(\alpha) & \text{otherwise} \end{cases}$$

We say that a kinding environment is closed if all the type variables that appear in the types in its range also appear in its domain. We say it is canonical if it is infinite and contains infinitely many variables of every kind.

**Definition A.12 (Type schemes).** A type scheme $\sigma$ is of the form $\forall A. K \triangleright \tau$, where:

* $A$ is a finite set $\{\alpha_1, ..., \alpha_n\}$ of type variables;

* $K$ is a kinding environment such that $\text{dom}(K) = A$.
# A. Appendix

In this Appendix, we present full definitions of the language and type systems we have described, together with complete proofs of all results.

## A.1 The language of polymorphic variants

### A.1.1 Syntax

We assume that there exist a countable set $\mathcal{X}$ of expression variables, ranged over by $x, y, z, \dots$, a set $\mathcal{C}$ of constants, ranged over by $c$, and a set $\mathcal{L}$ of tags, ranged over by `tag`.

**Definition A.1 (Expressions).** An expression $e$ is a term inductively generated by the following grammar:

$$e ::= x \mid c \mid \lambda x. e \mid e e \mid (e, e) \mid \text{'tag}(e) \mid \text{match } e \text{ with } (p_i \to e_i)_{i \in I}$$

where $p$ ranges over the set $\mathcal{P}$ of patterns, defined below. We write $\mathcal{E}$ to denote the set of all expressions.

We define $fv(e)$ to be the set of expression variables occurring free in the expression $e$, and we say that $e$ is closed if and only if $fv(e)$ is empty.

As customary, we consider expressions up to $\alpha$-renaming of the variables bound by abstractions and by patterns.

**Definition A.2 (Patterns).** A pattern $p$ is a term inductively generated by the following grammar:

$$p ::= \_ | x \mid c \mid (p, p) \mid \text{'tag}(p) \mid p \& p \mid p | p$$

such that

* in a pair pattern $(p_1, p_2)$ or an intersection pattern $p_1 \& p_2$, $capt(p_1) \cap capt(p_2) = \emptyset$;

* in a union pattern $p_1|p_2$, $capt(p_1) = capt(p_2)$,

where $capt(p)$ denotes the set of expression variables occurring as sub-terms in a pattern $p$ (called the capture variables of $p$).

We write $\mathcal{P}$ to denote the set of all patterns.

### A.1.2 Semantics

**Definition A.3 (Values).** A value $v$ is a closed expression inductively generated by the following grammar.

$$v ::= c \mid \lambda x. e \mid (v, v) \mid \text{'tag}(v)$$

**Definition A.4 (Expression substitution).** An expression substitution $\zeta$ is a partial mapping of expression variables to values. We write $[v_i/x_i \mid i \in I]$ for the substitution which replaces free occurrences of $x_i$ with $v_i$, for each $i \in I$. We write $e_\zeta$ for the application of the substitution to an expression $e$. We write $\zeta_1 \cup \zeta_2$ for the union of disjoint substitutions.

**Definition A.5 (Semantics of pattern matching).** We write $v/p$ for the result of matching a value $v$ against a pattern $p$. We have either $v/p = \zeta$, where $\zeta$ is a substitution defined on the variables in $capt(p)$, or $v/p = \Omega$. In the former case, we say that $v$ matches $p$ (or that $p$ accepts $v$); in the latter, we say that matching fails.

The definition of $v/p$ is given inductively in Figure 6.

**Definition A.6 (Evaluation contexts).** Let the symbol $[]$ denote a hole. An evaluation context $E$ is a term inductively generated by the following grammar.

$$E ::= [] \mid E e \mid v E \mid (E, e) \mid (v, E) \mid \text{'tag}(E) \mid \text{match } E \text{ with } (p_i \to e_i)_{i \in I}$$

We write $E[e]$ for the expression obtained by replacing the hole in $E$ with the expression $e$.

**Definition A.7 (Reduction).** The reduction relation $\rightsquigarrow$ between expressions is given by the rules in Figure 7.

## A.2 Typing variants with kinding constraints

### A.2.1 Definition of the $\mathbb{K}$ type system

We assume that there exists a countable set $\mathcal{V}$ of type variables, ranged over by $\alpha, \beta, \gamma, \dots$. We also consider a finite set $\mathcal{B}$ of basic types, ranged over by $b$, and a function $b(\cdot)$ from constants to basic types.

**Definition A.8 (Types).** A type $\tau$ is a term inductively generated by the following grammar.

$$\tau ::= \alpha \mid b \mid \tau \to \tau \mid \tau \times \tau$$
We identify a type scheme $\forall \emptyset$. $\emptyset \triangleright \tau$, which quantifies no variable, with the type $\tau$ itself. We consider type schemes up to renaming of the variables they bind and disregard useless quantification (i.e., quantification of variables that do not occur in the type).

**Definition A.13 (Free variables).** The set of free variables $var_K(\sigma)$ of a type scheme $\sigma$ with respect to a kinding environment $K$ is the minimum set satisfying the following equations.

$$
\begin{align*}
\mathit{var}_K(\forall A. K' \triangleright \tau) &= \mathit{var}_{K,K'}(\tau) \setminus A \\
\mathit{var}_K(\alpha) &= \begin{cases} \{\alpha\} \cup \bigcup_{\tau \in T} \mathit{var}_K(\tau) & \text{if } K(\alpha) = (L, U, T) \\ \{\alpha\} & \text{otherwise} \end{cases} \\
\mathit{var}_K(b) &= \emptyset \\
\mathit{var}_K(\tau_1 \to \tau_2) &= \mathit{var}_K(\tau_1) \cup \mathit{var}_K(\tau_2) \\
\mathit{var}_K(\tau_1 \times \tau_2) &= \mathit{var}_K(\tau_1) \cup \mathit{var}_K(\tau_2)
\end{align*}
$$

We say that a type $\tau$ is ground or closed if and only if $var_\emptyset(\tau)$ is empty. We say that a type or a type scheme is closed in a kinding environment $K$ if all its free variables are in the domain of $K$.

**Definition A.14 (Type substitutions).** A type substitution $\theta$ is a finite mapping of type variables to types. We write $[\tau_i/\alpha_i | i \in I]$ for the type substitution which simultaneously replaces $\alpha_i$ with $\tau_i$, for each $i \in I$. We write $\tau\theta$ for the application of the substitution $\theta$ to the type $\tau$, which is defined as follows.

$$
\begin{align*}
\alpha\theta &= \begin{cases} \tau' & \text{if } \tau'/\alpha \in \theta \\ \alpha & \text{otherwise} \end{cases} \\
b\theta &= b \\
(\tau_1 \to \tau_2)\theta &= (\tau_1\theta) \to (\tau_2\theta) \\
(\tau_1 \times \tau_2)\theta &= (\tau_1\theta) \times (\tau_2\theta)
\end{align*}
$$

We extend the var operation to substitutions as

$$
\mathrm{var}_K(\theta) = \bigcup_{\alpha \in \mathrm{dom}(\theta)} \mathrm{var}_K(\alpha\theta).
$$

We extend application of substitutions to the typing component of a constrained kind (L, U, T):
$T\theta$ is given by the pointwise application of $\theta$ to all types in T. We extend it to kinding environments:
$K\theta$ is given by the pointwise application of $\theta$ to the typing component of every constrained kind
in the range of K. We extend it to type schemes $\forall A. K \triangleright \tau$: by renaming quantified variables, we
assume $A \cap (\mathrm{dom}(\theta) \cup \mathrm{var}_\emptyset(\theta)) = \emptyset$, and we have $(\forall A. K \triangleright \tau)\theta = \forall A. K\theta \triangleright \tau\theta$.

We write $\theta_1 \cup \theta_2$ for the union of disjoint substitutions and $\theta_1 \circ \theta_2$ for the composition of substitutions.

**Definition A.15 (Admissibility of a type substitution).** A type substitution $\theta$ is admissible between two kinding environments $K$ and $K'$, written $K \vdash \theta$: $K'$, if and only if, for every type variable $\alpha$ such that $K(\alpha) = (L, U, T)$, $\alpha\theta$ is a type variable such that $K'(\alpha\theta) = (L', U', T')$ and $(L', U', T') \models (L, U, T\theta)$.

**Definition A.16 (Type environments).** A type environment $\Gamma$ is a partial mapping from expression variables to type schemes. We write type environments as $\Gamma = \{x_1: \sigma_1, \dots, x_n: \sigma_n\}$.

We write $\Gamma, \Gamma'$ for the updating of the type environment $\Gamma$ with the new bindings in $\Gamma'$. It is
defined as follows.

$$
(\Gamma, \Gamma')(x) = \begin{cases} \Gamma'(x) & \text{if } x \in \operatorname{dom}(\Gamma') \\ \Gamma(x) & \text{otherwise} \end{cases}
$$

We extend the var operation to type environments as

$$
\mathrm{var}_K(\Gamma) = \bigcup_{\sigma \in \mathrm{range}(\Gamma)} \mathrm{var}_K(\sigma).
$$

**Definition A.17 (Generalization).** We define the generalization of a type $\tau$ with respect to a kinding environment $K$ and a type environment $\Gamma$ as the type scheme

$$
\operatorname{gen}_{K;\Gamma}(\tau) = \forall A. K' \triangleright \tau
$$

where $A = \mathit{var}_K(\tau) \setminus \mathit{var}_K(\Gamma)$ and $K' = \{\alpha :: K(\alpha) | \alpha \in A\}$.

We extend this definition to type environments which only contain types (i.e., trivial type schemes) as

$$
\mathrm{gen}_{K;\Gamma}(\{x_i : \tau_i \mid i \in I\}) = \{x_i : \mathrm{gen}_{K;\Gamma}(\tau_i) \mid i \in I\}.
$$
$v/- = []$

$v/x = [v/x]$

$$v/c = \begin{cases} [] & \text{if } v = c \\ \Omega & \text{otherwise} \end{cases}$$

$$v/(p_1, p_2) = \begin{cases} \varsigma_1 \cup \varsigma_2 & \text{if } v = (v_1, v_2) \text{ and } \forall i. v_i/p_i = \varsigma_i \\ \Omega & \text{otherwise} \end{cases}$$

$$v/\text{'tag}(p_1) = \begin{cases} \varsigma_1 & \text{if } v = \text{'tag}(v_1) \text{ and } v_1/p_1 = \varsigma_1 \\ \Omega & \text{otherwise} \end{cases}$$

$$v/p_1 \& p_2 = \begin{cases} \varsigma_1 \cup \varsigma_2 & \text{if } \forall i. v/p_i = \varsigma_i \\ \Omega & \text{otherwise} \end{cases}$$

$$v/p_1|p_2 = \begin{cases} v/p_1 & \text{if } v/p_1 \neq \Omega \\ v/p_2 & \text{otherwise} \end{cases}$$

<caption>**Figure 6.** Semantics of pattern matching.</caption>

$$\begin{array}{l} \text{R-Appl} \quad \frac{v/p_j = \varsigma \quad \forall i < j. v/p_i = \Omega}{(\lambda x. e) v \rightsquigarrow e^{[v/x]}} \quad j \in I} \\ \text{R-Match} \\ \text{R-Ctx} \quad \frac{e \rightsquigarrow e'}{E[e] \rightsquigarrow E[e']}
\end{array}$$

<caption>**Figure 7.** Small-step reduction relation.</caption>

**Definition A.9 (Kinds).** A kind $κ$ is either the unconstrained kind “•” or a constrained kind, that is, a triple $(L, U, T)$ where:

* $L$ is a finite set of tags {$\text{'tag}_1, \dots, \text{'tag}_n$};

* $U$ is either a finite set of tags or the set $\mathcal{L}$ of all tags;

* $T$ is a finite set of pairs of a tag and a type, written {$\text{'tag}_1: \tau_1, \dots, \text{'tag}_n: \tau_n$} (its domain $\text{dom}(T)$ is the set of tags occurring in it);

and where the following conditions hold:

* $L \subseteq U, L \subseteq \text{dom}(T)$, and, if $U \neq \mathcal{L}, U \subseteq \text{dom}(T)$;

* tags in $L$ have a single type in $T$, that is, if `tag ∈ L`, whenever both `tag: τ₁ ∈ T` and `tag: τ₂ ∈ T`, we have $τ₁ = τ₂$.

**Definition A.10 (Kind entailment).** The entailment relation $\vdash$ between constrained kinds is defined as

$$(L, U, T) \models (L', U', T') \iff L \supseteq L' \wedge U \subseteq U' \wedge T \supseteq T.$$

**Definition A.11 (Kinding environments).** A kinding environment $K$ is a partial mapping from type variables to kinds. We write kinding environments as $K = \{\alpha_1 :: \kappa_1, \dots, \alpha_n :: \kappa_n\}$. We write $K, K'$ for the updating of the kinding environment $K$ with the new bindings in $K'$. It is defined as follows.

$$(K, K')(\alpha) = \begin{cases} K'(\alpha) & \text{if } \alpha \in \text{dom}(K') \\ K(\alpha) & \text{otherwise} \end{cases}$$

We say that a kinding environment is closed if all the type variables that appear in the types in its range also appear in its domain. We say it is canonical if it is infinite and contains infinitely many variables of every kind.

**Definition A.12 (Type schemes).** A type scheme $\sigma$ is of the form $\forall A. K \triangleright \tau$, where:

* $A$ is a finite set $\{\alpha_1, \dots, \alpha_n\}$ of type variables;

* $K$ is a kinding environment such that $\text{dom}(K) = A$.
$$ \underline{\text{TPk-Wildcard}} \quad \overline{K \vdash \_ : \tau \Rightarrow \emptyset} $$

$$ \underline{\text{TPk-Var}} \quad \overline{K \vdash x : \tau \Rightarrow \{x : \tau\}} $$

$$ \underline{\text{TPk-Const}} \quad \overline{K \vdash c : b_c \Rightarrow \emptyset} $$

$$ \underline{\text{TPk-Pair}} \quad \frac{K \vdash p_1 : \tau_1 \Rightarrow \Gamma_1 \quad K \vdash p_2 : \tau_2 \Rightarrow \Gamma_2}{K \vdash (p_1, p_2) : \tau_1 \times \tau_2 \Rightarrow \Gamma_1 \cup \Gamma_2} $$

$$ \underline{\text{TPk-Tag}} \quad \frac{K \vdash p : \tau \Rightarrow \Gamma \quad K(\alpha) = (L, U, T) \quad (\text{'tag} \in U \text{ implies } \text{'tag} : \tau \in T)}{K \vdash \text{'tag}(p) : \alpha \Rightarrow \Gamma} $$

$$ \underline{\text{TPk-And}} \quad \frac{K \vdash p_1 : \tau \Rightarrow \Gamma_1 \quad K \vdash p_2 : \tau \Rightarrow \Gamma_2}{K \vdash p_1 \& p_2 : \tau \Rightarrow \Gamma_1 \cup \Gamma_2} $$

$$ \underline{\text{TPk-Or}} \quad \frac{K \vdash p_1 : \tau \Rightarrow \Gamma \quad K \vdash p_2 : \tau \Rightarrow \Gamma}{K \vdash p_1 | p_2 : \tau \Rightarrow \Gamma} $$

<caption>**Figure 8.** Pattern environment generation for $K$.</caption>

$$ \underline{\text{Tk-Var}} \quad \frac{\tau \in \text{inst}_K(\Gamma(x))}{K; \Gamma \vdash_K x : \tau} $$

$$ \underline{\text{Tk-Const}} \quad \overline{K; \Gamma \vdash_K c : b_c} $$

$$ \underline{\text{Tk-Abstr}} \quad \frac{K; \Gamma, \{x : \tau_1\} \vdash_K e : \tau_2}{K; \Gamma \vdash_K \lambda x. e : \tau_1 \to \tau_2} $$

$$ \underline{\text{Tk-Appl}} \quad \frac{K; \Gamma \vdash_K e_1 : \tau' \to \tau \quad K; \Gamma \vdash_K e_2 : \tau'}{K; \Gamma \vdash_K e_1 e_2 : \tau} $$

$$ \underline{\text{Tk-Pair}} \quad \frac{K; \Gamma \vdash_K e_1 : \tau_1 \quad K; \Gamma \vdash_K e_2 : \tau_2}{K; \Gamma \vdash_K (e_1, e_2) : \tau_1 \times \tau_2} $$

$$ \underline{\text{Tk-Tag}} \quad \frac{K; \Gamma \vdash_K e : \tau \quad K(\alpha) \models (\{\text{'tag}\}, \mathcal{L}, \{\text{'tag} : \tau\})}{K; \Gamma \vdash_K \text{'tag}(e) : \alpha} $$

$$ \underline{\text{Tk-Match}} \quad \frac{\forall i \in I \quad K; \Gamma \vdash_K e_0 : \tau_0 \quad \tau_0 \preceq_K \{p_i | i \in I\} \quad K \vdash p_i : \tau_0 \Rightarrow \Gamma_i \quad K; \Gamma, \text{gen}_{K;\Gamma}(\Gamma_i) \vdash_K e_i : \tau}{K; \Gamma \vdash_K \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau} $$

<caption>**Figure 9.** Typing relation for $K$.</caption>

**Definition A.18 (Instances of a type scheme).** The set of instances of a type scheme $\forall A. K' \triangleright \tau$ in a kinding environment $K$ is defined as

$$ \text{inst}_K(\forall A. K' \triangleright \tau) = \{ \tau \theta \mid \text{dom}(\theta) \subseteq A \wedge K, K' \triangleright \theta : K \}. $$

We say that a type scheme $\sigma_1$ is more general than a type scheme $\sigma_2$ in $K$, and we write $\sigma_1 \sqsubseteq_K \sigma_2$, if $\text{inst}_K(\sigma_1) \supseteq \text{inst}_K(\sigma_2)$.

We extend this notion to type environments as

$$ \Gamma_1 \sqsubseteq_K \Gamma_2 \iff \text{dom}(\Gamma_1) = \text{dom}(\Gamma_2) \wedge \forall x \in \text{dom}(\Gamma_1). \Gamma_1(x) \sqsubseteq_K \Gamma_2(x). $$

**Definition A.19 (Pattern environment generation).** The environment generated by pattern matching is given by the relation $K \vdash p : \tau \Rightarrow \Gamma$ (the pattern $p$ can match type $\tau$ in $K$, producing the bindings in $\Gamma$), defined by the rules in Figure 8.

**Definition A.20 (Exhaustiveness).** We say that a set of patterns $P$ is exhaustive with respect to a type $\tau$ in a kinding environment $K$, and we write $\tau \preceq_K P$, when

$$ \forall K', \theta, v. (K \vdash \theta : K' \wedge K'; \emptyset \vdash_K v : \tau \theta) \Rightarrow \exists p \in P, \zeta. v/p = \zeta. $$

**Definition A.21 (Typing relation).** The typing relation $K; \Gamma \vdash_K e : \tau$ (e is given type $\tau$ in the kinding environment $K$ and the type environment $\Gamma$) is defined by the rules in Figure 9, where we require $K$ to be closed and $\Gamma$ and $\tau$ to be closed with respect to $K$. We also assume that $K$ is canonical.

### A.2.2 Properties of the $K$ type system

**Lemma A.1 (Generation for values).** Let $v$ be a value. Then:

* if $K; \Gamma \vdash_K v : b$, then $v = c$ for some constant $c$ such that $b_c = b$;

* if $K; \Gamma \vdash_K v : \tau_1 \to \tau_2$, then $v$ is of the form $\lambda x. e$ and $K; \Gamma, \{x : \tau_1\} \vdash_K e : \tau_2$;

* if $K; \Gamma \vdash_K v : \tau_1 \times \tau_2$, then $v$ is of the form $(v_1, v_2)$, $K; \Gamma \vdash_K v_1 : \tau_1$, and $K; \Gamma \vdash_K v_2 : \tau_2$;
We identify a type scheme $\forall \emptyset$. $\emptyset \triangleright \tau$, which quantifies no variable, with the type $\tau$ itself. We consider type schemes up to renaming of the variables they bind and disregard useless quantification (i.e., quantification of variables that do not occur in the type).

**Definition A.13 (Free variables).** The set of free variables $var_K(\sigma)$ of a type scheme $\sigma$ with respect to a kinding environment $K$ is the minimum set satisfying the following equations.

$$var_K(\forall A. K' \triangleright \tau) = var_{K,K'}(\tau) \setminus A$$

$$var_K(\alpha) = \begin{cases} \{\alpha\} \cup \bigcup_{\tau \in T} var_K(\tau) & \text{if } K(\alpha) = (L, U, T) \\ \{\alpha\} & \text{otherwise} \end{cases}$$

$$var_K(b) = \emptyset$$

$$var_K(\tau_1 \to \tau_2) = var_K(\tau_1) \cup var_K(\tau_2)$$

$$var_K(\tau_1 \times \tau_2) = var_K(\tau_1) \cup var_K(\tau_2)$$

We say that a type $\tau$ is ground or closed if and only if $var_\emptyset(\tau)$ is empty. We say that a type or a type scheme is closed in a kinding environment $K$ if all its free variables are in the domain of $K$.

**Definition A.14 (Type substitutions).** A type substitution $\theta$ is a finite mapping of type variables to types. We write $[\tau_i/\alpha_i | i \in I]$ for the type substitution which simultaneously replaces $\alpha_i$ with $\tau_i$, for each $i \in I$. We write $\tau\theta$ for the application of the substitution $\theta$ to the type $\tau$, which is defined as follows.

$$\alpha\theta = \begin{cases} \tau' & \text{if } \tau'/\alpha \in \theta \\ \alpha & \text{otherwise} \end{cases}$$

$$b\theta = b$$

$$(\tau_1 \to \tau_2)\theta = (\tau_1\theta) \to (\tau_2\theta)$$

$$(\tau_1 \times \tau_2)\theta = (\tau_1\theta) \times (\tau_2\theta)$$

We extend the var operation to substitutions as

$$var_K(\theta) = \bigcup_{\alpha \in \text{dom}(\theta)} var_K(\alpha\theta).$$

We extend application of substitutions to the typing component of a constrained kind $(L, U, T)$: $T\theta$ is given by the pointwise application of $\theta$ to all types in $T$. We extend it to kinding environments: $K\theta$ is given by the pointwise application of $\theta$ to the typing component of every constrained kind in the range of $K$. We extend it to type schemes $\forall A. K \triangleright \tau$: by renaming quantified variables, we assume $A \cap (\text{dom}(\theta) \cup \text{var}_\emptyset(\theta)) = \emptyset$, and we have $(\forall A. K \triangleright \tau)\theta = \forall A. K\theta \triangleright \tau\theta$.

We write $\theta_1 \cup \theta_2$ for the union of disjoint substitutions and $\theta_1 \circ \theta_2$ for the composition of substitutions.

**Definition A.15 (Admissibility of a type substitution).** A type substitution $\theta$ is admissible between two kinding environments $K$ and $K'$, written $K \vdash \theta$: $K'$, if and only if, for every type variable $\alpha$ such that $K(\alpha) = (L, U, T)$, $\alpha\theta$ is a type variable such that $K'(\alpha\theta) = (L', U', T')$ and $(L', U', T') \models (L, U, T\theta)$.

**Definition A.16 (Type environments).** A type environment $\Gamma$ is a partial mapping from expression variables to type schemes. We write type environments as $\Gamma = \{x_1: \sigma_1, \dots, x_n: \sigma_n\}$.

We write $\Gamma$, $\Gamma'$ for the updating of the type environment $\Gamma$ with the new bindings in $\Gamma'$. It is defined as follows.

$$(\Gamma, \Gamma')(x) = \begin{cases} \Gamma'(x) & \text{if } x \in \text{dom}(\Gamma') \\ \Gamma(x) & \text{otherwise} \end{cases}$$

We extend the var operation to type environments as

$$var_K(\Gamma) = \bigcup_{\sigma \in \text{range}(\Gamma)} var_K(\sigma).$$

**Definition A.17 (Generalization).** We define the generalization of a type $\tau$ with respect to a kinding environment $K$ and a type environment $\Gamma$ as the type scheme

$$\text{gen}_{K;\Gamma}(\tau) = \forall A. K' \triangleright \tau$$

where $A = var_K(\tau) \setminus var_K(\Gamma)$ and $K' = \{\alpha :: K(\alpha) | \alpha \in A\}$.

We extend this definition to type environments which only contain types (i.e., trivial type schemes) as

$$\text{gen}_{K;\Gamma}(\{x_i: \tau_i | i \in I\}) = \{x_i: \text{gen}_{K;\Gamma}(\tau_i) | i \in I\}.$$
• if $K; \Gamma \vdash_K v : \alpha$, then $v$ is of the form `tag($v_1$), $K(\alpha) = (L, U, T)$, `tag $\in L$, and $K; \Gamma \vdash_K v_1 : \tau_1$ for the only type $\tau_1$ such that `tag : $\tau_1 \in T$.

**Proof.** The typing rules are syntax-directed, so the last rule applied to type a value is fixed by its form. All these rules derive types of different forms, thus the form of the type assigned to a value determines the last rule used. In each case the premises of the rule entail the consequences above. □

**Lemma A.2 (Correctness of environment generation).** Let $p$ be a pattern and $v$ a value such that $v/p = \zeta$. If $K; \Gamma \vdash_K v : \tau$ and $K \vdash p : \tau \Rightarrow \Gamma'$, then, for all $x \in \text{capt}(p)$, $K; \Gamma \vdash_K x\zeta : \Gamma'(x)$.

**Proof.** By induction on the derivation of $K \vdash p : \tau \Rightarrow \Gamma'$. We reason by cases on the last applied rule.

**Cases TPk-Wildcard and TPk-Const** There is nothing to prove since $\text{capt}(p) = \emptyset$.

**Case TPk-Var** We have

$$v/x = [v/x] \qquad K \vdash x : \tau \Rightarrow \{x : \tau\}$$

and must prove $K; \Gamma \vdash_K x^{[v/x]} : \{x : \tau\}(x)$, which we know by hypothesis.

**Case TPk-Pair** We have

$$K \vdash (p_1, p_2) : \tau_1 \times \tau_2 \Rightarrow \Gamma'_1 \cup \Gamma'_2 \qquad K \vdash p_1 : \tau_1 \Rightarrow \Gamma'_1 \qquad K \vdash p_2 : \tau_2 \Rightarrow \Gamma'_2.$$

By Lemma A.1, $K; \Gamma \vdash_K v : \tau_1 \times \tau_2$ implies $v = (v_1, v_2)$ and $K; \Gamma \vdash_K v_i : \tau_i$ for both $i$. Furthermore, $(v_1, v_2)/(p_1, p_2) = \zeta = \zeta_1 \cup \zeta_2$, and $v_i/p_i = \zeta_i$ for both $i$. For each capture variable $x$, we can apply the induction hypothesis to the sub-pattern which contains $x$ and conclude.

**Case TPk-Tag** We have

$$K \vdash \text{'tag}(p_1) : \alpha \Rightarrow \Gamma' \qquad K \vdash p_1 : \tau_1 \Rightarrow \Gamma' \\ K(\alpha) = (L, U, T) \qquad (\text{'tag} \in U \text{ implies 'tag} : \tau_1 \in T).$$

Since $v/\text{'tag}(p_1) = \zeta$, we know $v = \text{'tag}(v_1)$. Hence, by Lemma A.1, we have `tag $\in L$` and $K; \Gamma \vdash_K v_1 : \tau'_1$ with `tag : $\tau'_1 \in T$. Since `tag $\in U$, we also have `tag : $\tau_1 \in T$ and hence $\tau_1 = \tau'_1$ (as `tag is also in $L$ and can only have a single type in $T$).

We therefore know $K \vdash p_1 : \tau_1 \Rightarrow \Gamma'$ and $K; \Gamma \vdash_K v_1 : \tau_1$, as well as $v_1/p_1 = \zeta$. We can apply the induction hypothesis to conclude.

**Cases TPk-And and TPk-Or** Straightforward application of the induction hypothesis, to both sub-patterns for intersections and to the one that is actually selected for unions. □

**Lemma A.3 (Stability of environment generation under type substitutions).** If $K \vdash p : \tau \Rightarrow \Gamma$, then $K' \vdash p : \tau\theta \Rightarrow \Gamma\theta$ for every type substitution $\theta$ such that $K \vdash \theta : K'$.

**Proof.** By induction on the derivation of $K \vdash p : \tau \Rightarrow \Gamma$. We reason by cases on the last applied rule.

**Cases TPk-Wildcard, TPk-Var, and TPk-Const** Straightforward.

**Case TPk-Pair** We have

$$K \vdash (p_1, p_2) : \tau_1 \times \tau_2 \Rightarrow \Gamma_1 \cup \Gamma_2 \qquad K \vdash p_1 : \tau_1 \Rightarrow \Gamma_1 \qquad K \vdash p_2 : \tau_2 \Rightarrow \Gamma_2.$$

By the induction hypothesis we derive both $K' \vdash p_1 : \tau_1\theta \Rightarrow \Gamma_1\theta$ and $K' \vdash p_2 : \tau_2\theta \Rightarrow \Gamma_2\theta$, then we apply TPk-Pair again to conclude.

**Case TPk-Tag** We have

$$K \vdash \text{'tag}(p_1) : \alpha \Rightarrow \Gamma \qquad K \vdash p_1 : \tau_1 \Rightarrow \Gamma \\ K(\alpha) = (L, U, T) \qquad (\text{'tag} \in U \text{ implies 'tag} : \tau_1 \in T).$$

By the induction hypothesis we derive $K' \vdash p_1 : \tau_1\theta \Rightarrow \Gamma\theta$. Since $K \vdash \theta : K'$, $\alpha\theta$ must be a variable $\beta$ such that $K'(\beta) = (L', U', T')$. To apply TPk-Tag and conclude, we must establish that, if `tag $\in U'$, then `tag : $\tau_1\theta \in T'$. Since admissibility also implies $(L', U', T') \vdash (L, U, T\theta)$, we have $U' \subseteq U$ and $T\theta \subseteq T'$. Hence, if `tag $\in U'$, then `tag $\in U$, in which case `tag : $\tau_1\theta \in T$ and therefore `tag : $\tau_1\theta \in T'$, and `tag : $\tau_1\theta \in T'$.

**Cases TPk-And and TPk-Or** Straightforward application of the induction hypothesis, analogously to the case of pair patterns. □
$$ \overline{\text{TPk-Wildcard}} \quad \overline{K \vdash_- : \tau \Rightarrow \emptyset} \qquad \overline{\text{TPk-Var}} \quad \overline{K \vdash x : \tau \Rightarrow \{x : \tau\}} $$

$$ \overline{\text{TPk-Const}} \qquad \overline{K \vdash c : b_c \Rightarrow \emptyset} \qquad \overline{\text{TPk-Pair}} \qquad \frac{K \vdash p_1 : \tau_1 \Rightarrow \Gamma_1 \quad K \vdash p_2 : \tau_2 \Rightarrow \Gamma_2}{K \vdash (p_1, p_2) : \tau_1 \times \tau_2 \Rightarrow \Gamma_1 \cup \Gamma_2} $$

$$ \overline{\text{TPk-Tag}} \qquad \frac{K \vdash p : \tau \Rightarrow \Gamma \qquad K(\alpha) = (L, U, T) \qquad (\text{'tag} \in U \text{ implies } \text{'tag} : \tau \in T)}{K \vdash \text{'tag}(p) : \alpha \Rightarrow \Gamma} $$

$$ \overline{\text{TPk-And}} \qquad \frac{K \vdash p_1 : \tau \Rightarrow \Gamma_1 \qquad K \vdash p_2 : \tau \Rightarrow \Gamma_2}{K \vdash p_1 \& p_2 : \tau \Rightarrow \Gamma_1 \cup \Gamma_2} $$

$$ \overline{\text{TPk-Or}} \qquad \frac{K \vdash p_1 : \tau \Rightarrow \Gamma \qquad K \vdash p_2 : \tau \Rightarrow \Gamma}{K \vdash p_1 | p_2 : \tau \Rightarrow \Gamma} $$

<caption>**Figure 8.** Pattern environment generation for $K$.</caption>

$$ \begin{array}{lll} \text{Tk-Var} & \frac{\tau \in \text{inst}_K(\Gamma(x))}{K; \Gamma \vdash_K x : \tau} & \text{Tk-Const} \quad \overline{K; \Gamma \vdash_K c : b_c} \qquad \text{Tk-Abstr} \quad \overline{K; \Gamma \vdash_K \lambda x. e : \tau_1 \to \tau_2} \\ \text{Tk-Appl} & \frac{K; \Gamma \vdash_K e_1 : \tau' \to \tau \qquad K; \Gamma \vdash_K e_2 : \tau'}{K; \Gamma \vdash_K e_1 e_2 : \tau} & \text{Tk-Pair} \quad \frac{K; \Gamma \vdash_K e_1 : \tau_1 \qquad K; \Gamma \vdash_K e_2 : \tau_2}{K; \Gamma \vdash_K (e_1, e_2) : \tau_1 \times \tau_2} \\ \text{Tk-Tag} & \frac{K; \Gamma \vdash_K e : \tau \qquad K(\alpha) \models (\{\text{'tag}\}, \mathcal{L}, \{\text{'tag} : \tau\})}{K; \Gamma \vdash_K \text{'tag}(e) : \alpha} & \\ \text{Tk-Match} & \frac{\forall i \in I \qquad \begin{array}{l} K; \Gamma \vdash_K e_0 : \tau_0 \qquad \tau_0 \preceq_K \{p_i \mid i \in I\} \\ K \vdash p_i : \tau_0 \Rightarrow \Gamma_i \qquad K; \Gamma, \text{gen}_{K;\Gamma}(\Gamma_i) \vdash_K e_i : \tau \end{array}}{K; \Gamma \vdash_K \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau} & \end{array} $$

<caption>**Figure 9.** Typing relation for $K$.</caption>

**Definition A.18 (Instances of a type scheme).** The set of instances of a type scheme $\forall A. K' \triangleright \tau$ in a kinding environment $K$ is defined as

$$ \text{inst}_K(\forall A. K' \triangleright \tau) = \{ \tau \theta \mid \text{dom}(\theta) \subseteq A \wedge K, K' \triangleright \theta : K \}. $$

We say that a type scheme $\sigma_1$ is more general than a type scheme $\sigma_2$ in $K$, and we write $\sigma_1 \sqsubseteq_K \sigma_2$, if $\text{inst}_K(\sigma_1) \supseteq \text{inst}_K(\sigma_2)$.

We extend this notion to type environments as

$$ \Gamma_1 \sqsubseteq_K \Gamma_2 \iff \text{dom}(\Gamma_1) = \text{dom}(\Gamma_2) \wedge \forall x \in \text{dom}(\Gamma_1). \Gamma_1(x) \sqsubseteq_K \Gamma_2(x). $$

**Definition A.19 (Pattern environment generation).** The environment generated by pattern matching is given by the relation $K \vdash p : \tau \Rightarrow \Gamma$ (the pattern $p$ can match type $\tau$ in $K$, producing the bindings in $\Gamma$), defined by the rules in Figure 8.

**Definition A.20 (Exhaustiveness).** We say that a set of patterns $P$ is exhaustive with respect to a type $\tau$ in a kinding environment $K$, and we write $\tau \preceq_K P$, when

$$ \forall K', \theta, v. (K \vdash \theta : K' \wedge K'; \emptyset \vdash_K v : \tau \theta) \Rightarrow \exists p \in P, \zeta. v/p = \zeta. $$

**Definition A.21 (Typing relation).** The typing relation $K; \Gamma \vdash_K e : \tau$ (e is given type $\tau$ in the kinding environment $K$ and the type environment $\Gamma$) is defined by the rules in Figure 9, where we require $K$ to be closed and $\Gamma$ and $\tau$ to be closed with respect to $K$. We also assume that $K$ is canonical.

### A.2.2 Properties of the $K$ type system

**Lemma A.1 (Generation for values).** Let $v$ be a value. Then:

* if $K; \Gamma \vdash_K v : b$, then $v = c$ for some constant $c$ such that $b_c = b$;

* if $K; \Gamma \vdash_K v : \tau_1 \to \tau_2$, then $v$ is of the form $\lambda x. e$ and $K; \Gamma, \{x : \tau_1\} \vdash_K e : \tau_2$;

* if $K; \Gamma \vdash_K v : \tau_1 \times \tau_2$, then $v$ is of the form $(v_1, v_2)$, $K; \Gamma \vdash_K v_1 : \tau_1$, and $K; \Gamma \vdash_K v_2 : \tau_2$;
**Lemma A.4 (Stability of exhaustiveness under type substitutions).** If $\tau \preceq_K P$, then $\tau\theta \preceq_{K'} P$ for any type substitution $\theta$ such that $K \vdash \theta: K'$.

*Proof.* We must prove, for every $K''$, $\theta'$ such that $K' \vdash \theta': K''$ and every $v$ such that $K''$: $\emptyset \vdash_K v$: $\tau\theta\theta'$, that there exists a $p \in P$ which accepts $v$. This holds because $\theta' \circ \theta$ is such that $K \vdash \theta' \circ \theta: K''$: for any $\alpha$ such that $K(\alpha) = (L, U, T)$, we have $K'(\alpha\theta) = (L', U', T')$ and hence $K''(\alpha\theta\theta') = (L'', U'', T'')$; we have $(L', U', T') \vdash (L, U, T\theta)$ and $(L'', U'', T'') \vdash (L', U', T'\theta')$ and therefore $(L'', U'', T'') \vdash (L, U, T\theta\theta')$. The conclusion follows by the definition of $\tau \preceq_K P$. $\square$

**Lemma A.5.** If $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$, then, for every type $\tau$, $\mathrm{gen}_{K;\Gamma_1}(\tau) \subseteq_K \mathrm{gen}_{K;\Gamma_2}(\tau)$.

*Proof.* An instance of $\mathrm{gen}_{K;\Gamma_2}(\tau)$ is a type $\tau\theta$ such that $\mathrm{dom}(\theta) \subseteq \mathrm{var}_K(\tau) \setminus \mathrm{var}_K(\Gamma_2)$ and $K \vdash \theta: K$. It is also an instance of $\mathrm{gen}_{K;\Gamma_1}(\tau)$, with the same $\theta$, since $\mathrm{var}_K(\tau) \setminus \mathrm{var}_K(\Gamma_2) \subseteq \mathrm{var}_K(\tau) \setminus \mathrm{var}_K(\Gamma_1)$. $\square$

**Lemma A.6 (Weakening).** Let $K$ be a kinding environment and $\Gamma_1, \Gamma_2$ two type environments such that $\Gamma_1 \subseteq_K \Gamma_2$ and $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$. If $K; \Gamma_2 \vdash_K e: \tau$, then $K; \Gamma_1 \vdash_K e: \tau$.

*Proof.* By induction on the derivation of $K; \Gamma_2 \vdash_K e: \tau$. We reason by cases on the last applied rule.

*Case Tk-Var* We have:

$$K; \Gamma_2 \vdash_K x: \tau \quad \tau \in \mathrm{inst}_K(\Gamma_2(x))$$

and hence, since $\Gamma_1 \subseteq_K \Gamma_2$, we have $\tau \in \mathrm{inst}_K(\Gamma_1(x))$ and apply Tk-Var to conclude.

*Case Tk-Const* Straightforward.

*Case Tk-Abstr* We have:

$$K; \Gamma_2 \vdash_K \lambda x. e_1: \tau_1 \rightarrow \tau_2 \quad K; \Gamma_2, \{x: \tau_1\} \vdash_K e_1: \tau_2.$$

Since $\Gamma_1 \subseteq_K \Gamma_2$, we have $\Gamma_1, \{x: \tau_1\} \subseteq_K \Gamma_2, \{x: \tau_1\}$, and, since $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$, we have $\mathrm{var}_K(\Gamma_1, \{x: \tau_1\}) \subseteq \mathrm{var}_K(\Gamma_2, \{x: \tau_1\})$. Thus we may derive $K; \Gamma_1, \{x: \tau_1\} \vdash_K e_1: \tau_2$ by the induction hypothesis and apply Tk-Abstr to conclude.

*Cases Tk-Appl, Tk-Pair, and Tk-Tag* Straightforward application of the induction hypothesis.

*Case Tk-Match* We have

$$\begin{align*}
K; \Gamma_2 \vdash_K \mathrm{match} e_0 \text{ with } (p_i \rightarrow e_i)_{i \in I}: \tau \\
K; \Gamma_2 \vdash_K e_0: \tau_0 \qquad \tau_0 \preceq_K \{p_i \mid i \in I\} \\
\forall i \in I. \quad K \vdash p_i: \tau_0 \Rightarrow \Gamma_i \quad K; \Gamma_2, \mathrm{gen}_{K;\Gamma_2}(\Gamma_i) \vdash_K e_i: \tau.
\end{align*}$$

By the induction hypothesis, we derive $K; \Gamma_1 \vdash_K e_0: \tau_0$.

For every branch, note that by Lemma A.5 $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$ implies $\mathrm{gen}_{K;\Gamma_1}(\tau) \subseteq_K \mathrm{gen}_{K;\Gamma_2}(\tau)$ for any $\tau$. Hence, we have $\Gamma_1, \mathrm{gen}_{K;\Gamma_1}(\Gamma_i) \subseteq_K \Gamma_2, \mathrm{gen}_{K;\Gamma_2}(\Gamma_i)$. Additionally, since $\mathrm{var}_K(\mathrm{gen}_{K;\Gamma_1}(\Gamma_i)) \subseteq \mathrm{var}_K(\Gamma_1, \mathrm{gen}_{K;\Gamma_1}(\Gamma_i)) \subseteq \mathrm{var}_K(\Gamma_2, \mathrm{gen}_{K;\Gamma_2}(\Gamma_i))$.

Hence we may apply the induction hypothesis for all $i$ to derive $K; \Gamma_1, \mathrm{gen}_{K;\Gamma_1}(\Gamma_i) \vdash_K e_i: \tau$ and then apply Tk-Match to conclude. $\square$

**Lemma A.7 (Stability of typing under type substitutions).** Let $K, K'$ be two closed, canonical kinding environments and $\theta$ a type substitution such that $K \vdash \theta: K'$. If $K; \Gamma \vdash_K e: \tau$, then $K'; \Gamma\theta \vdash_K e: \tau\theta$.

*Proof.* By induction on the derivation of $K; \Gamma \vdash_K e: \tau$. We reason by cases on the last applied rule.

*Case Tk-Var* We have

$$\begin{gather*}
K; \Gamma \vdash_K x: \tau \quad \tau \in \mathrm{inst}_K(\Gamma(x)) \\
\Gamma(x) = \forall A. K_x \triangleright \tau_x \quad \tau = \tau_x \theta_x \quad \mathrm{dom}(\theta_x) \subseteq A \quad K, K_x \vdash \theta_x: K
\end{gather*}$$

and must show

$$K'; \Gamma\theta \vdash_K x: \tau\theta.$$

By $\alpha$-renaming we can assume that $\theta$ does not involve $A$, that is, $A \cap \mathrm{dom}(\theta) = \emptyset$ and $A \cap \mathrm{var}_\emptyset(\theta) = \emptyset$, and also that $A \cap (\mathrm{dom}(K') \cup \mathrm{var}_\emptyset(K')) = \emptyset$, that is, that the variables in $A$ are not assigned a kind in $K'$ nor do they appear in the types in the typing component of the kinds in $K'$.

Under these assumptions, $(\Gamma\theta)(x) = \forall A. K_x\theta \triangleright \tau_x\theta$. We must show that $\tau\theta = \tau_x\theta\theta'_x$ for a substitution $\theta'_x$ such that $\mathrm{dom}(\theta'_x) \subseteq A$ and $K_x\theta \vdash \theta'_x: K'$.
• if $K; \Gamma \vdash_K v: \alpha$, then $v$ is of the form `tag($v_1$), $K(\alpha) = (L, U, T)$, `tag $\in L$, and $K; \Gamma \vdash_K v_1: \tau_1$ for the only type $\tau_1$ such that `tag: $\tau_1 \in T$.

**Proof.** The typing rules are syntax-directed, so the last rule applied to type a value is fixed by its form. All these rules derive types of different forms, thus the form of the type assigned to a value determines the last rule used. In each case the premises of the rule entail the consequences above. □

**Lemma A.2 (Correctness of environment generation).** Let $p$ be a pattern and $v$ a value such that $v/p = \zeta$. If $K; \Gamma \vdash_K v: \tau$ and $K \vdash p: \tau \Rightarrow \Gamma'$, then, for all $x \in \text{capt}(p)$, $K; \Gamma \vdash_K x\zeta: \Gamma'(x)$.

**Proof.** By induction on the derivation of $K \vdash p: \tau \Rightarrow \Gamma'$. We reason by cases on the last applied rule.

**Cases TPk-Wildcard and TPk-Const** There is nothing to prove since $\text{capt}(p) = \emptyset$.

**Case TPk-Var** We have

$$v/x = [v/x] \qquad K \vdash x: \tau \Rightarrow \{x: \tau\}$$

and must prove $K; \Gamma \vdash_K x^{[v/x]}: \{x: \tau\}(x)$, which we know by hypothesis.

**Case TPk-Pair** We have

$$K \vdash (p_1, p_2): \tau_1 \times \tau_2 \Rightarrow \Gamma'_1 \cup \Gamma'_2 \qquad K \vdash p_1: \tau_1 \Rightarrow \Gamma'_1 \qquad K \vdash p_2: \tau_2 \Rightarrow \Gamma'_2.$$

By Lemma A.1, $K; \Gamma \vdash_K v: \tau_1 \times \tau_2$ implies $v = (v_1, v_2)$ and $K; \Gamma \vdash_K v_i: \tau_i$ for both $i$. Furthermore, $(v_1, v_2)/(p_1, p_2) = \zeta = \zeta_1 \cup \zeta_2$, and $v_i/p_i = \zeta_i$ for both $i$. For each capture variable $x$, we can apply the induction hypothesis to the sub-pattern which contains $x$ and conclude.

**Case TPk-Tag** We have

$$K \vdash \text{'tag}(p_1): \alpha \Rightarrow \Gamma' \qquad K \vdash p_1: \tau_1 \Rightarrow \Gamma' \\ K(\alpha) = (L, U, T) \qquad (\text{'tag} \in U \text{ implies 'tag: } \tau_1 \in T).$$

Since $v/\text{'tag}(p_1) = \zeta$, we know $v = \text{'tag}(v_1)$. Hence, by Lemma A.1, we have `tag $\in L$` and $K; \Gamma \vdash_K v_1: \tau'_1$ with `tag: $\tau'_1 \in T$. Since `tag $\in U$, we also have `tag: $\tau_1 \in T$ and hence $\tau_1 = \tau'_1$ (as `tag is also in $L$ and can only have a single type in $T$).

We therefore know $K \vdash p_1: \tau_1 \Rightarrow \Gamma'$ and $K; \Gamma \vdash_K v_1: \tau_1$, as well as $v_1/p_1 = \zeta$. We can apply the induction hypothesis to conclude.

**Cases TPk-And and TPk-Or** Straightforward application of the induction hypothesis, to both sub-patterns for intersections and to the one that is actually selected for unions. □

**Lemma A.3 (Stability of environment generation under type substitutions).** If $K \vdash p: \tau \Rightarrow \Gamma$, then $K' \vdash p: \tau\theta \Rightarrow \Gamma\theta$ for every type substitution $\theta$ such that $K \vdash \theta: K'$.

**Proof.** By induction on the derivation of $K \vdash p: \tau \Rightarrow \Gamma$. We reason by cases on the last applied rule.

**Cases TPk-Wildcard, TPk-Var, and TPk-Const** Straightforward.

**Case TPk-Pair** We have

$$K \vdash (p_1, p_2): \tau_1 \times \tau_2 \Rightarrow \Gamma_1 \cup \Gamma_2 \qquad K \vdash p_1: \tau_1 \Rightarrow \Gamma_1 \qquad K \vdash p_2: \tau_2 \Rightarrow \Gamma_2.$$

By the induction hypothesis we derive both $K' \vdash p_1: \tau_1\theta \Rightarrow \Gamma_1\theta$ and $K' \vdash p_2: \tau_2\theta \Rightarrow \Gamma_2\theta$, then we apply TPk-Pair again to conclude.

**Case TPk-Tag** We have

$$K \vdash \text{'tag}(p_1): \alpha \Rightarrow \Gamma \qquad K \vdash p_1: \tau_1 \Rightarrow \Gamma \\ K(\alpha) = (L, U, T) \qquad (\text{'tag} \in U \text{ implies 'tag: } \tau_1 \in T).$$

By the induction hypothesis we derive $K' \vdash p_1: \tau_1\theta \Rightarrow \Gamma\theta$. Since $K \vdash \theta: K'$, $\alpha\theta$ must be a variable $\beta$ such that $K'(\beta) = (L', U', T')$. To apply TPk-Tag and conclude, we must establish that, if `tag $\in U'$, then `tag: $\tau_1\theta \in T'$. Since admissibility also implies $(L', U', T') \vdash (L, U, T\theta)$, we have $U' \subseteq U$ and $T\theta \subseteq T'$. Hence, if `tag $\in U'$, then `tag $\in U$, in which case `tag: $\tau_1 \in T$ and therefore `tag: $\tau_1\theta \in T\theta$, and `tag: $\tau_1\theta \in T'$.

**Cases TPk-And and TPk-Or** Straightforward application of the induction hypothesis, analogously to the case of pair patterns. □
Let $\theta'_x = [\alpha\theta_x\theta/\alpha | \alpha \in A]$. First, we show that $\tau_x\theta\theta'_x = \tau_x\theta_x\theta = \tau\theta$, by showing that, for any $\alpha$, $\alpha\theta\theta'_x = \alpha\theta_x\theta$. If $\alpha \in A$, then $\alpha\theta\theta'_x = \alpha\theta'_x = \alpha\theta_x\theta$ ($\theta$ is not defined on the variables in A). If $\alpha \notin A$, then $\alpha\theta\theta'_x = \alpha\theta$ ($\theta$ never produces any variable in A) and $\alpha\theta_x\theta = \alpha\theta$ as $\alpha \notin \text{dom}(\theta_x)$.

Since $\text{dom}(\theta'_x) \subseteq A$ holds, we only need to establish that $K', K_x\theta \vdash \theta'_x: K'$. This requires proving, for each $\alpha$ such that $(K', K_x\theta)(\alpha) = (L, U, T)$, that $\alpha\theta'_x$ is a type variable such that $K'(\alpha\theta'_x) = (L', U', T')$ and $(L', U', T') \vdash (L, U, T\theta'_x)$.

Such an $\alpha$ can either be in the domain of $K_x\theta$ (if and only if it is in A) or in the domain of $K'$. In the latter case, we have $\alpha\theta'_x = \alpha$, since $\alpha \notin A$, and hence its kind in $K'$ is the same as in $K'$, $K_x\theta$. We must prove $(L, U, T) \vdash (L, U, T\theta'_x)$, which holds because the variables in A do not appear in T since $(L, U, T) \in \text{range}(K')$.

In the former case, we have $(K_x\theta)(\alpha) = (L, U, T)$ and hence $K_x(\alpha) = (L, U, T_1)$, with $T = T_1\theta$. Also, $\alpha\theta'_x = \alpha\theta_x\theta$. Since $K, K_x \vdash \theta_x: K, K(\alpha\theta_x) = (L_2, U_2, T_2)$. Then, since $K \vdash \theta: K', K'(\alpha\theta_x\theta) = (L', U', T')$. We know $(L_2, U_2, T_2) \vdash (L, U, T_1\theta_x)$ and $(L', U', T') \vdash (L_2, U_2, T_2\theta)$. Both $L' \supseteq L$ and $U' \subseteq U$ hold by transitivity. We show $T' \supseteq T\theta'_x$ holds as well. If `tag: $\tau \in T\theta'_x$, since $T = T_1\theta$, then `tag: $\tau_1 \in T_1$ and $\tau = \tau_1\theta\theta'_x = \tau_1\theta_x\theta$. We thus have `tag: $\tau_1\theta_x \in T_1\theta_x$ and therefore `tag: $\tau_1\theta_x \in T_2$ and `tag: $\tau_1\theta_x\theta \in T'$.

**Case Tk-Const** Straightforward.

**Case Tk-Abstr** We have:

$$K; \Gamma \vdash_K \lambda x. e_1 : \tau_1 \rightarrow \tau_2 \qquad K; \Gamma, \{x : \tau_1\} \vdash_K e_1 : \tau_2.$$

By the induction hypothesis we have $K'$; $\Gamma\theta, \{x : \tau_1\theta\} \vdash_K e_1 : \tau_2\theta$. Then by Tk-Abstr we derive $K'$; $\Gamma\theta \vdash_K \lambda x. e_1 : (\tau_1 \rightarrow \tau_2)\theta$, since $(\tau_1 \rightarrow \tau_2)\theta = (\tau_1\theta) \rightarrow (\tau_2\theta)$.

**Cases Tk-Appl and Tk-Pair** Straightforward application of the induction hypothesis.

**Case Tk-Match** For the sake of clarity, we first prove the simpler case corresponding to (the encoding of) let, where—simplifying environment generation—we have

$$K; \Gamma \vdash_K \mathit{match} \, e_0 \, \mathit{with} \, x \to e_1 : \tau \qquad K; \Gamma \vdash_K e_0 : \tau_0 \qquad K; \Gamma, \mathit{gen}_{K;\Gamma}(\{x : \tau_0\}) \vdash_K e_1 : \tau$$

and must show

$$K'; \Gamma \theta \vdash_K \mathit{match} \, e_0 \, \mathit{with} \, x \to e_1 : \tau \theta$$

which we prove by establishing, for some type $\hat{\tau}_0$, that

$$K'; \Gamma \theta \vdash_K e_0 : \hat{\tau}_0 \qquad K'; \Gamma \theta, \mathit{gen}_{K';\Gamma\theta}(\{x : \hat{\tau}_0\}) \vdash_K e_1 : \tau \theta.$$

Let $A = \{\alpha_1, \dots, \alpha_n\} = \mathit{var}_K(\tau_0) \setminus \mathit{var}_K(\Gamma)$. We assume that the variables in A do not appear in the kinds of variables not in A, that is, that if $K(\alpha) = (L, U, T)$ and $\alpha \notin A$, then $\mathit{var}_K(T) \cap A = \emptyset$.

This assumption is justified by the following observations. The variables in A only appear quantified in the environment used for the typing derivation for $e_1$. Therefore we may assume that they do not appear in $\tau$: if they do, it is because they have been chosen when instantiating some type scheme and, since K is canonical, we might have chosen some other variable of the same kind. As for the occurrences of the variables in A in the derivation for $e_0$, a similar reasoning applies. These variables do not appear free in the environment (neither directly in a type in $\Gamma$, nor in the kinds of variables which appear free in $\Gamma$). Therefore, if they occur in $\tau_0$ it is because they have been chosen either during instantiation of a type scheme or when typing an abstraction, and in both cases we might have chosen a different variable.

Now we rename these variables so that $\theta$ will not have effect on them. Let $B = \{\beta_1, \dots, \beta_n\}$ be a set of type variables such that $B \cap (\text{dom}(\theta) \cup \text{var}_\emptyset(\theta)) = \emptyset$ and $B \cap \text{var}_\emptyset(\Gamma) = \emptyset$. Let $\theta_0 = [\beta_1/\alpha_1, \dots, \beta_n/\alpha_n]$ and $\theta' = \theta \circ \theta_0$. Since $K'$ is canonical, we can choose each $\beta_i$ so that, if $K(\alpha_i) = \bullet$, then $K'(\beta_i) = \bullet$, and if $K(\alpha_i) = (L, U, T)$, then $K(\beta_i) = (L, U, T')$. As for A, we choose B so that the kinds in $K'$ for variables not in B do not contain variables of B.

We show $K \vdash \theta' : K'$. For each $\alpha$ such that $K(\alpha) = (L, U, T)$, if $\alpha \in A$ then $\alpha = \alpha_i$ for some $i$, $\alpha\theta' = \beta_i$ and kind entailment holds straightforwardly by our choice of $\beta_i$. If $\alpha \notin A$, then $\alpha\theta' = \alpha\theta$ and the admissibility of $\theta$ implies $K'(\alpha\theta) = (L', U', T')$ and $(L', U', T') \vdash (L, U, T\theta)$. We have $T\theta = T\theta'$ because of our assumption on A.

Since $\theta'$ is admissibile, by the induction hypothesis applied to $\theta'$, we derive $K; \Gamma\theta' \vdash_K e_0 : \tau_0\theta'$. Since the variables in A do not appear in $\Gamma$, we have $\Gamma\theta' = \Gamma\theta$. We choose $\hat{\tau}_0$ to be $\tau_0\theta'$.

We apply the induction hypothesis to the derivation for $e_1$, this time using $\theta$ as the substitution. Now we have:

$$K'; \Gamma \theta \vdash_K e_0 : \tau_0 \theta' \qquad K'; \Gamma \theta, (\mathit{gen}_{K;\Gamma}(\{x : \tau_0\})) \theta \vdash_K e_1 : \tau \theta.$$
**Lemma A.4 (Stability of exhaustiveness under type substitutions).** If $\tau \preceq_K P$, then $\tau\theta \preceq_{K'} P$ for any type substitution $\theta$ such that $K \vdash \theta: K'$.

*Proof.* We must prove, for every $K''$, $\theta'$ such that $K' \vdash \theta'$: $K''$ and every $v$ such that $K''$: $\emptyset \vdash_K v$: $\tau\theta\theta'$, that there exists a $p \in P$ which accepts $v$. This holds because $\theta' \circ \theta$ is such that $K \vdash \theta' \circ \theta$: $K''$: for any $\alpha$ such that $K(\alpha) = (L, U, T)$, we have $K'(\alpha\theta) = (L', U', T')$ and hence $K''(\alpha\theta\theta') = (L'', U'', T'')$; we have $(L', U', T') \vdash (L, U, T\theta)$ and $(L'', U'', T'') \vdash (L', U', T'\theta')$ and therefore $(L'', U'', T'') \vdash (L, U, T\theta\theta')$. The conclusion follows by the definition of $\tau \preceq_K P$. $\square$

**Lemma A.5.** If $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$, then, for every type $\tau$, $\mathrm{gen}_{K;\Gamma_1}(\tau) \subseteq_K \mathrm{gen}_{K;\Gamma_2}(\tau)$.

*Proof.* An instance of $\mathrm{gen}_{K;\Gamma_2}(\tau)$ is a type $\tau\theta$ such that $\mathrm{dom}(\theta) \subseteq \mathrm{var}_K(\tau) \setminus \mathrm{var}_K(\Gamma_2)$ and $K \vdash \theta: K$. It is also an instance of $\mathrm{gen}_{K;\Gamma_1}(\tau)$, with the same $\theta$, since $\mathrm{var}_K(\tau) \setminus \mathrm{var}_K(\Gamma_2) \subseteq \mathrm{var}_K(\tau) \setminus \mathrm{var}_K(\Gamma_1)$. $\square$

**Lemma A.6 (Weakening).** Let $K$ be a kinding environment and $\Gamma_1, \Gamma_2$ two type environments such that $\Gamma_1 \subseteq_K \Gamma_2$ and $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$. If $K; \Gamma_2 \vdash_K e: \tau$, then $K; \Gamma_1 \vdash_K e: \tau$.

*Proof.* By induction on the derivation of $K; \Gamma_2 \vdash_K e: \tau$. We reason by cases on the last applied rule.

*Case Tk-Var* We have:

$$K; \Gamma_2 \vdash_K x: \tau \quad \tau \in \mathrm{inst}_K(\Gamma_2(x))$$

and hence, since $\Gamma_1 \subseteq_K \Gamma_2$, we have $\tau \in \mathrm{inst}_K(\Gamma_1(x))$ and apply Tk-Var to conclude.

*Case Tk-Const* Straightforward.

*Case Tk-Abstr* We have:

$$K; \Gamma_2 \vdash_K \lambda x. e_1: \tau_1 \to \tau_2 \quad K; \Gamma_2, \{x: \tau_1\} \vdash_K e_1: \tau_2.$$

Since $\Gamma_1 \subseteq_K \Gamma_2$, we have $\Gamma_1, \{x: \tau_1\} \subseteq_K \Gamma_2, \{x: \tau_1\}$, and, since $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$, we have $\mathrm{var}_K(\Gamma_1, \{x: \tau_1\}) \subseteq \mathrm{var}_K(\Gamma_2, \{x: \tau_1\})$. Thus we may derive $K; \Gamma_1, \{x: \tau_1\} \vdash_K e_1: \tau_2$ by the induction hypothesis and apply Tk-Abstr to conclude.

*Cases Tk-Appl, Tk-Pair, and Tk-Tag* Straightforward application of the induction hypothesis.

*Case Tk-Match* We have

$$\begin{align*}
K; \Gamma_2 \vdash_K \mathrm{match} e_0 \text{ with } (p_i \to e_i)_{i \in I}: \tau \\
K; \Gamma_2 \vdash_K e_0: \tau_0 \qquad \tau_0 \preceq_K \{p_i \mid i \in I\} \\
\forall i \in I. \quad K \vdash p_i: \tau_0 \Rightarrow \Gamma_i \quad K; \Gamma_2, \mathrm{gen}_{K;\Gamma_2}(\Gamma_i) \vdash_K e_i: \tau.
\end{align*}$$

By the induction hypothesis, we derive $K; \Gamma_1 \vdash_K e_0: \tau_0$.

For every branch, note that by Lemma A.5 $\mathrm{var}_K(\Gamma_1) \subseteq \mathrm{var}_K(\Gamma_2)$ implies $\mathrm{gen}_{K;\Gamma_1}(\tau) \subseteq_K \mathrm{gen}_{K;\Gamma_2}(\tau)$ for any $\tau$. Hence, we have $\Gamma_1, \mathrm{gen}_{K;\Gamma_1}(\Gamma_i) \subseteq_K \Gamma_2, \mathrm{gen}_{K;\Gamma_2}(\Gamma_i)$. Additionally, since $\mathrm{var}_K(\mathrm{gen}_{K;\Gamma_1}(\Gamma_i)) \subseteq \mathrm{var}_K(\Gamma_1, \mathrm{gen}_{K;\Gamma_1}(\Gamma_i)) \subseteq \mathrm{var}_K(\Gamma_2, \mathrm{gen}_{K;\Gamma_2}(\Gamma_i))$.

Hence we may apply the induction hypothesis for all $i$ to derive $K; \Gamma_1, \mathrm{gen}_{K;\Gamma_1}(\Gamma_i) \vdash_K e_i: \tau$ and then apply Tk-Match to conclude. $\square$

**Lemma A.7 (Stability of typing under type substitutions).** Let $K, K'$ be two closed, canonical kinding environments and $\theta$ a type substitution such that $K \vdash \theta: K'$. If $K; \Gamma \vdash_K e: \tau$, then $K'; \Gamma\theta \vdash_K e: \tau\theta$.

*Proof.* By induction on the derivation of $K; \Gamma \vdash_K e: \tau$. We reason by cases on the last applied rule.

*Case Tk-Var* We have

$$\begin{gathered}
K; \Gamma \vdash_K x: \tau \quad \tau \in \mathrm{inst}_K(\Gamma(x)) \\
\Gamma(x) = \forall A. K_x \triangleright \tau_x \quad \tau = \tau_x \theta_x \quad \mathrm{dom}(\theta_x) \subseteq A \quad K, K_x \vdash \theta_x: K
\end{gathered}$$

and must show

$$K'; \Gamma\theta \vdash_K x: \tau\theta.$$

By $\alpha$-renaming we can assume that $\theta$ does not involve $A$, that is, $A \cap \mathrm{dom}(\theta) = \emptyset$ and $A \cap \mathrm{var}_\emptyset(\theta) = \emptyset$, and also that $A \cap (\mathrm{dom}(K') \cup \mathrm{var}_\emptyset(K')) = \emptyset$, that is, that the variables in $A$ are not assigned a kind in $K'$ nor do they appear in the types in the typing component of the kinds in $K'$.

Under these assumptions, $(\Gamma\theta)(x) = \forall A. K_x\theta \triangleright \tau_x\theta$. We must show that $\tau\theta = \tau_x\theta\theta'_x$ for a substitution $\theta'_x$ such that $\mathrm{dom}(\theta'_x) \subseteq A$ and $K_x\theta \vdash \theta'_x: K'$.
We apply weakening (Lemma A.6) to derive from the latter the typing we need, that is,

$$K'; \Gamma \theta, \mathrm{gen}_{K'; \Gamma \theta}(\{x : \tau_0 \theta'\}) \vdash_K e_1 : \tau \theta.$$

To do so we must show

$$\Gamma \theta, \mathrm{gen}_{K'; \Gamma \theta}(\{x : \tau_0 \theta'\}) \subseteq_{K'} \Gamma \theta, (\mathrm{gen}_{K; \Gamma}(\{x : \tau_0\}))\theta \\ \mathrm{var}_{K'}(\Gamma \theta, \mathrm{gen}_{K'; \Gamma \theta}(\{x : \tau_0 \theta'\})) \subseteq \mathrm{var}_{K'}(\Gamma \theta, (\mathrm{gen}_{K; \Gamma}(\{x : \tau_0\}))\theta).$$

The latter holds because $\mathrm{var}_{K'}(\Gamma \theta, \mathrm{gen}_{K'; \Gamma \theta}(\{x : \tau_0 \theta'\})) \subseteq \mathrm{var}_{K'}(\Gamma \theta)$.

As for the former, we prove $\mathrm{gen}_{K'; \Gamma \theta}(\{x : \tau_0 \theta'\}) \subseteq_{K'} (\mathrm{gen}_{K; \Gamma}(\{x : \tau_0\}))\theta$. We have

$$\mathrm{gen}_{K; \Gamma}(\{x : \tau_0\}) = \forall A. K_x \triangleright \tau_0 \qquad K_x = \{ \alpha :: K(\alpha) \mid \alpha \in A \}.$$

By $\alpha$-renaming of the quantified variables we can write

$$\mathrm{gen}_{K; \Gamma}(\{x : \tau_0\}) = \forall B. K_x^* \triangleright \tau_0 \theta_0 \\ K_x^* = \{ \beta_i :: \bullet \mid \alpha_i :: \bullet \in K_x \} \cup \{ \beta_i :: (L, U, T \theta_0) \mid \alpha_i :: (L, U, T) \in A \}$$

and, since $\theta$ does not involve $B$,

$$(\mathrm{gen}_{K; \Gamma}(\{x : \tau_0\}))\theta = \forall B. K_x^* \theta \triangleright \tau_0 \theta_0 \theta = \forall B. K_x' \triangleright \tau_0 \theta' \\ K_x' = \{ \beta :: K'(\beta) \mid \beta \in B \}.$$

The other type scheme is

$$\mathrm{gen}_{K'; \Gamma \theta}(\tau_0 \theta') = \forall C. K_C' \triangleright \tau_0 \theta' \\ C = \mathrm{var}_{K'}(\tau_0 \theta') \setminus \mathrm{var}_{K'}(\Gamma \theta) \qquad K_C' = \{ \beta :: K'(\beta) \mid \beta \in C \}.$$

We show $B \subseteq C$, which concludes the proof (because the kinding environments are both restrictions of $K'$). Consider $\beta_i \in B$. We have $\alpha_i \in \mathrm{var}_K(\tau_0) \setminus \mathrm{var}_K(\Gamma)$. Then $\beta_i = \alpha_i \theta' \in \mathrm{var}_{K'}(\tau_0 \theta')$. Furthermore $\beta_i \notin \mathrm{var}_{K'}(\Gamma \theta)$ holds because $\Gamma \theta$ does not contain variables in $B$ ($\Gamma$ does not contain them and $\theta$ does not introduce them) and variables in $B$ do not appear in the kinds of other variables which are not themselves in $B$.

We now consider the rule *Tk-Match* in its generality. We have

$$K; \Gamma \vdash_K \mathit{match} e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau \\ K; \Gamma \vdash_{\bar{K}} e_0 : \tau_0 \qquad \tau_0 \preceq_K \{ p_i \mid i \in I \} \\ \forall i \in I. \quad K \vdash p_i : \tau_0 \Rightarrow \Gamma_i \qquad K; \Gamma, \mathrm{gen}_{K; \Gamma}(\Gamma_i) \vdash_{\bar{K}} e_i : \tau$$

and must show

$$K'; \Gamma \theta \vdash_K \mathit{match} e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau \theta$$

which we prove by establishing, for some $\hat{\tau}_0$ and $\{ \hat{\Gamma}_i \mid i \in I \}$, that

$$K'; \Gamma \theta \vdash_{\bar{K}} e_0 : \hat{\tau}_0 \qquad \hat{\tau}_0 \preceq_{K'} \{ p_i \mid i \in I \} \\ \forall i \in I. \quad K' \vdash p_i : \hat{\tau}_0 \Rightarrow \hat{\Gamma}_i \qquad K'; \Gamma \theta, \mathrm{gen}_{K'; \Gamma \theta}(\hat{\Gamma}_i) \vdash_{\bar{K}} e_i : \tau \theta.$$

For the derivation for $e_0$ we proceed as above and have $\hat{\tau}_0 = \tau_0 \theta'$. By Lemma A.4 we have $\tau_0 \theta' \preceq_{K'} \{ p_i \mid i \in I \}$. By Lemma A.3, we have $K' \vdash p_i : \tau_0 \theta' \Rightarrow \Gamma_i \theta'$ and thus take $\hat{\Gamma}_i = \Gamma_i \theta'$.

We proceed as before also for the derivations for each branch. The difference is that, to apply weakening, we must prove the two premises for the environments and not for $\tau_0$ alone. The condition on variables is straightforward, as before. For the other we prove, for each $x \in \mathrm{capt}(p_i)$ and assuming $\Gamma_i(x) = \tau_x$,

$$\Gamma \theta, \mathrm{gen}_{K'; \Gamma \theta}(\tau_x \theta') \subseteq_{K'} \Gamma \theta, (\mathrm{gen}_{K; \Gamma}(\tau_x))\theta.$$

We show it as for $\tau_0$ above: $\mathrm{var}_K(\tau_x)$ is always a subset of $\mathrm{var}_K(\tau_0)$ because environment generation does not introduce new variables. $\square$

**Lemma A.8 (Expression substitution).** Let $x_1, \dots, x_n$ be distinct variables and $v_1, \dots, v_n$ values. Let $\Gamma' = \{x_1 : \sigma_1, \dots, x_n : \sigma_n\}$ and $\zeta = [v_1/x_1, \dots, v_n/x_n]$.

If $K; \Gamma, \Gamma' \vdash_K e : \tau$ and, for all $k \in \{1, \dots, n\}$ and for all $\tau_k \in \mathrm{inst}_K(\sigma_k)$, $K; \Gamma \vdash_{\bar{K}} v_k : \tau_k$, then $K; \Gamma \vdash_{\bar{K}} e \zeta : \tau$.

*Proof.* By induction on the derivation of $K; \Gamma, \Gamma' \vdash_K e : \tau$. We reason by cases on the last applied rule.

*Case Tk-Var* We have

$$K; \Gamma, \Gamma' \vdash_K x : \tau \qquad \tau \in \mathrm{inst}_K((\Gamma, \Gamma')(x)).$$
Let $\theta'_x = [\alpha\theta_x\theta/\alpha | \alpha \in A]$. First, we show that $\tau_x\theta\theta'_x = \tau_x\theta_x\theta = \tau\theta$, by showing that, for any $\alpha$, $\alpha\theta\theta'_x = \alpha\theta_x\theta$. If $\alpha \in A$, then $\alpha\theta\theta'_x = \alpha\theta'_x = \alpha\theta_x\theta$ ($\theta$ is not defined on the variables in A). If $\alpha \notin A$, then $\alpha\theta\theta'_x = \alpha\theta$ ($\theta$ never produces any variable in A) and $\alpha\theta_x\theta = \alpha\theta$ as $\alpha \notin \text{dom}(\theta_x)$.

Since $\text{dom}(\theta'_x) \subseteq A$ holds, we only need to establish that $K', K_x\theta \vdash \theta'_x: K'$. This requires proving, for each $\alpha$ such that $(K', K_x\theta)(\alpha) = (L, U, T)$, that $\alpha\theta'_x$ is a type variable such that $K'(\alpha\theta'_x) = (L', U', T')$ and $(L', U', T') \vdash (L, U, T\theta'_x)$.

Such an $\alpha$ can either be in the domain of $K_x\theta$ (if and only if it is in A) or in the domain of $K'$. In the latter case, we have $\alpha\theta'_x = \alpha$, since $\alpha \notin A$, and hence its kind in $K'$ is the same as in $K'$, $K_x\theta$. We must prove $(L, U, T) \vdash (L, U, T\theta'_x)$, which holds because the variables in A do not appear in T since $(L, U, T) \in \text{range}(K')$.

In the former case, we have $(K_x\theta)(\alpha) = (L, U, T)$ and hence $K_x(\alpha) = (L, U, T_1)$, with $T = T_1\theta$. Also, $\alpha\theta'_x = \alpha\theta_x\theta$. Since $K, K_x \vdash \theta_x: K, K(\alpha\theta_x) = (L_2, U_2, T_2)$. Then, since $K \vdash \theta: K', K'(\alpha\theta_x\theta) = (L', U', T')$. We know $(L_2, U_2, T_2) \vdash (L, U, T_1\theta_x)$ and $(L', U', T') \vdash (L_2, U_2, T_2\theta)$. Both $L' \supseteq L$ and $U' \subseteq U$ hold by transitivity. We show $T' \supseteq T\theta'_x$ holds as well. If `tag: $\tau \in T\theta'_x$, since $T = T_1\theta$, then `tag: $\tau_1 \in T_1$ and $\tau = \tau_1\theta\theta'_x = \tau_1\theta_x\theta$. We thus have `tag: $\tau_1\theta_x \in T_1\theta_x$ and therefore `tag: $\tau_1\theta_x \in T_2$ and `tag: $\tau_1\theta_x\theta \in T'$.

**Case Tk-Const** Straightforward.

**Case Tk-Abstr** We have:

$$ K; \Gamma \vdash_K \lambda x. e_1 : \tau_1 \rightarrow \tau_2 \qquad K; \Gamma, \{x : \tau_1\} \vdash_K e_1 : \tau_2. $$

By the induction hypothesis we have $K'; \Gamma\theta, \{x : \tau_1\theta\} \vdash_K e_1 : \tau_2\theta$. Then by Tk-Abstr we derive $K'; \Gamma\theta \vdash_K \lambda x. e_1 : (\tau_1 \rightarrow \tau_2)\theta$, since $(\tau_1 \rightarrow \tau_2)\theta = (\tau_1\theta) \rightarrow (\tau_2\theta)$.

**Cases Tk-Appl and Tk-Pair** Straightforward application of the induction hypothesis.

**Case Tk-Match** For the sake of clarity, we first prove the simpler case corresponding to (the encoding of) let, where—simplifying environment generation—we have

$$ K; \Gamma \vdash_K \mathit{match} \ e_0 \ \mathit{with} \ x \ \to \ e_1 : \tau \qquad K; \Gamma \vdash_K e_0 : \tau_0 \qquad K; \Gamma, \mathit{gen}_{K;\Gamma}(\{x : \tau_0\}) \vdash_K e_1 : \tau $$

and must show

$$ K'; \Gamma\theta \vdash_K \mathit{match} \ e_0 \ \mathit{with} \ x \ \to \ e_1 : \tau\theta $$

which we prove by establishing, for some type $\hat{\tau}_0$, that

$$ K'; \Gamma\theta \vdash_K e_0 : \hat{\tau}_0 \qquad K'; \Gamma\theta, \mathit{gen}_{K';\Gamma\theta}(\{x : \hat{\tau}_0\}) \vdash_K e_1 : \tau\theta. $$

Let $A = \{\alpha_1, \dots, \alpha_n\} = \mathit{var}_K(\tau_0) \setminus \mathit{var}_K(\Gamma)$. We assume that the variables in A do not appear in the kinds of variables not in A, that is, that if $K(\alpha) = (L, U, T)$ and $\alpha \notin A$, then $\mathit{var}_K(T) \cap A = \emptyset$.

This assumption is justified by the following observations. The variables in A only appear quantified in the environment used for the typing derivation for $e_1$. Therefore we may assume that they do not appear in $\tau$: if they do, it is because they have been chosen when instantiating some type scheme and, since K is canonical, we might have chosen some other variable of the same kind. As for the occurrences of the variables in A in the derivation for $e_0$, a similar reasoning applies. These variables do not appear free in the environment (neither directly in a type in $\Gamma$, nor in the kinds of variables which appear free in $\Gamma$). Therefore, if they occur in $\tau_0$ it is because they have been chosen either during instantiation of a type scheme or when typing an abstraction, and in both cases we might have chosen a different variable.

Now we rename these variables so that $\theta$ will not have effect on them. Let $B = \{\beta_1, \dots, \beta_n\}$ be a set of type variables such that $B \cap (\text{dom}(\theta) \cup \text{var}_\emptyset(\theta)) = \emptyset$ and $B \cap \text{var}_\emptyset(\Gamma) = \emptyset$. Let $\theta_0 = [\beta_1/\alpha_1, \dots, \beta_n/\alpha_n]$ and $\theta' = \theta \circ \theta_0$. Since $K'$ is canonical, we can choose each $\beta_i$ so that, if $K(\alpha_i) = \bullet$, then $K'(\beta_i) = \bullet$, and if $K(\alpha_i) = (L, U, T)$, then $K(\beta_i) = (L, U, T')$. As for A, we choose B so that the kinds in $K'$ for variables not in B do not contain variables of B.

We show $K \vdash \theta' : K'$. For each $\alpha$ such that $K(\alpha) = (L, U, T)$, if $\alpha \in A$ then $\alpha = \alpha_i$ for some $i$, $\alpha\theta' = \beta_i$ and kind entailment holds straightforwardly by our choice of $\beta_i$. If $\alpha \notin A$, then $\alpha\theta' = \alpha\theta$ and the admissibility of $\theta$ implies $K'(\alpha\theta) = (L', U', T')$ and $(L', U', T') \vdash (L, U, T\theta)$. We have $T\theta = T\theta'$ because of our assumption on A.

Since $\theta'$ is admissibile, by the induction hypothesis applied to $\theta'$, we derive $K; \Gamma\theta' \vdash_K e_0 : \tau_0\theta'$. Since the variables in A do not appear in $\Gamma$, we have $\Gamma\theta' = \Gamma\theta$. We choose $\hat{\tau}_0$ to be $\tau_0\theta'$.

We apply the induction hypothesis to the derivation for $e_1$, this time using $\theta$ as the substitution. Now we have:

$$ K'; \Gamma\theta \vdash_K e_0 : \tau_0\theta' \qquad K'; \Gamma\theta, (\mathit{gen}_{K;\Gamma}(\{x : \tau_0\}))\theta \vdash_K e_1 : \tau\theta. $$
Either $x = x_k$ for some $k$ or not. In the latter case, $x\zeta = x, x \notin \text{dom}(\Gamma')$ and hence $(\Gamma, \Gamma')(x) = \Gamma(x)$. Then, since $\tau \in \text{inst}_K((\Gamma, \Gamma')(x)), \tau \in \text{inst}_K(\Gamma(x))$ and Tk-Var can be applied.

If $x = x_k$, then $(\Gamma, \Gamma')(x) = \Gamma'(x) = \sigma_k$. We must then prove $K; \Gamma \vdash_{\mathfrak{k}} v_k : \tau$, which we know by hypothesis since $\tau \in \text{inst}_K(\sigma_k)$.

*Case Tk-Const* Straightforward.

*Case Tk-Abstr* We have

$$K; \Gamma, \Gamma' \vdash_{\mathfrak{k}} \lambda x. e_1 : \tau_1 \rightarrow \tau_2 \qquad K; \Gamma, \Gamma', \{x : \tau_1\} \vdash_{\mathfrak{k}} e_1 : \tau_2.$$

By $\alpha$-renaming we can assume $x \notin \text{dom}(\Gamma')$; then $(\lambda x. e_1)\zeta = \lambda x. (e_1\zeta)$ and $\Gamma, \Gamma', \{x : \tau_1\} = \Gamma, \{x : \tau_1\}, \Gamma'$. Therefore we have $K; \Gamma, \{x : \tau_1\}, \Gamma' \vdash_{\mathfrak{k}} e_1 : \tau_2$ and, by the induction hypothesis, $K; \Gamma, \{x : \tau_1\} \vdash_{\mathfrak{k}} e_1\zeta : \tau_2$. We apply Tk-Abstr to conclude.

*Cases Tk-Appl, Tk-Pair, and Tk-Tag* Straightforward application of the induction hypothesis.

*Case Tk-Match* We have

$$K; \Gamma, \Gamma' \vdash_{\mathfrak{k}} \text{match } e_0 \text{ with } (p_i \rightarrow e_i)_{i \in I} : \tau$$

$$K; \Gamma, \Gamma' \vdash_{\mathfrak{k}} e_0 : \tau_0 \qquad \tau_0 \preceq_K \{p_i \mid i \in I\}$$

$$\forall i \in I. \quad K \vdash p_i : \tau_0 \Rightarrow \Gamma_i \qquad K; \Gamma, \Gamma', \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i) \vdash_{\mathfrak{k}} e_i : \tau.$$

We assume by $\alpha$-renaming that no capture variable of any pattern is in the domain of $\Gamma'$. Then, (match $e_0$ with $(p_i \rightarrow e_i)_{i \in I})\zeta = \text{match } e_0\zeta$ with $(p_i \rightarrow e_i)_{i \in I}$ and $\Gamma, \Gamma', \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i) = \Gamma, \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i), \Gamma'$ for any $i$.

By the induction hypothesis, we derive $K; \Gamma \vdash_{\mathfrak{k}} e_0\zeta : \tau_0$ and $K; \Gamma, \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i) \vdash_{\mathfrak{k}} e_i\zeta : \tau$ for all $i$. From the latter, we prove $K; \Gamma, \text{gen}_{K;\Gamma}(\Gamma_i) \vdash_{\mathfrak{k}} e_i\zeta : \tau$ by weakening (Lemma A.6): we have $\text{gen}_{K;\Gamma}(\Gamma_i) \subseteq_K \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i)$ by Lemma A.5—since $\text{var}_K(\Gamma) \subseteq \text{var}_K(\Gamma, \Gamma')$—and clearly we have $\text{var}_K(\Gamma, \text{gen}_{K;\Gamma}(\Gamma_i)) \subseteq \text{var}_K(\Gamma, \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i))$ since $\text{var}_K(\text{gen}_{K;\Gamma}(\Gamma_i)) \subseteq \text{var}_K(\Gamma)$. $\square$

**Theorem A.9 (Progress).** Let $e$ be a well-typed, closed expression. Then, either $e$ is a value or there exists an expression $e'$ such that $e \rightsquigarrow e'$.

*Proof.* By hypothesis we have $K; \emptyset \vdash_{\mathfrak{k}} e : \tau$. The proof is by induction on its derivation; we reason by cases on the last applied rule.

*Case Tk-Var* This case does not occur because variables are not closed.

*Case Tk-Const* In this case $e$ is a constant $c$ and therefore a value.

*Case Tk-Abstr* In this case $e$ is an abstraction $\lambda x. e_1$. Since it is also closed, it is a value.

*Case Tk-Appl* We have

$$K; \emptyset \vdash_{\mathfrak{k}} e_1 e_2 : \tau \qquad K; \emptyset \vdash_{\mathfrak{k}} e_1 : \tau' \rightarrow \tau \qquad K; \emptyset \vdash_{\mathfrak{k}} e_2 : \tau'$$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e_1'$, then $e_1 e_2 \rightsquigarrow e_1' e_2$. If $e_1$ is a value and $e_2 \rightsquigarrow e_2'$, then $e_1 e_2 \rightsquigarrow e_1 e_2'$.

If both are values then, by Lemma A.1, $e_1$ has the form $\lambda x. e_3$ for some $e_3$. Then, we can apply R-Appl and $e_1 e_2 \rightsquigarrow e_3[e^2/x]$.

*Case Tk-Pair* We have

$$K; \emptyset \vdash_{\mathfrak{k}} (e_1, e_2) : \tau_1 \times \tau_2 \qquad K; \emptyset \vdash_{\mathfrak{k}} e_1 : \tau_1 \qquad K; \emptyset \vdash_{\mathfrak{k}} e_2 : \tau_2.$$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e_1'$, then $(e_1, e_2) \rightsquigarrow (e_1', e_2)$. If $e_1$ is a value and $e_2 \rightsquigarrow e_2'$, then $(e_1, e_2) \rightsquigarrow (e_1, e_2')$. If both are values, then $(e_1, e_2)$ is also a value.

*Case Tk-Tag* We have

$$K; \emptyset \vdash_{\mathfrak{k}} 'tag(e_1) : \alpha \qquad K; \emptyset \vdash_{\mathfrak{k}} e_1 : \tau_1.$$

Analogously to the previous case, by the induction hypothesis we have that either $e_1$ is a value or $e_1 \rightsquigarrow e_1'$. In the former case, '$tag(e_1)$ is a value as well. In the latter, we have '$tag(e_1) \rightsquigarrow tag(e_1)'.

*Case Tk-Match* We have

$$K; \emptyset \vdash_{\mathfrak{k}} \text{match } e_0 \text{ with } (p_i \rightarrow e_i)_{i \in I} : \tau \qquad K; \emptyset \vdash_{\mathfrak{k}} e_0 : \tau_0 \qquad \tau_0 \preceq_K \{p_i \mid i \in I\}.$$

By the inductive hypothesis, either $e_0$ is a value or it may reduce. In the latter case, if $e_0 \rightsquigarrow e_0'$, then match $e_0$ with $(p_i \rightarrow e_i)_{i \in I} \rightsquigarrow \text{match } e_0'$ with $(p_i \rightarrow e_i)_{i \in I}$.
We apply weakening (Lemma A.6) to derive from the latter the typing we need, that is,

$$K'; \Gamma\theta, \mathrm{gen}_{K';\Gamma\theta}(\{x : \tau_0\theta'\}) \vdash_K e_1 : \tau\theta.$$

To do so we must show

$$\Gamma\theta, \mathrm{gen}_{K';\Gamma\theta}(\{x : \tau_0\theta'\}) \subseteq_{K'} \Gamma\theta, (\mathrm{gen}_{K;\Gamma}(\{x : \tau_0\}))\theta \\ \mathrm{var}_{K'}(\Gamma\theta, \mathrm{gen}_{K';\Gamma\theta}(\{x : \tau_0\theta'\})) \subseteq \mathrm{var}_{K'}(\Gamma\theta, (\mathrm{gen}_{K;\Gamma}(\{x : \tau_0\}))\theta).$$

The latter holds because $\mathrm{var}_{K'}(\Gamma\theta, \mathrm{gen}_{K';\Gamma\theta}(\{x : \tau_0\theta'\})) \subseteq \mathrm{var}_{K'}(\Gamma\theta)$.

As for the former, we prove $\mathrm{gen}_{K';\Gamma\theta}(\{x : \tau_0\theta'\}) \subseteq_{K'} (\mathrm{gen}_{K;\Gamma}(\{x : \tau_0\}))\theta$. We have

$$\mathrm{gen}_{K;\Gamma}(\{x : \tau_0\}) = \forall A. K_x \triangleright \tau_0 \qquad K_x = \{ \alpha :: K(\alpha) \mid \alpha \in A \}.$$

By $\alpha$-renaming of the quantified variables we can write

$$\mathrm{gen}_{K;\Gamma}(\{x : \tau_0\}) = \forall B. K_x^* \triangleright \tau_0\theta_0 \\ K_x^* = \{ \beta_i :: \bullet \mid \alpha_i :: \bullet \in K_x \} \cup \{ \beta_i :: (L, U, T\theta_0) \mid \alpha_i :: (L, U, T) \in A \}$$

and, since $\theta$ does not involve $B$,

$$(\mathrm{gen}_{K;\Gamma}(\{x : \tau_0\}))\theta = \forall B. K_x^*\theta \triangleright \tau_0\theta_0\theta = \forall B. K_x'\triangleright \tau_0\theta' \\ K_x' = \{ \beta :: K'(\beta) \mid \beta \in B \}.$$

The other type scheme is

$$\mathrm{gen}_{K';\Gamma\theta}(\tau_0\theta') = \forall C. K_C' \triangleright \tau_0\theta' \\ C = \mathrm{var}_{K'}(\tau_0\theta') \setminus \mathrm{var}_{K'}(\Gamma\theta) \qquad K_C' = \{ \beta :: K'(\beta) \mid \beta \in C \}.$$

We show $B \subseteq C$, which concludes the proof (because the kinding environments are both restrictions of $K'$). Consider $\beta_i \in B$. We have $\alpha_i \in \mathrm{var}_K(\tau_0) \setminus \mathrm{var}_K(\Gamma)$. Then $\beta_i = \alpha_i\theta' \in \mathrm{var}_{K'}(\tau_0\theta')$. Furthermore $\beta_i \notin \mathrm{var}_{K'}(\Gamma\theta)$ holds because $\Gamma\theta$ does not contain variables in $B$ ($\Gamma$ does not contain them and $\theta$ does not introduce them) and variables in $B$ do not appear in the kinds of other variables which are not themselves in $B$.

We now consider the rule *Tk-Match* in its generality. We have

$$K; \Gamma \vdash_K \mathit{match} e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau \\ K; \Gamma \vdash_K e_0 : \tau_0 \qquad \tau_0 \preceq_K \{ p_i \mid i \in I \} \\ \forall i \in I. \quad K \vdash p_i : \tau_0 \Rightarrow \Gamma_i \qquad K; \Gamma, \mathrm{gen}_{K;\Gamma}(\Gamma_i) \vdash_K e_i : \tau$$

and must show

$$K'; \Gamma\theta \vdash_K \mathit{match} e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau\theta$$

which we prove by establishing, for some $\hat{\tau}_0$ and $\{\hat{\Gamma}_i \mid i \in I\}$, that

$$K'; \Gamma\theta \vdash_K e_0 : \hat{\tau}_0 \qquad \hat{\tau}_0 \preceq_{K'} \{ p_i \mid i \in I \} \\ \forall i \in I. \quad K' \vdash p_i : \hat{\tau}_0 \Rightarrow \hat{\Gamma}_i \qquad K'; \Gamma\theta, \mathrm{gen}_{K';\Gamma\theta}(\hat{\Gamma}_i) \vdash_K e_i : \tau\theta.$$

For the derivation for $e_0$ we proceed as above and have $\hat{\tau}_0 = \tau_0\theta'$. By Lemma A.4 we have $\tau_0\theta' \preceq_{K'} \{p_i \mid i \in I\}$. By Lemma A.3, we have $K' \vdash p_i : \tau_0\theta' \Rightarrow \Gamma_i\theta'$ and thus take $\hat{\Gamma}_i = \Gamma_i\theta'$.

We proceed as before also for the derivations for each branch. The difference is that, to apply weakening, we must prove the two premises for the environments and not for $\tau_0$ alone. The condition on variables is straightforward, as before. For the other we prove, for each $x \in \mathrm{capt}(p_i)$ and assuming $\Gamma_i(x) = \tau_x$,

$$\Gamma\theta, \mathrm{gen}_{K';\Gamma\theta}(\tau_x\theta') \subseteq_{K'} \Gamma\theta, (\mathrm{gen}_{K;\Gamma}(\tau_x))\theta.$$

We show it as for $\tau_0$ above: $\mathrm{var}_K(\tau_x)$ is always a subset of $\mathrm{var}_K(\tau_0)$ because environment generation does not introduce new variables. $\square$

**Lemma A.8 (Expression substitution).** Let $x_1, \dots, x_n$ be distinct variables and $v_1, \dots, v_n$ values. Let $\Gamma' = \{x_1 : \sigma_1, \dots, x_n : \sigma_n\}$ and $\zeta = [v_1/x_1, \dots, v_n/x_n]$.

If $K; \Gamma, \Gamma' \vdash_K e : \tau$ and, for all $k \in \{1, \dots, n\}$ and for all $\tau_k \in \mathrm{inst}_K(\sigma_k)$, $K; \Gamma \vdash_K v_k : \tau_k$, then $K; \Gamma \vdash_K e\zeta : \tau$.

*Proof.* By induction on the derivation of $K; \Gamma, \Gamma' \vdash_K e : \tau$. We reason by cases on the last applied rule.

*Case Tk-Var* We have

$$K; \Gamma, \Gamma' \vdash_K x : \tau \qquad \tau \in \mathrm{inst}_K((\Gamma, \Gamma')(x)).$$
If $e_0$ is a value, on the other hand, the expression may reduce by application of R-Match. Since $\tau_0 \preceq_K \{p_i | i \in I\}$ and $e_0$ is a value of type $\tau_0$ (and therefore satisfies the premises of the definition of exhaustiveness, with $\theta = []$ and $K = K'$), there exists at least an $i \in I$ such that $e_0/p_i = \zeta$ for some substitution $\zeta$. Let $j$ be the least of these $i$ and $\zeta_j$ the corresponding substitution; then match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow e_j \zeta_j$. □

**Theorem A.10 (Subject reduction).** Let $e$ be an expression and $\tau$ a type such that $K; \Gamma \vdash_K e: \tau$. If $e \rightsquigarrow e'$, then $K; \Gamma \vdash_K e': \tau$.

*Proof.* By induction on the derivation of $K; \Gamma \vdash_K e: \tau$. We reason by cases on the last applied rule.

**Cases Tk-Var, Tk-Const, and Tk-Abstr** These cases may not occur: variables, constants, and abstractions never reduce.

**Case Tk-Appl** We have

$$K; \Gamma \vdash_K e_1 e_2: \tau \qquad K; \Gamma \vdash_K e_1: \tau' \to \tau \qquad K; \Gamma \vdash_K e_2: \tau'$$

$e_1 e_2 \rightsquigarrow e'$ occurs in any of three ways: (i) $e_1 \rightsquigarrow e'_1$ and $e' = e'_1 e_2$; (ii) $e_1$ is a value, $e_2 \rightsquigarrow e'_2$ and $e' = e_1 e'_2$; (iii) both $e_1$ and $e_2$ are values, $e_1$ is of the form $\lambda x.e_3$, and $e' = e_3[e^2/x]$.

In the first case, we derive by the induction hypothesis that $K; \Gamma \vdash_K e'_1: \tau' \to \tau$ and conclude by applying Tk-Appl again. The second case is analogous.

In the third case, we know by Lemma A.1 that $K; \Gamma, \{x: \tau'\} \vdash_K e_3: \tau$. We also know that $e_2$ is a value such that $K; \Gamma \vdash_K e_2: \tau'$. Then, by Lemma A.8, $K; \Gamma \vdash_K e_3[e^2/x]: \tau$.

**Case Tk-Pair** We have

$$K; \Gamma \vdash_K (e_1, e_2): \tau_1 \times \tau_2 \qquad K; \Gamma \vdash_K e_1: \tau_1 \qquad K; \Gamma \vdash_K e_2: \tau_2.$$

$(e_1, e_2) \rightsquigarrow e'$ occurs either because $e_1 \rightsquigarrow e'_1$ and $e' = (e'_1, e_2)$, or because $e_1$ is a value, $e_2 \rightsquigarrow e'_2$, and $e' = (e_1, e'_2)$. In either case, the induction hypothesis allows us to derive that the type of the component that reduces is preserved; therefore, we can apply Tk-Pair again to conclude.

**Case Tk-Tag** Analogously to the previous case, a variant expression only reduces if its argument does, so we apply the induction hypothesis and Tk-Tag to conclude.

**Case Tk-Match** We have

$$K; \Gamma \vdash_K \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I}: \tau \qquad K; \Gamma \vdash_K e_0: \tau_0 \qquad \forall i \in I. K \vdash p_i: \tau_0 \Rightarrow \Gamma_i \qquad K; \Gamma, \text{gen}_{K;\Gamma}(\Gamma_i) \vdash_K e_i: \tau.$$

match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow e'$ occurs either because $e_0 \rightsquigarrow e'_0$ and $e' = \text{match } e'_0$ with $(p_i \to e_i)_{i \in I}$ or because $e_0$ is a value and $e' = e_j \zeta$, where $e_0/p_j = \zeta$ and, for all $i < j$, $e_0/p_i = \Omega$. In the former case, we apply the induction hypothesis and conclude by Tk-Match.

In the latter case, $\zeta$ is a substitution from the capture variables of $p_j$ to values, and we know by Lemma A.2 that, for all $x \in \text{capt}(p_j)$, $K; \Gamma \vdash_K x\zeta: \Gamma_j(x)$. We show that, additionally, $K; \Gamma \vdash_K x\zeta: \tau_x$ holds for every $\tau_x \in \text{inst}_K(\text{gen}_{K;\Gamma}(\Gamma_j(x)))$. Every such $\tau_x$ is equal to $\Gamma_j(x)\theta$ for a $\theta$ such that $\text{dom}(\theta) \subseteq \text{var}_K(\Gamma_j(x)) \setminus \text{var}_K(\Gamma)$ and $K \vdash \theta: K$ (the kinding environment captured by generalization is just a subset of $K$). Then, $K; \Gamma \vdash_K x\zeta: \Gamma_j(x)\theta$ holds by Lemma A.14, since $\Gamma\theta = \Gamma$ (the substitution does not change any free variable of $\Gamma$).

From $K; \Gamma, \text{gen}_{K;\Gamma}(\Gamma_j) \vdash_K e_j: \tau$ and from the fact that we have $K; \Gamma \vdash_K x\zeta: \tau_x$ for all $x \in \text{dom}(\Gamma_j)$ and all $\tau_x \in \text{inst}_K(\text{gen}_{K;\Gamma}(\Gamma_j(x)))$, we derive $K; \Gamma \vdash_K e_j\zeta: \tau$ by Lemma A.8. □

**Corollary A.11 (Type soundness).** Let $e$ be a well-typed, closed expression, that is, such that $K; \emptyset \vdash_K e: \tau$ holds for some $\tau$. Then, either $e$ diverges or it reduces to a value $v$ such that $K; \emptyset \vdash_K v: \tau$.

*Proof.* Consequence of Theorem A.9 and Theorem A.10. □

## A.3 Typing variants with set-theoretic types

### A.3.1 Definition of the $\mathfrak{S}$ type system

We consider a set $\mathcal{V}$ of type variables (ranged over by $\alpha, \beta, \gamma, \dots$) and the sets $\mathcal{C}, \mathcal{L}$, and $\mathcal{B}$ of language constants, tags, and basic types (ranged over by $c, \text{'tag},$ and $b$ respectively).

**Definition A.22 (Types).** A type $t$ is a term coinductively produced by the following grammar:

$$t ::= \alpha | b | c | t \to t | t \times t | \text{'tag}(t) | t \lor t | \neg t | \emptyset$$

which satisfies two additional constraints:
Either $x = x_k$ for some $k$ or not. In the latter case, $x_\zeta = x, x \notin \text{dom}(\Gamma')$ and hence $(\Gamma, \Gamma')(x) = \Gamma(x)$. Then, since $\tau \in \text{inst}_K((\Gamma, \Gamma')(x)), \tau \in \text{inst}_K(\Gamma(x))$ and Tk-Var can be applied.

If $x = x_k$, then $(\Gamma, \Gamma')(x) = \Gamma'(x) = \sigma_k$. We must then prove $K; \Gamma \vdash_K v_k : \tau$, which we know by hypothesis since $\tau \in \text{inst}_K(\sigma_k)$.

**Case Tk-Const** Straightforward.

**Case Tk-Abstr** We have

$$K; \Gamma, \Gamma' \vdash_K \lambda x. e_1 : \tau_1 \to \tau_2 \qquad K; \Gamma, \Gamma', \{x : \tau_1\} \vdash_K e_1 : \tau_2.$$

By $\alpha$-renaming we can assume $x \notin \text{dom}(\Gamma')$; then $(\lambda x. e_1)_\zeta = \lambda x. (e_1_\zeta)$ and $\Gamma, \Gamma', \{x : \tau_1\} = \Gamma, \{x : \tau_1\}, \Gamma'$. Therefore we have $K; \Gamma, \{x : \tau_1\}, \Gamma' \vdash_K e_1 : \tau_2$ and, by the induction hypothesis, $K; \Gamma, \{x : \tau_1\} \vdash_K e_1_\zeta : \tau_2$. We apply Tk-Abstr to conclude.

**Cases Tk-Appl, Tk-Pair, and Tk-Tag** Straightforward application of the induction hypothesis.

**Case Tk-Match** We have

$$K; \Gamma, \Gamma' \vdash_K \text{ match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau$$

$$K; \Gamma, \Gamma' \vdash_K e_0 : \tau_0 \qquad \tau_0 \preceq_K \{p_i \mid i \in I\}$$

$$\forall i \in I. \quad K \vdash p_i : \tau_0 \Rightarrow \Gamma_i \qquad K; \Gamma, \Gamma', \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i) \vdash_K e_i : \tau.$$

We assume by $\alpha$-renaming that no capture variable of any pattern is in the domain of $\Gamma'$. Then, (match $e_0$ with $(p_i \to e_i)_{i \in I})_\zeta = \text{match } e_0_\zeta$ with $(p_i \to e_i)_\zeta$ and $\Gamma, \Gamma', \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i) = \Gamma, \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i), \Gamma'$ for any $i$.

By the induction hypothesis, we derive $K; \Gamma \vdash_K e_0_\zeta : \tau_0$ and $K; \Gamma, \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i) \vdash_K e_i_\zeta : \tau$ for all $i$. From the latter, we prove $K; \Gamma, \text{gen}_{K;\Gamma}(\Gamma_i) \vdash_K e_i_\zeta : \tau$ by weakening (Lemma A.6): we have $\text{gen}_{K;\Gamma}(\Gamma_i) \subseteq_K \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i)$ by Lemma A.5—since $\text{var}_K(\Gamma) \subseteq \text{var}_K(\Gamma, \Gamma')$—and clearly we have $\text{var}_K(\Gamma, \text{gen}_{K;\Gamma}(\Gamma_i)) \subseteq \text{var}_K(\Gamma, \text{gen}_{K;\Gamma,\Gamma'}(\Gamma_i))$ since $\text{var}_K(\text{gen}_{K;\Gamma}(\Gamma_i)) \subseteq \text{var}_K(\Gamma)$. $\square$

**Theorem A.9 (Progress).** Let $e$ be a well-typed, closed expression. Then, either $e$ is a value or there exists an expression $e'$ such that $e \rightsquigarrow e'$.

*Proof.* By hypothesis we have $K; \emptyset \vdash_K e : \tau$. The proof is by induction on its derivation; we reason by cases on the last applied rule.

**Case Tk-Var** This case does not occur because variables are not closed.

**Case Tk-Const** In this case $e$ is a constant $c$ and therefore a value.

**Case Tk-Abstr** In this case $e$ is an abstraction $\lambda x. e_1$. Since it is also closed, it is a value.

**Case Tk-Appl** We have

$$K; \emptyset \vdash_K e_1 e_2 : \tau \qquad K; \emptyset \vdash_K e_1 : \tau' \to \tau \qquad K; \emptyset \vdash_K e_2 : \tau'$$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e'_1$, then $e_1 e_2 \rightsquigarrow e'_1 e_2$. If $e_1$ is a value and $e_2 \rightsquigarrow e'_2$, then $e_1 e_2 \rightsquigarrow e_1 e'_2$.

If both are values then, by Lemma A.1, $e_1$ has the form $\lambda x. e_3$ for some $e_3$. Then, we can apply R-Appl and $e_1 e_2 \rightsquigarrow e_3[e^2/x]$.

**Case Tk-Pair** We have

$$K; \emptyset \vdash_K (e_1, e_2) : \tau_1 \times \tau_2 \qquad K; \emptyset \vdash_K e_1 : \tau_1 \qquad K; \emptyset \vdash_K e_2 : \tau_2.$$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e'_1$, then $(e_1, e_2) \rightsquigarrow (e'_1, e_2)$. If $e_1$ is a value and $e_2 \rightsquigarrow e'_2$, then $(e_1, e_2) \rightsquigarrow (e_1, e'_2)$. If both are values, then $(e_1, e_2)$ is also a value.

**Case Tk-Tag** We have

$$K; \emptyset \vdash_K \text{'tag}(e_1) : \alpha \qquad K; \emptyset \vdash_K e_1 : \tau_1.$$

Analogously to the previous case, by the induction hypothesis we have that either $e_1$ is a value or $e_1 \rightsquigarrow e'_1$. In the former case, `tag(e_1)` is a value as well. In the latter, we have `tag(e_1) \rightsquigarrow tag(e'_1)`.

**Case Tk-Match** We have

$$K; \emptyset \vdash_K \text{ match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : \tau \qquad K; \emptyset \vdash_K e_0 : \tau_0 \qquad \tau_0 \preceq_K \{p_i \mid i \in I\}.$$

By the inductive hypothesis, either $e_0$ is a value or it may reduce. In the latter case, if $e_0 \rightsquigarrow e'_0$, then match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow \text{match } e'_0$ with $(p_i \to e_i)_{i \in I}$.
* (regularity) the term must have a finite number of different sub-terms;

* (contractivity) every infinite branch must contain an infinite number of occurrences of atoms (i.e., a type variable or the immediate application of a type constructor: basic, constant, arrow, product, or variant).

We introduce the following abbreviations:

$$t_1 \wedge t_2 \stackrel{\text{def}}{=} \neg(\neg t_1 \vee \neg t_2) \quad t_1 \setminus t_2 \stackrel{\text{def}}{=} t_1 \wedge (\neg t_2) \quad 1 \stackrel{\text{def}}{=} \neg \emptyset.$$

**Definition A.23 (Type schemes).** A type scheme $s$ is of the form $\forall A. t$, where $A$ is a finite set $\{\alpha_1, \dots, \alpha_n\}$ of type variables.

We identify a type scheme $\forall \emptyset. t$ with the type $t$ itself. Furthermore, we consider type schemes up to renaming of the variables they bind, and we disregard useless quantification.

**Definition A.24 (Free variables).** We write $\text{var}(t)$ for the set of type variables occurring in a type $t$; we say they are the free variables of $t$, and we say that $t$ is ground or closed if and only if $\text{var}(t)$ is empty.

We extend the definition to type schemes as $\text{var}(\forall A. t) = \text{var}(t) \setminus A$.

The (coinductive) definition of $\text{var}$ can be found in Castagna et al. (2014, Definition A.2).

**Definition A.25 (Meaningful variables).** We define the set $\text{mvar}(t)$ of meaningful variables of a type $t$ as

$$\text{mvar}(t) = \{ \alpha \in \text{var}(t) \mid t[\emptyset/\alpha] \not\approx t \}.$$

We extend the definition to type schemes as $\text{mvar}(\forall A. t) = \text{mvar}(t) \setminus A$.

**Definition A.26 (Type substitutions).** A type substitution $\theta$ is a finite mapping of type variables to types. We write $[t_i/\alpha_i | i \in I]$ for the type substitution which simultaneously replaces $\alpha_i$ with $t_i$, for each $i \in I$. We write $t\theta$ for the application of the substitution $\theta$ to the type $t$; application is defined coinductively by the following equations.

$$\alpha\theta = \begin{cases} t' & \text{if } t'/\alpha \in \theta \\ \alpha & \text{otherwise} \end{cases}$$

$$b\theta = b$$

$$c\theta = c$$

$$(t_1 \rightarrow t_2)\theta = (t_1\theta) \rightarrow (t_2\theta)$$

$$(t_1 \times t_2)\theta = (t_1\theta) \times (t_2\theta)$$

$$(\text{'tag}(t))\theta = \text{'tag}(t\theta)$$

$$(t_1 \vee t_2)\theta = (t_1\theta) \vee (t_2\theta)$$

$$(\neg t)\theta = \neg(t\theta)$$

$$\emptyset\theta = \emptyset$$

We extend the var operation to substitutions as

$$\text{var}(\theta) = \bigcup_{\alpha \in \text{dom}(\theta)} \text{var}(\alpha\theta).$$

and we extend $\text{mvar}$ likewise.

We extend application of substitutions to type schemes $\forall A. t$: by renaming quantified variables, we assume $A \cap (\text{dom}(\theta) \cup \text{var}(\theta)) = \emptyset$, and we have $(\forall A. t)\theta = \forall A. t\theta$.

We write $\theta_1 \cup \theta_2$ for the union of disjoint substitutions and $\theta_1 \circ \theta_2$ for the composition of substitutions.

**Definition A.27 (Type environments).** A type environment $\Gamma$ is a partial mapping from expression variables to type schemes. We write type environments as $\Gamma = \{x_1: s_1, \dots, x_n: s_n\}$.

We write $\Gamma, \Gamma'$ for the updating of the type environment $\Gamma$ with the new bindings in $\Gamma'$. It is defined as follows.

$$(\Gamma, \Gamma')(x) = \begin{cases} \Gamma'(x) & \text{if } x \in \text{dom}(\Gamma') \\ \Gamma(x) & \text{otherwise} \end{cases}$$

We extend the var operation to type environments as

$$\text{var}(\Gamma) = \bigcup_{s \in \text{range}(\Gamma)} \text{var}(s),$$

and we extend $\text{mvar}$ likewise.
If $e_0$ is a value, on the other hand, the expression may reduce by application of R-Match. Since $\tau_0 \preceq_K \{p_i | i \in I\}$ and $e_0$ is a value of type $\tau_0$ (and therefore satisfies the premises of the definition of exhaustiveness, with $\theta = []$ and $K = K'$), there exists at least an $i \in I$ such that $e_0/p_i = \zeta$ for some substitution $\zeta$. Let $j$ be the least of these $i$ and $\zeta_j$ the corresponding substitution; then match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow e_j \zeta_j$. $\square$

**Theorem A.10 (Subject reduction).** Let $e$ be an expression and $\tau$ a type such that $K; \Gamma \vdash_K e: \tau$. If $e \rightsquigarrow e'$, then $K; \Gamma \vdash_K e': \tau$.

*Proof.* By induction on the derivation of $K; \Gamma \vdash_K e: \tau$. We reason by cases on the last applied rule.

**Cases Tk-Var, Tk-Const, and Tk-Abstr** These cases may not occur: variables, constants, and abstractions never reduce.

**Case Tk-Appl** We have

$$K; \Gamma \vdash_K e_1 e_2: \tau \qquad K; \Gamma \vdash_K e_1: \tau' \to \tau \qquad K; \Gamma \vdash_K e_2: \tau'$$

$e_1 e_2 \rightsquigarrow e'$ occurs in any of three ways: (i) $e_1 \rightsquigarrow e'_1$ and $e' = e'_1 e_2$; (ii) $e_1$ is a value, $e_2 \rightsquigarrow e'_2$ and $e' = e_1 e'_2$; (iii) both $e_1$ and $e_2$ are values, $e_1$ is of the form $\lambda x.e_3$, and $e' = e_3[e^2/x]$.

In the first case, we derive by the induction hypothesis that $K; \Gamma \vdash_K e'_1: \tau' \to \tau$ and conclude by applying *Tk-Appl* again. The second case is analogous.

In the third case, we know by Lemma A.1 that $K; \Gamma, \{x: \tau'\} \vdash_K e_3: \tau$. We also know that $e_2$ is a value such that $K; \Gamma \vdash_K e_2: \tau'$. Then, by Lemma A.8, $K; \Gamma \vdash_K e_3[e^2/x]: \tau$.

**Case Tk-Pair** We have

$$K; \Gamma \vdash_K (e_1, e_2): \tau_1 \times \tau_2 \qquad K; \Gamma \vdash_K e_1: \tau_1 \qquad K; \Gamma \vdash_K e_2: \tau_2$$

$(e_1, e_2) \rightsquigarrow e'$ occurs either because $e_1 \rightsquigarrow e'_1$ and $e' = (e'_1, e_2)$, or because $e_1$ is a value, $e_2 \rightsquigarrow e'_2$, and $e' = (e_1, e'_2)$. In either case, the induction hypothesis allows us to derive that the type of the component that reduces is preserved; therefore, we can apply *Tk-Pair* again to conclude.

**Case Tk-Tag** Analogously to the previous case, a variant expression only reduces if its argument does, so we apply the induction hypothesis and *Tk-Tag* to conclude.

**Case Tk-Match** We have

$$K; \Gamma \vdash_K \text{ match } e_0 \text{ with } (p_i \to e_i)_{i \in I}: \tau \\ K; \Gamma \vdash_K e_0: \tau_0 \quad \forall i \in I. \quad K \vdash p_i: \tau_0 \Rightarrow \Gamma_i \quad K; \Gamma, \text{ gen}_{K;\Gamma}(\Gamma_i) \vdash_K e_i: \tau.$$

match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow e'$ occurs either because $e_0 \rightsquigarrow e'_0$ and $e' = \text{match } e'_0$ with $(p_i \to e_i)_{i \in I}$ or because $e_0$ is a value and $e' = e_j \zeta$, where $e_0/p_j = \zeta$ and, for all $i < j$, $e_0/p_i = \Omega$. In the former case, we apply the induction hypothesis and conclude by *Tk-Match*.

In the latter case, $\zeta$ is a substitution from the capture variables of $p_j$ to values, and we know by Lemma A.2 that, for all $x \in \text{capt}(p_j)$, $K; \Gamma \vdash_K x_\zeta: \Gamma_j(x)$. We show that, additionally, $K; \Gamma \vdash_K x_\zeta: \tau_x$ holds for every $\tau_x \in \text{inst}_K(\text{gen}_{K;\Gamma}(\Gamma_j(x)))$. Every such $\tau_x$ is equal to $\Gamma_j(x)\theta$ for a $\theta$ such that $\text{dom}(\theta) \subseteq \text{var}_K(\Gamma_j(x)) \setminus \text{var}_K(\Gamma)$ and $K \vdash \theta: K$ (the kinding environment captured by generalization is just a subset of $K$). Then, $K; \Gamma \vdash_K x_\zeta: \Gamma_j(x)\theta$ holds by Lemma A.14, since $\Gamma\theta = \Gamma$ (the substitution does not change any free variable of $\Gamma$).

From $K; \Gamma, \text{gen}_{K;\Gamma}(\Gamma_j) \vdash_K e_j: \tau$ and from the fact that we have $K; \Gamma \vdash_K x_\zeta: \tau_x$ for all $x \in \text{dom}(\Gamma_j)$ and all $\tau_x \in \text{inst}_K(\text{gen}_{K;\Gamma}(\Gamma_j(x)))$, we derive $K; \Gamma \vdash_K e_j\zeta: \tau$ by Lemma A.8. $\square$

**Corollary A.11 (Type soundness).** Let $e$ be a well-typed, closed expression, that is, such that $K; \emptyset \vdash_K e: \tau$ holds for some $\tau$. Then, either $e$ diverges or it reduces to a value $v$ such that $K; \emptyset \vdash_K v: \tau$.

*Proof.* Consequence of Theorem A.9 and Theorem A.10. $\square$

## A.3 Typing variants with set-theoretic types

### A.3.1 Definition of the $\mathfrak{S}$ type system

We consider a set $\mathcal{V}$ of type variables (ranged over by $\alpha, \beta, \gamma, \dots$) and the sets $\mathcal{C}, \mathcal{L}$, and $\mathcal{B}$ of language constants, tags, and basic types (ranged over by $c, \text{'tag}$, and $b$ respectively).

**Definition A.22 (Types).** A type $t$ is a term coinductively produced by the following grammar:

$$t ::= \alpha | b | c | t \to t | t \times t | \text{'tag}(t) | t \lor t | \neg t | \emptyset$$

which satisfies two additional constraints:
**Definition A.28 (Generalization).** We define the generalization of a type $t$ with respect to the type environment $\Gamma$ as the type scheme

$$ \text{gen}_{\Gamma}(t) = \forall A. t $$

$$ \text{where } A = \text{var}(t) \setminus \text{mvar}(\Gamma). $$

We extend this definition to type environments which only contain types (i.e., trivial type schemes) as

$$ \text{gen}_{\Gamma}(\{x_i : t_i \mid i \in I\}) = \{x_i : \text{gen}_{\Gamma}(t_i) \mid i \in I\}. $$

**Definition A.29 (Instances of a type scheme).** The set of instances of a type scheme $\forall A. t$ is defined as

$$ \text{inst}(\forall A. t) = \{t \theta \mid \text{dom}(\theta) \subseteq A\}. $$

We say that a type scheme $s_1$ is more general than a type scheme $s_2$, and we write $s_1 \subseteq s_2$, if

$$ \forall t_2 \in \text{inst}(s_2). \exists t_1 \in \text{inst}(s_1). t_1 \le t_2. $$

We extend this notion to type environments as

$$ \Gamma_1 \subseteq \Gamma_2 \iff \text{dom}(\Gamma_1) = \text{dom}(\Gamma_2) \land \forall x \in \text{dom}(\Gamma_1). \Gamma_1(x) \subseteq \Gamma_2(x). $$

**Definition A.30 (Accepted type).** The accepted type $\lceil p \rceil$ of a pattern $p$ is defined inductively as:

$$ \lceil \_ \rceil = \lceil x \rceil = 1 $$

$$ \lceil c \rceil = c $$

$$ \lceil (p_1, p_2) \rceil = \lceil p_1 \rceil \times \lceil p_2 \rceil $$

$$ \lceil \text{'tag}(p) \rceil = \text{'tag}(\lceil p \rceil) $$

$$ \lceil p_1 \& p_2 \rceil = \lceil p_1 \rceil \land \lceil p_2 \rceil $$

$$ \lceil p_1 | p_2 \rceil = \lceil p_1 \rceil \lor \lceil p_2 \rceil. $$

The projection operators $\pi_1$ and $\pi_2$ for product types are defined by Castagna et al. (2014, Appendix C.2.1). We do not repeat the definition, but we state below the properties we need in the proofs. The projection operators for variant types correspond to $\pi_2$ if we encode variant types as pairs; we therefore rephrase the same properties for them.

**Property A.31 (Projections of product types).** There exist two functions $\pi_1$ and $\pi_2$ which, given a type $t \le 1 \times 1$, yield types $\pi_1(t)$ and $\pi_2(t)$ such that:

* $t \le \pi_1(t) \times \pi_2(t)$;

* if $t \le t_1 \times t_2$, then $\pi_1(t) \le t_1$;

* if $t \le t' \le 1 \times 1$, then $\pi_1(t) \le \pi_1(t')$;

* for all type substitutions $\theta$, $\pi_1(t\theta) \le \pi_1(t)\theta$.

**Property A.32 (Projections of variant arguments).** For every tag `tag` there exists a function $\pi_{tag}$ which, given a type $t \le \text{'tag}(1)$, yields a type $\pi_{tag}(t)$ such that:

* $t \le \text{'tag}(\pi_{tag}(t))$;

* if $t \le \text{'tag}(t')$, then $\pi_{tag}(t) \le t'$;

* if $t \le t' \le \text{'tag}(1)$, then $\pi_{tag}(t) \le \pi_{tag}(t')$;

* for all type substitutions $\theta$, $\pi_{tag}(t\theta) \le \pi_{tag}(t)\theta$.

**Definition A.33 (Pattern environment generation).** Given a pattern $p$ and a type $t \le \lceil p \rceil$, the type environment $t//p$ generated by pattern matching is defined inductively as:

$$ t//_{\_} = \emptyset $$

$$ t//x = \{x : t\} $$

$$ t//c = \emptyset $$

$$ t// (p_1, p_2) = \pi_1(t) // p_1 \cup \pi_2(t) // p_2 $$

$$ t//\text{'tag}(p) = \pi_{tag}(t) // p $$

$$ t//p_1 \& p_2 = t//p_1 \cup t//p_2 $$

$$ t//p_1 | p_2 = (t \land \lceil p_1 \rceil) // p_1 \lor (t \setminus \lceil p_1 \rceil) // p_2, $$

$$ \text{where } (\Gamma \lor \Gamma')(x) = \Gamma(x) \lor \Gamma'(x). $$

**Definition A.34 (Typing relation).** The typing relation $\Gamma \vdash_5 e : t$ ($e$ is given type $t$ in the type environment $\Gamma$) is defined by the rules in Figure 10.

### A.3.2 Properties of the $\mathfrak{S}$ type system

**Lemma A.12 (Generation for values).** Let $v$ be a value. Then:

* if $\Gamma \vdash_5 v : c$, then $v = c$;

* if $\Gamma \vdash_5 v : b$, then $v = c$ for some $c$ such that $b_c \le b$;

* if $\Gamma \vdash_5 v : t_1 \to t_2$, then $v$ is of the form $\lambda x. e$ and $\Gamma$, $\{x : t_1\} \vdash_5 e : t_2$;
* (regularity) the term must have a finite number of different sub-terms;

* (contractivity) every infinite branch must contain an infinite number of occurrences of atoms (i.e., a type variable or the immediate application of a type constructor: basic, constant, arrow, product, or variant).

We introduce the following abbreviations:

$$t_1 \wedge t_2 \stackrel{\text{def}}{=} \neg(\neg t_1 \vee \neg t_2) \quad t_1 \setminus t_2 \stackrel{\text{def}}{=} t_1 \wedge (\neg t_2) \quad 1 \stackrel{\text{def}}{=} \neg \emptyset.$$

**Definition A.23 (Type schemes).** A type scheme $s$ is of the form $\forall A. t$, where $A$ is a finite set $\{\alpha_1, \dots, \alpha_n\}$ of type variables.

We identify a type scheme $\forall \emptyset. t$ with the type $t$ itself. Furthermore, we consider type schemes up to renaming of the variables they bind, and we disregard useless quantification.

**Definition A.24 (Free variables).** We write $\text{var}(t)$ for the set of type variables occurring in a type $t$; we say they are the free variables of $t$, and we say that $t$ is ground or closed if and only if $\text{var}(t)$ is empty.

We extend the definition to type schemes as $\text{var}(\forall A. t) = \text{var}(t) \setminus A$.

The (coinductive) definition of $\text{var}$ can be found in Castagna et al. (2014, Definition A.2).

**Definition A.25 (Meaningful variables).** We define the set $\text{mvar}(t)$ of meaningful variables of a type $t$ as

$$\text{mvar}(t) = \{ \alpha \in \text{var}(t) \mid t^{[\emptyset/\alpha]} \not\approx t \}.$$

We extend the definition to type schemes as $\text{mvar}(\forall A. t) = \text{mvar}(t) \setminus A$.

**Definition A.26 (Type substitutions).** A type substitution $\theta$ is a finite mapping of type variables to types. We write $[t_i/\alpha_i | i \in I]$ for the type substitution which simultaneously replaces $\alpha_i$ with $t_i$, for each $i \in I$. We write $t\theta$ for the application of the substitution $\theta$ to the type $t$; application is defined coinductively by the following equations.

$$\alpha\theta = \begin{cases} t' & \text{if } t'/\alpha \in \theta \\ \alpha & \text{otherwise} \end{cases}$$

$$b\theta = b$$

$$c\theta = c$$

$$(t_1 \rightarrow t_2)\theta = (t_1\theta) \rightarrow (t_2\theta)$$

$$(t_1 \times t_2)\theta = (t_1\theta) \times (t_2\theta)$$

$$(\text{\textit{tag}}(t))\theta = \text{\textit{tag}}(t\theta)$$

$$(t_1 \vee t_2)\theta = (t_1\theta) \vee (t_2\theta)$$

$$(\neg t)\theta = \neg(t\theta)$$

$$\emptyset\theta = \emptyset$$

We extend the var operation to substitutions as

$$\text{var}(\theta) = \bigcup_{\alpha \in \text{dom}(\theta)} \text{var}(\alpha\theta).$$

and we extend mvar likewise.

We extend application of substitutions to type schemes $\forall A. t$: by renaming quantified variables, we assume $A \cap (\text{dom}(\theta) \cup \text{var}(\theta)) = \emptyset$, and we have $(\forall A. t)\theta = \forall A. t\theta$.

We write $\theta_1 \cup \theta_2$ for the union of disjoint substitutions and $\theta_1 \circ \theta_2$ for the composition of substitutions.

**Definition A.27 (Type environments).** A type environment $\Gamma$ is a partial mapping from expression variables to type schemes. We write type environments as $\Gamma = \{x_1: s_1, \dots, x_n: s_n\}$.

We write $\Gamma, \Gamma'$ for the updating of the type environment $\Gamma$ with the new bindings in $\Gamma'$. It is defined as follows.

$$(\Gamma, \Gamma')(x) = \begin{cases} \Gamma'(x) & \text{if } x \in \text{dom}(\Gamma') \\ \Gamma(x) & \text{otherwise} \end{cases}$$

We extend the var operation to type environments as

$$\text{var}(\Gamma) = \bigcup_{s \in \text{range}(\Gamma)} \text{var}(s),$$

and we extend mvar likewise.
$$ Ts-Var \quad \frac{t \in \text{inst}(\Gamma(x))}{\Gamma \vdash_{\mathfrak{s}} x : t} \qquad Ts-Const \quad \overline{\Gamma \vdash_{\mathfrak{s}} c : c} \qquad Ts-Abstr \quad \frac{\Gamma, \{x: t_1\} \vdash_{\mathfrak{s}} e : t_2}{\Gamma \vdash_{\mathfrak{s}} \lambda x. e : t_1 \to t_2} $$

$$ Ts-Appl \quad \frac{\Gamma \vdash_{\mathfrak{s}} e_1: t' \to t \qquad \Gamma \vdash_{\mathfrak{s}} e_2: t'}{\Gamma \vdash_{\mathfrak{s}} e_1 e_2: t} \qquad Ts-Pair \quad \frac{\Gamma \vdash_{\mathfrak{s}} e_1: t_1 \qquad \Gamma \vdash_{\mathfrak{s}} e_2: t_2}{\Gamma \vdash_{\mathfrak{s}} (e_1, e_2): t_1 \times t_2} $$

$$ Ts-Tag \quad \frac{\Gamma \vdash_{\mathfrak{s}} e : t}{\Gamma \vdash_{\mathfrak{s}} \text{tag}(e) : \text{tag}(t)} $$

$$ Ts-Match \quad \frac{\Gamma \vdash_{\mathfrak{s}} e_0: t_0 \qquad t_0 \le \bigvee_{i \in I} \{p_i\} \qquad t_i = (t_0 \setminus \bigvee_{j<i} \{p_j\}) \wedge \{p_i\} \quad \forall i \in I \quad \Gamma, \text{gen}_{\Gamma}(t_i // p_i) \vdash_{\mathfrak{s}} e_i : t_i' \quad \Gamma \vdash_{\mathfrak{s}} \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I}: \bigvee_{i \in I} t_i'}{\Gamma \vdash_{\mathfrak{s}} \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I}: \bigvee_{i \in I} t_i'} $$

$$ Ts-Subsum \quad \frac{\Gamma \vdash_{\mathfrak{s}} e : t' \qquad t' \le t}{\Gamma \vdash_{\mathfrak{s}} e : t} $$

<caption>**Figure 10.** Typing relation of the $\mathfrak{S}$ type system.</caption>

* if $\Gamma \vdash_{\mathfrak{s}} v: t_1 \times t_2$, then $v$ is of the form $(v_1, v_2)$, $\Gamma \vdash_{\mathfrak{s}} v_1: t_1$, and $\Gamma \vdash_{\mathfrak{s}} v_2: t_2$;

* if $\Gamma \vdash_{\mathfrak{s}} v: \text{tag}(t_1)$, then $v$ is of the form $\text{tag}(v_1)$ and $\Gamma \vdash_{\mathfrak{s}} v_1: t_1$.

*Proof.* By induction on the typing derivation: values must be typed by an application of the rule corresponding to their form to appropriate premises, possibly followed by applications of *Ts-Subsum*.

The base cases are straightforward. In the inductive step, we just apply the induction hypothesis; for abstractions, the result follows from the behaviour of subtyping on arrow types. □

We state the next three lemmas without proof, as they rely on the model of types which we have not discussed. Details can be found in Frisch et al. (2008) and Castagna and Xu (2011), as well as in Alain Frisch's PhD thesis.<fnref n="9" />

**Lemma A.13.** For each $i \in I$, let $p_i$ be a pattern. If $\Gamma \vdash_{\mathfrak{s}} v: \bigvee_{i \in I} \{p_i\}$, then there exists an $i \in I$ such that $\Gamma \vdash_{\mathfrak{s}} v: \{p_i\}$.

**Lemma A.14.** Let $t$ be a type. Let $t'$ be a type such that either $t' = \{p\}$ or $t' = \neg\{p\}$, for some pattern $p$. If $\Gamma \vdash_{\mathfrak{s}} v: t$ and $\Gamma \vdash_{\mathfrak{s}} v: t'$, then $\Gamma \vdash_{\mathfrak{s}} v: t \wedge t'$.

**Lemma A.15.** Let $v$ be a well-typed value (i.e., $\emptyset \vdash_{\mathfrak{s}} v: t$ holds for some $t$) and $p$ a pattern. Then:

* $\emptyset \vdash_{\mathfrak{s}} v: \{p\}$ holds if and only if $v/p = \zeta$ for some substitution $\zeta$;

* $\emptyset \vdash_{\mathfrak{s}} v: \neg\{p\}$ holds if and only if $v/p = \Omega$.

**Lemma A.16.** Let $p$ be a pattern and $t, t'$ two types. If $t \le t' \le \{p\}$, then, for all $x \in \text{capt}(p)$, $(t//p)(x) \le (t'//p)(x)$.

*Proof.* By structural induction on $p$.

Cases $p = \_\_\_$ and $p = c$ There is nothing to prove since $\text{capt}(p) = \emptyset$.

Case $p = x$ We must prove $(t//x)(x) \le (t'//x)(x)$, that is, $t \le t'$, which we know by hypothesis.

Case $p = (p_1, p_2)$ Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t//p)(x) = (\pi_i(t)//p_i)(x)$ and $(t'//p)(x) = (\pi_i(t')//p_i)(x)$. Since $t \le t'$ implies $\pi_i(t) \le \pi_i(t')$ by Property A.31, we can apply the induction hypothesis to conclude.

Case $p = \text{tag}(p)$ Analogous to the previous case, because $t \le t'$ implies $\pi_{\text{tag}}(t) \le \pi_{\text{tag}}(t')$ by Property A.32.

Case $p = p_1 \& p_2$ Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t//p)(x) = (t//p_i)(x)$ and $(t'//p)(x) = (t'//p_i)(x)$. We apply the induction hypothesis to conclude.

<footnote n="9">⁹ A. Frisch. *Théorie, conception et réalisation d'un langage de programmation adapté à XML*. PhD thesis, Université Paris 7 – Denis Diderot, 2004.</footnote>
**Definition A.28 (Generalization).** We define the generalization of a type *t* with respect to the type environment Γ as the type scheme

$$ \text{gen}_{\Gamma}(t) = \forall A. t $$

$$ \text{where } A = \text{var}(t) \setminus \text{mvar}(\Gamma). $$

We extend this definition to type environments which only contain types (i.e., trivial type schemes) as

$$ \text{gen}_{\Gamma}(\{x_i : t_i \mid i \in I\}) = \{x_i : \text{gen}_{\Gamma}(t_i) \mid i \in I\}. $$

**Definition A.29 (Instances of a type scheme).** The set of instances of a type scheme $\forall A. t$ is defined as

$$ \text{inst}(\forall A. t) = \{t \theta \mid \text{dom}(\theta) \subseteq A\}. $$

We say that a type scheme $s_1$ is more general than a type scheme $s_2$, and we write $s_1 \subseteq s_2$, if

$$ \forall t_2 \in \text{inst}(s_2). \exists t_1 \in \text{inst}(s_1). t_1 \le t_2. $$

We extend this notion to type environments as

$$ \Gamma_1 \subseteq \Gamma_2 \iff \text{dom}(\Gamma_1) = \text{dom}(\Gamma_2) \land \forall x \in \text{dom}(\Gamma_1). \Gamma_1(x) \subseteq \Gamma_2(x). $$

**Definition A.30 (Accepted type).** The accepted type $\lceil p \rceil$ of a pattern *p* is defined inductively as:

$$ \lceil_\_ \rceil = \lceil x \rceil = 1 $$

$$ \lceil c \rceil = c $$

$$ \lceil(p_1, p_2)\rceil = \lceil p_1 \rceil \times \lceil p_2 \rceil $$

$$ \lceil \text{'tag}(p) \rceil = \text{'tag}(\lceil p \rceil) $$

$$ \lceil p_1 \& p_2 \rceil = \lceil p_1 \rceil \land \lceil p_2 \rceil $$

$$ \lceil p_1 | p_2 \rceil = \lceil p_1 \rceil \lor \lceil p_2 \rceil. $$

The projection operators $\pi_1$ and $\pi_2$ for product types are defined by Castagna et al. (2014, Appendix C.2.1). We do not repeat the definition, but we state below the properties we need in the proofs. The projection operators for variant types correspond to $\pi_2$ if we encode variant types as pairs; we therefore rephrase the same properties for them.

**Property A.31 (Projections of product types).** There exist two functions $\pi_1$ and $\pi_2$ which, given a type $t \le 1 \times 1$, yield types $\pi_1(t)$ and $\pi_2(t)$ such that:

* $t \le \pi_1(t) \times \pi_2(t)$;

* if $t \le t_1 \times t_2$, then $\pi_1(t) \le t_1$;

* if $t \le t' \le 1 \times 1$, then $\pi_1(t) \le \pi_1(t')$;

* for all type substitutions $\theta$, $\pi_1(t\theta) \le \pi_1(t)\theta$.

**Property A.32 (Projections of variant arguments).** For every tag `tag` there exists a function $\pi_{tag}$ which, given a type $t \le \text{'tag}(1)$, yields a type $\pi_{tag}(t)$ such that:

* $t \le \text{'tag}(\pi_{tag}(t))$;

* if $t \le \text{'tag}(t')$, then $\pi_{tag}(t) \le t'$;

* if $t \le t' \le \text{'tag}(1)$, then $\pi_{tag}(t) \le \pi_{tag}(t')$;

* for all type substitutions $\theta$, $\pi_{tag}(t\theta) \le \pi_{tag}(t)\theta$.

**Definition A.33 (Pattern environment generation).** Given a pattern *p* and a type $t \le \lceil p \rceil$, the type environment $t//p$ generated by pattern matching is defined inductively as:

$$ t//_{\_} = \emptyset $$

$$ t//x = \{x : t\} $$

$$ t//c = \emptyset $$

$$ t//\lceil p_1, p_2 \rceil = \pi_1(t) // \lceil p_1 \rceil \cup \pi_2(t) // \lceil p_2 \rceil $$

$$ t//\text{'tag}(p) = \pi_{tag}(t) // p $$

$$ t//p_1 \& p_2 = t//p_1 \cup t//p_2 $$

$$ t//p_1 | p_2 = (t \land \lceil p_1 \rceil) // p_1 \lor (t \land \lceil p_2 \rceil) // p_2, $$

$$ \text{where } (\Gamma \lor \Gamma')(x) = \Gamma(x) \lor \Gamma'(x). $$

**Definition A.34 (Typing relation).** The typing relation $\Gamma \vdash_5 e : t$ ($e$ is given type $t$ in the type environment $\Gamma$) is defined by the rules in Figure 10.

### A.3.2 Properties of the $\mathfrak{S}$ type system

**Lemma A.12 (Generation for values).** Let $v$ be a value. Then:

* if $\Gamma \vdash_5 v : c$, then $v = c$;

* if $\Gamma \vdash_5 v : b$, then $v = c$ for some $c$ such that $b_c \le b$;

* if $\Gamma \vdash_5 v : t_1 \rightarrow t_2$, then $v$ is of the form $\lambda x. e$ and $\Gamma$, $\{x : t_1\} \vdash_5 e : t_2$;
Case $p = p_1|p_2$. Every $x \in \text{capt}(p)$ is both in $\text{capt}(p_1)$ and in $\text{capt}(p_2)$. We have that $(t//p)(x) = (t\wedge[p_1]//p_1)(x) \vee (t\wedge[p_1]//p_2)(x)$ and likewise for $t'$. Since $t\wedge[p_1] \le t'\wedge[p_1]$ and $t\wedge[p_1] \le t'\wedge[p_1]$, we can apply the induction hypothesis to both sub-patterns to derive $(t\wedge[p_1]//p_1)(x) \le (t'\wedge[p_1]//p_1)(x)$ and $(t\wedge[p_1]//p_2)(x) \le (t'\wedge[p_1]//p_2)(x)$. Then we have $(t\wedge[p_1]//p_1)(x) \vee (t\wedge[p_1]//p_2)(x) \le (t'\wedge[p_1]//p_1)(x) \vee (t'\wedge[p_1]//p_2)(x). \quad \square$

**Lemma A.17** (Correctness of environment generation). Let $p$ be a pattern and $v$ a value such that $\Gamma \vdash_{\emptyset} v: t$ for some $t \le [p]$. Then, for all $x \in \text{capt}(p)$, $\Gamma \vdash_{\emptyset} x(v/p): (t//p)(x)$.

*Proof.* By structural induction on $p$.

Cases $p = \_\_\_$ and $p = c$. There is nothing to prove since $\text{capt}(p) = \emptyset$.

Case $p = x$. We must prove $\Gamma \vdash_{\emptyset} x[v/x]: (t//x)(x)$, which is the hypothesis $\Gamma \vdash_{\emptyset} v: t$.

Case $p = (p_1, p_2)$. We have $t \le 1 \times 1$, hence $t \le \pi_1(t) \times \pi_2(t)$; then, since $\Gamma \vdash_{\emptyset} v: \pi_1(t) \times \pi_2(t)$ by subsumption, we have by Lemma A.12 that $v = (v_1, v_2)$ and that $\Gamma \vdash_{\emptyset} v_i: \pi_1(t)$ for both $i$. Moreover, $t \le [p_1, p_2] = [p_1] \times [p_2]$. Hence, by Property A.31, $\pi_i(t) \le [p_i]$ for both $i$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, we can directly apply the induction hypothesis since $t \le [p_1 \& p_2]$ implies $t \le [p_1]$ and $t \le [p_2]$.

Case $p = \text{'tag}(p)$. Analogous to the previous case.

Case $p = p_1 \& p_2$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, we can directly apply the induction hypothesis since $t \le [p_1 \& p_2]$ implies $t \le [p_1]$ and $t \le [p_2]$.

Case $p = p_1|p_2$. Either $v/p = v/p_1$ or $v/p = v/p_2$ (in which case $v/p_1 = \Omega$).

Case $v/p = v/p_1$. By Lemma A.15 we have $\Gamma \vdash_{\emptyset} v: [p_1]$; by Lemma A.14 we have $\Gamma \vdash_{\emptyset} v: t \wedge [p_1]$. Since $t \wedge [p_1] \le [p_1]$, by the induction hypothesis we have, for all $x \in \text{capt}(p_1) = \text{capt}(p)$, $\Gamma \vdash_{\emptyset} x(v/p): (t \wedge [p_1]//p_1)(x)$ and, by subsumption, $\Gamma \vdash_{\emptyset} x(v/p): (t \wedge [p_1]//p_1)(x) \vee (t \wedge [p_1]//p_2)(x)$.

Case $v/p = v/p_2$. By Lemma A.15 and Lemma A.14, we have $\Gamma \vdash_{\emptyset} v: t \wedge [p_1]$. Additionally, $t \wedge [p_1] \le [p_2]$ holds because it is equivalent to $t \le [p_1] \vee [p_2]$. Therefore by the induction hypothesis we have, for all $x \in \text{capt}(p_1) = \text{capt}(p)$, $\Gamma \vdash_{\emptyset} x(v/p): (t \wedge [p_1]//p_2)(x)$ and, by subsumption, $\Gamma \vdash_{\emptyset} x(v/p): (t \wedge [p_1]//p_1)(x) \vee (t \wedge [p_1]//p_2)(x)$. $\quad \square$

**Lemma A.18.** Let $p$ be a pattern, $t$ a type such that $t \le [p]$, and $\theta$ a type substitution. Then, for all $x \in \text{capt}(p)$, $(t\theta//p)(x) \le ((t//p)(x))\theta$.

*Proof.* By structural induction on $p$.

Cases $p = \_\_\_$ and $p = c$. There is nothing to prove since $\text{capt}(p) = \emptyset$.

Case $p = x$. We must prove $(t\theta//x)(x) \le (t//x)(x)\theta$, which is $t\theta \le t\theta$.

Case $p = (p_1, p_2)$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t\theta//p)(x) = (\pi_i(t\theta)//p_i)(x)$ and $(t//p)(x)\theta = (\pi_i(t)//p_i)(x)\theta$. Since $\pi_i(t\theta) \le \pi_i(t)\theta$, by Lemma A.16 we have $(\pi_i(t\theta)//p_i)(x) \le (\pi_i(t)\theta//p_i)(x)$. By the induction hypothesis we have $(\pi_i(t)\theta//p_i)(x) \le (\pi_i(t)//p_i)(x)\theta$.

Case $p = \text{'tag}(p)$. Analogous to the previous case, since $\pi_{\text{'tag}}(t\theta) \le \pi_{\text{'tag}}(t)\theta$.

Case $p = p_1 \& p_2$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t\theta//p)(x) = (t\theta//p_i)(x)$ and $(t//p)(x)\theta = (t//p_i)(x)\theta$. We conclude by the induction hypothesis.

Case $p = p_1|p_2$. Every $x \in \text{capt}(p)$ is both in $\text{capt}(p_1)$ and in $\text{capt}(p_2)$. We have $(t\theta//p)(x) = ((t \wedge [p_1])\theta//p_1)(x) \vee ((t \wedge [p_1])\theta//p_2)(x)$—pattern types are closed, so we can apply $\theta$ to them too—and $(t//p)(x)\theta = (t \wedge [p_1]//p_1)(x)\theta \vee (t \wedge [p_1]//p_2)(x)\theta$. We conclude by applying the induction hypothesis to both members of the union. $\quad \square$

**Lemma A.19.** Let $t_1$ and $t_2$ be equivalent types ($t_1 \simeq t_2$). Then, $\text{mvar}(t_1) = \text{mvar}(t_2)$.

*Proof.* Since subtyping is preserved by type substitutions, for every $\alpha$ we have $t_1[\alpha] \simeq t_2[\alpha]$. If $\alpha \in \text{mvar}(t_1)$, we have $t_1[\alpha] \not\simeq t_1$ by the definition of mvar. This necessarily implies $t_2[\alpha] \not\simeq t_2$, otherwise we would have $t_1[\alpha] \simeq t_1$ by transitivity. $\quad \square$
$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\text{Ts-Var} & \frac{t \in \text{inst}(\Gamma(x))}{\Gamma \vdash_{\mathfrak{s}} x : t} & \text{Ts-Const} & \overline{\Gamma \vdash_{\mathfrak{s}} c : c} \\
\text{Ts-Appl} & \frac{\Gamma \vdash_{\mathfrak{s}} e_1 : t' \to t}{\Gamma \vdash_{\mathfrak{s}} e_1 : e_2 : t} & \text{Ts-Pair} & \frac{\Gamma \vdash_{\mathfrak{s}} e_1 : t_1}{\Gamma \vdash_{\mathfrak{s}} (e_1, e_2) : t_1 \times t_2}
\end{array}
$$

$$
\text{Ts-Tag} \quad \frac{\Gamma \vdash_{\mathfrak{s}} e : t}{\Gamma \vdash_{\mathfrak{s}} \text{tag}(e) : \text{tag}(t)}
$$

$$
\text{Ts-Match} \quad \frac{\Gamma \vdash_{\mathfrak{s}} e_0 : t_0 \quad t_0 \le \bigvee_{i \in I} \mathcal{L}(p_i) \quad t_i = (t_0 \setminus \bigvee_{j<i} \mathcal{L}(p_j)) \land \mathcal{L}(p_i) \quad \forall i \in I \quad \Gamma, \operatorname{gen}_{\Gamma}(t_i // p_i) \vdash_{\mathfrak{s}} e_i : t_i' \quad \Gamma \vdash_{\mathfrak{s}} \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : \bigvee_{i \in I} t_i'}{\Gamma \vdash_{\mathfrak{s}} \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : \bigvee_{i \in I} t_i'}
$$

$$
\text{Ts-Subsum} \quad \frac{\Gamma \vdash_{\mathfrak{s}} e : t' \quad t' \le t}{\Gamma \vdash_{\mathfrak{s}} e : t}
$$

<caption>Figure 10. Typing relation of the S type system.</caption>

• if $\Gamma \vdash_{\mathfrak{s}} v : t_1 \times t_2$, then $v$ is of the form $(v_1, v_2)$, $\Gamma \vdash_{\mathfrak{s}} v_1 : t_1$, and $\Gamma \vdash_{\mathfrak{s}} v_2 : t_2$;

• if $\Gamma \vdash_{\mathfrak{s}} v : \mathtt{tag}(t_1)$, then $v$ is of the form $\mathtt{tag}(v_1)$ and $\Gamma \vdash_{\mathfrak{s}} v_1 : t_1$.

*Proof.* By induction on the typing derivation: values must be typed by an application of the rule corresponding to their form to appropriate premises, possibly followed by applications of *Ts-Subsum*.

The base cases are straightforward. In the inductive step, we just apply the induction hypothesis;
for abstractions, the result follows from the behaviour of subtyping on arrow types. □

We state the next three lemmas without proof, as they rely on the model of types which we have
not discussed. Details can be found in Frisch et al. (2008) and Castagna and Xu (2011), as well as
in Alain Frisch's PhD thesis.<fnref n="9" />

**Lemma A.13.** For each $i \in I$, let $p_i$ be a pattern. If $\Gamma \vdash_{\mathfrak{s}} v : \bigvee_{i \in I} \mathcal{L}(p_i)$, then there exists an $i \in I$ such that $\Gamma \vdash_{\mathfrak{s}} v : \mathcal{L}(p_i)$.

**Lemma A.14.** Let $t$ be a type. Let $t'$ be a type such that either $t' = \mathcal{L}(p) \text{ or } t' = \neg\mathcal{L}(p)$, for some pattern $p$. If $\Gamma \vdash_{\mathfrak{s}} v : t$ and $\Gamma \vdash_{\mathfrak{s}} v : t'$, then $\Gamma \vdash_{\mathfrak{s}} v : t \land t'$.

**Lemma A.15.** Let $v$ be a well-typed value (i.e., $\emptyset \vdash_{\mathfrak{s}} v : t$ holds for some $t$) and $p$ a pattern. Then:

• $\emptyset \vdash_{\mathfrak{s}} v : \mathcal{L}(p)$ holds if and only if $v/p = \zeta$ for some substitution $\zeta$;

• $\emptyset \vdash_{\mathfrak{s}} v : \neg\mathcal{L}(p)$ holds if and only if $v/p = \Omega$.

**Lemma A.16.** Let $p$ be a pattern and $t, t'$ two types. If $t \le t' \le \mathcal{L}(p)$, then, for all $x \in \text{capt}(p)$, $(t//p)(x) \le (t'//p)(x)$.

*Proof.* By structural induction on $p$.

Cases $p = -$ and $p = c$ There is nothing to prove since capt($p$) = $\emptyset$.

Case $p = x$ We must prove $(t//x)(x) \le (t'//x)(x)$, that is, $t \le t'$, which we know by hypothesis.

Case $p = (p_1, p_2)$ Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t//p)(x) = (\pi_i(t)//p_i)(x)$ and $(t'//p)(x) = (\pi_i(t')//p_i)(x)$. Since $t \le t'$ implies $\pi_i(t) \le \pi_i(t')$ by Property A.31, we can apply the induction hypothesis to conclude.

Case $p = \mathtt{tag}(p)$ Analogous to the previous case, because $t \le t'$ implies $\pi_{\mathtt{tag}}(t) \le \pi_{\mathtt{tag}}(t')$ by Property A.32.

Case $p = p_1 \& p_2$ Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t//p)(x) = (t//p_i)(x)$ and $(t'//p)(x) = (t'//p_i)(x)$. We apply the induction hypothesis to conclude.

<footnote n="9">⁹ A. Frisch. Théorie, conception et réalisation d'un langage de programmation adapté à XML. PhD thesis,
Université Paris 7 – Denis Diderot, 2004.</footnote>
**Lemma A.20.** Let $t$ be a type and $\theta$ a type substitution such that $\text{dom}(\theta) \cap \text{mvar}(t) = \emptyset$. Then $t\theta \simeq t$.

*Proof.* Let $t' = t[0/\alpha_1, \dots, 0/\alpha_n]$ where $\{\alpha_1, \dots, \alpha_n\} = \text{var}(t) \setminus \text{mvar}(t)$. We have $t \simeq t'$ and $\text{var}(t') = \text{mvar}(t)$. Since substitutions preserve subtyping (and hence equivalence), we have also $t\theta \simeq t'\theta$. But $t'\theta = t' \simeq t$; hence, we reach the conclusion by the transitivity of equivalence. $\square$

**Lemma A.21.** Let $\Gamma_1, \Gamma_2$ be two type environments such that $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$ and $t_1, t_2$ two types such that $t_1 \le t_2$. Then, $\text{gen}_{\Gamma_1}(t_1) \subseteq \text{gen}_{\Gamma_2}(t_2)$.

*Proof.* An instance of $\text{gen}_{\Gamma_2}(t_2)$ is a type $t_2\theta_2$ such that $\text{dom}(\theta_2) \subseteq \text{var}(t_2) \setminus \text{mvar}(\Gamma_2)$. Let $\theta_1$ be the restriction of $\theta_2$ to the variables in $\text{var}(t_1) \setminus \text{mvar}(\Gamma_1)$. Then, $t_1\theta_1$ is an instance of $\text{gen}_{\Gamma_1}(t_1)$. We have $t_1\theta_1 = t_1\theta_2$ because the two substitutions differ only on variables in $\text{var}(t_2) \setminus \text{var}(t_1)$ (which do not appear in $t_1$ at all) or in $\text{mvar}(\Gamma_1) \setminus \text{mvar}(\Gamma_2)$ (which is empty). Finally, we have $t_1\theta_2 \le t_2\theta_2$ because subtyping is preserved by substitutions. $\square$

**Lemma A.22 (Weakening).** Let $\Gamma_1, \Gamma_2$ be two type environments such that $\Gamma_1 \subseteq \Gamma_2$ and $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$. If $\Gamma_2 \vdash_5 e: t$, then $\Gamma_1 \vdash_5 e: t$.

*Proof.* By induction on the derivation of $\Gamma_2 \vdash_5 e: t$. We reason by cases on the last applied rule.

**Case Ts-Var** We have

$$ \Gamma_2 \vdash_5 x: t \quad t \in \text{inst}(\Gamma_2(x)) $$

and hence, since $\Gamma_1 \subseteq \Gamma_2$, there exists a $t' \in \text{inst}(\Gamma_1(x))$ such that $t' \le t$. We apply Ts-Var to derive $\Gamma_1 \vdash_5 x: t'$ and Ts-Subsum to conclude.

**Case Ts-Const** Straightforward.

**Case Ts-Abstr** We have

$$ \Gamma_2 \vdash_5 \lambda x. e_1: t_1 \to t_2 \quad \Gamma_2, \{x: t_1\} \vdash_5 e_1: t_2. $$

Since $\Gamma_1 \subseteq \Gamma_2$, we have $\Gamma_1, \{x: t_1\} \subseteq \Gamma_2, \{x: t_1\}$; since $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$, we have $\text{mvar}(\Gamma_1, \{x: t_1\}) \subseteq \text{mvar}(\Gamma_2, \{x: t_1\})$. We derive $\Gamma_1, \{x: t_1\} \vdash_5 e_1: t_2$ by the induction hypothesis and apply Ts-Abstr to conclude.

**Cases Ts-Appl, Ts-Pair, Ts-Tag, and Ts-Subsum** Straightforward application of the induction hypothesis.

**Case Tk-Match** We have

$$ \Gamma_2 \vdash_5 \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I}: t \\ \Gamma_2 \vdash_5 e_0: t_0 \quad t_0 \le \bigvee_{i \in I} \{p_i\} \quad t_i = (t_0 \setminus \bigvee_{j<i} \{p_j\}) \wedge \{p_i\} \\ \forall i \in I. \quad \Gamma_2, \text{gen}_{\Gamma_2}(t_i//p_i) \vdash_5 e_i: t'_i \quad t = \bigvee_{i \in I} t'_i. $$

By the induction hypothesis, we derive $\Gamma_1 \vdash_5 e_0: t_0$.

For any branch, note that $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$ implies $\text{gen}_{\Gamma_1}(t) \subseteq \text{gen}_{\Gamma_2}(t)$ for any $t$ by Lemma A.21. Hence, we have $\Gamma_1, \text{gen}_{\Gamma_1}(t_i//p_i) \subseteq \Gamma_2, \text{gen}_{\Gamma_2}(t_i//p_i)$. Additionally, since $\text{mvar}(\text{gen}_{\Gamma_1}(t_i//p_i)) \subseteq \text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$, we have $\text{mvar}(\Gamma_1, \text{gen}_{\Gamma_1}(t_i//p_i)) \subseteq \text{mvar}(\Gamma_2, \text{gen}_{\Gamma_2}(t_i//p_i))$.

Hence we may apply the induction hypothesis for all $i$ to derive $\Gamma_1, \text{gen}_{\Gamma_1}(t_i//p_i) \vdash_5 e_i: t'_i$ and then apply Ts-Match to conclude. $\square$

**Lemma A.23 (Stability of typing under type substitutions).** Let $\theta$ be a type substitution. If $\Gamma \vdash_5 e: t$, then $\Gamma\theta \vdash_5 e: t\theta$.

*Proof.* By induction on the derivation of $\Gamma \vdash_5 e: t$. We reason by cases on the last applied rule.

**Case Ts-Var** We have

$$ \Gamma \vdash_5 x: t \quad t \in \text{inst}(\Gamma(x)) \quad \Gamma(x) = \forall A. t_x \quad t = t_x \theta_x \quad \text{dom}(\theta_x) \subseteq A $$

and must show $\Gamma\theta \vdash_5 x: t\theta$.

By $\alpha$-renaming we assume $A \cap (\text{dom}(\theta) \cup \text{var}(\theta)) = \emptyset$. Under this assumption, $(\Gamma\theta)(x) = \forall A. t_x\theta$. We must show that $t\theta = t_x\theta'_{x'}$ for a substitution $\theta'_{x'}$ such that $\text{dom}(\theta'_{x'}) \subseteq A$.

Let $\theta'_{x'} = [\alpha_{\theta'_{x'}}\theta/\alpha | \alpha \in A]$. We show that $t\theta'_{x'} = t_x\theta_x\theta = t\theta$, by showing that, for every $\alpha, \alpha\theta'_{x'} = \alpha\theta_x\theta$. If $\alpha \in A$, then $\alpha\theta'_{x'} = \alpha\theta_x' = \alpha\theta_x\theta$ ($\theta$ is not defined on the variables in A). If $\alpha \notin A$, then $\alpha\theta'_{x'} = \alpha\theta$ ($\theta$ never produces any variable in A) and $\alpha\theta_x\theta = \alpha\theta$ as $\alpha \notin \text{dom}(\theta_x)$.
Case $p = p_1|p_2$. Every $x \in \text{capt}(p)$ is both in $\text{capt}(p_1)$ and in $\text{capt}(p_2)$. We have that $(t//p)(x) = (t\wedge[p_1]//p_1)(x) \vee (t\setminus[p_1]//p_2)(x)$ and likewise for $t'$. Since $t\wedge[p_1] \le t'\wedge[p_1]$ and $t\setminus[p_1] \le t'\setminus[p_1]$, we can apply the induction hypothesis to both sub-patterns to derive $(t\wedge[p_1]//p_1)(x) \le (t'\wedge[p_1]//p_1)(x)$ and $(t\setminus[p_1]//p_2)(x) \le (t'\setminus[p_1]//p_2)(x)$. Then we have $(t\wedge[p_1]//p_1)(x) \vee (t\setminus[p_1]//p_2)(x) \le (t'\wedge[p_1]//p_1)(x) \vee (t'\setminus[p_1]//p_2)(x)$. $\square$

**Lemma A.17 (Correctness of environment generation).** Let $p$ be a pattern and $v$ a value such that $\Gamma \vdash_S v: t$ for some $t \le [p]$. Then, for all $x \in \text{capt}(p)$, $\Gamma \vdash_S x(v/p): (t//p)(x)$.

*Proof.* By structural induction on $p$.

Cases $p = -$ and $p = c$. There is nothing to prove since $\text{capt}(p) = \emptyset$.

Case $p = x$. We must prove $\Gamma \vdash_S x[v/x]: (t//x)(x)$, which is the hypothesis $\Gamma \vdash_S v: t$.

Case $p = (p_1, p_2)$. We have $t \le 1 \times 1$, hence $t \le \pi_1(t) \times \pi_2(t)$; then, since $\Gamma \vdash_S v: \pi_1(t) \times \pi_2(t)$ by subsumption, we have by Lemma A.12 that $v = (v_1, v_2)$ and that $\Gamma \vdash_S v_i: \pi_1(t)$ for both $i$. Moreover, $t \le [p_1, p_2] = [p_1] \times [p_2]$. Hence, by Property A.31, $\pi_i(t) \le [p_i]$ for both $i$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $x(v/p) = x(v_i/p_i)$ and $(t//p)(x) = (\pi_i(t)//p_i)(x)$. We apply the induction hypothesis to conclude.

Case $p = \text{'tag}(p)$. Analogous to the previous case.

Case $p = p_1 \& p_2$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, we can directly apply the induction hypothesis since $t \le [p_1 \& p_2]$ implies $t \le [p_1]$ and $t \le [p_2]$.

Case $p = p_1|p_2$. Either $v/p = v/p_1$ or $v/p = v/p_2$ (in which case $v/p_1 = \Omega$).

Case $v/p = v/p_1$. By Lemma A.15 we have $\Gamma \vdash_S v: [p_1]$; by Lemma A.14 we have $\Gamma \vdash_S v: t \wedge [p_1]$. Since $t \wedge [p_1] \le [p_1]$, by the induction hypothesis we have, for all $x \in \text{capt}(p_1) = \text{capt}(p)$, $\Gamma \vdash_S x(v/p): (t \wedge [p_1]//p_1)(x)$ and, by subsumption, $\Gamma \vdash_S x(v/p): (t \wedge [p_1]//p_1)(x) \vee (t \wedge [p_1]//p_2)(x)$.

Case $v/p = v/p_2$. By Lemma A.15 and Lemma A.14, we have $\Gamma \vdash_S v: t \setminus [p_1]$. Additionally, $t \setminus [p_1] \le [p_2]$ holds because it is equivalent to $t \le [p_1] \vee [p_2]$. Therefore by the induction hypothesis we have, for all $x \in \text{capt}(p_1) = \text{capt}(p)$, $\Gamma \vdash_S x(v/p): (t \setminus [p_1]//p_2)(x)$ and, by subsumption, $\Gamma \vdash_S x(v/p): (t \wedge [p_1]//p_1)(x) \vee (t \wedge [p_1]//p_2)(x)$. $\square$

**Lemma A.18.** Let $p$ be a pattern, $t$ a type such that $t \le [p]$, and $\theta$ a type substitution. Then, for all $x \in \text{capt}(p)$, $(t\theta//p)(x) \le ((t//p)(x))\theta$.

*Proof.* By structural induction on $p$.

Cases $p = -$ and $p = c$. There is nothing to prove since $\text{capt}(p) = \emptyset$.

Case $p = x$. We must prove $(t\theta//x)(x) \le (t//x)(x)\theta$, which is $t\theta \le t\theta$.

Case $p = (p_1, p_2)$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t\theta//p)(x) = (\pi_i(t\theta)//p_i)(x)$ and $(t//p)(x)\theta = (\pi_i(t)//p_i)(x)\theta$. Since $\pi_i(t\theta) \le \pi_i(t)\theta$, by Lemma A.16 we have $(\pi_i(t\theta)//p_i)(x) \le (\pi_i(t)\theta//p_i)(x)$. By the induction hypothesis we have $(\pi_i(t)\theta//p_i)(x) \le (\pi_i(t)//p_i)(x)\theta$.

Case $p = \text{'tag}(p)$. Analogous to the previous case, since $\pi_{\text{tag}}(t\theta) \le \pi_{\text{tag}}(t)\theta$.

Case $p = p_1 \& p_2$. Each $x \in \text{capt}(p)$ is either in $\text{capt}(p_1)$ or in $\text{capt}(p_2)$. Assume $x \in \text{capt}(p_i)$; then, $(t\theta//p)(x) = (t\theta//p_i)(x)$ and $(t//p)(x)\theta = (t//p_i)(x)\theta$. We conclude by the induction hypothesis.

Case $p = p_1|p_2$. Every $x \in \text{capt}(p)$ is both in $\text{capt}(p_1)$ and in $\text{capt}(p_2)$. We have $(t\theta//p)(x) = ((t \wedge [p_1])\theta//p_1)(x) \vee ((t \setminus [p_1])\theta//p_2)(x)$—pattern types are closed, so we can apply $\theta$ to them too—and $(t//p)(x)\theta = (t \wedge [p_1]//p_1)(x)\theta \vee (t \setminus [p_1]//p_2)(x)\theta$. We conclude by applying the induction hypothesis to both members of the union. $\square$

**Lemma A.19.** Let $t_1$ and $t_2$ be equivalent types ($t_1 \simeq t_2$). Then, $\text{mvar}(t_1) = \text{mvar}(t_2)$.

*Proof.* Since subtyping is preserved by type substitutions, for every $\alpha$ we have $t_1[\alpha] \simeq t_2[\alpha]$. If $\alpha \in \text{mvar}(t_1)$, we have $t_1[\alpha] \not\simeq t_1$ by the definition of mvar. This necessarily implies $t_2[\alpha] \not\simeq t_2$, otherwise we would have $t_1[\alpha] \simeq t_1$ by transitivity. $\square$
### Case Ts-Const Straightforward.

### Case Ts-Abstr We have

$$ \Gamma \vdash_{\S} \lambda x. e_1 : t_1 \to t_2 \qquad \Gamma, \{x : t_1\} \vdash_{\S} e_1 : t_2. $$

By the induction hypothesis we have $\Gamma\theta, \{x: t_1\} \vdash_{\S} e_1: t_2\theta$. Then by Ts-Abstr we derive $\Gamma\theta \vdash_{\S} \lambda x. e_1: (t_1\theta) \to (t_2\theta)$, which is $\Gamma\theta \vdash_{\S} \lambda x. e_1: (t_1 \to t_2)\theta$.

### Cases Ts-Appl, Ts-Pair, and Ts-Tag Straightforward application of the induction hypothesis.

### Case Ts-Match We have

$$ \Gamma \vdash_{\S} \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : t \\ \Gamma \vdash_{\S} e_0 : t_0 \qquad t_0 \leq \bigvee_{i \in I} \{p_i\} \qquad t_i = (t_0 \setminus \bigvee_{j<i} \{p_j\}) \wedge \{p_i\} \\ \forall i \in I. \quad \Gamma, \text{gen}_{\Gamma}(t_i//p_i) \vdash_{\S} e_i : t'_i \qquad t = \bigvee_{i \in I} t'_i $$

and must show $\Gamma\theta \vdash_{\S} \text{match } e_0$ with $(p_i \to e_i)_{i \in I} : t\theta$.

We prove it by establishing, for some types $\hat{t}_0$ and $\hat{t}_i$, $\hat{t}'_i$ for each $i$, that

$$ \Gamma\theta \vdash_{\S} e_0 : \hat{t}_0 \qquad \hat{t}_0 \leq \bigvee_{i \in I} \{p_i\} \qquad \hat{t}_i = (\hat{t}_0 \setminus \bigvee_{j<i} \{p_j\}) \wedge \{p_i\} \\ \forall i \in I. \quad \Gamma\theta, \text{gen}_{\Gamma\theta}(\hat{t}_i//p_i) \vdash_{\S} e_i : \hat{t}'_i \qquad \bigvee_{i \in I} \hat{t}'_i \leq t\theta. $$

Let $A = \{\alpha_1, \dots, \alpha_n\} = \text{var}(t_0) \setminus \text{mvar}(\Gamma)$. Let $B = \{\beta_1, \dots, \beta_n\}$ be a set of type variables such that $B \cap (\text{dom}(\theta) \cup \text{var}(\theta) \cup \text{var}(\Gamma)) = \emptyset$. Let $\theta_0 = [\beta_1/\alpha_1, \dots, \beta_n/\alpha_n]$ and $\theta' = \theta \circ \theta_0$.

By the induction hypothesis, using $\theta'$, we derive $\Gamma\theta' \vdash_{\S} e_0: t_0\theta'$. From it, we derive $\Gamma\theta \vdash_{\S} e_0: t_0\theta'$ by weakening (Lemma A.22); we prove the required premises below. We take $\hat{t}_0 = t_0\theta'$: note that the exhaustiveness condition is satisfied because substitutions preserve subtyping (and all accepted types of patterns are closed). We have $\hat{t}_i = t_i\theta'$ for all $i$.

For all branches, we have $\Gamma, \text{gen}_{\Gamma}(t_i//p_i) \vdash_{\S} e_i: t'_i$ and, by the induction hypothesis using $\theta$, we can derive $\Gamma\theta, (\text{gen}_{\Gamma}(t_i//p_i))\theta \vdash_{\S} e_i: t'_i\theta$.

We apply Lemma A.22 to derive $\Gamma\theta, \text{gen}_{\Gamma\theta}(t_i\theta''//p_i) \vdash_{\S} e_i: t'_i\theta$ (we prove the required premises below). We take $\hat{t}'_i = t'_i\theta$.

*Proof of* $\Gamma\theta \vdash_{\S} e_0: t_0\theta'$ from $\Gamma\theta' \vdash_{\S} e_0: t_0\theta'$ We prove this by Lemma A.22, which requires us to show $\Gamma\theta \sqsubseteq \Gamma\theta'$ and $\text{mvar}(\Gamma\theta) \subseteq \text{mvar}(\Gamma\theta')$. We show this by showing, for every $(x: \forall A_x. t_x) \in \Gamma$—assume by $\alpha$-renaming $A_x \cap (\text{dom}(\theta) \cup \text{var}(\theta) \cup A \cup B) = \emptyset$, $t_x\theta \simeq t_x\theta'$, which implies both $\forall A_x. t_x\theta \sqsubseteq \forall A_x. t_x\theta'$ and $\text{mvar}(\forall A_x. t_x\theta) \subseteq \text{mvar}(\forall A_x. t_x\theta')$ (by Lemma A.21 and Lemma A.19).

We have $t_x\theta_0 \simeq t_x$ by Lemma A.20: $\text{dom}(\theta_0) \cap \text{mvar}(t_x) = \emptyset$ because every $\alpha \in \text{mvar}(t_x)$ is either in $A_x$ or $\text{mvar}(\Gamma)$, and in both cases this means it cannot be in $\text{dom}(\theta_0)$. Hence—since substitutions preserve subtyping—we have also $t_x\theta' = t_x\theta_0\theta \simeq t_x\theta$.

*Proof of* $\Gamma\theta, \text{gen}_{\Gamma\theta}(t_i\theta''//p_i) \vdash_{\S} e_i: t'_i\theta$ from $\Gamma\theta, (\text{gen}_{\Gamma}(t_i//p_i))\theta \vdash_{\S} e_i: t'_i\theta$ To apply Lemma A.22, we must show

$$ \text{gen}_{\Gamma\theta}(t_i\theta''//p_i) \subseteq (\text{gen}_{\Gamma}(t_i//p_i))\theta \\ \text{mvar}(\Gamma\theta, \text{gen}_{\Gamma\theta}(t_i\theta''//p_i)) \subseteq \text{mvar}(\Gamma\theta, (\text{gen}_{\Gamma}(t_i//p_i))\theta). $$

The latter holds because every variable in $\text{mvar}(\Gamma\theta, \text{gen}_{\Gamma\theta}(t_i\theta''//p_i))$ is in $\text{mvar}(\Gamma\theta)$.

For the former, we prove that, for every $x \in \text{capt}(p_i)$,

$$ \text{gen}_{\Gamma\theta}((t_i\theta''//p_i)(x)) \subseteq (\text{gen}_{\Gamma}((t_i//p_i)(x)))\theta. $$

Let

$$ t'_x = (t_i\theta''//p_i)(x) \qquad t_x = (t_i//p_i)(x); $$

the statement becomes

$$ \text{gen}_{\Gamma\theta}(t'_x) \subseteq (\text{gen}_{\Gamma}(t_x))\theta. $$

We have $\text{gen}_{\Gamma}(t_x) = \forall A_x. t_x$, where $A_x = \text{var}(t_x) \setminus \text{mvar}(\Gamma)$. Since $\text{var}(t_x) \subseteq \text{var}(t_i) = \text{var}(t_0)$, $A_x \subseteq A$. Let $J = \{j | \alpha_j \in A_x\}$; thus $J \subseteq \{1, \dots, n\}$ and $A_x = A|_J = \{\alpha_j | j \in J\}$. Let $B|_J = \{\beta_j | j \in J\}$. We have $\text{gen}_{\Gamma}(t_x) = \forall B|_J. t_x\theta_0$ by $\alpha$-renaming (we are substituting also the $\alpha_i$ such that $i \notin J$, but it makes no difference as they not in $t_x$). Thus—since $B \cap (\text{dom}(\theta) \cup \text{var}(\theta)) = \emptyset$—we have

$$ (\text{gen}_{\Gamma}(t_x))\theta = \forall B|_J. t_x\theta_0\theta = \forall B|_J. t_x\theta'. $$

The instances of this type scheme are all types $t_x\theta'\theta_x$, with $\text{dom}(\theta_x) \subseteq B|_J$. Given such a type, we must construct an instance of $\text{gen}_{\Gamma\theta}(t'_x)$ that is a subtype of it. Let $\theta'_x$ be
**Lemma A.20.** Let $t$ be a type and $\theta$ a type substitution such that $\text{dom}(\theta) \cap \text{mvar}(t) = \emptyset$. Then $t\theta \simeq t$.

*Proof.* Let $t' = t[^{0}/\alpha_1, \dots, ^{0}/\alpha_n]$ where $\{\alpha_1, \dots, \alpha_n\} = \text{var}(t) \setminus \text{mvar}(t)$. We have $t \simeq t'$ and $\text{var}(t') = \text{mvar}(t)$. Since substitutions preserve subtyping (and hence equivalence), we have also $t\theta \simeq t'\theta$. But $t'\theta = t' \simeq t$; hence, we reach the conclusion by the transitivity of equivalence. $\square$

**Lemma A.21.** Let $\Gamma_1, \Gamma_2$ be two type environments such that $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$ and $t_1, t_2$ two types such that $t_1 \le t_2$. Then, $\text{gen}_{\Gamma_1}(t_1) \subseteq \text{gen}_{\Gamma_2}(t_2)$.

*Proof.* An instance of $\text{gen}_{\Gamma_2}(t_2)$ is a type $t_2\theta_2$ such that $\text{dom}(\theta_2) \subseteq \text{var}(t_2) \setminus \text{mvar}(\Gamma_2)$. Let $\theta_1$ be the restriction of $\theta_2$ to the variables in $\text{var}(t_1) \setminus \text{mvar}(\Gamma_1)$. Then, $t_1\theta_1$ is an instance of $\text{gen}_{\Gamma_1}(t_1)$. We have $t_1\theta_1 = t_1\theta_2$ because the two substitutions differ only on variables in $\text{var}(t_2) \setminus \text{var}(t_1)$ (which do not appear in $t_1$ at all) or in $\text{mvar}(\Gamma_1) \setminus \text{mvar}(\Gamma_2)$ (which is empty). Finally, we have $t_1\theta_2 \le t_2\theta_2$ because subtyping is preserved by substitutions. $\square$

**Lemma A.22 (Weakening).** Let $\Gamma_1, \Gamma_2$ be two type environments such that $\Gamma_1 \subseteq \Gamma_2$ and $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$. If $\Gamma_2 \vdash_5 e: t$, then $\Gamma_1 \vdash_5 e: t$.

*Proof.* By induction on the derivation of $\Gamma_2 \vdash_5 e: t$. We reason by cases on the last applied rule.

*Case Ts-Var* We have

$$ \Gamma_2 \vdash_5 x: t \quad t \in \text{inst}(\Gamma_2(x)) $$

and hence, since $\Gamma_1 \subseteq \Gamma_2$, there exists a $t' \in \text{inst}(\Gamma_1(x))$ such that $t' \le t$. We apply *Ts-Var* to derive $\Gamma_1 \vdash_5 x: t'$ and *Ts-Subsum* to conclude.

*Case Ts-Const* Straightforward.

*Case Ts-Abstr* We have

$$ \Gamma_2 \vdash_5 \lambda x. e_1: t_1 \to t_2 \quad \Gamma_2, \{x: t_1\} \vdash_5 e_1: t_2. $$

Since $\Gamma_1 \subseteq \Gamma_2$, we have $\Gamma_1, \{x: t_1\} \subseteq \Gamma_2, \{x: t_1\}$; since $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$, we have $\text{mvar}(\Gamma_1, \{x: t_1\}) \subseteq \text{mvar}(\Gamma_2, \{x: t_1\})$. We derive $\Gamma_1, \{x: t_1\} \vdash_5 e_1: t_2$ by the induction hypothesis and apply *Ts-Abstr* to conclude.

*Cases Ts-Appl, Ts-Pair, Ts-Tag, and Ts-Subsum* Straightforward application of the induction hypothesis.

*Case Tk-Match* We have

$$ \Gamma_2 \vdash_5 \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I}: t \\ \Gamma_2 \vdash_5 e_0: t_0 \quad t_0 \le \bigvee_{i \in I} \{p_i\} \quad t_i = (t_0 \setminus \bigvee_{j<i} \{p_j\}) \wedge \{p_i\} \\ \forall i \in I. \quad \Gamma_2, \text{gen}_{\Gamma_2}(t_i//p_i) \vdash_5 e_i: t'_i \quad t = \bigvee_{i \in I} t'_i. $$

By the induction hypothesis, we derive $\Gamma_1 \vdash_5 e_0: t_0$.

For any branch, note that $\text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$ implies $\text{gen}_{\Gamma_1}(t) \subseteq \text{gen}_{\Gamma_2}(t)$ for any $t$ by Lemma A.21. Hence, we have $\Gamma_1, \text{gen}_{\Gamma_1}(t_i//p_i) \subseteq \Gamma_2, \text{gen}_{\Gamma_2}(t_i//p_i)$. Additionally, since $\text{mvar}(\text{gen}_{\Gamma_1}(t_i//p_i)) \subseteq \text{mvar}(\Gamma_1) \subseteq \text{mvar}(\Gamma_2)$, we have $\text{mvar}(\Gamma_1, \text{gen}_{\Gamma_1}(t_i//p_i)) \subseteq \text{mvar}(\Gamma_2, \text{gen}_{\Gamma_2}(t_i//p_i))$.

Hence we may apply the induction hypothesis for all $i$ to derive $\Gamma_1, \text{gen}_{\Gamma_1}(t_i//p_i) \vdash_5 e_i: t'_i$ and then apply *Ts-Match* to conclude. $\square$

**Lemma A.23 (Stability of typing under type substitutions).** Let $\theta$ be a type substitution. If $\Gamma \vdash_5 e: t$, then $\Gamma\theta \vdash_5 e: t\theta$.

*Proof.* By induction on the derivation of $\Gamma \vdash_5 e: t$. We reason by cases on the last applied rule.

*Case Ts-Var* We have

$$ \Gamma \vdash_5 x: t \quad t \in \text{inst}(\Gamma(x)) \quad \Gamma(x) = \forall A. t_x \quad t = t_x \theta_x \quad \text{dom}(\theta_x) \subseteq A $$

and must show $\Gamma\theta \vdash_5 x: t\theta$.

By $\alpha$-renaming we assume $A \cap (\text{dom}(\theta) \cup \text{var}(\theta)) = \emptyset$. Under this assumption, $(\Gamma\theta)(x) = \forall A. t_x\theta$. We must show that $t\theta = t_x\theta'_{x}$ for a substitution $\theta'_{x}$ such that $\text{dom}(\theta'_{x}) \subseteq A$.

Let $\theta'_{x} = [\alpha_{\theta x} \theta / \alpha | \alpha \in A]$. We show that $t\theta'_{x} = t_x \theta_x \theta = t\theta$, by showing that, for every $\alpha, \alpha\theta\theta'_{x} = \alpha\theta_x\theta$. If $\alpha \in A$, then $\alpha\theta\theta'_{x} = \alpha\theta'_{x} = \alpha\theta_x\theta$ ($\theta$ is not defined on the variables in $A$). If $\alpha \notin A$, then $\alpha\theta\theta'_{x} = \alpha\theta$ ($\theta$ never produces any variable in $A$) and $\alpha\theta_x\theta = \alpha\theta$ as $\alpha \notin \text{dom}(\theta_x)$.
the restriction of $\theta_x$ to variables in $\mathrm{var}(t'_x) \setminus \mathrm{mvar}(\Gamma\theta)$. Then $t'_x\theta'_x$ is a valid instance of $\mathrm{gen}_{\Gamma\theta}(t'_x)$. We prove $t'_x\theta'_x \le t_x\theta'\theta_x$.

We have $t'_x\theta'_x = t'_x\theta_x$: the two substitutions differ only on variables in $B|_J \setminus \mathrm{var}(t'_x)$ (variables which do not appear in the type at all) and on variables in $B|_J \cap \mathrm{mvar}(\Gamma\theta)$ (which is empty, because $B$ was chosen fresh). By Lemma A.16, we have $t'_x = (t_i\theta'//p_i)(x) \le (t_i//p_i)(x)\theta'$: hence, $t'_x\theta_x = (t_i\theta'//p_i)(x)\theta_x \le (t_i//p_i)(x)\theta'\theta_x = t_x\theta'\theta_x$.

**Case Ts-Subsum** The conclusion follows from the induction hypothesis since substitutions preserve subtyping. □

**Corollary A.24.** Let $\Gamma$ be a type environment and $\theta$ a type substitution such that $\mathrm{dom}(\theta) \cap \mathrm{mvar}(\Gamma) = \emptyset$. If $\Gamma \vdash_e t: t$, then $\Gamma \vdash_e e: t\theta$.

*Proof.* From $\Gamma \vdash_e e: t$ we derive $\Gamma\theta \vdash_e e: t\theta$ by Lemma A.23. Then, we show $\Gamma \sqsubseteq \Gamma\theta$ and $\mathrm{mvar}(\Gamma) \subseteq \mathrm{mvar}(\Gamma\theta)$, which allow us to apply Lemma A.22 to derive $\Gamma \vdash_e e: t\theta$.

To show the two conditions above, we show that, for every $(x: \forall A. t) \in \Gamma$—assume by $\alpha$-renaming $A \cap (\mathrm{dom}(\theta) \cup \mathrm{var}(\theta)) = \emptyset$, $\forall A. t \sqsubseteq \forall A. t\theta$ and $\mathrm{mvar}(\forall A. t) \subseteq \mathrm{mvar}(\forall A. t\theta)$.

We show $t \simeq t\theta$, which implies both (by Lemma A.21 and Lemma A.19). The equivalence holds by Lemma A.20: $\mathrm{dom}(\theta) \cap \mathrm{mvar}(t) = \emptyset$ because every $\alpha \in \mathrm{mvar}(t)$ is either in $A$ or $\mathrm{mvar}(\Gamma)$, and in both cases this means it cannot be in $\mathrm{dom}(\theta)$. □

**Lemma A.25 (Expression substitution).** Let $x_1, \dots, x_n$ be distinct variables and $v_1, \dots, v_n$ values. Let $\Gamma' = \{x_1: s_1, \dots, x_n: s_n\}$ and $\zeta = [v_1/x_1, \dots, v_n/x_n]$.

If $\Gamma, \Gamma' \vdash_e e: t$ and, for all $k \in \{1, \dots, n\}$ and for all $t_k \in \mathrm{inst}(s_k)$, $\Gamma \vdash_e v_k: t_k$, then $\Gamma \vdash_e e_\zeta: t$.

*Proof.* By induction on the derivation of $\Gamma, \Gamma' \vdash_e e: t$. We reason by cases on the last applied rule.

**Case Ts-Var** We have

$$ \Gamma, \Gamma' \vdash_e x: t \quad t \in \mathrm{inst}((\Gamma, \Gamma')(x)). $$

Either $x = x_k$ for some $k$ or not. In the latter case, $x_\zeta = x$, $x \notin \mathrm{dom}(\Gamma')$ and hence $(\Gamma, \Gamma')(x) = \Gamma(x)$. Then, since $t \in \mathrm{inst}((\Gamma, \Gamma')(x)), t \in \mathrm{inst}(\Gamma(x))$ and we can apply Ts-Var.

If $x = x_k$, then $(\Gamma, \Gamma')(x) = \Gamma'(x) = s_k$. We must then prove $\Gamma \vdash_e v_k: t$, which we know by hypothesis since $t \in \mathrm{inst}(s_k)$.

**Case Ts-Const** Straightforward.

**Case Ts-Abstr** We have

$$ \Gamma, \Gamma' \vdash_e \lambda x. e_1: t_1 \rightarrow t_2 \quad \Gamma, \Gamma', \{x: t_1\} \vdash_e e_1: t_2. $$

By $\alpha$-renaming we can assume $x \notin \mathrm{dom}(\Gamma, \Gamma')$; then $(\lambda x. e_1)\zeta = \lambda x. (e_1\zeta)$ and $\Gamma, \Gamma', \{x: t_1\} = \Gamma, \{x: t_1\}, \Gamma'$. Therefore we have $\Gamma, \{x: t_1\}, \Gamma' \vdash_e e_1: t_2$ and hence $\Gamma, \{x: t_1\} \vdash_e e_1\zeta: t_2$ by the induction hypothesis. We apply Ts-Abstr to conclude.

**Cases Ts-Appl, Ts-Pair, Ts-Tag, and Ts-Subsum** Straightforward application of the induction hypothesis.

**Case Ts-Match** We have

$$ \Gamma, \Gamma' \vdash_e \mathrm{match} \ e_0 \ \mathrm{with} \ (p_i \rightarrow e_i)_{i \in I}: t \\ \Gamma, \Gamma' \vdash_e e_0: t_0 \quad t_0 \le \bigvee_{i \in I} \lceil p_i \rceil \quad t_i = (t_0 \setminus \bigvee_{j<i} \lceil p_j \rceil) \wedge \lceil p_i \rceil \\ \forall i \in I. \ \Gamma, \Gamma', \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i) \vdash_e e_i: t'_i \quad t = \bigvee_{i \in I} t'_i. $$

We assume by $\alpha$-renaming that no capture variable of any pattern is in the domain of $\Gamma$ or $\Gamma'$. Then, $(\mathrm{match} \ e_0 \ \mathrm{with} \ (p_i \rightarrow e_i)_{i \in I})\zeta = \mathrm{match} \ e_0\zeta \ \mathrm{with} \ (p_i \rightarrow e_i\zeta)_{i \in I}$ and $\Gamma, \Gamma', \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i) = \Gamma, \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i), \Gamma'$ for any $i$.

By the induction hypothesis, we derive $\Gamma \vdash_e e_0\zeta: t_0$ and $\Gamma, \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i) \vdash_e e_i\zeta: t'_i$ for all $i$. From the latter, we prove $\Gamma, \mathrm{gen}_{\Gamma}(t_i//p_i) \vdash_e e_i\zeta: t'_i$ by weakening (Lemma A.22): we have $\mathrm{gen}_{\Gamma}(t_i//p_i) \sqsubseteq \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i)$ by Lemma A.21—since $\mathrm{mvar}(\Gamma) \subseteq \mathrm{mvar}(\Gamma, \Gamma')$ and clearly we have $\mathrm{mvar}(\Gamma, \mathrm{gen}_{\Gamma}(t_i//p_i)) \subseteq \mathrm{mvar}(\Gamma, \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i))$ since $\mathrm{mvar}(\mathrm{gen}_{\Gamma}(t_i//p_i)) \subseteq \mathrm{mvar}(\Gamma)$.

**Theorem A.26 (Progress).** Let $e$ be a well-typed, closed expression (i.e., $\emptyset \vdash_e e: t$ holds for some $t$). Then, either $e$ is a value or there exists an expression $e'$ such that $e \leadsto e'$.

*Proof.* By hypothesis we have $\emptyset \vdash_e e: t$. The proof is by induction on its derivation; we reason by cases on the last applied rule.
**Case Ts-Const** Straightforward.

**Case Ts-Abstr** We have

$$ \Gamma \vdash_{\S} \lambda x. e_1 : t_1 \to t_2 \qquad \Gamma, \{x : t_1\} \vdash_{\S} e_1 : t_2. $$

By the induction hypothesis we have $\Gamma\theta, \{x: t_1\} \vdash_{\S} e_1: t_2\theta$. Then by Ts-Abstr we derive $\Gamma\theta \vdash_{\S} \lambda x. e_1: (t_1\theta) \to (t_2\theta)$, which is $\Gamma\theta \vdash_{\S} \lambda x. e_1: (t_1 \to t_2)\theta$.

**Cases Ts-Appl, Ts-Pair, and Ts-Tag** Straightforward application of the induction hypothesis.

**Case Ts-Match** We have

$$ \Gamma \vdash_{\S} \mathit{match} e_0 \mathit{ with} (p_i \to e_i)_{i \in I} : t \\ \Gamma \vdash_{\S} e_0 : t_0 \qquad t_0 \le \bigvee_{i \in I} \langle p_i \rangle \qquad t_i = (t_0 \setminus \bigvee_{j<i} \langle p_j \rangle) \wedge \langle p_i \rangle \\ \forall i \in I. \quad \Gamma, \mathit{gen}_{\Gamma}(t_i//p_i) \vdash_{\S} e_i : t'_i \qquad t = \bigvee_{i \in I} t'_i $$

and must show $\Gamma\theta \vdash_{\S} \mathit{match} e_0$ with $(p_i \to e_i)_{i \in I} : t\theta$.

We prove it by establishing, for some types $\hat{t}_0$ and $\hat{t}_i$, $\hat{t}'_i$ for each $i$, that

$$ \Gamma\theta \vdash_{\S} e_0 : \hat{t}_0 \qquad \hat{t}_0 \le \bigvee_{i \in I} \langle p_i \rangle \qquad \hat{t}_i = (\hat{t}_0 \setminus \bigvee_{j<i} \langle p_j \rangle) \wedge \langle p_i \rangle \\ \forall i \in I. \quad \Gamma\theta, \mathit{gen}_{\Gamma\theta}(\hat{t}_i//p_i) \vdash_{\S} e_i : \hat{t}'_i \qquad \bigvee_{i \in I} \hat{t}'_i \le t\theta. $$

Let $A = \{\alpha_1, \dots, \alpha_n\} = \mathit{var}(t_0) \setminus \mathit{mvar}(\Gamma)$. Let $B = \{\beta_1, \dots, \beta_n\}$ be a set of type variables such that $B \cap (\mathit{dom}(\theta) \cup \mathit{var}(\theta) \cup \mathit{var}(\Gamma)) = \emptyset$. Let $\theta_0 = [\beta_1/\alpha_1, \dots, \beta_n/\alpha_n]$ and $\theta' = \theta \circ \theta_0$.

By the induction hypothesis, using $\theta'$, we derive $\Gamma\theta' \vdash_{\S} e_0: t_0\theta'$. From it, we derive $\Gamma\theta \vdash_{\S} \lambda e_0: t_0\theta'$ by weakening (Lemma A.22); we prove the required premises below. We take $\hat{t}_0 = t_0\theta'$: note that the exhaustiveness condition is satisfied because substitutions preserve subtyping (and all accepted types of patterns are closed). We have $\hat{t}_i = t_i\theta'$ for all $i$.

For all branches, we have $\Gamma, \mathit{gen}_{\Gamma}(t_i//p_i) \vdash_{\S} e_i: t'_i$ and, by the induction hypothesis using $\theta$, we can derive $\Gamma\theta, (\mathit{gen}_{\Gamma}(t_i//p_i))\theta \vdash_{\S} e_i: t'_i\theta$.

We apply Lemma A.22 to derive $\Gamma\theta, \mathit{gen}_{\Gamma\theta}(t_i\theta''//p_i) \vdash_{\S} e_i: t'_i\theta$ (we prove the required premises below). We take $\hat{t}'_i = t'_i\theta$.

*Proof of* $\Gamma\theta \vdash_{\S} e_0: t_0\theta'$ from $\Gamma\theta' \vdash_{\S} e_0: t_0\theta'$ We prove this by Lemma A.22, which requires us to show $\Gamma\theta \sqsubseteq \Gamma\theta'$ and $\mathit{mvar}(\Gamma\theta) \subseteq \mathit{mvar}(\Gamma\theta')$. We show this by showing, for every $(x: \forall A_x. t_x) \in \Gamma$—assume by $\alpha$-renaming $A_x \cap (\mathit{dom}(\theta) \cup \mathit{var}(\theta) \cup A \cup B) = \emptyset$, $t_x\theta \simeq t_x\theta'$, which implies both $\forall A_x. t_x\theta \sqsubseteq \forall A_x. t_x\theta'$ and $\mathit{mvar}(\forall A_x. t_x\theta) \subseteq \mathit{mvar}(\forall A_x. t_x\theta')$ (by Lemma A.21 and Lemma A.19).

We have $t_x\theta_0 \simeq t_x$ by Lemma A.20: $\mathit{dom}(\theta_0) \cap \mathit{mvar}(t_x) = \emptyset$ because every $\alpha \in \mathit{mvar}(t_x)$ is either in $A_x$ or $\mathit{mvar}(\Gamma)$, and in both cases this means it cannot be in $\mathit{dom}(\theta_0)$. Hence—since substitutions preserve subtyping—we have also $t_x\theta' = t_x\theta_0\theta \simeq t_x\theta$.

*Proof of* $\Gamma\theta, \mathit{gen}_{\Gamma\theta}(t_i\theta''//p_i) \vdash_{\S} e_i: t'_i\theta$ from $\Gamma\theta, (\mathit{gen}_{\Gamma}(t_i//p_i))\theta \vdash_{\S} e_i: t'_i\theta$ To apply Lemma A.22, we must show

$$ \mathit{gen}_{\Gamma\theta}(t_i\theta''//p_i) \subseteq (\mathit{gen}_{\Gamma}(t_i//p_i))\theta \\ \mathit{mvar}(\Gamma\theta, \mathit{gen}_{\Gamma\theta}(t_i\theta''//p_i)) \subseteq \mathit{mvar}(\Gamma\theta, (\mathit{gen}_{\Gamma}(t_i//p_i))\theta). $$

The latter holds because every variable in $\mathit{mvar}(\Gamma\theta, \mathit{gen}_{\Gamma\theta}(t_i\theta''//p_i))$ is in $\mathit{mvar}(\Gamma\theta)$. For the former, we prove that, for every $x \in \mathit{capt}(p_i)$,

$$ \mathit{gen}_{\Gamma\theta}((t_i\theta''//p_i)(x)) \subseteq (\mathit{gen}_{\Gamma}((t_i//p_i)(x)))\theta. $$

Let

$$ t'_x = (t_i\theta''//p_i)(x) \qquad t_x = (t_i//p_i)(x); $$

the statement becomes

$$ \mathit{gen}_{\Gamma\theta}(t'_x) \subseteq (\mathit{gen}_{\Gamma}(t_x))\theta. $$

We have $\mathit{gen}_{\Gamma}(t_x) = \forall A_x. t_x$, where $A_x = \mathit{var}(t_x) \setminus \mathit{mvar}(\Gamma)$. Since $\mathit{var}(t_x) \subseteq \mathit{var}(t_i) = \mathit{var}(t_0)$, $A_x \subseteq A$. Let $J = \{j | \alpha_j \in A_x\}$; thus $J \subseteq \{1, \dots, n\}$ and $A_x = A|_J = \{\alpha_j | j \in J\}$. Let $B|_J = \{\beta_j | j \in J\}$. We have $\mathit{gen}_{\Gamma}(t_x) = \forall B|_J. t_x\theta_0$ by $\alpha$-renaming (we are substituting also the $\alpha_i$ such that $i \notin J$, but it makes no difference as they not in $t_x$). Thus—since $B \cap (\mathit{dom}(\theta) \cup \mathit{var}(\theta)) = \emptyset$—we have

$$ (\mathit{gen}_{\Gamma}(t_x))\theta = \forall B|_J. t_x\theta_0\theta = \forall B|_J. t_x\theta'. $$

The instances of this type scheme are all types $t_x\theta'\theta_x$, with $\mathit{dom}(\theta_x) \subseteq B|_J$. Given such a type, we must construct an instance of $\mathit{gen}_{\Gamma\theta}(t'_x)$ that is a subtype of it. Let $\theta'_x$ be
**Case Ts-Var** This case does not occur because variables are not closed.

**Case Ts-Const** In this case $e$ is a constant $c$ and therefore a value.

**Case Ts-Abstr** In this case $e$ is an abstraction $\lambda x. e_1$. Since it is also closed, it is a value.

**Case Ts-Appl** We have

$$ \emptyset \vdash_{\emptyset} e_1 e_2 : t \qquad \emptyset \vdash_{\emptyset} e_1 : t' \to t \qquad \emptyset \vdash_{\emptyset} e_2 : t'. $$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e'_1$, then $e_1 e_2 \rightsquigarrow e'_1 e_2$. If $e_1$ is a value and $e_2 \rightsquigarrow e'_2$, then $e_1 e_2 \rightsquigarrow e_1 e'_2$.

If both are values then, by Lemma A.12, $e_1$ has the form $\lambda x. e_3$ for some $e_3$. Then, we can apply $R-Appl$ and $e_1 e_2 \rightsquigarrow e_3[e_2/x]$.

**Case Ts-Pair** We have

$$ \emptyset \vdash_{\emptyset} (e_1, e_2) : t_1 \times t_2 \qquad \emptyset \vdash_{\emptyset} e_1 : t_1 \qquad \emptyset \vdash_{\emptyset} e_2 : t_2. $$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e'_1$, then $(e_1, e_2) \rightsquigarrow (e'_1, e_2)$. If $e_1$ is a value and $e_2 \rightsquigarrow e'_2$, then $(e_1, e_2) \rightsquigarrow (e_1, e'_2)$. If both are values, then $(e_1, e_2)$ is also a value.

**Case Ts-Tag** We have

$$ \emptyset \vdash_{\emptyset} \text{tag}(e_1) : \text{tag}(t_1) \qquad \emptyset \vdash_{\emptyset} e_1 : t_1. $$

Analogously to the previous case, by the induction hypothesis we have that either $e_1$ is a value or $e_1 \rightsquigarrow e'_1$. In the former case, `tag(e1)` is a value as well. In the latter, we have `tag(e1) \rightsquigarrow tag(e'_1)`.

**Case Ts-Match** We have

$$ \emptyset \vdash_{\emptyset} \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : t \qquad \emptyset \vdash_{\emptyset} e_0 : t_0 \qquad t_0 \le \bigvee_{i \in I} \lceil p_i \rceil. $$

By the inductive hypothesis, either $e_0$ is a value or it may reduce. In the latter case, if $e_0 \rightsquigarrow e'_0$, then match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow \text{match } e'_0$ with $(p_i \to e_i)_{i \in I}$.

If $e_0$ is a value, on the other hand, the expression may reduce by application of $R-Match$. Since $t_0 \le \bigvee_{i \in I} \lceil p_i \rceil$, $\emptyset \vdash_{\emptyset} e_0 : \bigvee_{i \in I} \lceil p_i \rceil$ holds by subsumption. Hence, since $e_0$ is a value, $\emptyset \vdash_{\emptyset} e_0 : \lceil p_i \rceil$ holds for at least one $i$ (by Lemma A.13); for each such $i$ we have $e_0/p_i = \zeta_i$ (by Lemma A.15). Let $j$ be the least of these $i$; then match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow e_j \zeta_j$.

**Case Ts-Subsum** Straightforward application of the induction hypothesis. $\square$

**Theorem A.27 (Subject reduction).** Let $e$ be an expression and $t$ a type such that $\Gamma \vdash_{\emptyset} e : t$. If $e \rightsquigarrow e'$, then $\Gamma \vdash_{\emptyset} e' : t$.

*Proof.* By induction on the derivation of $\Gamma \vdash_{\emptyset} e : t$. We reason by cases on the last applied rule.

**Cases Ts-Var, Ts-Const, and Ts-Abstr** These cases do not occur: variables, constants, and abstractions never reduce.

**Case Ts-Appl** We have

$$ \Gamma \vdash_{\emptyset} e_1 e_2 : t \qquad \Gamma \vdash_{\emptyset} e_1 : t' \to t \qquad \Gamma \vdash_{\emptyset} e_2 : t'. $$

$e_1 e_2 \rightsquigarrow e'$ occurs in any of three ways: (i) $e_1 \rightsquigarrow e'_1$ and $e' = e'_1 e_2$; (ii) $e_1$ is a value, $e_2 \rightsquigarrow e'_2$ and $e' = e_1 e'_2$; (iii) both $e_1$ and $e_2$ are values, $e_1$ is of the form $\lambda x. e_3$, and $e' = e_3[e_2/x]$.

In the first case, we derive by the induction hypothesis that $\Gamma \vdash_{\emptyset} e'_1 : t' \to t$ and conclude by applying $Ts-Appl$ again. The second case is analogous.

In the third case, we know by Lemma A.12 that $\Gamma, \{x : t'\} \vdash_{\emptyset} e_3 : t$. We also know that $e_2$ is a value such that $\Gamma \vdash_{\emptyset} e'_2 : t'$. Then, by Lemma A.25, $\Gamma \vdash_{\emptyset} e_3[e_2/x] : t$.

**Case Ts-Pair** We have

$$ \Gamma \vdash_{\emptyset} (e_1, e_2) : t_1 \times t_2 \qquad \Gamma \vdash_{\emptyset} e_1 : t_1 \qquad \Gamma \vdash_{\emptyset} e_2 : t_2. $$

$(e_1, e_2) \rightsquigarrow e'$ occurs either because $e_1 \rightsquigarrow e'_1$ and $e' = (e'_1, e_2)$, or because $e_1$ is a value, $e_2 \rightsquigarrow e'_2$, and $e' = (e_1, e'_2)$. In either case, the induction hypothesis allows us to derive that the type of the component that reduces is preserved; therefore, we can apply $Ts-Pair$ again to conclude.

**Case Ts-Tag** Analogously to the previous case, a variant expression only reduces if its argument does, so we apply the induction hypothesis and $Ts-Tag$ to conclude.
the restriction of $\theta_x$ to variables in $\mathrm{var}(t'_x) \setminus \mathrm{mvar}(\Gamma\theta)$. Then $t'_x\theta'_x$ is a valid instance of $\mathrm{gen}_{\Gamma\theta}(t'_x)$. We prove $t'_x\theta'_x \le t_x\theta'\theta_x$.

We have $t'_x\theta'_x = t'_x\theta_x$: the two substitutions differ only on variables in $B|_J \setminus \mathrm{var}(t'_x)$ (variables which do not appear in the type at all) and on variables in $B|_J \cap \mathrm{mvar}(\Gamma\theta)$ (which is empty, because $B$ was chosen fresh). By Lemma A.16, we have $t'_x = (t_i\theta''//p_i)(x) \le (t_i//p_i)(x)\theta'$: hence, $t'_x\theta_x = (t_i\theta''//p_i)(x)\theta_x \le (t_i//p_i)(x)\theta'\theta_x = t_x\theta'\theta_x$.

**Case Ts-Subsum** The conclusion follows from the induction hypothesis since substitutions preserve subtyping. □

**Corollary A.24.** Let $\Gamma$ be a type environment and $\theta$ a type substitution such that $\mathrm{dom}(\theta) \cap \mathrm{mvar}(\Gamma) = \emptyset$. If $\Gamma \vdash_{\emptyset} e: t$, then $\Gamma \vdash_{\emptyset} e: t\theta$.

*Proof.* From $\Gamma \vdash_{\emptyset} e: t$ we derive $\Gamma\theta \vdash_{\emptyset} e: t\theta$ by Lemma A.23. Then, we show $\Gamma \sqsubseteq \Gamma\theta$ and $\mathrm{mvar}(\Gamma) \subseteq \mathrm{mvar}(\Gamma\theta)$, which allow us to apply Lemma A.22 to derive $\Gamma \vdash_{\emptyset} e: t\theta$.

To show the two conditions above, we show that, for every $(x: \forall A. t) \in \Gamma$—assume by $\alpha$-renaming $A \cap (\mathrm{dom}(\theta) \cup \mathrm{var}(\theta)) = \emptyset$, $\forall A. t \sqsubseteq \forall A. t\theta$ and $\mathrm{mvar}(\forall A. t) \subseteq \mathrm{mvar}(\forall A. t\theta)$.

We show $t \simeq t\theta$, which implies both (by Lemma A.21 and Lemma A.19). The equivalence holds by Lemma A.20: $\mathrm{dom}(\theta) \cap \mathrm{mvar}(t) = \emptyset$ because every $\alpha \in \mathrm{mvar}(t)$ is either in $A$ or $\mathrm{mvar}(\Gamma)$, and in both cases this means it cannot be in $\mathrm{dom}(\theta)$. □

**Lemma A.25 (Expression substitution).** Let $x_1, \dots, x_n$ be distinct variables and $v_1, \dots, v_n$ values. Let $\Gamma' = \{x_1: s_1, \dots, x_n: s_n\}$ and $\zeta = [v_1/x_1, \dots, v_n/x_n]$.

If $\Gamma, \Gamma' \vdash_{\emptyset} e: t$ and, for all $k \in \{1, \dots, n\}$ and for all $t_k \in \mathrm{inst}(s_k)$, $\Gamma \vdash_{\emptyset} v_k: t_k$, then $\Gamma \vdash_{\emptyset} e\zeta: t$.

*Proof.* By induction on the derivation of $\Gamma, \Gamma' \vdash_{\emptyset} e: t$. We reason by cases on the last applied rule.

**Case Ts-Var** We have

$$ \Gamma, \Gamma' \vdash_{\emptyset} x: t \quad t \in \mathrm{inst}((\Gamma, \Gamma')(x)). $$

Either $x = x_k$ for some $k$ or not. In the latter case, $x\zeta = x$, $x \notin \mathrm{dom}(\Gamma')$ and hence $(\Gamma, \Gamma')(x) = \Gamma(x)$. Then, since $t \in \mathrm{inst}((\Gamma, \Gamma')(x)), t \in \mathrm{inst}(\Gamma(x))$ and we can apply **Ts-Var**.

If $x = x_k$, then $(\Gamma, \Gamma')(x) = \Gamma'(x) = s_k$. We must then prove $\Gamma \vdash_{\emptyset} v_k: t$, which we know by hypothesis since $t \in \mathrm{inst}(s_k)$.

**Case Ts-Const** Straightforward.

**Case Ts-Abstr** We have

$$ \Gamma, \Gamma' \vdash_{\emptyset} \lambda x. e_1: t_1 \to t_2 \quad \Gamma, \Gamma', \{x: t_1\} \vdash_{\emptyset} e_1: t_2. $$

By $\alpha$-renaming we can assume $x \notin \mathrm{dom}(\Gamma, \Gamma')$; then $(\lambda x. e_1)\zeta = \lambda x. (e_1\zeta)$ and $\Gamma, \Gamma', \{x: t_1\} = \Gamma, \{x: t_1\}, \Gamma'$. Therefore we have $\Gamma, \{x: t_1\}, \Gamma' \vdash_{\emptyset} e_1: t_2$ and hence $\Gamma, \{x: t_1\} \vdash_{\emptyset} e_1\zeta: t_2$ by the induction hypothesis. We apply **Ts-Abstr** to conclude.

**Cases Ts-Appl, Ts-Pair, Ts-Tag, and Ts-Subsum** Straightforward application of the induction hypothesis.

**Case Ts-Match** We have

$$ \Gamma, \Gamma' \vdash_{\emptyset} \mathrm{match} e_0 \text{ with } (p_i \to e_i)_{i \in I}: t \\ \Gamma, \Gamma' \vdash_{\emptyset} e_0: t_0 \quad t_0 \le \bigvee_{i \in I} \lceil p_i \rceil \quad t_i = (t_0 \setminus \bigvee_{j<i} \lceil p_j \rceil) \land \lceil p_i \rceil \\ \forall i \in I. \quad \Gamma, \Gamma', \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i) \vdash_{\emptyset} e_i: t'_i \quad t = \bigvee_{i \in I} t'_i. $$

We assume by $\alpha$-renaming that no capture variable of any pattern is in the domain of $\Gamma$ or $\Gamma'$. Then, $(\mathrm{match} e_0 \text{ with } (p_i \to e_i)_{i \in I})\zeta = \mathrm{match} e_0\zeta$ with $(p_i \to e_i)_{i \in I}$ and $\Gamma, \Gamma', \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i) = \Gamma, \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i)$, $\Gamma'$ for any $i$.

By the induction hypothesis, we derive $\Gamma \vdash_{\emptyset} e_0\zeta: t_0$ and $\Gamma, \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i) \vdash_{\emptyset} e_i\zeta: t'_i$ for all $i$. From the latter, we prove $\Gamma, \mathrm{gen}_{\Gamma}(t_i//p_i) \vdash_{\emptyset} e_i\zeta: t'_i$ by weakening (Lemma A.22): we have $\mathrm{gen}_{\Gamma}(t_i//p_i) \subseteq \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i)$ by Lemma A.21—since $\mathrm{mvar}(\Gamma) \subseteq \mathrm{mvar}(\Gamma')$ and clearly we have $\mathrm{mvar}(\Gamma, \mathrm{gen}_{\Gamma}(t_i//p_i)) \subseteq \mathrm{mvar}(\Gamma, \mathrm{gen}_{\Gamma, \Gamma'}(t_i//p_i))$ since $\mathrm{mvar}(\mathrm{gen}_{\Gamma}(t_i//p_i)) \subseteq \mathrm{mvar}(\Gamma)$.

**Theorem A.26 (Progress).** Let $e$ be a well-typed, closed expression (i.e., $\emptyset \vdash_{\emptyset} e: t$ holds for some $t$). Then, either $e$ is a value or there exists an expression $e'$ such that $e \rightsquigarrow e'$.

*Proof.* By hypothesis we have $\emptyset \vdash_{\emptyset} e: t$. The proof is by induction on its derivation; we reason by cases on the last applied rule.
$$R-Fix \quad \frac{\Upsilon (\lambda x. e) \rightsquigarrow e [\Upsilon (\lambda x. e)/x]}{\Upsilon (\lambda x. e) \rightsquigarrow e [\Upsilon (\lambda x. e)/x]}$$

$$Tk-Fix \quad \frac{K; \Gamma \vdash_K e : \tau \rightarrow \tau}{K; \Gamma \vdash_K e : \tau}$$

$$Ts-Fix \quad \frac{\Gamma \vdash_S e : t \rightarrow t}{\Gamma \vdash_S e : t}$$

<caption>**Figure 11.** Rules for the fixed-point combinator.</caption>

**Case Ts-Match** We have

$$\Gamma \vdash_S \text{ match } e_0 \text{ with } (p_i \rightarrow e_i)_{i \in I} : t \\
\Gamma \vdash_S e_0 : t_0 \qquad t_0 \le \bigvee_{i \in I} \lceil p_i \rceil \qquad t_i = (t_0 \setminus \bigvee_{j<i} \lceil p_j \rceil) \wedge \lceil p_i \rceil \\
\forall i \in I. \quad \Gamma, \text{gen}_\Gamma (t_i // p_i) \vdash_S e_i : t'_i \qquad t = \bigvee_{i \in I} t'_i.$$

The reduction match $e_0$ with $(p_i \rightarrow e_i)_{i \in I} \rightsquigarrow e'$ occurs either because $e_0 \rightsquigarrow e'_0$ and $e' = \text{match } e'_0$ with $(p_i \rightarrow e_i)_{i \in I}$ or because $e_0$ is a value and $e' = e_j \zeta$, where $e_0/p_j = \zeta$ and, for all $i < j$, $e_0/p_i = \Omega$. In the former case, we apply the induction hypothesis and conclude by Ts-Match.

In the latter case, $\zeta$ is a substitution from the capture variables of $p_j$ to values. We can derive

$$\Gamma \vdash_S e_0 : \lceil p_j \rceil \quad \forall i < j. \quad \Gamma \vdash_S e_0 : \neg \lceil p_i \rceil$$

by Lemma A.15 and thence $\Gamma \vdash_S e_0 : t_j$ by Lemma A.14. Therefore, by Lemma A.17, we have that, for all $x \in \text{capt}(p_j)$, $\Gamma \vdash_S x \zeta : (t_j // p_j)(x)$. Let $\Gamma' = t_j // p_j$.

We show that, additionally, $\Gamma \vdash_S x \zeta : t_x$ holds for every $t_x \in \text{inst}(\text{gen}_\Gamma(\Gamma'(x)))$. Every such $t_x$ is equal to $\Gamma'(x)\theta$ for a $\theta$ such that $\text{dom}(\theta) \subseteq \text{var}(\Gamma'(x)) \setminus \text{mvar}(\Gamma)$. Then, $\Gamma \vdash_S x \zeta : \Gamma'(x)\theta$ holds by Corollary A.24, since $\text{dom}(\theta) \cap \text{mvar}(\Gamma) = \emptyset$ (the substitution does not change any meaningful variable of $\Gamma$).

From $\Gamma, \text{gen}_\Gamma(\Gamma') \vdash_S e_j : t'_j$ and from the fact that we have $\Gamma \vdash_S x \zeta : t_x$ for all $x \in \text{capt}(p_j)$ and all $t_x \in \text{inst}(\text{gen}_\Gamma(\Gamma'(x)))$, we derive $\Gamma \vdash_S e_j \zeta : t'_j$ by Lemma A.25 and then conclude by subsumption.

**Case Ts-Subsum** Straightforward application of the induction hypothesis. $\square$

**Corollary A.28** (Type soundness). Let $e$ be a well-typed, closed expression, that is, such that $\emptyset \vdash_S e : t$ holds for some $t$. Then, either $e$ diverges or it reduces to a value $v$ such that $\emptyset \vdash_S v : t$.

**Proof.** Consequence of Theorem A.26 and Theorem A.27. $\square$

### A.3.3 Completeness of $\mathcal{S}$ with respect to $\mathcal{K}$

In the proof of completeness, we consider a calculus and type systems extended with the addition of a fixed-point combinator $\Upsilon$: this simplifies the proof (as it allows us to assume that all arrow types are inhabited) and it would be desirable anyway in order to use the system in pratice. We add a new production $\Upsilon e$ to the grammar defining expressions, a new production $\Upsilon E$ to the grammar of evaluation contexts, and the new reduction rule $R-Fix$ in Figure 11. We extend $\mathcal{K}$ and $\mathcal{S}$ with the addition, respectively, of the rules $Tk-Fix$ and $Ts-Fix$ in Figure 11.

As mentioned in Section 4.3, we prove completeness of $\mathcal{S}$ with respect to $\mathcal{K}$ using inductive techniques which do not account for the presence of recursion in kinds: we therefore have to restrict ourselves to only consider kinding environments which do not feature recursion, (the non-recursive environments defined below). We conjecture that coinductive techniques could be used instead to prove the result for general kinding environments.

**Definition A.35** (Non-recursive kinding environments). We say that a kinding environment $K$ is non-recursive if, for all $\alpha$ such that $K(\alpha) = (L, U, T)$, we have $\alpha \notin \bigcup_{\gamma \in K} \text{var}_K(\tau)$.

**Definition A.36.** We define a function $w$ which, given a $\mathcal{k}$-type $\tau$ in a non-recursive kinding environment $K$, yields the measure $w(\tau, K)$ of $\tau$ in $K$. It is defined by the following equations.

$$\begin{align*}
w(\alpha, K) &= \begin{cases} 1 + \sum_{\gamma \in K} w(\tau, K) & \text{if } K(\alpha) = (L, U, T) \\ 1 & \text{otherwise} \end{cases} \\
w(b, K) &= 1 \\
w(\tau_1 \rightarrow \tau_2, K) &= w(\tau_1, K) + w(\tau_2, K) + 1 \\
w(\tau_1 \times \tau_2, K) &= w(\tau_1, K) + w(\tau_2, K) + 1
\end{align*}$$

**Definition A.37** (Translation of types). Given a $\mathcal{k}$-type $\tau$ in a non-recursive kinding environment $K$, its translation is the $\mathcal{s}$-type $[\tau]_K$ defined inductively by the rules in Figure 12.
**Case Ts-Var** This case does not occur because variables are not closed.

**Case Ts-Const** In this case $e$ is a constant $c$ and therefore a value.

**Case Ts-Abstr** In this case $e$ is an abstraction $\lambda x. e_1$. Since it is also closed, it is a value.

**Case Ts-Appl** We have

$$ \emptyset \vdash_{\emptyset} e_1 e_2 : t \qquad \emptyset \vdash_{\emptyset} e_1 : t' \to t \qquad \emptyset \vdash_{\emptyset} e_2 : t'. $$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e'_1$, then $e_1 e_2 \rightsquigarrow e'_1 e_2$. If $e_1$ is a value and $e_2 \rightsquigarrow e'_2$, then $e_1 e_2 \rightsquigarrow e_1 e'_2$.

If both are values then, by Lemma A.12, $e_1$ has the form $\lambda x. e_3$ for some $e_3$. Then, we can apply $R-Appl$ and $e_1 e_2 \rightsquigarrow e_3[e_2/x]$.

**Case Ts-Pair** We have

$$ \emptyset \vdash_{\emptyset} (e_1, e_2) : t_1 \times t_2 \qquad \emptyset \vdash_{\emptyset} e_1 : t_1 \qquad \emptyset \vdash_{\emptyset} e_2 : t_2. $$

By the induction hypothesis, each of $e_1$ and $e_2$ either is a value or may reduce. If $e_1 \rightsquigarrow e'_1$, then $(e_1, e_2) \rightsquigarrow (e'_1, e_2)$. If $e_1$ is a value and $e_2 \rightsquigarrow e'_2$, then $(e_1, e_2) \rightsquigarrow (e_1, e'_2)$. If both are values, then $(e_1, e_2)$ is also a value.

**Case Ts-Tag** We have

$$ \emptyset \vdash_{\emptyset} \text{tag}(e_1) : \text{tag}(t_1) \qquad \emptyset \vdash_{\emptyset} e_1 : t_1. $$

Analogously to the previous case, by the induction hypothesis we have that either $e_1$ is a value or $e_1 \rightsquigarrow e'_1$. In the former case, `tag(e1)` is a value as well. In the latter, we have `tag(e1) \rightsquigarrow tag(e'_1)`.

**Case Ts-Match** We have

$$ \emptyset \vdash_{\emptyset} \text{match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : t \qquad \emptyset \vdash_{\emptyset} e_0 : t_0 \qquad t_0 \le \bigvee_{i \in I} \lceil p_i \rceil. $$

By the inductive hypothesis, either $e_0$ is a value or it may reduce. In the latter case, if $e_0 \rightsquigarrow e'_0$, then match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow \text{match } e'_0$ with $(p_i \to e_i)_{i \in I}$.

If $e_0$ is a value, on the other hand, the expression may reduce by application of $R-Match$. Since $t_0 \le \bigvee_{i \in I} \lceil p_i \rceil$, $\emptyset \vdash_{\emptyset} e_0 : \bigvee_{i \in I} \lceil p_i \rceil$ holds by subsumption. Hence, since $e_0$ is a value, $\emptyset \vdash_{\emptyset} e_0 : \lceil p_i \rceil$ holds for at least one $i$ (by Lemma A.13); for each such $i$ we have $e_0/p_i = \zeta_i$ (by Lemma A.15). Let $j$ be the least of these $i$; then match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow e_j \zeta_j$.

**Case Ts-Subsum** Straightforward application of the induction hypothesis. $\square$

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

**Theorem A.27 (Subject reduction).** Let $e$ be an expression and $t$ a type such that $\Gamma \vdash_{\emptyset} e : t$. If $e \rightsquigarrow e'$, then $\Gamma \vdash_{\emptyset} e' : t$.

*Proof.* By induction on the derivation of $\Gamma \vdash_{\emptyset} e : t$. We reason by cases on the last applied rule.

**Cases Ts-Var, Ts-Const, and Ts-Abstr** These cases do not occur: variables, constants, and abstractions never reduce.

**Case Ts-Appl** We have

$$ \Gamma \vdash_{\emptyset} e_1 e_2 : t \qquad \Gamma \vdash_{\emptyset} e_1 : t' \to t \qquad \Gamma \vdash_{\emptyset} e_2 : t'. $$

$e_1 e_2 \rightsquigarrow e'$ occurs in any of three ways: (i) $e_1 \rightsquigarrow e'_1$ and $e' = e'_1 e_2$; (ii) $e_1$ is a value, $e_2 \rightsquigarrow e'_2$ and $e' = e_1 e'_2$; (iii) both $e_1$ and $e_2$ are values, $e_1$ is of the form $\lambda x. e_3$, and $e' = e_3[e_2/x]$.

In the first case, we derive by the induction hypothesis that $\Gamma \vdash_{\emptyset} e'_1 : t' \to t$ and conclude by applying $Ts-Appl$ again. The second case is analogous.

In the third case, we know by Lemma A.12 that $\Gamma, \{x : t'\} \vdash_{\emptyset} e_3 : t$. We also know that $e_2$ is a value such that $\Gamma \vdash_{\emptyset} e'_2 : t'$. Then, by Lemma A.25, $\Gamma \vdash_{\emptyset} e_3[e_2/x] : t$.

**Case Ts-Pair** We have

$$ \Gamma \vdash_{\emptyset} (e_1, e_2) : t_1 \times t_2 \qquad \Gamma \vdash_{\emptyset} e_1 : t_1 \qquad \Gamma \vdash_{\emptyset} e_2 : t_2. $$

$(e_1, e_2) \rightsquigarrow e'$ occurs either because $e_1 \rightsquigarrow e'_1$ and $e' = (e'_1, e_2)$, or because $e_1$ is a value, $e_2 \rightsquigarrow e'_2$, and $e' = (e_1, e'_2)$. In either case, the induction hypothesis allows us to derive that the type of the component that reduces is preserved; therefore, we can apply $Ts-Pair$ again to conclude.

**Case Ts-Tag** Analogously to the previous case, a variant expression only reduces if its argument does, so we apply the induction hypothesis and $Ts-Tag$ to conclude.
$$ \llbracket \alpha \rrbracket_K = \begin{cases} \alpha & \text{if } K(\alpha) = \bullet \\ (\text{low}_K(L, T) \lor \alpha) \land \text{upp}_K(U, T) & \text{if } K(\alpha) = (L, U, T) \end{cases} $$

$$ \llbracket \tau_1 \to \tau_2 \rrbracket_K = \llbracket \tau_1 \rrbracket_K \to \llbracket \tau_2 \rrbracket_K $$ $$ \llbracket \tau_1 \times \tau_2 \rrbracket_K = \llbracket \tau_1 \rrbracket_K \times \llbracket \tau_2 \rrbracket_K $$

where:

$$ \text{low}_K(L, T) = \bigvee_{\gamma \in L} \text{tag}(\bigwedge_{\gamma \in T} \llbracket \tau \rrbracket_K) $$ $$ \text{upp}_K(U, T) = \begin{cases} \bigvee_{\gamma \in U} \text{tag}(\bigwedge_{\gamma \in T} \llbracket \tau \rrbracket_K) & \text{if } U \neq \mathcal{L} \\ \bigvee_{\gamma \in \text{dom}(T)} \text{tag}(\bigwedge_{\gamma \in T} \llbracket \tau \rrbracket_K) \lor (1_v \land \bigvee_{\gamma \in \text{dom}(T)} \text{tag}(1)) & \text{if } U = \mathcal{L} \end{cases} $$

<caption>**Figure 12.** Translation of k-types to s-types.</caption>

We define the translation of type schemes as $\llbracket \forall A. K' \triangleright \tau \rrbracket_K = \forall A. \llbracket \tau \rrbracket_{K,K'}$ and of type environments by translating each type scheme pointwise.

**Lemma A.29.** For any k-type $\tau$ in a non-recursive kinding environment $K$, we have $\text{var}(\llbracket \tau \rrbracket_K) \subseteq \text{var}_K(\tau)$. Likewise, for any k-scheme $\sigma$ and k-type environment $\Gamma$, we have $\text{var}(\llbracket \sigma \rrbracket_K) \subseteq \text{var}_K(\sigma)$ and $\text{var}(\llbracket \Gamma \rrbracket_K) \subseteq \text{var}_K(\Gamma)$.

*Proof.* The translation does not introduce new variables, therefore we can show $\text{var}(\llbracket \tau \rrbracket_K) \subseteq \text{var}_K(\tau)$ by induction on $w(\tau, K)$. We extend this straightforwardly to type schemes and environments. □

**Lemma A.30.** Let $p$ be a pattern and $t \le \lceil p \rceil$ an s-type. If $K \vdash p: \tau \Rightarrow \Gamma$ and $t \le \llbracket \tau \rrbracket_K$, then, for all $x \in \text{capt}(p)$, $(t//p)(x) \le \llbracket \Gamma(x) \rrbracket_K$.

*Proof.* By structural induction on $p$.

Cases $p = \_\_\_\_\_$ and $p = c$ There is nothing to prove since $\text{capt}(p) = \emptyset$.

Case $p = x$ We have

$$ K \vdash p: \tau \Rightarrow \{x: \tau\} \quad t//x = \{x: t\} $$

and must prove $\{x: t\}(x) \le \llbracket \{x: \tau\}(x) \rrbracket_K$, that is, $t \le \llbracket \tau \rrbracket_K$, which is true by hypothesis.

Case $p = (p_1, p_2)$ We have

$$ K \vdash p: \tau_1 \times \tau_2 \Rightarrow \Gamma \quad \Gamma = \Gamma_1 \cup \Gamma_2 \quad \forall i. K \vdash p_i: \tau_i \Rightarrow \Gamma_i $$ $$ t//p = \pi_1(t)//p_1 \cup \pi_2(t)//p_2. $$

Since $t \le \llbracket \tau_1 \rrbracket_K \times \llbracket \tau_2 \rrbracket_K$, by Property A.31 we have $\pi_i(t) \le \llbracket \tau_i \rrbracket_K$. Likewise, $\pi_i(t) \le \lceil p_i \rceil$. We apply the induction hypothesis to conclude.

Case $p = \text{tag}(p_1)$ We have

$$ K \vdash p: \alpha \Rightarrow \Gamma \quad K \vdash p_1: \tau_1 \Rightarrow \Gamma $$ $$ K(\alpha) = (L, U, T) \quad (\text{tag} \in U \text{ implies } \text{tag}: \tau_1 \in T) \quad t//p = \pi_{\text{tag}}(t)//p_1. $$

Since $t \le \lceil \text{tag}(p_1) \rceil = \lceil \text{tag}(\lceil p_1 \rceil) \rceil$, by Property A.32 we have $\pi_{\text{tag}}(t) \le \lceil p_1 \rceil$. We next prove $\pi_{\text{tag}}(t) \le \llbracket \tau_1 \rrbracket_K$, which allows us to apply the induction hypothesis and conclude.

The translation of $\alpha$ is $\llbracket \alpha \rrbracket_K = (\text{low}_K(L, T) \lor \alpha) \land \text{upp}_K(U, T)$. We have $t \le \llbracket \alpha \rrbracket_K$ and hence $t \le \text{upp}_K(U, T)$. Since $t \le \text{tag}(1)$, $t \le \text{upp}_K(U, T) \land \text{tag}(1)$. We distribute the intersection over the summands of $\text{upp}_K(U, T)$, which is a union.

If $\text{tag} \notin U$ (in which case $U \ne \mathcal{L}$), then all summands have the form $\text{tag}_1(\tau')$ and for each $\text{tag}_1$ we have $\text{tag}_1 \ne \text{tag}:$ hence, the intersection is empty and thus we have $t \le \emptyset \simeq \text{tag}(\emptyset)$. Then $\pi_{\text{tag}}(t) \le \emptyset \le \llbracket \tau_1 \rrbracket_K$.

If $\text{tag} \in U$, then necessarily $\text{tag} \in \text{dom}(T)$ holds as well. In that case the intersection $\text{upp}_K(U, T) \land \text{tag}(1)$ is equivalent to $\text{tag}(\bigwedge_{\gamma \in T} \llbracket \tau' \rrbracket_K)$. Hence $t \le \text{tag}(\bigwedge_{\gamma \in T} \llbracket \tau' \rrbracket_K)$ and $\pi_{\text{tag}}(t) \le \bigwedge_{\gamma' \in T} \llbracket \tau' \rrbracket_K$. Since $\text{tag}: \tau_1 \in T$, $\bigwedge_{\gamma' \in T} \llbracket \tau' \rrbracket_K \le \llbracket \tau_1 \rrbracket_K$, from which follows $\pi_{\text{tag}}(t) \le \llbracket \tau_1 \rrbracket_K$.

Case $p = p_1 \& p_2$ We directly apply the induction hypothesis to both sub-patterns and conclude.
$$R-Fix \quad \overline{\Upsilon(\lambda x. e)} \rightsquigarrow e[\Upsilon(\lambda x. e)/x]$$

$$Tk-Fix \quad \frac{K; \Gamma \vdash_K e : \tau \to \tau}{K; \Gamma \vdash_K e : \tau}$$

$$Ts-Fix \quad \frac{\Gamma \vdash_S e : t \to t}{\Gamma \vdash_S e : t}$$

<caption>**Figure 11.** Rules for the fixed-point combinator.</caption>

**Case Ts-Match** We have

$$\Gamma \vdash_S \text{ match } e_0 \text{ with } (p_i \to e_i)_{i \in I} : t \\
\Gamma \vdash_S e_0 : t_0 \qquad t_0 \le \bigvee_{i \in I} \lceil p_i \rceil \qquad t_i = (t_0 \setminus \bigvee_{j<i} \lceil p_j \rceil) \wedge \lceil p_i \rceil \\
\forall i \in I. \quad \Gamma, \text{gen}_\Gamma(t_i // p_i) \vdash_S e_i : t'_i \qquad t = \bigvee_{i \in I} t'_i.$$

The reduction match $e_0$ with $(p_i \to e_i)_{i \in I} \rightsquigarrow e'$ occurs either because $e_0 \rightsquigarrow e'_0$ and $e' = \text{match } e'_0$ with $(p_i \to e_i)_{i \in I}$ or because $e_0$ is a value and $e' = e_j \zeta$, where $e_0/p_j = \zeta$ and, for all $i < j$, $e_0/p_i = \Omega$. In the former case, we apply the induction hypothesis and conclude by Ts-Match.

In the latter case, $\zeta$ is a substitution from the capture variables of $p_j$ to values. We can derive

$$\Gamma \vdash_S e_0 : \lceil p_j \rceil \quad \forall i < j. \quad \Gamma \vdash_S e_0 : \neg \lceil p_i \rceil$$

by Lemma A.15 and thence $\Gamma \vdash_S e_0 : t_j$ by Lemma A.14. Therefore, by Lemma A.17, we have that, for all $x \in \text{capt}(p_j)$, $\Gamma \vdash_S x \zeta : (t_j // p_j)(x)$. Let $\Gamma' = t_j // p_j$.

We show that, additionally, $\Gamma \vdash_S x \zeta : t_x$ holds for every $t_x \in \text{inst}(\text{gen}_\Gamma(\Gamma'(x)))$. Every such $t_x$ is equal to $\Gamma'(x)\theta$ for a $\theta$ such that $\text{dom}(\theta) \subseteq \text{var}(\Gamma'(x)) \setminus \text{mvar}(\Gamma)$. Then, $\Gamma \vdash_S x \zeta : \Gamma'(x)\theta$ holds by Corollary A.24, since $\text{dom}(\theta) \cap \text{mvar}(\Gamma) = \emptyset$ (the substitution does not change any meaningful variable of $\Gamma$).

From $\Gamma, \text{gen}_\Gamma(\Gamma') \vdash_S e_j : t'_j$ and from the fact that we have $\Gamma \vdash_S x \zeta : t_x$ for all $x \in \text{capt}(p_j)$ and all $t_x \in \text{inst}(\text{gen}_\Gamma(\Gamma'(x)))$, we derive $\Gamma \vdash_S e_j \zeta : t'_j$ by Lemma A.25 and then conclude by subsumption.

**Case Ts-Subsum** Straightforward application of the induction hypothesis. $\square$

**Corollary A.28** (Type soundness). Let $e$ be a well-typed, closed expression, that is, such that $\emptyset \vdash_S e : t$ holds for some $t$. Then, either $e$ diverges or it reduces to a value $v$ such that $\emptyset \vdash_S v : t$.

**Proof.** Consequence of Theorem A.26 and Theorem A.27. $\square$

### A.3.3 Completeness of $\mathcal{S}$ with respect to $\mathcal{K}$

In the proof of completeness, we consider a calculus and type systems extended with the addition of a fixed-point combinator $\Upsilon$: this simplifies the proof (as it allows us to assume that all arrow types are inhabited) and it would be desirable anyway in order to use the system in pratice. We add a new production $\Upsilon e$ to the grammar defining expressions, a new production $\Upsilon E$ to the grammar of evaluation contexts, and the new reduction rule $R-Fix$ in Figure 11. We extend $\mathcal{K}$ and $\mathcal{S}$ with the addition, respectively, of the rules $Tk-Fix$ and $Ts-Fix$ in Figure 11.

As mentioned in Section 4.3, we prove completeness of $\mathcal{S}$ with respect to $\mathcal{K}$ using inductive techniques which do not account for the presence of recursion in kinds: we therefore have to restrict ourselves to only consider kinding environments which do not feature recursion, (the non-recursive environments defined below). We conjecture that coinductive techniques could be used instead to prove the result for general kinding environments.

**Definition A.35** (Non-recursive kinding environments). We say that a kinding environment $K$ is non-recursive if, for all $\alpha$ such that $K(\alpha) = (L, U, T)$, we have $\alpha \notin \bigcup_{\gamma \in K} \text{var}_K(\tau)$.

**Definition A.36.** We define a function $w$ which, given a $\mathcal{k}$-type $\tau$ in a non-recursive kinding environment $K$, yields the measure $w(\tau, K)$ of $\tau$ in $K$. It is defined by the following equations.

$$\begin{align*}
w(\alpha, K) &= \begin{cases} 1 + \sum_{\gamma \in K} w(\tau, K) & \text{if } K(\alpha) = (L, U, T) \\ 1 & \text{otherwise} \end{cases} \\
w(b, K) &= 1 \\
w(\tau_1 \to \tau_2, K) &= w(\tau_1, K) + w(\tau_2, K) + 1 \\
w(\tau_1 \times \tau_2, K) &= w(\tau_1, K) + w(\tau_2, K) + 1
\end{align*}$$

**Definition A.37** (Translation of types). Given a $\mathcal{k}$-type $\tau$ in a non-recursive kinding environment $K$, its translation is the $\mathcal{s}$-type $[\tau]_K$ defined inductively by the rules in Figure 12.
Case $p = p_1|p_2$ We have

$$K \vdash p: \tau \Rightarrow \Gamma \quad \forall i. K \vdash p_i: \tau \Rightarrow \Gamma$$
$$t//p = (t \wedge \mathcal{I}_1) // p_1 \quad \mathcal{W} (t \vee \mathcal{I}_2) // p_2.$$

Since $t \wedge \mathcal{I}_1$ and $t \vee \mathcal{I}_2$ are subtypes of $t$, they are also subtypes of $\llbracket \tau \rrbracket_K$. We can apply the induction hypothesis and, for each $x$, derive both that $(t \wedge \mathcal{I}_1) // p_1)(x) \le \llbracket \Gamma(x) \rrbracket_K$ and that $(t \vee \mathcal{I}_2) // p_2)(x) \le \llbracket \Gamma(x) \rrbracket_K$. Hence, $(t//p)(x) \le \llbracket \Gamma(x) \rrbracket_K$. $\square$

**Lemma A.31 (Translation of type substitutions).** Let $K, K'$ be two non-recursive kinding environments such that $dom(K') \cap (dom(K) \cup var_\emptyset(K)) = \emptyset$. Let $\theta$ be a $k$-type substitution such that $dom(\theta) \subseteq dom(K')$ and $K, K' \vdash \theta: K$.

Let $\theta'$ be the $\mathfrak{s}$-type substitution defined as $[\llbracket \alpha \theta \rrbracket_K / \alpha \mid \alpha \in dom(K')]$. For every $k$-type $\tau$, we have $\llbracket \tau \rrbracket_{K,K'} \theta' \simeq \llbracket \tau \theta \rrbracket_K$.

*Proof.* By complete induction on $w(\tau, (K, K'))$. We proceed by cases on $\tau$ and assume that the lemma holds for all $\tau'$ such that $w(\tau', (K, K')) < w(\tau, (K, K'))$.

*Case* $\tau = \alpha$, with $(K, K')(\alpha) = \bullet$ We have $\llbracket \alpha \rrbracket_{K,K'} = \alpha$, hence $\llbracket \alpha \rrbracket_{K,K'} \theta' = \alpha \theta'$. Either $\alpha \in dom(K)$ or $\alpha \in dom(K')$ (the domains are disjoint). In the former case, $\alpha \theta = \alpha$ and $\alpha \theta' = \alpha$. Thus we have $\llbracket \alpha \rrbracket_{K,K'} \theta' = \alpha = \llbracket \alpha \theta \rrbracket_K$. In the latter, $\alpha \theta' = \llbracket \alpha \theta \rrbracket_K$ holds by definition of $\theta'$.

*Case* $\tau = \alpha$, with $K(\alpha) = (L, U, T)$ and $\alpha \notin dom(K')$ We have $\llbracket \alpha \rrbracket_{K,K'} = \llbracket \alpha \rrbracket_K$ because no variable in the kind of $\alpha$ is in $dom(K')$. For the same reason, since the translation does not add variables, $\llbracket \alpha \rrbracket_{K,K'} \theta' = \llbracket \alpha \rrbracket_K$. Additionally, $\alpha \theta = \alpha$, so also $\llbracket \alpha \theta \rrbracket_K = \llbracket \alpha \rrbracket_K$.

*Case* $\tau = \alpha$, with $K'(\alpha) = (L', U', T')$ Because $K, K' \vdash \theta: K$, we know that $\alpha \theta$ is some variable $\beta$ such that $K(\beta) = (L, U, T)$ and $(L, U, T) \models (L', U', T' \theta)$.

We have

$$\llbracket \alpha \theta \rrbracket_K = \llbracket \beta \rrbracket_K = (\mathrm{low}_K(L, T) \vee \beta) \wedge \mathrm{upp}_K(U, T)$$

and

$$\begin{align*}
\llbracket \alpha \rrbracket_{K,K'} \theta' &= ((\mathrm{low}_{K,K'}(L', T') \vee \alpha) \wedge \mathrm{upp}_{K,K'}(U', T')) \theta' \\
&= (\mathrm{low}_{K,K'}(L', T') \theta' \vee \alpha \theta') \wedge \mathrm{upp}_{K,K'}(U', T') \theta' \\
&= (\mathrm{low}_{K,K'}(L', T') \theta' \vee ((\mathrm{low}_K(L, T) \vee \beta) \wedge \mathrm{upp}_K(U, T))) \wedge \mathrm{upp}_{K,K'}(U', T') \theta'.
\end{align*}$$

Let us define

$$l = \mathrm{low}_K(L, T)$$

$$u = \mathrm{upp}_K(U, T)$$

$$l' = \mathrm{low}_{K,K'}(L', T') \theta'$$

$$u' = \mathrm{upp}_{K,K'}(U', T') \theta'$$

and assume that the following hold (we prove them below):

$$l \le u \qquad l' \le u' \qquad l' \le l \qquad u \le u'$$

Then we have also $l' \le u$ by transitivity. Whenever $t \le t'$, we have $t \wedge t' \simeq t$ and $t \vee t' \simeq t'$.

Thus we have the following equivalences:

$$\begin{align*}
\llbracket \alpha \rrbracket_{K,K'} \theta' &= (l' \vee ((l \vee \beta) \wedge u)) \wedge u' \\
&\approx (l' \wedge u') \vee ((l \vee \beta) \wedge u \wedge u') && \text{distributivity} \\
&\approx l' \vee ((l \vee \beta) \wedge u) && l' \le u' \text{ and } u \le u' \\
&\approx (l' \vee l \vee \beta) \wedge (l' \vee u) && \text{distributivity} \\
&\approx (l \vee \beta) \wedge u && l' \le l \text{ and } l' \le u
\end{align*}$$

by which we conclude.

We now prove our four assumptions. The first, $l \le u$, holds because $L \subseteq U$ and $L \subseteq dom(T)$: hence each branch of $l$ appears in $u$ as well. The second is analogous.

For the other assumptions, note that $\llbracket \tau \rrbracket_{K,K'} \theta' \simeq \llbracket \tau' \theta \rrbracket_K$ holds for all $\tau'$ in the range of $T'$. To prove $l' \le l$, note that $L' \subseteq L$ and $T' \theta \subseteq T$. In $l'$, we distribute the application of $\theta'$ over all the summands of the union and inside all variant type constructors. Then, we show `tag(\wedge_{tag: \tau' \in T'} \llbracket \tau' \rrbracket_{K,K'} \theta') \le l` for each `tag` in $L'$. We have `tag(\wedge_{tag: \tau' \in T'} \llbracket \tau' \rrbracket_{K,K'} \theta') \simeq `tag(\wedge_{tag: \tau' \in T'} \llbracket \tau' \theta \rrbracket_K) = `tag(\wedge_{tag: \tau' \in T'} \llbracket \tau' \theta \rrbracket_K)`. Since $L' \subseteq L$, there is a summand of $l$ with the same tag. Since `tag` is in the lower bound, it has a single type in both $T$ and $T'$ and, since $T' \theta \subseteq T$, the type it has in $T$ must be $\tau' \theta$.

To prove $u \le u'$, note that $U \subseteq U'$. If $U = \mathcal{L}$, then $U' = \mathcal{L}$. Then both $u$ and $u'$ are unions of two types: the union of tags mentioned respectively in $T$ and $T'$ and the rest. For each `tag`, if