$\Delta;\Pi\vdash e_{1}:\tau_{1}$ $\Delta;\Pi\vdash e_{2}:\tau_{2}$ (new ty-
tup) $\Delta;\Pi\vdash\langle
e_{1}:\tau_{1},e_{2}:\tau_{2}\rangle:\tau_{1}*\tau_{2}$

#### Case forms

As we mentioned before, our variant disallows nested patterns and requires
exhaustive matches. Without nesting, matching on tuples (which can be unpacked
using the fst and snd operations) and unit is not really useful, so we remove
it from our variant.

Since our pattern matching requires all branches to be of the same
constructor, we actually know statically which GADT is being matched by a
particular match. To simplify the encoding, we can also include this
information at the syntax level. Just like the type annotations, this can be
trivially reconstructed from an unannotated variant coupled with a typing
derivation. The match form that used to be
$\operatorname{\mathbf{case}}e\operatorname{\mathbf{of}}ms$ now becomes
$\operatorname{\mathbf{matchgadt}}e\operatorname{\mathbf{as}}T\operatorname{\mathbf{returning}}\tau_{\mathit{ret}}\operatorname{\mathbf{with}}ms$,
where $T$ is the name of the matched GADT and $\tau_{\mathit{ret}}$ is the
type that is being returned by the whole match.

Because we have removed the nesting of pattern matches and the matching of
tuples and unit, the only rule left from the pat- rules is pat-cons. When
removing nesting we actually need to merge it with pat-var, thus we create the
following new rule:

$\Sigma(c)=\forall\vec{\alpha}.\tau\to(\vec{\tau_{1}})T$
$\Delta_{0},\vec{\alpha},\vec{\tau_{1}}\equiv\vec{\tau_{2}}\vdash\tau:*$ (pat-
cons’) $\Delta_{0}\vdash
c[\vec{\alpha}](x)\downarrow(\vec{\tau_{2}})T\Rightarrow\vec{\alpha},\vec{\tau_{1}}\equiv\vec{\tau_{2}};x:\tau$

Due to our syntactic changes, the ty-case rule becomes:

$\Delta;\Gamma\vdash e:(\vec{\sigma})T$ $\Delta;\Gamma\vdash
ms:(\vec{\sigma})T\Rightarrow\tau_{2}$ (ty-case”)
$\Delta;\Gamma\vdash\operatorname{\mathbf{matchgadt}}e\operatorname{\mathbf{as}}T\operatorname{\mathbf{returning}}\tau_{2}\operatorname{\mathbf{with}}ms:\tau_{2}$

The rule used in the mechanization of the calculus goes one step further and
inlines pat-cons’ in ty-case’ to create a single big rule. This helps with the
mechanized proof, but would decrease the clarity on paper, so we will use the
rules as shown above. The rule used in the mechanization is however equivalent
to this pair of rules.

###  A.2. Encoding definition

In this section, we present the translation from $\lambda_{2,G\mu}$ into cDOT.
The translation was originally presented by Waśko (2021) and is presented here
with some minor modifications (mostly notational).

Moreover, we add yet one more modification to the typing relation: we rely on
a weaker $\vDash$ notion which is a strict weakening of the original one. The
paper introduced a relation $\vdash$ defined by a set of rules (see Figure 7)
and proved that it is equivalent to the original $\vDash$. We weaken the
relation by removing some of the rules. We will call this new relation
$\vdash^{\prime}$ and use it in place of $\vDash$. We remove the ex falso-like
rules and the ones allowing to infer equalities from equality of type lambdas
and arrows. The remaining rules will be enumerated as part of proof of lemma
5.8.

For conciseness, we will use some shorthand conventions when working with cDOT
terms. For example, instead of writing $\\{a\\}\wedge\\{b\\}$ we will
sometimes write $\\{a;b\\}$. Also to avoid repetition, we will use $\\{A=T\\}$
as a shorthand for $\\{A:T..T\\}$. We will also use a more concise syntax for
defining objects: instead of writing
$\nu(s:\\{A:T..T;x:U\\})[p.B]\\{A=T;x=u\\}$ we write:

$\displaystyle\nu(s)[p.B]\\{A=T;x:U;x=u\\}$

Whenever we use some variables that do not appear in the inputs of the
encoding functions, we mean that these are some freshly generated identifiers
that do not appear anywhere else in the program. We use the underscore for
names which are not referred to anywhere.

Now we can show the encoding of types:

$\displaystyle\mathcal{T}(\alpha,\Theta)$ $\displaystyle=\Theta(\alpha)$
$\displaystyle\mathcal{T}(\mathbf{1},\Theta)$
$\displaystyle=\texttt{lib.Unit}$
$\displaystyle\mathcal{T}(\tau_{1}*\tau_{2},\Theta)$
$\displaystyle=\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{1},\Theta)\\}\wedge\\{T_{1}=\mathcal{T}(\tau_{2},\Theta)\\}$
$\displaystyle\mathcal{T}(\tau_{1}\to\tau_{2},\Theta)$
$\displaystyle=\forall\left(\mathit{arg}:\mathcal{T}(\tau_{1},\Theta)\right).\;\mathcal{T}(\tau_{2},\Theta)$
$\displaystyle\mathcal{T}(\left(\tau_{1},\dots,\tau_{n}\right)T,\Theta)$
$\displaystyle=\texttt{env.T}\wedge\\{A_{1}=\mathcal{T}(\tau_{1},\Theta)\\}\wedge\dots\wedge\\{A_{n}=\mathcal{T}(\tau_{n},\Theta)\\}$
$\displaystyle\mathcal{T}(\forall\alpha.\tau,\Theta)$
$\displaystyle=\forall\left(A:\\{T:\bot..\top\\}\right).\;\mathcal{T}(\tau,\Theta[\alpha\mapsto
A.T])$

Then we introduce the term for encoding tuples and unit (the lib) and the
construction of env which encodes the signature $\Sigma$.

⬇

let lib = $\nu$[lib.Any](lib: {

Any : $\bot$..$\top$

Unit = {U: $\bot$..$\top$}

unit : lib.Unit

Tuple = $\mu$(s: {$T_{1}$: $\bot$..$\top$; $T_{2}$: $\bot$..$\top$; fst:
s.$T_{1}$; snd: s.$T_{2}$})

tuple : $\forall$(tl: {$T_{1}$: $\bot$..$\top$; $T_{2}$: $\bot$..$\top$})

$\forall$(x1: tl.$T_{1}$) $\forall$(x2: tl.$T_{2}$)

lib.Tuple $\wedge$ {$T_{1}$ = tl.$T_{1}$} $\wedge$ {$T_{2}$ = tl.$T_{2}$}

}) {

Any = $\top$

Unit = {U: $\bot$..$\top$}

unit = $\nu$[lib.Unit](s: {U=$\top$})

Tuple = $\mu$(s: {$T_{1}$: $\bot$..$\top$; $T_{2}$: $\bot$..$\top$; fst:
s.$T_{1}$; snd: s.$T_{2}$})

tuple = $\lambda$(tl: {$T_{1}$: $\bot$..$\top$; $T_{2}$: $\bot$..$\top$})

$\lambda$(x1: tl.$T_{1}$) $\lambda$(x2: tl.$T_{2}$)

$\nu$[lib.Tuple](s: {$T_{1}$ = tl.$T_{1}$; $T_{2}$ = tl.$T_{2}$; fst = x1; snd
= x2})

}) in ...

We assume that the provided $\Sigma$ is described by the concrete syntax as
described in Section 2.2 of the paper (Xi et al., 2003), and consists of a
list of definitions ($\Sigma=\mathbb{T}_{1},\ldots,\mathbb{T}_{n}$) where
$\mathbb{T}_{i}$ has form the following form:

⬇

(type, ..., type) T = {$\vec{\beta_{1}}$}. ($\vec{\sigma_{1}}$) $c_{1}$ of
$\tau_{1}$

| ...

| {$\vec{\beta_{n}}$}. ($\vec{\sigma_{n}}$) $c_{n}$ of $\tau_{n}$

The type symbol is repeated $m$-times and indicates the cardinality of a given
type constructor $T$. Each $c_{i}$ denotes a name of one of its $n$
constructors. In each $j$th constructor, $\vec{\beta_{j}}$ denotes the list of
its type parameter names, $\tau_{j}$ indicates the type of the constructor
value-level parameter and $\vec{\sigma_{j}}$ indicates to what type each of
the type constructor parameters is instantiated in a given case. Each of
$\vec{\sigma_{j}}$ can reference the parameters $\vec{\beta_{j}}$.

We also use $\Sigma$ as a mapping of GADT constructor signatures. With a
definition like the above, we will have
$\Sigma(c_{j})=\forall\vec{\beta_{j}}.\tau_{j}\to(\vec{\sigma_{j}})T$.

For example, the definition of a GADT emulating equality would look like
following:

⬇

(type, type) T = {$\beta$}. ($\beta$, $\beta$) refl of $\mathbf{1}$

The function EncodeSigma that we define below takes a list of type definitions
($\mathbb{T}_{i}$) and returns an env object encoding each $\mathbb{T}_{i}$ as
a base type and its associated constructors.

⬇

EncodeSigma($\mathbb{T}_{1}$, ..., $\mathbb{T}_{n}$) =

$\nu$[lib.Any](env: {

EncodeGADT($\mathbb{T}_{1}$)

...

EncodeGADT($\mathbb{T}_{n}$)

})

To make the definitions more concise, we define a scheme for helper
substitutions:

(1) $\theta^{(x)}_{\vec{\beta_{i}}}=[\beta_{i,1}\mapsto
x.B_{i,1},\;\dots,\;\beta_{i,m_{i}}\mapsto x.B_{i,m_{i}}]$

With these tools, we can now define the EncodeGADT function, as shown on
Figure 9.

To avoid name clashes we assume that all constructor and type names in
$\Sigma$ are unique.

And finally the encoding of terms. Note that the $\mathit{xf}$ ligature is
used to denote that this rule applies both to $x$-variables and $f$-variables.

$\displaystyle\mathcal{E}(\mathit{xf},\;\Theta)$
$\displaystyle=\Theta(\mathit{xf})$
$\displaystyle\mathcal{E}(c_{i}[\vec{\tau}](e),\;\Theta)$
$\displaystyle=\begin{aligned}
&\operatorname{\mathbf{let}}ts=\nu[\texttt{lib.Any}](ts:\\{B_{i,1}=\mathcal{T}(\tau_{1},\Theta);\;\ldots;\;B_{i,m_{i}}=\mathcal{T}(\tau_{m_{i}},\Theta)\\})\operatorname{\mathbf{in}}\\\
&\operatorname{\mathbf{let}}v=\mathcal{E}(e,\Theta)\operatorname{\mathbf{in}}\\\
&\quad\texttt{env.}c_{i}\;\;ts\;\;v\\\ \end{aligned}$
$\displaystyle\mathcal{E}(\left<\right>,\;\Theta)$
$\displaystyle=\texttt{lib.unit}$
$\displaystyle\mathcal{E}(\left<e_{1}:\tau_{1},e_{2}:\tau_{2}\right>,\;\Theta)$
$\displaystyle=\begin{aligned}
&\operatorname{\mathbf{let}}v_{1}=\mathcal{E}(e_{1},\Theta)\operatorname{\mathbf{in}}\\\
&\operatorname{\mathbf{let}}v_{2}=\mathcal{E}(e_{2},\Theta)\operatorname{\mathbf{in}}\\\
&\quad\texttt{lib.tuple}\;\nu[\texttt{lib.Any}](\\_:\\{T_{1}=\mathcal{T}(\tau_{1},\Theta);T_{2}=\mathcal{T}(\tau_{2},\Theta)\\})\;v_{1}\;v_{2}\\\
\end{aligned}$ $\displaystyle\mathcal{E}(\mathbf{fst}(e),\;\Theta)$
$\displaystyle=\operatorname{\mathbf{let}}v=\mathcal{E}(e,\Theta)\operatorname{\mathbf{in}}v.\texttt{fst}$
$\displaystyle\mathcal{E}(\mathbf{snd}(e),\;\Theta)$
$\displaystyle=\operatorname{\mathbf{let}}v=\mathcal{E}(e,\Theta)\operatorname{\mathbf{in}}v.\texttt{snd}$
$\displaystyle\mathcal{E}(\lambda x:\tau_{1}.e,\;\Theta)$
$\displaystyle=\lambda(x_{0}:\mathcal{T}(\tau_{1},\Theta))\;\mathcal{E}(e,\Theta[x\mapsto
x_{0}])$ $\displaystyle\mathcal{E}(e_{1}(e_{2}),\;\Theta)$
$\displaystyle=\begin{aligned}
&\operatorname{\mathbf{let}}v_{1}=\mathcal{E}(e_{1},\Theta)\operatorname{\mathbf{in}}\\\
&\operatorname{\mathbf{let}}v_{2}=\mathcal{E}(e_{2},\Theta)\operatorname{\mathbf{in}}\\\
&\quad v_{1}\;v_{2}\end{aligned}$
$\displaystyle\mathcal{E}(\Lambda\alpha.e,\;\Theta)$
$\displaystyle=\lambda\left(x_{\alpha}:\\{T:\bot..\top\\}\right)\;\mathcal{E}(e,\Theta[\alpha\mapsto
x_{\alpha}.T])$ $\displaystyle\mathcal{E}(e[\tau_{1}],\;\Theta)$
$\displaystyle=\textbf{let
}tl\,=\,\nu[\texttt{lib.Any}](\\_:\\{T=\mathcal{T}(\tau_{1},\Theta)\\})\textbf{
in }\mathcal{E}(e,\Theta)\;tl$ $\displaystyle\mathcal{E}(\textbf{fix
}f:\tau.e,\;\Theta)$ $\displaystyle=\begin{aligned}
&\operatorname{\mathbf{let}}\mathit{hlpObj}=\nu[\texttt{lib.Any}](\mathit{self}:\\{\\\
&\quad\mathit{fix}=\lambda\left(\\_:\texttt{lib.Unit}\right)\;\mathcal{E}(e,\Theta\left[f\mapsto\mathit{self}.\mathit{fix}\;\;\texttt{lib.unit}\right])\\\
&\\})\operatorname{\mathbf{in}}\mathit{hlpObj}.\mathit{fix}\;\;\texttt{lib.unit}\\\
\end{aligned}$
$\displaystyle\mathcal{E}(\operatorname{\mathbf{let}}x=e_{1}\operatorname{\mathbf{in}}e_{2}\textbf{
end},\;\Theta)$ $\displaystyle=\textbf{let
}x\,=\,\mathcal{E}(e_{1},\Theta)\textbf{ in }\mathcal{E}(e_{2},\Theta[x\mapsto
x])$ $\displaystyle\mathcal{E}(\textbf{matchgadt }e\textbf{ as }T\textbf{
returning }\tau_{ret}\textbf{ with }$
$\displaystyle\qquad\qquad\qquad|\;c_{1}[\beta_{1,1},...,\beta_{1,m_{1}}](x_{1})\Rightarrow
e_{1}\;$ $\displaystyle\qquad\qquad\qquad\ldots$
$\displaystyle\qquad\qquad\qquad|\;c_{n}[\beta_{n,1},...,\beta_{n,m_{n}}](x_{n})\Rightarrow
e_{n},\;\Theta)=$
$\displaystyle\quad\operatorname{\mathbf{let}}tl=\nu[\texttt{lib.Any}](tl:\\{R=\mathcal{T}(\tau_{ret},\Theta)\\})\operatorname{\mathbf{in}}$
$\displaystyle\quad\operatorname{\mathbf{let}}v=\mathcal{E}(e,\Theta)\operatorname{\mathbf{in}}$
$\displaystyle\quad\operatorname{\mathbf{let}}\texttt{case}_{c_{1}}=\lambda\left(arg_{1}:\texttt{env.T}_{C_{1}}\wedge
v.\text{type}\right)$
$\displaystyle\quad\quad\operatorname{\mathbf{let}}x^{\prime}_{1}=arg_{1}\texttt{.data
in }$ $\displaystyle\quad\quad\mathcal{E}(e_{1},\Theta[x_{1}\mapsto
x^{\prime}_{1},\beta_{1,1}\mapsto
arg_{1}.B_{1,1},\;...,\;\beta_{1,m_{1}}\mapsto arg_{1}.B_{1,m_{1}}])$
$\displaystyle\quad\operatorname{\mathbf{in}}$ $\displaystyle\quad...$
$\displaystyle\quad\operatorname{\mathbf{let}}\texttt{case}_{c_{n}}=\lambda\left(arg_{n}:\texttt{env.T}_{C_{n}}\wedge
v.\text{type}\right)$
$\displaystyle\quad\quad\operatorname{\mathbf{let}}x^{\prime}_{n}=arg_{n}\texttt{.data
in }$ $\displaystyle\quad\quad\mathcal{E}(e_{n},\Theta[x_{n}\mapsto
x^{\prime}_{n},\beta_{n,1}\mapsto
arg_{n}.B_{n,1},\;...,\;\beta_{n,m_{n}}\mapsto arg_{n}.B_{n,m_{n}}])$
$\displaystyle\quad\operatorname{\mathbf{in}}$ $\displaystyle\quad
v\texttt{.pmatch}\;\;tl\;\;\texttt{case}_{c_{1}}\;\;...\;\;\texttt{case}_{c_{n}}$

Figure 9. The definition of encoding of a single GADT from the signature
$\Sigma$.

⬇

EncodeGADT(

typecon (type1, ..., typem) T = {$\vec{\beta_{1}}$}. ($\vec{\sigma_{1}}$)
$c_{1}$ of $\tau_{1}$

| ...

| {$\vec{\beta_{n}}$}. ($\vec{\sigma_{n}}$) $c_{n}$ of $\tau_{n}$)

) =

T = $\mu$(s: {

$A_{1}$: $\bot$..$\top$; ... $A_{m}$: $\bot$..$\top$

pmatch: $\forall$(r: {R:$\bot$..$\top$})

$\forall$(case${}_{c_{1}}$: $\forall$(arg: env.T${}_{c_{1}}$ $\wedge$ s.type)
r.R)

...

$\forall$(case${}_{c_{n}}$: $\forall$(arg: env.T${}_{c_{n}}$ $\wedge$ s.type)
r.R)

r.R

})

// and for each constructor from $c_{1}$ to $c_{n}$

T${}_{c_{i}}$ = $\mu$(s: env.T $\wedge$ {

$B_{i,1}$ : $\bot$..$\top$, ..., $B_{i,m_{i}}$: $\bot$..$\top$

$A_{1}$ = $\mathcal{T}$($\sigma_{i,1}$, $\theta^{(s)}_{\vec{\beta_{i}}}$),
..., $A_{m}$ = $\mathcal{T}$($\sigma_{i,m}$, $\theta^{(s)}_{\vec{\beta_{i}}}$)

data: $\mathcal{T}$($\tau_{i}$, $\theta^{(s)}_{\vec{\beta_{i}}}$)

})

$c_{i}$ : $\forall$(ts: {$B_{i,1}$: $\bot$..$\top$; ...; $B_{i,m_{i}}$:
$\bot$..$\top$})

$\forall$(v: $\mathcal{T}$($\tau_{i}$, $\theta^{(ts)}_{\vec{\beta_{i}}}$))

env.T $\wedge$ {$A_{1}$ = $\mathcal{T}$($\sigma_{i,1}$,
$\theta^{(ts)}_{\vec{\beta_{i}}}$); ...; $A_{m}$ =
$\mathcal{T}$($\sigma_{i,m}$, $\theta^{(ts)}_{\vec{\beta_{i}}}$)}

$c_{i}$ = $\lambda$(ts: {$B_{i,1}$: $\bot$..$\top$; ...; $B_{i,m_{i}}$:
$\bot$..$\top$}) $\lambda$(v: $\mathcal{T}$($\tau_{i}$,
$\theta^{(ts)}_{\vec{\beta_{i}}}$))

let s = $\nu$[env.T${}_{c_{i}}$](s: {

$B_{i,1}$ = ts.$B_{i,1}$, ..., $B_{i,m_{i}}$ = ts.$B_{i,m_{i}}$

$A_{1}$ = $\mathcal{T}$($\sigma_{i,1}$, $\theta^{(s)}_{\vec{\beta_{i}}}$),
..., $A_{m}$ = $\mathcal{T}$($\sigma_{i,m}$, $\theta^{(s)}_{\vec{\beta_{i}}}$)

data = v

pmatch = $\lambda$(r: {R:$\bot$..$\top$})

$\lambda$(case${}_{c_{1}}$: $\forall$(arg: env.T${}_{c_{1}}$ $\wedge$ s.type)
r.R)

...

$\lambda$(case${}_{c_{n}}$: $\forall$(arg: env.T${}_{c_{n}}$ $\wedge$ s.type)
r.R)

let h=$\nu$[lib.Any](_: {z=s}) in case${}_{c_{i}}$ h.z

}) in s

###  A.3. Correctness proof for the GADT encoding

Our proof will rely on many simple properties of cDOT derived from cDOT and of
the $=:=$ relation. While they are rather trivial, a more thorough discussion
of them can be found in section 4.5 of (Waśko, 2021). One notable example that
we will use quite a lot is the following lemma:

###### Lemma A.1 (Lemma 6 from (Waśko, 2021)).

For any types $A$, $B$, $C$ and $D$, if $\Gamma\vdash A=:=B$ and $\Gamma\vdash
C=:=D$, then $\Gamma\vdash A\wedge C=:=B\wedge D$.

###### Proof.

By Trans and And subtyping rules212121A mechanized proof can be found in the
attached artifacts, in translation/Helpers.v under the name eq_and_merge.. ∎

###### Lemma A.2.

The term for lib from the encoding and the ones generated by EncodeGADT are
well-typed and satisfy the requirements stated in the 5.4.

###### Proof.

The typing proof of lib has been mechanized222222See translation/Library.v
within attached artifacts. and quite simple so we skip it here and refer to
the mechanization for details.

The env contains necessary definitions to encode each GADT from $\Sigma$.
Let’s consider a single GADT definition and show that the term returned by
EncodeGADT admits the expected type. We start by {}-I, then the type
definitions are trivially checked by the Def-Typ rule. The non-trivial part
are the constructors $c_{i}$. We start with the Def-All rule, followed by two
rather standard applications of All-I rule.

Now, we need to show that the new object created in the body of the lambda is
itself well-typed and satisfies the expected type. As always, we start with
{}-I and will assign to the result the type that directly stems from the
definition — we will generalize it to the desired result type and to show that
it fits the ascribed tag a few lines later. This “primitive” result type will
be232323The symbol $\theta^{(s)}_{\vec{\beta_{i}}}$ is defined as before in
Equation 1.:

$\mu(s:\\{B_{i,1}=ts.B_{i,1}\\}\wedge\ldots\wedge\\{A_{1}=\mathcal{T}(\sigma_{i,1},\theta^{(s)}_{\vec{\beta_{i}}})\\}\wedge...\wedge\\{\mathrm{data}:v.type\\}\wedge\\{\mathrm{pmatch}:...\\})$

(we omit the $\mathrm{pmatch}$ type as it is very long but it is exactly the
same as inside of $\mathrm{env}.T$).

The types can be checked trivially with Def-Typ, the data field gets ascribed
type $v.type$ by Def-Path. Finally, the hardest part is the $\mathrm{pmatch}$
lambda. We use Def-All followed by All-I, in a rather standard way. Inside the
body of the lambda we construct a value $h$ of type $\\{z:s.type\\}$ (checked
by {}-I, Def-Path and Rec-E) and use it to apply $h.z$ to
$\texttt{case}_{c_{i}}$. To typecheck this application we need to show that
$h.z$ fits the type $\mathrm{env}.T_{c_{i}}\wedge s.type$. We have
$h.z:s.type$ trivially by Fld-E. We proceed to show
$h.z:\mathrm{env}.T_{c_{i}}$. We have $h.z:s.type$, and by Sngl-Trans so now
all it remains to be shown is that $s:\mathrm{env}.T_{c_{i}}$. But from the
assumption of {}-I we know that $s$ admits the “primitive” type described
earlier. We use Rec-E, then split the big intersection type into parts using
Sub with And1-<: and And2-<:. After we generalize each type to fit
$\mathrm{env}.T_{c_{i}}$ (shown in the next paragraph), we can rebuild the
type back using &-I and ‘close’ it with Rec-I.

We generalize the type of data using Fld-E, Sngl-Trans again with $v.type$ and
then get back with Fld-I. $v$ itself has type
$\mathcal{T}(\tau_{i},\theta^{(ts)}_{\vec{\beta_{i}}})$ and we need
$\mathcal{T}(\tau_{i},\theta^{(s)}_{\vec{\beta_{i}}})$. We can get from
$\theta^{(ts)}_{\vec{\beta_{i}}}$ to $\theta^{(s)}_{\vec{\beta_{i}}}$, because
they differ only in mapping each $\beta_{i,j}$ to $ts.B_{i,j}$ and $s.B_{i,j}$
respectively. But by definition of $s$, $s.B_{i,j}=:=ts.B_{i,j}$, so we can
simply perform the replacement by A.4.

We generalize the types of $B_{i,j}$ from $\\{B_{i,j}=ts.B_{i,j}\\}$ to
$\\{B_{i,j}:\bot..\top\\}$ by Sub with Typ-<:-Typ.

The types $A_{j}$ stay as-is. This makes us fit the requirements of
$\mathrm{env}.T_{c_{i}}$ apart from one — its first requirement is for the
overall type to also fit $\mathrm{env}.T$. But that is easy — the
$\mathrm{pmatch}$ function already has the right type and we simply generalize
types $A_{j}$ in the same way as we did with $B_{i,j}$. Then we collect the
parts with &-I and Rec-I, in a standard way.

All this allows us to derive both $s:\mathrm{env}.T$ and finally
$s:\mathrm{env}.T_{c_{i}}$, thus giving us $h.z:\mathrm{env}.T_{c_{i}}\wedge
s.type$. Thus the application $\texttt{case}_{c_{i}}\;h.z$ is valid — its
result is $r.R$, like we want.

We have shown that the constructor constructs a valid object, with the
primitive type described earlier. All that remains is to generalize it.
Firstly, we need to remember that the newly created $\nu(\ldots)$ object is
bound to a path thanks to the expression $\textbf{let
}s\,=\,\nu[\mathrm{env}.T_{c_{i}}](\ldots)\textbf{ in }s$. We have that
$s:\mu(s:\ldots)$ where $\ldots$ is the primitive type mentioned before. We
now need to show that
$s:\mathcal{T}((\sigma_{i,1},\ldots,\sigma_{i,m})T,\theta^{(ts)}_{\vec{\beta_{i}}})$
and so we will be able to finish with Let. First, we can unfold $\mathcal{T}$
a bit, so that what we actually have to show is
$\mathrm{env}.T\wedge\\{A_{1}=\mathcal{T}(\sigma_{i,1},\theta^{(ts)}_{\vec{\beta_{i}}};...;A_{m}=\mathcal{T}(\sigma_{i,m},\theta^{(ts)}_{\vec{\beta_{i}}})\\}$.
We use exactly the same reasoning that we did inside of &-I to get that
$s:\mathrm{env}.T$ and $s:\mathrm{env}.T_{c_{i}}$ to satisfy the additional
requirement of {}-I. Now we just need to show
$s:\\{A_{j}=\mathcal{T}(\sigma_{i,j},\theta^{(ts)}_{\vec{\beta_{i}}})\\}$. But
the primitive type already gives us
$s:\\{A_{j}=\mathcal{T}(\sigma_{i,j},\theta{s})\\}$ (after we unpack it with
Rec-E etc., obviously). Now, again we can easily show that the two types are
equal by A.4. Again, $\theta^{(ts)}_{\vec{\beta_{i}}}$ and
$\theta^{(s)}_{\vec{\beta_{i}}}$ map each $\beta_{i,k}$ to $ts.B_{i,k}$ and
$s.B_{i,k}$ respectively, and from the primitive type we also have
$s:\\{B_{i,k}=ts.B_{i,k}\\}$, giving us $s.B_{i,k}=:=ts.B_{i,k}$ by <:-Sel and
Sel-<:. ∎

Before we can prove the preservation of types, we need to show that we can
‘emulate’ all equalities of our modified entailment relation $\vdash^{\prime}$
from $\lambda_{2,G\mu}$ in cDOT. To do so we prove the following lemma:

See 5.8

###### Proof.

The proof proceeds by induction on the derivation of the judgment
$\vdash^{\prime}$. We inspect each case.

$\vec{\alpha}\vdash^{\prime}\tau:*$
$\vec{\alpha}\vdash^{\prime}\tau\equiv\tau$

This case is trivially handled by the Refl rule.

$\vec{\alpha},\Delta\vdash^{\prime}\tau_{1}\equiv\tau_{2}$
$\vec{\alpha},\alpha\equiv\alpha,\Delta\vdash^{\prime}\tau_{1}\equiv\tau_{2}$

We have some $\Gamma$ and $\Theta$ where
$\Psi(\vec{\alpha},\alpha\equiv\alpha,\Delta;\Theta;\Gamma)$ holds and want to
prove that
$\Gamma\vdash\mathcal{T}(\tau_{1},\Theta)=:=\mathcal{T}(\tau_{2},\Theta)$
holds. We can just use the inductive hypothesis: we just need to show that
$\Psi(\vec{\alpha},\Delta;\Theta;\Gamma)$ holds. But that is a weaker
requirement242424Technically it is equivalent because $\alpha\equiv\alpha$
does not introduce any new information — it holds in every environment., so it
holds trivially.

$\vec{\alpha},\Delta[\alpha\mapsto\tau]\vdash^{\prime}\tau_{1}[\alpha\mapsto\tau]\equiv\tau_{2}[\alpha\mapsto\tau]$
$\alpha\text{ has no free occurrences in }\tau$
$\vec{\alpha},\tau\equiv\alpha,\Delta\vdash^{\prime}\tau_{1}\equiv\tau_{2}$

$\vec{\alpha},\Delta[\alpha\mapsto\tau]\vdash^{\prime}\tau_{1}[\alpha\mapsto\tau]\equiv\tau_{2}[\alpha\mapsto\tau]$
$\alpha\text{ has no free occurrences in }\tau$
$\vec{\alpha},\alpha\equiv\tau,\Delta\vdash^{\prime}\tau_{1}\equiv\tau_{2}$

The two rules are symmetric so we will describe the proof for the second one,
the first one is completely analogous.

We want to show that
$\Gamma\vdash\mathcal{T}(\tau_{1},\Theta)=:=\mathcal{T}(\tau_{2},\Theta)$. We
know that $\Psi(\vec{\alpha},\alpha\equiv\tau,\Delta;\Theta;\Gamma)$. This
gives us $\Gamma\vdash\mathcal{T}(\alpha,\Theta)=:=\mathcal{T}(\tau,\Theta)$,
equivalently $\Gamma\vdash\Theta(\alpha)=:=\mathcal{T}(\tau,\Theta)$.

From the inductive hypothesis we know that
$\Gamma\vdash\mathcal{T}(\tau_{1}[\alpha\mapsto\tau],\Theta)=:=\mathcal{T}(\tau_{2}[\alpha\mapsto\tau],\Theta)$
if only we can show that
$\Psi(\vec{\alpha},\Delta[\alpha\mapsto\tau];\Theta;\Gamma)$. From the
assumption $\Psi(\vec{\alpha},\alpha\equiv\tau,\Delta;\Theta;\Gamma)$ we have
that for any $\tau^{\prime}_{1}\equiv\tau^{\prime}_{2}\in\Delta$, we have
$\Gamma\vdash\mathcal{T}(\tau^{\prime}_{1},\Theta)=:=\mathcal{T}(\tau^{\prime}_{2},\Theta)$.
Now, we need to show the same thing for any
$\tau^{\prime\prime}_{1}\equiv\tau^{\prime\prime}_{2}\in\Delta[\alpha\mapsto\tau]$.
But for any
$\tau^{\prime\prime}_{1}\equiv\tau^{\prime\prime}_{2}\in\Delta[\alpha\mapsto\tau]$,
we know that there are some
$\tau^{\prime}_{1}\equiv\tau^{\prime}_{2}\in\Delta$ such that
$\tau^{\prime\prime}_{1}=\tau^{\prime}_{1}[\alpha\mapsto\tau]$ and
$\tau^{\prime\prime}_{2}=\tau^{\prime}_{2}[\alpha\mapsto\tau]$. Thus we know
that
$\Gamma\vdash\mathcal{T}(\tau^{\prime}_{1},\Theta)=:=\mathcal{T}(\tau^{\prime}_{2},\Theta)$
and just need to show
$\Gamma\vdash\mathcal{T}(\tau^{\prime}_{1}[\alpha\mapsto\tau],\Theta)=:=\mathcal{T}(\tau^{\prime}_{2}[\alpha\mapsto\tau],\Theta)$.
We will get
$\Gamma\vdash\mathcal{T}(\tau^{\prime}_{1}[\alpha\mapsto\tau],\Theta)=:=\mathcal{T}(\tau^{\prime}_{1},\Theta)$
by A.5 and analogously for $\tau_{2}$ and get the desired conclusion by
transitivity of $=:=$.

We have proven $\Psi(\vec{\alpha},\Delta[\alpha\mapsto\tau];\Theta;\Gamma)$,
which gives us
$\Gamma\vdash\mathcal{T}(\tau_{1}[\alpha\mapsto\tau],\Theta)=:=\mathcal{T}(\tau_{2}[\alpha\mapsto\tau],\Theta)$.
Again, in the same way we use A.5 to show that
$\Gamma\vdash\mathcal{T}(\tau_{1}[\alpha\mapsto\tau],\Theta)=:=\mathcal{T}(\tau_{1},\Theta)$
and also analogously for $\tau_{2}$ — then the conclusion follows trivially
from transitivity of $=:=$.

In the last rule we handle the $T$ type constructor could stand for the GADT
type constructors but also tuple and arrow types. However, due to our
restriction the arrow rule is removed, so we stay with the following two
rules: one for GADTs and one for tuples.

$\vec{\alpha},\vec{\tau_{A}}\equiv\vec{\tau_{B}}\vdash^{\prime}\tau_{1}\equiv\tau_{2}$
$\vec{\alpha},(\vec{\tau_{A}})T\equiv(\vec{\tau_{B}})T\vdash^{\prime}\tau_{1}\equiv\tau_{2}$

$\vec{\alpha},\tau_{A_{1}}\equiv\tau_{B_{1}},\tau_{A_{2}}\equiv\tau_{B_{2}}\vdash^{\prime}\tau_{1}\equiv\tau_{2}$
$\vec{\alpha},\tau_{A_{1}}*\tau_{A_{2}}\equiv\tau_{B_{1}}*\tau_{B_{2}}\vdash^{\prime}\tau_{1}\equiv\tau_{2}$

Let’s analyze the tuple example first.

To get the desired equation we can just apply the inductive hypothesis, so it
suffices that we show
$\Psi(\vec{\alpha},\tau_{A_{1}}\equiv\tau_{B_{1}},\tau_{A_{2}}\equiv\tau_{B_{2}},\Theta,\Gamma)$.

From our assumptions, we have
$\Psi(\vec{\alpha},\tau_{A_{1}}*\tau_{A_{2}}\equiv\tau_{B_{1}}*\tau_{B_{2}};\Theta;\Gamma)$.
Unpacking the definition of $\Psi$, we know that
$\Gamma\vdash\mathcal{T}(\tau_{A_{1}}*\tau_{A_{2}},\Theta)=:=\mathcal{T}(\tau_{B_{1}}*\tau_{B_{2}},\Theta)$.
Let’s introduce shorthands for the tuple types:

$U_{1}\triangleq\mathcal{T}(\tau_{A_{1}}*\tau_{A_{2}},\Theta)$
$U_{2}\triangleq\mathcal{T}(\tau_{B_{1}}*\tau_{B_{2}},\Theta)$

Unfolding $\mathcal{T}$, we get

$U_{1}=\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{A_{1}},\Theta)\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{A_{2}},\Theta)\\}$
$U_{2}=\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{B_{1}},\Theta)\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{B_{2}},\Theta)\\}$

We will want to use Typ-$<:$-Typ-Inv1 and Typ-$<:$-Typ-Inv2 to get
$\Gamma\vdash\mathcal{T}(\tau_{A_{1}},\Theta)=:=\mathcal{T}(\tau_{B_{1}},\Theta)$.
However, we cannot do this straight away, as the lib.Tuple is not acceptable
in the $\searrow$ judgment. Instead, let’s use the judgment
$\Gamma\vdash\texttt{lib.Tuple}=:=\mathit{TupleDef}$ where $\mathit{TupleDef}$
stands for the tuple type definition $\mu(\ldots)$ found in lib. By A.1, we
can replace the reference with the expanded definition to get
$U^{\prime}_{1}=\mathit{TupleDef}\wedge\\{T_{1}=\mathcal{T}(\tau_{B_{1}},\Theta)\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{B_{2}},\Theta)\\}$
with an equation $\Gamma\vdash U^{\prime}_{1}=:=U_{1}$, and analogously for
$U^{\prime}_{2}$. Now it suffices to show $\Gamma\vdash
U^{\prime}_{1}=:=U^{\prime}_{2}$ and through the helper equations and
transitivity we will get the desired equation. Because
$\mathit{TupleDef}=\mu(\ldots)$, we can now derive
$U^{\prime}_{1}\searrow\\{T_{1}=\mathcal{T}(\tau_{A_{1}},\Theta)\\}$ and
analogously
$U^{\prime}_{2}\searrow\\{T_{1}=\mathcal{T}(\tau_{B_{1}},\Theta)\\}$, thus
using the inversion rules we get
$\Gamma\vdash\mathcal{T}(\tau_{A_{1}},\Theta)=:=\mathcal{T}(\tau_{B_{1}},\Theta)$.
We have shown that indeed $\Gamma$ with $\Theta$ satisfies the equation
$\tau_{A_{1}}\equiv\tau_{B_{1}}$252525A mechanized version of this part of the
proof (inverting the tuple equality) is attached with the paper. See
translation/DestructTupleLemma.v.. We show $\tau_{A_{2}}\equiv\tau_{B_{2}}$
completely analogously.

The case for GADTs is also analogous — we have an equality
$\mathrm{env}.T\wedge\\{A1=\mathcal{T}(\tau_{A_{1}},\Theta)\\}\wedge\ldots=:=\mathrm{env}.T\wedge\\{A1=\mathcal{T}(\tau_{B_{1}},\Theta)\\}\wedge\ldots$
and using the same technique we invert it to get
$\mathcal{T}(\tau_{A_{1}},\Theta)=:=\mathcal{T}(\tau_{B_{1}},\Theta)$ and the
analogous for all other pairs of corresponding type parameters. This way, we
show $\Psi(\vec{\alpha},\vec{\tau_{A}}\equiv\vec{\tau_{B}};\Theta;\Gamma)$,
which (as above) gives us the desired equation by the inductive hypothesis. ∎

See 5.7

###### Proof.

We prove the theorem by induction on the derivation of the typing judgment.

  * –

(ty-unit) We get
$\Gamma\vdash\mathrm{lib}.\texttt{unit}:\mathrm{lib}.\texttt{Unit}$ by
weakening and from the trivial conclusion that
$\Gamma\vdash\mathrm{lib}:\\{\texttt{unit}:\mathrm{lib}.\texttt{Unit}\\}$
because $\Gamma$ is defined to contain the bindings of $\mathcal{S}(\Sigma)$.

  * –

(ty-var) From the assumption we know that $\Pi(\mathit{xf})=\tau$, since
$\mathcal{E}(\mathit{xf},\Theta)=\Theta(\mathit{xf})$, we get the result from
$\Phi(\Delta;\Pi;\Theta;\Gamma)$.

  * –

(ty-tup) Let’s introduce aliases for shortening the notation:

$\mathit{tupleApp}\triangleq\texttt{lib.tuple}\;\nu(\\{T_{1}=\mathcal{T}(\tau_{1},\Theta);T_{2}=\mathcal{T}(\tau_{2},\Theta)\\})\;x_{1}\;x_{2}$
$\mathit{tupleTyp}\triangleq\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{1},\Theta)\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{2},\Theta)\\}$

We want to prove that

$\Gamma\vdash\textbf{let }x_{1}\,=\,\mathcal{E}(e_{1},\Theta)\textbf{ in
}\textbf{let }x_{2}\,=\,\mathcal{E}(e_{2},\Theta)\textbf{ in
}\mathit{tupleApp}:\mathit{tupleTyp}$

From the inductive hypotheses we have
$\Gamma\vdash\mathcal{E}(e_{1},\Theta):\mathcal{T}(\tau_{1},\Theta)$ and
analogously for $e_{2}$ with $\tau_{2}$. Let’s define

$\Gamma^{\prime}\triangleq\Gamma,x_{1}:\mathcal{T}(\tau_{1},\Theta),x_{2}:\mathcal{T}(\tau_{2},\Theta)$

We can use the Let rule to get to
$\Gamma^{\prime}\vdash\mathit{tupleApp}:\mathit{tupleTyp}$. There we can just
use the standard application rules and the definition of lib.tuple.

  * –

(ty-fst) We need to prove that $\Gamma\vdash\textbf{let
}x\,=\,\mathcal{E}(e,\Theta)\textbf{ in
}x.\mathit{fst}:\mathcal{T}(\tau_{1},\Theta)$. From the inductive hypothesis,
we have
$\Gamma\vdash\mathcal{E}(e,\Theta):\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{1},\Theta)\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{2},\Theta)\\}$,
we apply the Let rule and then we can derive262626 In short, from
$x:\texttt{lib.Tuple}$ we get $x:\\{\mathit{fst}:x.T_{1}\\}$ and then from
$x:\\{T_{1}=\mathcal{T}(\tau_{1},\Theta)\\}$ we get
$x.T_{1}<:\mathcal{T}(\tau_{1},\Theta)$ allowing us to derive the conclusion.
$\Gamma,x:\ldots\vdash x:\\{\mathit{fst}:\mathcal{T}(\tau_{1},\Theta)\\}$ to
get the desired result.

  * –

(ty-snd) Analogously as above.

  * –

(ty-lam) Let’s allocate a fresh $x_{0}\notin\text{dom}(\Gamma)$. We can easily
show that since $\Phi(\Delta;\Pi;\Theta;\Gamma)$, then also
$\Phi(\Delta;\Pi,x:\tau_{1};\Theta[x\mapsto
x_{0}];\Gamma,x_{0}:\mathcal{T}(\tau_{1},\Theta))$. This allows us to get from
the inductive hypothesis that

$\Gamma,x_{0}:\mathcal{T}(\tau_{1},\Theta)\vdash\mathcal{E}(e,\Theta[x\mapsto
x_{0}]):\mathcal{T}(\tau_{2},(\Theta[x\mapsto x_{0}]))$

Then, with the All-I rule we prove that

$\Gamma\vdash\lambda(x_{0}:\mathcal{T}(\tau_{1},\Theta))\,\mathcal{E}(e,\Theta[x\mapsto
x_{0}]):\forall(x_{0}:\mathcal{T}(\tau_{1},\Theta))\,\mathcal{T}(\tau_{2},\Theta)$

  * –

(ty-app) From the inductive hypotheses we have (we pick a fresh $x_{0}$ and
$\alpha$-rename the type properly):

$\Gamma\vdash\mathcal{E}(e_{1},\Theta):\forall(x_{0}:\mathcal{T}(\tau_{1},\Theta))\mathcal{T}(\tau_{2},\Theta)$

and

$\Gamma\vdash\mathcal{E}(e_{2},\Theta):\mathcal{T}(\tau_{1},\Theta)$

We can then use the Let rule twice to get from the goal of

$\Gamma\vdash\textbf{let }x_{1}\,=\,\mathcal{E}(e_{1},\Theta)\textbf{ in
}\textbf{let }x_{2}\,=\,\mathcal{E}(e_{2},\Theta)\textbf{ in
}x_{1}\;x_{2}:\mathcal{T}(\tau_{2},\Theta)$

to

$\Gamma,x_{1}:\forall(x_{0}:\mathcal{T}(\tau_{1},\Theta))\mathcal{T}(\tau_{2},\Theta),x_{2}:\mathcal{T}(\tau_{1},\Theta)\vdash
x_{1}\;x_{2}:\mathcal{T}(\tau_{2},\Theta)$

and finish with All-E by noticing that
$\mathcal{T}(\tau_{2},\Theta)[x_{2}/x_{0}]=\mathcal{T}(\tau_{2},\Theta)$,
because from construction
$x_{0}\notin\text{fv}(\mathcal{T}(\tau_{2},\Theta))$.

  * –

(ty-tlam) We need to show

$\Gamma\vdash\mathcal{E}(\Lambda\alpha.e,\Theta):\mathcal{T}(\forall\alpha.\tau,\Theta)$

Unfolding the encoding (assuming that $x_{\alpha}$ is some fresh name) that
is:

$\Gamma\vdash\lambda(x_{\alpha}:\\{T:\bot..\top\\})\,\mathcal{E}(e,\Theta[\alpha\mapsto
x_{\alpha}.T]):\forall(x_{\alpha}:\\{T:\bot..\top\\})\,\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha}.T])$

Since we have $\Phi(\Delta;\Pi;\Theta;\Gamma)$ then clearly we also have

$\Phi(\Delta,\alpha;\Pi;\Theta[\alpha\mapsto
x_{\alpha}.T];\Gamma,x_{\alpha}:\\{T:\bot..\top\\})$

Thus from the inductive hypothesis, we get

$\Gamma,x_{\alpha}:\\{T:\bot..\top\\}\vdash\mathcal{E}(e,\Theta[\alpha\mapsto
x_{\alpha}.T]):\mathcal{T}(\tau,\Theta[\alpha\mapsto x_{\alpha}.T])$

Clearly, $x_{\alpha}\notin\text{fv}(\\{T:\bot..\top\\})$. Thus we can use the
All-I rule to get what we needed:

$\Gamma\vdash\lambda(x_{\alpha}:\\{T:\bot..\top\\})\,\mathcal{E}(e,\Theta[\alpha\mapsto
x_{\alpha}.T]):\forall(x_{\alpha}:\\{T:\bot..\top\\})\,\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha}.T])$

  * –

(ty-tapp) We want to show that

$\Gamma\vdash\mathcal{E}(e[\tau_{1}],\Theta):\mathcal{T}(\tau[\alpha\mapsto\tau_{1}],\Theta)$

Unfolding the $\mathcal{E}$, that is

$\Gamma\vdash\textbf{let }x_{1}\,=\,\mathcal{E}(e,\Theta)\textbf{ in
}\textbf{let }tl\,=\,\nu(\\_:\\{T=\mathcal{T}(\tau_{1},\Theta)\\})\textbf{ in
}x_{1}\;tl:\mathcal{T}(\tau[\alpha\mapsto\tau_{1}],\Theta)$

From the inductive hypothesis we know that, for some fresh $x_{\alpha}$:

$\Gamma\vdash\mathcal{E}(e,\Theta):\forall(x_{\alpha}:\\{T:\bot..\top\\})\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha}.T])$

Thus by applying the Let rule twice272727We also use {}-I and a trivial
instantiation Rec-E to typecheck $tl$, but it’s completely standard.. Let’s
define

$\Gamma^{\prime}\triangleq\Gamma,x_{1}:\forall(x_{\alpha}:\\{T:\bot..\top\\})\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha}.T]),tl:\\{T=\mathcal{T}(\tau_{1},\Theta)\\}$

We can then transform our goal into

$\Gamma^{\prime}\vdash
x_{1}\;tl:\mathcal{T}(\tau[\alpha\mapsto\tau_{1}],\Theta)$

We can use Sub with Typ-<:-Typ to get $\Gamma^{\prime}\vdash
tl:\\{T:\bot..\top\\}$. Thus, we can use the All-E rule to get

$\Gamma^{\prime}\vdash x_{1}\;tl:\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha}.T])[tl/x_{\alpha}]$

Now, knowing that $\Gamma^{\prime}\vdash tl.T=:=\mathcal{T}(\tau_{1},\Theta)$,
we need to use A.3 (proven just below) to get

$\Gamma^{\prime}\vdash\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha}.T])[tl/x_{\alpha}]=:=\mathcal{T}(\tau[\alpha\mapsto\tau_{1}],\Theta)$

With that we can conclude by using the Sub rule and replacing the type we have
with the desired type.

  * –

(ty-fix) We want to prove

$\displaystyle\Gamma\vdash\,$ $\displaystyle\textbf{let
}h\,=\,\nu[lib.Any](\mathit{self}:\\{\mathit{fix}=\lambda(x:\texttt{lib.Unit})\;\mathcal{E}(e,\Theta[f\mapsto\mathit{self}.\mathit{fix}\;\texttt{lib.unit}])\\})\textbf{
in }$ $\displaystyle\quad
h.\mathit{fix}\;\texttt{lib.unit}:\mathcal{T}(\tau,\Theta)$

Let’s define

$\Gamma^{\prime}\triangleq\Gamma,\mathit{self}:\mu(\mathit{self}:\\{\mathit{fix}:\forall(x:\texttt{lib.Unit})\mathcal{T}(\tau,\Theta)\\})$

First, we show that
$\Phi(\Delta;\Pi,f:\tau;\Gamma^{\prime};\Theta[f\mapsto\mathit{self}.\mathit{fix}\;\texttt{lib.unit}])$.
This goes easily by Rec-E, Fld-E and All-E.

This allows us to use the inductive hypothesis to get

$\Gamma^{\prime}\vdash\mathcal{E}(e,\Theta[f\mapsto\mathit{self}.\mathit{fix}\;\texttt{lib.unit}]):\mathcal{T}(\tau,\Theta)$

This allows us to typecheck the $\nu$ in $h$ as
$\mu(\mathit{self}:\\{\mathit{fix}:\forall(x:\texttt{lib.Unit})\mathcal{T}(\tau,\Theta)\\})$
(we also need to show that $\mathit{self}$ types to lib.Any, but that is
trivial since $\texttt{lib.Any}<:\top$).

Then we proceed with the Let rule followed by Rec-E, which transforms our $h$
to have type
$\\{\mathit{fix}:\forall(x:\texttt{lib.Unit})\mathcal{T}(\tau,\Theta)\\}$ and
then we can easily finish by All-E.

  * –

(ty-let) Follows directly by the Let rule. Clearly
$\Theta_{x}(x)\notin\text{fv}(\mathcal{T}(\tau_{1},\Theta))$ as
$\lambda_{2,G\mu}$ does not allow variable references in types.

  * –

(ty-eq) From the inductive hypothesis we have
$\Gamma\vdash\mathcal{E}(e,\Theta):\mathcal{T}(\tau_{1},\Theta)$. We also know
that $\Delta\vDash\tau_{1}\equiv\tau_{2}$, so by 5.8, we have
$\Gamma\vdash\mathcal{T}(\tau_{1},\Theta)=:=\mathcal{T}(\tau_{2},\Theta)$,
thus by Sub we get the desired result.

  * –

(ty-cons) To avoid getting lost in identifier names, let’s rewrite the rule to
the following:

$\Sigma(c_{i})=\forall\vec{\alpha}.\tau_{A}\to\tau_{B}$
$\Delta\vdash\vec{\tau}:\vec{*}$ $\Delta;\Pi\vdash
e:\tau_{A}[\vec{\alpha}\mapsto\vec{\tau}]$ (ty-cons) $\Delta;\Pi\vdash
c_{i}[\vec{\tau}](e):\tau_{B}[\vec{\alpha}\mapsto\vec{\tau}]$

and let $\vec{\tau}\triangleq(\tau_{1},...,\tau_{m})$,
$\vec{\alpha}\triangleq(\alpha_{1},...,\alpha_{m})$.

We need to prove that

$\displaystyle\Gamma\vdash\,$ $\displaystyle\textbf{let
}ts\,=\,\nu(ts:\\{B_{i,1}=\mathcal{T}(\tau_{1},\Theta);...\\})\textbf{ in }$
$\displaystyle\textbf{let }x\,=\,\mathcal{E}(e,\Theta)\textbf{ in }$
$\displaystyle\textbf{let }tmp\,=\,\mathrm{env}.c_{i}\;ts\textbf{ in }tmp\;x$
$\displaystyle:\mathcal{T}(\tau_{B}[\vec{\alpha}\mapsto\vec{\tau}],\Theta)$

From the assumption about $\Sigma(c_{i})$ we know that $\mathrm{env}.c_{i}$
has the type:

$\forall(ts:\\{B_{i,1}=\mathcal{T}(\tau_{1},\Theta);...\\})\;\forall(v:\mathcal{T}(\tau_{A},\theta^{(ts)}_{\vec{\alpha}}))\;\mathcal{T}(\tau_{B},\theta^{(ts)}_{\vec{\alpha}})$

where $\theta^{(ts)}_{\vec{\alpha}}$ is defined as before.

First we prove the typing of $ts$ by applying {}-I and then numerously
applying Def-Typ. From the inductive hypothesis we get
$\Gamma\vdash\mathcal{E}(e,\Theta):\mathcal{T}(\tau_{A}[\vec{\alpha}\mapsto\vec{\tau}])$,
so also $x$ will have that type.

Now we will use Let and All-E twice to finish the derivation.

First, we can type $tmp$ as
$(\forall(v:\mathcal{T}(\tau_{A},\theta^{(ts)}_{\vec{\alpha}}))\;\mathcal{T}(\tau_{B},\theta^{(ts)}_{\vec{\alpha}}))[ts\mapsto
ts]$.

Because $\tau_{A}$ and $\tau_{B}$ should not have any free variables apart
from $\vec{\alpha}$, we can type $tmp$ as
$(\forall(v:\mathcal{T}(\tau_{A},\Theta\cup\theta^{(ts)}_{\vec{\alpha}}))\;\mathcal{T}(\tau_{B},\Theta\cup\theta^{(ts)}_{\vec{\alpha}}))[ts\mapsto
ts]$.

Let $\Gamma^{\prime}$ be the context $\Gamma$ extended with $ts$, $x$ and
$tmp$ with types as shown above. We have $\Gamma^{\prime}\vdash
ts.{B_{i,j}}=:=\mathcal{T}(\tau_{j},\Theta)$. Thus, we can use the A.3
repeatedly to get

$\Gamma^{\prime}\vdash\mathcal{T}(\tau_{A},\Theta\cup\theta^{(ts)}_{\vec{\alpha}})[ts\mapsto
ts]=:=\mathcal{T}(\tau_{A}[\vec{\alpha}\mapsto\vec{\tau}],\Theta)$

and the same for $\tau_{B}$. Thus, using the Sub rule, we show that indeed the
argument $x$ fits the expected type in $tmp$ and the return type of the
application $tmp\;x$ can indeed be coerced to what we wanted in the first
place.

  * –

(ty-case) We need to typecheck the following term:

$\displaystyle\textbf{let
}tl\,=\,\nu(tl:\\{R=\mathcal{T}(\tau_{2},\Theta)\\})\textbf{ in }$
$\displaystyle\textbf{let }v\,=\,\mathcal{E}(e,\Theta)\textbf{ in }$
$\displaystyle\textbf{let
}case_{c_{1}}\,=\,(\lambda(arg_{1}:\mathrm{env}.T_{c_{1}}\wedge v.type)$
$\displaystyle\quad\quad\quad\textbf{let
}x_{1}\,=\,arg_{1}.\mathrm{data}\textbf{ in }$
$\displaystyle\quad\quad\quad\mathcal{E}(e_{1},\Theta[\beta_{1,1}\mapsto
arg.B_{1,1},...])$ $\displaystyle)\textbf{ in }$ $\displaystyle...$
$\displaystyle v.\mathrm{pmatch}{}\;tl\;case_{c_{1}}\;...\;case_{c_{n}}$

as having type $\mathcal{T}(\tau_{2},\Theta)$.

The last application is a series of multiple applications so technically, it
should be replaced with a stack of let bindings with temporary names for
intermediate step — we skip that this time for clarity, as the application
itself is pretty routine.

From the inductive hypothesis we get that
$\Gamma\vdash\mathcal{E}(e,\Theta):\mathcal{T}(\tau_{1},\Theta)$.

From the restrictions placed on our variant of the calculus, we know that all
pattern matching is only performed on GADTs, so
$\tau_{1}=(\delta_{1},\dots,\delta_{m})T$ for some types $\vec{\delta}$ and
some GADT name $T$. Thus, we have
$\Gamma\vdash\mathcal{E}(e,\Theta):\mathrm{env}.T\wedge\\{A_{1}=\mathcal{T}(\delta_{1},\Theta)\\}\wedge\ldots$.

From that and through routine usage of Let we have
$v:\mathrm{env}.T\wedge\\{A_{1}=\mathcal{T}(\delta_{1},\Theta)\\}\wedge\ldots$.
Thus, $v.pmatch$ has type
$\forall(r:\\{R:\bot..\top\\})\forall(case_{c_{1}}:\forall(arg:\mathrm{env}.T_{c_{1}}\wedge
s.type)r.R)\ldots r.R$. So by rather standard application of All-E we will
have

$v.pmatch\;tl:\forall(case_{c_{1}}:\forall(arg:\mathrm{env}.T_{c_{1}}\wedge
s.type)tl.R)\ldots tl.R$

Thus, by continuously using All-E, assuming that each $case_{c_{i}}$ has the
expected type (we will show that in a moment), we get that the whole
application types to $tl.R$. Since we have
$tl.R=:=\mathcal{T}(\tau_{2},\Theta)$ by the Sel rules, we get exactly what we
needed.

Now we just need to verify that for each branch, the generated lambda has the
correct type.

Let’s consider the branch $i$. From the assumptions of ty-case, we have
$\Delta;\Pi\vdash(p_{i}\Rightarrow e_{i}):(\tau_{1}\Rightarrow\tau_{2})$ which
means in particular that $\Delta\vdash
p\downarrow\tau_{1}\Rightarrow(\Delta^{\prime},\Pi^{\prime})$ and that
$\Delta,\Delta^{\prime};\Pi,\Pi^{\prime}\vdash e_{i}:\tau_{2}$. From the
restrictions, we know that $p_{i}$ must have the form
$c_{i}[\beta_{i,1},\ldots,\beta_{i,m_{i}}](x_{i})$ and so that the first
judgment must have been derived by pat-cons’.

From that, we get
$\Sigma(c_{i})=\forall\vec{\beta_{i}}.\tau_{C}\to(\sigma_{i,1},\ldots,\sigma_{i,m_{i}})T$.
Note that the $\sigma_{i,j}$ here are the same as in the definition of
$\mathrm{env}.T_{c_{i}}$, this will be important in a moment. More
importantly, because we were matching type $(\vec{\delta})T$, we know that
$\Delta^{\prime}=\vec{\beta_{i}},\vec{\sigma_{i}}\equiv\vec{\delta}$ and
$\Pi^{\prime}=x_{i}:\tau_{C}$. Thus the second judgment has form
$\Delta,\vec{\beta_{i}},\vec{\sigma_{i}}\equiv\vec{\delta};\Pi,x_{i}:\tau_{C}\vdash
e_{i}:\tau_{2}$.

We want to show that

$\lambda(arg_{i}:\mathrm{env}.T_{c_{i}}\wedge v.type)\;\;\textbf{let
}x^{\prime}_{i}\,=\,arg_{i}.data\textbf{ in
}\mathcal{E}(e_{i},\Theta[x_{i}\mapsto x^{\prime}_{i},\beta_{i,1}\mapsto
arg.B_{i,1},\ldots])$

types to $\mathcal{T}(\tau_{2},\Theta)$. We can apply All-I followed by Let,
knowing that $arg_{i}.data:\mathcal{T}(\tau_{C},\hat{\Theta})$ where

$\hat{\Theta}\triangleq[\beta_{i,1}\mapsto arg_{i}.B_{i,1},...]$

to get to the goal282828Technically in the meantime our environment
accumulated some more identifiers, for example earlier case branch definitions
are visible in the latter ones - we can ignore them though because independent
branches do not rely on them and can be typechecked without them, and then add
them using the weakening lemma.

$\Gamma^{\prime}\vdash\mathcal{E}(e_{i},\Theta^{\prime}):\mathcal{T}(\tau_{2},\Theta)$

where

$\Gamma^{\prime}\triangleq\Gamma,v:\mathrm{env}.T\wedge\\{A_{1}=\mathcal{T}(\delta_{1},\Theta)\\}\wedge\ldots,arg_{i}:\mathrm{env}.T_{c_{i}}\wedge
v.type,x^{\prime}_{i}:\mathcal{T}(\tau_{C},\hat{\Theta})$
$\Theta^{\prime}\triangleq\Theta[x_{i}\mapsto
x^{\prime}_{i},\beta_{i,1}\mapsto arg.B_{i,1},\ldots]$

Now, as long as we can ensure that
$\Phi(\Delta,\vec{\beta_{i}},\vec{\sigma_{i}}\equiv\vec{\delta};\Pi,x_{i}:\tau_{C};\Theta^{\prime};\Gamma^{\prime})$
we can finish by applying the inductive hypothesis from the assumption

$\Delta,\vec{\beta_{i}},\vec{\sigma_{i}}\equiv\vec{\delta};\Pi,x_{i}:\tau_{C}\vdash
e_{i}:\tau_{2}$

giving us

$\Gamma^{\prime}\vdash\mathcal{E}(e_{i},\Theta^{\prime}):\mathcal{T}(\tau_{2},\Theta^{\prime})$

Trivially,
$\mathcal{T}(\tau_{2},\Theta^{\prime})=\mathcal{T}(\tau_{2},\Theta)$, because
we can assume all the added identifiers $\beta_{i,j}$ are fresh in $\tau_{2}$.

So now we just need to show
$\Phi(\Delta,\vec{\beta_{i}},\vec{\sigma_{i}}\equiv\vec{\delta};\Pi,x_{i}:\tau_{C};\Theta^{\prime};\Gamma^{\prime})$
to finish the proof.

We already know that $\Phi(\Delta;\Pi;\Theta;\Gamma)$. What remains to be
shown is that the conditions of $\Phi$ hold for the added parts:

    * –

For each $\beta_{i,j}$ we know that
$\Theta^{\prime}(\beta_{i,j})=arg_{i}.B_{i,j}$ and since
$arg_{i}:\mathrm{env}.T_{c_{i}}$, we can get292929We do this based on the
definition of $\mathrm{env}.T_{c_{i}}$ in $\Gamma^{\prime}$; we need to use
Rec-E and Andi-¡: to get there. $arg_{i}:\\{B_{i,j}:\bot..\top\\}$.

    * –

We need to show that
$\Gamma^{\prime}\vdash\Theta^{\prime}(x_{i}):\mathcal{T}(\tau_{C},\Theta^{\prime})$
which is equivalent to $\Gamma^{\prime}\vdash
x^{\prime}_{i}:\mathcal{T}(\tau_{C},\Theta^{\prime})$ but since
$\mathcal{T}(\tau_{C},\Theta^{\prime})=\mathcal{T}(\tau_{C},\hat{\Theta})$303030Because
$\text{fv}(\tau_{C})=\\{\beta_{i,1},...,\beta_{i,m_{i}}\\}$ and for each $j$,
$\Theta^{\prime}(\beta_{i,j})=\hat{\Theta}(\beta_{i,j})$., it follows directly
from Var.

    * –

For each $\sigma_{i,j}\equiv\delta_{j}$, we need to show that
$\Gamma^{\prime}\vdash\mathcal{T}(\sigma_{i,j},\Theta^{\prime})=:=\mathcal{T}(\delta_{j},\Theta^{\prime})$.
For the same reason as previously,
$\mathcal{T}(\sigma_{i,j},\Theta^{\prime})=\mathcal{T}(\sigma_{i,j},\hat{\Theta})$.
Now, because $arg_{i}:\mathrm{env}.T_{c_{i}}$, we have
$arg_{i}:\\{A_{j}=\mathcal{T}(\sigma_{i,j},\hat{\Theta})\\}$. We also have
already mentioned that $v:\\{A_{j}=\mathcal{T}(\delta_{j},\Theta)\\}$. With
that, we can prove the desired equality:

$\mathcal{T}(\sigma_{i,j},\Theta^{\prime})=\mathcal{T}(\sigma_{i,j},\hat{\Theta})=:=arg_{i}.A_{j}=:=v.A_{j}=:=\mathcal{T}(\delta_{j},\Theta)$

The two outer equalities rely on the Sel rules and the inner equality is
derived by the two Sngl rules, because we have $arg_{i}:v.type$.

∎

###### Lemma A.3 (Substitution through translation).

For every $\Delta$, $\alpha$, $\tau_{1}$ and $\tau_{2}$, if
$\Delta\vdash\tau_{1}:*$ and $\Delta,\alpha\vdash\tau_{2}:*$, then for every
$\Gamma$ and $\Theta$ such that $\Psi(\Delta;\Theta;\Gamma)$, if $\Gamma\vdash
a.T=:=\mathcal{T}(\tau_{1},\Theta)$ for some $a$, then for every fresh
$x_{\alpha}$, we have $\Gamma\vdash\mathcal{T}(\tau_{2},\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]=:=\mathcal{T}(\tau_{2}[\alpha\mapsto\tau_{1}],\Theta)$.

###### Proof.

The proof goes by induction on the structure of $\tau_{2}$.

  * –

$\tau_{2}=\mathbf{1}$: the equality stems trivially from the Refl rule,
because $\mathcal{T}(\mathbf{1},\ldots)=\texttt{lib.Unit}$, so both sides are
syntactically equal.

  * –

$\tau_{2}=\tau_{A}*\tau_{B}$: from the inductive hypotheses we have
$\Gamma\vdash\mathcal{T}(\tau_{A},\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]=:=\mathcal{T}(\tau_{A}[\alpha\mapsto\tau_{1}],\Theta)$
and the same for $\tau_{B}$.

We can transform both sides of the equation:

$\displaystyle\mathcal{T}(\tau_{A}*\tau_{B},\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]=$
$\displaystyle\quad\quad(\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{A},\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{B},\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]\\})$
$\displaystyle\mathcal{T}((\tau_{A}*\tau_{B})[\alpha\mapsto\tau_{1}],\Theta)=$
$\displaystyle\quad\quad\mathcal{T}(\tau_{A}[\alpha\mapsto\tau_{1}]*\tau_{B}[\alpha\mapsto\tau_{1}],\Theta)=$
$\displaystyle\quad\quad\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{A}[\alpha\mapsto\tau_{1}],\Theta)\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{B}[\alpha\mapsto\tau_{1}],\Theta)\\}$

By using the rules Typ-<:-Typ, from the inductive hypotheses we get

$\Gamma\vdash\\{T_{1}=\mathcal{T}(\tau_{A}[\alpha\mapsto\tau_{1}],\Theta)\\}=:=\\{T_{1}=\mathcal{T}(\tau_{A},\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]\\}$

and the same for $\tau_{B}$, then by A.1 (applied twice), we get the desired
result.

  * –

The case $\tau_{2}=(\vec{\tau})T$ goes analogously as for the tuples - we get
inductive hypotheses for each type in $\vec{\tau}$, we can push the
substitution down the structure and get the final equality by applying A.1
enough times.

  * –

$\tau_{2}=\tau_{A}\to\tau_{B}$ goes also analogously as above, but instead we
use the All-<:-All rule together with weakening.

  * –

$\tau_{2}=\forall\alpha^{\prime}.\tau$: We can unfold the lhs:

$\mathcal{T}(\forall\alpha^{\prime}.\tau,\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]=\forall(x_{\alpha^{\prime}}:\\{T:\bot..\top\\})\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha}.T,\alpha^{\prime}\mapsto x_{\alpha^{\prime}}.T])[a/x_{\alpha}]$

where $x_{\alpha^{\prime}}$ is some fresh identifier. Let’s consider two
cases:

    * –

$\alpha^{\prime}=\alpha$: In this case the lhs further simplifies313131 We can
get rid of the $[a/x_{\alpha}]$ substitution at the end, because if the
$\mapsto x_{\alpha}.T$ disappeared, then from the freshness of $x_{\alpha}$
for $\Theta$, we know that this substitution will act as identity. to
$\forall(x_{\alpha^{\prime}}:\\{T:\bot..\top\\})\mathcal{T}(\tau,\Theta[\alpha\mapsto
x_{\alpha^{\prime}}.T])$.

The rhs can be unfolded323232Again, we are free to remove the substitution
$[\alpha\mapsto\tau_{1}]$ inside of $\mathcal{T}$, because the name is aliased
by the same name in $\forall\alpha$. to
$\mathcal{T}(\forall\alpha.\tau,\Theta)$, and from the definition of
$\mathcal{T}$, this is exactly the same as the transformed lhs.

    * –

$\alpha^{\prime}\not=\alpha$:

In the rhs we can push the substitution deeper:

$\mathcal{T}((\forall\alpha^{\prime}.\tau)[\alpha\mapsto\tau_{1}],\Theta)=\mathcal{T}(\forall\alpha^{\prime}.(\tau[\alpha\mapsto\tau_{1}]),\Theta)=\forall(x_{\alpha^{\prime}}:\\{T:\bot..\top\\})\mathcal{T}(\tau[\alpha\mapsto\tau_{1}],\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T])$

We can reorder the substitution in the lhs to get:

$\forall(x_{\alpha^{\prime}}:\\{T:\bot..\top\\})\mathcal{T}(\tau,\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T,\alpha\mapsto x_{\alpha}.T])[a/x_{\alpha}]$

After applying the All-<:-All rule to get the subtyping in both directions, it
suffices to prove

$\Gamma,x_{\alpha^{\prime}}:\\{T:\bot..\top\\}\vdash\mathcal{T}(\tau[\alpha\mapsto\tau_{1}],\Theta^{\prime})=:=\mathcal{T}(\tau,\Theta^{\prime}[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]$

where

$\Theta^{\prime}\triangleq\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T]$

Clearly,
$\Psi(\Delta,\alpha^{\prime};\Theta^{\prime};\Gamma,x_{\alpha^{\prime}}:\\{T:\bot..\top\\})$
so we get the desired equality by the inductive hypothesis.

  * –

Finally, $\tau_{2}=\alpha^{\prime}$. Let’s consider two cases:

    * –

$\alpha^{\prime}=\alpha$: The lhs is $\mathcal{T}(\alpha,\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]=(x_{\alpha}.T)[a/x_{\alpha}]=a.T$ and the rhs is
$\mathcal{T}(\alpha[\alpha\mapsto\tau_{1}],\Theta)=\mathcal{T}(\tau_{1},\Theta)$,
so we just use the assumption $\Gamma\vdash
a.T=:=\mathcal{T}(\tau_{1},\Theta)$.

    * –

$\alpha^{\prime}\not=\alpha$: The lhs is
$\mathcal{T}(\alpha^{\prime},\Theta[\alpha\mapsto
x_{\alpha}.T])[a/x_{\alpha}]=\Theta(\alpha^{\prime})[a/x_{\alpha}]=\Theta(\alpha^{\prime})$
(we can do the last transformation, because we know that $x_{\alpha}$ was
fresh for $\Theta$). The rhs is
$\mathcal{T}(\alpha^{\prime}[\alpha\mapsto\tau_{1}],\Theta)=\Theta(\alpha^{\prime})$,
so both sides are equal: we get the type equality by Refl.

∎

###### Lemma A.4.

For any type $\tau$ and any substitutions $\Theta_{1}$ and $\Theta_{2}$, if
$\text{fv}(\tau)\subseteq\text{dom}(\Theta_{1})=\text{dom}(\Theta_{2})$ and
for every $x\in\text{dom}(\Theta_{1})$,
$\Gamma\vdash\Theta_{1}(x)=:=\Theta_{2}(x)$, then also
$\Gamma\vdash\mathcal{T}(\tau,\Theta_{1})=:=\mathcal{T}(\tau,\Theta_{2})$.

###### Proof.

Easy induction on the structure of $\tau$. The base case is for variables and
it goes directly from the assumption
$\Gamma\vdash\Theta_{1}(x)=:=\Theta_{2}(x)$. All the other cases are trivial
or can be handled by constructing equations on terms based on equations on the
sub-terms derived from the inductive hypotheses, in the same way as in A.3. ∎

###### Lemma A.5.

For any types $\tau_{A}$ and $\tau_{B}$, any variable $\alpha$, substitution
$\Theta$ and environment $\Gamma$, if
$\Gamma\vdash\Theta(\alpha)=:=\mathcal{T}(\tau_{A},\Theta)$ then
$\Gamma\vdash\mathcal{T}(\tau_{B},\Theta)=:=\mathcal{T}(\tau_{B}[\alpha\mapsto\tau_{A}],\Theta)$.

###### Proof.

Easy induction on the structure of $\tau_{B}$.

The base case for the variable $\alpha$ goes directly from the assumption
$\Gamma\vdash\Theta(\alpha)=:=\mathcal{T}(\tau_{A},\Theta)$. For any
$\alpha^{\prime}\not=\alpha$, we have
$\mathcal{T}(\alpha^{\prime},\Theta)=\mathcal{T}(\alpha^{\prime}[\alpha\mapsto\tau_{A}],\Theta)$,
so it goes by Refl.

All the other cases are trivial or can be handled by constructing equations on
terms based on equations on the sub-terms derived from the inductive
hypotheses, in the same way as in A.3.

For example in the case of tuples, i.e. if $\tau_{B}=\tau_{1}*\tau_{2}$, from
the inductive hypotheses we have

$\Gamma\vdash\mathcal{T}(\tau_{1},\Theta)=:=\mathcal{T}(\tau_{1}[\alpha\mapsto\tau_{A}],\Theta)$

and same for $\tau_{2}$, then

$\mathcal{T}(\tau_{1}*\tau_{2},\Theta)=\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{1},\Theta)\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{2},\Theta)\\}$

and

$\mathcal{T}(\tau_{1}[\alpha\mapsto\tau_{A}],\Theta)=\texttt{lib.Tuple}\wedge\\{T_{1}=\mathcal{T}(\tau_{1},\Theta)[\alpha\mapsto\tau_{A}]\\}\wedge\\{T_{2}=\mathcal{T}(\tau_{2},\Theta)[\alpha\mapsto\tau_{A}]\\}$

and so we construct the necessary equation using Typ-<:-Typ and A.1.

One more interesting case that may be worth showing is
$\tau_{B}=\forall\alpha^{\prime}.\tau$. Let’s see two cases:

  * –

if $\alpha=\alpha^{\prime}$, then
$(\forall\alpha.\tau)[\alpha\mapsto\tau_{A}]=\forall\alpha.\tau$ so the
equality follows trivially from Refl.

  * –

$\alpha\not=\alpha^{\prime}$, then

$\mathcal{T}(\forall\alpha^{\prime}.\tau,\Theta)=\forall(x_{\alpha^{\prime}}:\\{T:\bot..\top\\})\mathcal{T}(\tau,\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T])$

and

$\mathcal{T}((\forall\alpha^{\prime}.\tau)[\alpha\mapsto\tau_{A}],\Theta)=\mathcal{T}(\forall\alpha^{\prime}.(\tau[\alpha\mapsto\tau_{A}]),\Theta)=\forall(x_{\alpha^{\prime}}:\\{T:\bot..\top\\})\mathcal{T}(\tau[\alpha\mapsto\tau_{A}],\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T])$

Of course, if $\Gamma\vdash\Theta(\alpha)=:=\mathcal{T}(\tau_{A},\Theta)$,
then by weakening also

$\Gamma,x_{\alpha^{\prime}}:\\{T:\bot..\top\\}\vdash\Theta(\alpha)=:=\mathcal{T}(\tau_{A},\Theta)$

and because $\alpha^{\prime}$ is fresh for $\tau_{A}$,
$\mathcal{T}(\tau_{A},\Theta)=\mathcal{T}(\tau_{A},\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T])$ and $(\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T])(\alpha)=\Theta(\alpha)$, so from the inductive
hypothesis we get

$\Gamma,x_{\alpha^{\prime}}:\\{T:\bot..\top\\}\vdash\mathcal{T}(\tau,\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T])=:=\mathcal{T}(\tau[\alpha\mapsto\tau_{A}],\Theta[\alpha^{\prime}\mapsto
x_{\alpha^{\prime}}.T])$

Now we use All-<:-All to get the desired equation.

∎

Using the 5.7 together with A.2 we finally can prove that the result of
EncodeProgram is well-typed.

##  Appendix B Soundness Proof of pDOT

Rapoport and Lhoták introduces the seven-level stratified typing rules in the
soundness of pDOT.

$\displaystyle{\tiny\text{General }(\vdash)\rightarrow\text{Tight
}(\vdash_{\\#})\rightarrow{\text{{Introduction-$qp$
}}(\vdash_{qp})}\rightarrow\text{Introduction-$pq$
}(\vdash_{pq})\rightarrow{\text{Elim-III
}(\vdash_{e3})}\rightarrow{\text{Elim-II
}(\vdash_{e2})}\rightarrow\text{Elim-I }(\vdash_{e1})}$

These levels in pDOT are designed and organized to tackle two key problems in
the metatheory: bad bounds and cycles in typing derivations. We will explain
the two problems along with pDOT’s solutions to them one by one.

$\displaystyle\begin{array}[]{@{}c@{}}\text{inert }\forall(x\colon
T)\,U\end{array}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\text{record
}T\end{array}}{\begin{array}[]{@{}c@{}}\text{inert }\mu\left(x\colon
T\right)\end{array}}$

$\displaystyle\begin{array}[]{@{}c@{}}\text{record }\left\\{A\colon
T..T\right\\}\end{array}$

$\displaystyle\begin{array}[]{@{}c@{}}\text{record }\left\\{a\colon
q\mathsf{.type}\right\\}\end{array}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\text{inert
}T}\end{array}}{\begin{array}[]{@{}c@{}}\text{record }\left\\{a\colon
T\right\\}\end{array}}$

Figure 10. Inert Types

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T<:\top\end{array}$
(Top#)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}\bot<:T\end{array}$
(Bot#)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T<:T\end{array}$
(Refl#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}S<:T\quad\quad\Gamma\vdash_{\\#}T<:U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}S<:U\end{array}}$
(Trans#)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T\wedge
U<:T\end{array}$ (And1-$<:$#)

$\displaystyle\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T\wedge
U<:U\end{array}$ (And2-$<:$#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}S<:T\quad\quad\Gamma\vdash_{\\#}S<:U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}S<:T\wedge
U\end{array}}$ ($<:$-And#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Gamma\vdash_{e3}p\colon\left\\{A\colon
S..S\right\\}}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}S<:{p}.A\end{array}}$
($<:$-Sel#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Gamma\vdash_{e3}p\colon\left\\{A\colon
S..S\right\\}}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}{p}.A<:S\end{array}}$
(Sel-$<:$#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash_{e2}q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T<:{T}\left[\nicefrac{{q}}{{{p}}}\right]\end{array}}$
(Snglpq-$<:$#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon
q\mathsf{.type}\quad\quad\Gamma\vdash_{e2}q\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T<:{T}\left[\nicefrac{{p}}{{{q}}}\right]\end{array}}$
(Snglqp-$<:$#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T<:U\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}\left\\{a\colon
T\right\\}<:\left\\{a\colon U\right\\}\end{array}}$ (Fld-$<:$-Fld#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}S_{2}<:S_{1}\quad\quad\Gamma\vdash_{\\#}T_{1}<:T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}\left\\{A\colon
S_{1}..T_{1}\right\\}<:\left\\{A\colon S_{2}..T_{2}\right\\}\end{array}}$
(Typ-$<:$-Typ#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}S_{2}<:S_{1}\\\
\Gamma,\,x\colon S_{2}\vdash
T_{1}<:T_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}\forall(x\colon
S_{1})\,T_{1}<:\forall(x\colon S_{2})\,T_{2}\end{array}}$ (All-$<:$-All#)

Figure 11. Tight subtyping rules of pDOT(Rapoport and Lhoták, 2019) and cDOT.

##### Bad bounds.

In DOT calculi, users can introduce arbitary subtyping relations using type
members, and they can be unsound. For example:

$\lambda(x:\left\\{A\colon\top..\bot\right\\})t$

When typing the body of the above function, the absurd subtyping judgment
$\Gamma\vdash\top<:\bot$ is derivable in the environment. DOT calculi are
designed in a way that bad bounds will not break soundness. Specifically, when
evaluating the program, the type member $x.A$ will be instantiated with a
concrete type, serving as the proof of the subtyping relation implied by its
bounds. Therefore, in the above example, the body of the function will never
get executed because it is impossible to supply such a $x$. Tight typing are
proposed to deal with the bad bounds problem in the soundness proof. Its main
difference of it from general typing is that it forbids type members from
introducing custom subtyping relationships by modifying the $<:$-Sel and
Sel-$<:$ rules.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon\hbox{\pagecolor{newrule}$\displaystyle\left\\{A\colon
T..T\right\\}$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}T<:{p}.A\end{array}}$
($<:$-Sel-#)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash_{e3}p\colon\hbox{\pagecolor{newrule}$\displaystyle\left\\{A\colon
T..T\right\\}$}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash_{\\#}p.A<:T\end{array}}$
(Sel-$<:$-#)

The full formulation of tight subtyping rule is presented in Figure 11. In
such a way, in the tight typing level, subtyping relations can always be
trusted. But how can we transform general typing to the tight typing level?
pDOT introduces the notion of _inertness_. We can prove the following lemma,
which states that general typing can be transformed to the tight level without
loss of expressiveness in an inert environment.

###### Lemma B.1 ($\vdash$ to $\vdash_{\\#}$).

If $\Gamma$ is inert and $\Gamma\vdash t\colon T$, then
$\Gamma\vdash_{\\#}t\colon T$.

##### Cycles in typing derivation.

pDOT typing rules can result in cycles in typing derivation. For example, we
can apply Rec-I and Rec-E repeatedly in the derivation tree. And we can
similarly produce cycles with the Fld-I, Fld-E, Snglpq-<: and Snglqp-<: rules.
Such cycles hinders the inductive reasoning of typing judgments. pDOT deals
with the cycles by seperating each pair of the symmetric typing rules into
different levels. For instance, the Snglpq-<: and Snglqp-<: rules are inlined
in Introduction-$qp$ ($\vdash_{qp}$) Introduction-$pq$ ($\vdash_{pq}$) levels
respectively. Starting from the Introduction-$qp$ level, pDOT separates the
reasoning about values and paths. Therefore, we have two sets of typing rules,
one for the values and another for the paths on these levels. Transformation
lemmas are proven for them respectively.