# What’s Decidable about (Atomic) Polymorphism?
(Extended Version)

Paolo Pistone111Università di Bologna<EMAIL_ADDRESS>Luca
Tranchini222Eberhard Karls Universität Tübingen<EMAIL_ADDRESS>
###### Abstract

Due to the undecidability of most type-related properties of System F like
type inhabitation or type checking, restricted polymorphic systems have been
widely investigated (the most well-known being ML-polymorphism). In this paper
we investigate System Fat, or atomic System F, a very weak predicative
fragment of System F whose typable terms coincide with the simply typable
ones. We show that the type-checking problem for Fat is decidable and we
propose an algorithm which sheds some new light on the source of
undecidability in full System F. Moreover, we investigate free theorems and
contextual equivalence in this fragment, and we show that the latter, unlike
in the simply typed lambda-calculus, is undecidable.

##  1 Introduction

Polymorphism has been a central topic in programming language theory since the
late sixties. Today, most general purpose programming languages employ some
kind of polymorphism. At the same time, under the Curry-Howard correspondence,
quantification over types corresponds to quantification over propositions,
that is, to second-order logic. In particular, System F, the archetypical type
system for polymorphism, can be seen as a proof-system for (the
$\Rightarrow,\forall$-fragment of) second-order intuitionistic logic.

In spite of the numerous applications of polymorphism, practically all
interesting type-related properties of (Curry-style) System F (e.g. type
checking, type inhabitation, etc.) are undecidable, making this language
impractical for any reasonable implementation. This is one of the reasons why
a wide literature has investigated more manageable subsystems of System F.
Notably, _$\mathrm{ML}$ -__polymorphism_ [41, 42, 40] has found much success
due to its decidable type-checking.

Another direction of research was that of investigating _predicative_
subsystems of System F [32, 33, 34, 6]. In particular, the so-called _finitely
stratified polymorphism_ [33] yields a stratification of System F through a
sequence of predicative systems $(\mathrm{F}_{n})_{n\in\mathbb{N}}$ of growing
expressive power (notably, $F_{0}$ is the simply typed $\lambda$-calculus
${\mathrm{ST\lambda C}}$, and $\mathrm{ML}$-polymorphism coincides with the
rank-1 part of ${\mathrm{F}_{1}}$). Yet, in spite of such limitations, type
checking becomes undecidable already at level 1 of this hierarchy [18].

Could one tell exactly at which point, in the range from the simply typed
$\lambda$-calculus and $\mathrm{ML}$ to full System F, the type-related
properties of polymorphism become undecidable?

#### Atomic Polymorphism

In more recent times Ferreira et al. have undertaken the investigation of what
can be seen as the least expressive predicative fragment of F, System
${\mathrm{F_{at}}}$, or _atomic_ System F [12, 11, 13, 15, 16, 10, 9]. The
predicative restriction of ${\mathrm{F_{at}}}$ is such that a universally
quantified type $\forall X.A$ can be instantiated solely with an atomic type,
i.e. a type variable. In this way ${\mathrm{F_{at}}}$ sits in between level 0
(i.e. ${\mathrm{ST\lambda C}}$) and level 1 of the finitely stratified
hierarchy. Actually, ${\mathrm{F_{at}}}$ can be seen as a _type refinement_
system (in the sense of [39]) of ${\mathrm{ST\lambda C}}$, since all terms
typable in ${\mathrm{F_{at}}}$ are simply typable (cf. Lemma 4.1).

In spite of its very limited expressive power, Ferreira et al. have shown
that, thanks to polymorphism, ${\mathrm{F_{at}}}$ enjoys some proof-theoretic
properties that ${\mathrm{ST\lambda C}}$ lacks. In particular, they defined a
predicative variant of the usual encoding of sum and product types inside F,
yielding an embedding of intuitionistic propositional logic inside
${\mathrm{F_{at}}}$. However, while propositional logic is decidable,
provability in second-order propositional intuitionistic logic, even with the
atomic restriction, is undecidable [55]. This argument (as recently observed
in [51]) can be extended to show that the _type inhabitation_ property, which
is decidable for ${\mathrm{ST\lambda C}}$, is undecidable for
${\mathrm{F_{at}}}$.

### Contributions

In this paper we investigate the following type-related properties of System
${\mathrm{F_{at}}}$:

Type inhabitation (TI): | given $A$, is there $t$ such that $\vdash t:A$?
---|---
Type-checking (TC): | given $\Gamma,A,t$, does $\Gamma\vdash t:A$?
Typability (T): | given $\Gamma,t$, is there $A$ such that $\Gamma\vdash t:A$?
Contextual equivalence (CE): | given $A,t,u$ such that $\vdash t,u:A$, do $\mathtt{C}[t]$ and $\mathtt{C}[u]$ reduce
| to the same boolean, for all context $\mathtt{C}[\
]:A\Rightarrow\mathsf{Bool}$?

In Fig. 1 we sum up what is already known and what is established in this
paper (in bold) about such properties in predicative fragments of System F.
Our main results are that in ${\mathrm{F_{at}}}$ (TC) and (T) are both
decidable, and that (CE) is decidable if one restricts oneself to numerical
functions, and undecidable in the general case.

Several decidability properties of ${\mathrm{F_{at}}}$ are tight, meaning that
they all fail already for ${\mathrm{F}_{1}}$. In these cases, our arguments
can be used to shed some new insights on the broader question of understanding
where the source of undecidability for such properties in full System F lies.

$\mathrm{F}_{0}={\mathrm{ST\lambda C}}$ ${\mathrm{F_{at}}}$ $\mathrm{ML}$
${\mathrm{F}_{1}}$ F TI decidable [58] undecidable [51] decidable undecidable
[56] undecidable [37] TC decidable [25] decidable decidable [40] undecidable
[18] undecidable [63] T decidable [25] decidable decidable [40] undecidable
[18] undecidable [63] $\begin{matrix}\text{CE}\\\ \text{\small(for
numerical}\\\ \text{\small functions)}\end{matrix}$ decidable [44] decidable
undecidable undecidable undecidable∗ $\begin{matrix}\text{CE}\\\
\text{\small(full)}\end{matrix}$ decidable [44] undecidable undecidable
undecidable undecidable∗∗

Figure 1: Decidable and undecidable properties of System F and some
predicative fragments (in bold the properties established in the present
paper).
∗: easy consequence of Rice’s theorem and the typability of all primitive
recursive functions in F.
∗∗: consequence of the undecidability of (CE) for numerical functions.

### Plan of the paper

After recalling the syntax of F and its fragment in Curry-style and Church-
style, we address the properties (TI), (TC), (T) and (CE).

#### Type Inhabitation

In Section 3 we shortly discuss the undecidability of (TI), by showing how the
argument in [56] for System F applies to ${\mathrm{F_{at}}}$ too. This
argument yields an encoding inside ${\mathrm{F_{at}}}$ of an undecidable
fragment of _first-order_ intuitionistic logic. We also observe that
${\mathrm{F_{at}}}$ is actually equivalent to a first-order system, namely to
the $\Rightarrow,\forall$-fragment $\mathrm{1Mon}^{\Rightarrow,\forall}$ of
first-order _monadic_ intuitionistic logic in a language with a unique monadic
predicate. To our knowledge, the undecidability of
$\mathrm{1Mon}^{\Rightarrow,\forall}$ has not been previously observed
(although some slightly more expressive fragments - e.g. including a primitive
disjunction [19] or finitely many monadic predicates [53] \- have been proven
undecidable).

#### Type-Checking and Typability

In Section 4 we consider the type-checking problem. The undecidability of (TC)
for System F was established by Wells in [63], and was later extended to all
predicative systems $\mathrm{F}_{n}$, for $n>0$ [18]. In all these cases this
result was obtained by reducing an undecidable variant of _second-order
unification_ (SOU) to the type-checking problem. On the other hand, the
decidability of (TC) for $\mathrm{ML}$ (and $\mathrm{F}_{0}={\mathrm{ST\lambda
C}}$) is based on the famous Hindley-Milner algorithm [40], which reduces this
problem to _first-order unification_ (FOU), which is decidable.

The fundamental source of undecidability of SOU is the presence of _cyclic_
dependences between second order variables, expressed in the simplest case by
equations of the form $X(t)=f(v_{1},\dots,v_{k-1},X(u),v_{k+1},\dots,v_{n})$.
In fact, _acyclic_ SOU is decidable [36]. When type-checking polymorphic
programs, such cyclic dependencies are generated by _self-applications_ , i.e.
terms of the form $\lambda\vec{x}.xt_{1}\dots t_{k-1}xt_{k+1}\dots t_{n}$. In
fact, in this case the type $\forall X.A$ assigned to the variable $x$ must
satisfy a cyclic equation of the form

$A[X\mapsto C_{1}]=B_{1}\Rightarrow\dots\Rightarrow B_{k-1}\Rightarrow
A[X\mapsto C_{2}]\Rightarrow B_{k+1}\Rightarrow\dots\Rightarrow B_{n}$

(where $C_{1},C_{2}$ are suitable type instantiations of $X$). By constrast,
no term containing a self-application can be typed in ${\mathrm{ST\lambda
C}}$, since cyclic equations cannot be solved by FOU.

Since the terms typable in ${\mathrm{F_{at}}}$ can also be typed in
${\mathrm{ST\lambda C}}$, it follows that self-applications cannot be typed in
${\mathrm{F_{at}}}$ either. Using this observation, we describe a type-
checking algorithm for ${\mathrm{F_{at}}}$ which works in two phases: first,
it checks (using FOU) the presence of cyclic dependencies, and returns
$\mathtt{failure}$ if it detects one; then, if phase 1 succeeds, it applies (a
suitable variant of) acyclic SOU to decide type-checking. From the
decidability of (TC), we deduce the decidability of (T) by a standard argument
(see [4]).

#### Contextual Equivalence

Studying the typable terms of ${\mathrm{F_{at}}}$ might not seem very
interesting from a computational viewpoint, as these terms are already typable
in ${\mathrm{ST\lambda C}}$. However, due to the presence of some form of
polymorphism, investigating programs in ${\mathrm{F_{at}}}$ can be interesting
for _equational_ reasoning, as we investigate in Sections 5 and 6. In standard
type systems, beyond the standard notions of program equivalence arising from
the operational semantics (i.e. $\beta\eta$-equivalence), there may exist
several other congruences arising from either denotational models or from some
notion of _contextual equivalence_. In ${\mathrm{ST\lambda C}}$, it is well-
known that $\simeq_{\beta\eta}$ coincides with the congruence induced by any
infinite extensional model [57], as well as with several notions of contextual
equivalence (see [5], [7]). In polymorphic type systems the picture is rather
different, since $\beta\eta$-equivalence is usually weaker than the
congruences arising from extensional models (see [3, 23]), and also weaker
than standard notions of contextual equivalence. Moreover, while
$\beta\eta$-equivalence is decidable, contextual equivalence is undecidable.
Since in many practical situations (see [61, 1]) it is more convenient to
reason up to notions of equivalence stronger than $\beta\eta$-equivalence,
several techniques to compute (approximations of) contextual equivalence have
been investigated, e.g.  _free theorems_ [62], _parametricity_ [52],
_dinaturality_ [3].

Our investigation of contextual equivalence starts in Section 5 with an
exploration of equational reasoning in ${\mathrm{F_{at}}}$ using free
theorems. We show that the predicative encodings of sum and product types of
Ferreira et al. produce products and coproducts in ${\mathrm{F_{at}}}$ in the
categorical sense, provided terms are considered up to (CE) (a fact which is
known to hold in F for the usual, impredicative, encodings [23, 60]). We then
investigate (CE) for typable numerical functions. Using the fact that the
primitive recursive functions are _uniquely_ defined in System F up to (CE),
we show that (CE) for the representable numerical functions is decidable in
${\mathrm{F_{at}}}$, and undecidable in $\mathrm{ML}$. Such results rely on
the observation that (CE) becomes undecidable as soon as some super-polynomial
function (like bounded multiplication) becomes representable. As a
consequence, (CE) is undecidable in all fragments $F_{n}$, for $n>0$, of the
finitely stratified hierarchy as well.

Finally, in Section 6 we establish that (CE) is undecidable also in
${\mathrm{F_{at}}}$, by showing that the type inhabitation problem for a
suitable extension of ${\mathrm{F_{at}}}$ can be reduced to it. This result,
together with the previous ones, shows that there is no hope to get a
decidable contextual equivalence for polymorphic programs through a
predicative restriction, and one has rather to look for other kinds of
restrictions (see for instance [49]).

##  2 Predicative Polymorphism and System ${\mathrm{F_{at}}}$

The systems we consider in this paper are all restrictions of usual Church-
style and Curry-style System F. The types are defined in both cases by the
grammar

$A,B::=X\mid A\Rightarrow B\mid\forall X.A$

starting from a countable set $\mathtt{Var}^{2}$ of type variables
$X_{1},X_{2},\dots$. The terms of Church-style System F are defined by the
grammar below:

$\displaystyle t^{A},u^{A}$ $\displaystyle::=x^{A}\mid(\lambda
x^{A}.t^{B})^{A\Rightarrow B}\mid t^{B\Rightarrow A}u^{B}\mid(\Lambda
X.t^{A})^{\forall X.A}\mid(t^{\forall X.A}C)^{A[C/X]}$

For readability, we will often omit type annotations, when these can be
guessed from the context. The terms of Curry-style System F are standard
$\lambda$-terms, with typing rules defined as in Fig. 2, where $\Gamma$
indicates a partial function from term variables to types with a finite
support, and by $X\notin\mathrm{FV}(\Gamma)$ we indicate that $X$ does not
occur free in any type in $\mathrm{Im}(\Gamma)$. We will call the type $C$
occurring in $(t^{\forall X.A}C)^{A[C/X]}$ and in the rule $\forall$E in Fig.
2 the _witness_ of the type instantiation.

We will indicate _term contexts_ (i.e. terms with a unique occurrence of the
_hole_ $[\ ]$) as $\mathtt{C}[\ ],\mathtt{D}[\ ]$. Moreover, we let
$\mathtt{C}[\ ]:A\vdash B$ be a shorthand for $x\mapsto
A\vdash\mathtt{C}[x]:B$.

$\begin{matrix}\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.47221pt\hbox{\vbox{\hbox{\hskip 4.0pt\hbox{$\Gamma(x)=A$}\hskip
4.0pt}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to48.57632pt{\xleaders\hrule\hfill}\lower
3.21666pt\hbox{\hskip
3.0pt$\mathrm{Var}$}}\vskip-1.21666pt\nointerlineskip\hbox{\hskip
0.55565pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash x:A$}\hskip
4.0pt}}}}}\ignorespaces\\\ \\\
\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.47221pt\hbox{\vbox{\hbox{\hskip 8.47223pt\hbox{\hskip
4.0pt\hbox{$\Gamma,x\mapsto A\vdash t:B$}\hskip
4.0pt}}\vskip-1.27223pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to84.99617pt{\xleaders\hrule\hfill}\lower
3.27222pt\hbox{\hskip
3.0pt$\mathrm{Abs}$}}\vskip-1.27222pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash\lambda x.t:A\Rightarrow B$}\hskip
4.0pt}}}}\ignorespaces\qquad\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.47221pt\hbox{\vbox{\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash
t:A\Rightarrow B$}\hskip 4.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash u:A$}\hskip
4.0pt}}\vskip-2.24445pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to130.93124pt{\xleaders\hrule\hfill}\lower
2.3pt\hbox{\hskip
3.0pt$\mathrm{Appl}$}}\vskip-2.24445pt\nointerlineskip\hbox{\hskip
39.6295pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash tu:B$}\hskip
4.0pt}}}}}\ignorespaces\\\ \\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.47221pt\hbox{\vbox{\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash t:B$}\hskip
4.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip
4.0pt\hbox{$X\notin\mathrm{FV}(\Gamma)$}\hskip
4.0pt}}\vskip-1.27223pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to115.80421pt{\xleaders\hrule\hfill}\lower
3.27222pt\hbox{\hskip
3.0pt$\forall$I}}\vskip-1.27222pt\nointerlineskip\hbox{\hskip
25.13142pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash t:\forall X.A$}\hskip
4.0pt}}}}}\ignorespaces\qquad\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
26.0pt\hbox{\vbox{\hbox{\hskip 5.73679pt\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash
t:\forall X.A$}\hskip 4.0pt}}\vskip-1.27223pt\nointerlineskip\hbox{\hskip
0.0pt\lower-0.2pt\hbox{}\hbox to77.01494pt{\xleaders\hrule\hfill}\lower
3.27222pt\hbox{\hskip
3.0pt$\forall$E}}\vskip-1.27222pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash t:A[C/X]$}\hskip 4.0pt}}}}\ignorespaces\end{matrix}$

Figure 2: Typing rules for Curry-style System F.

System F is impredicative: _any_ type can figure as a witness. In particular,
one can construct “circular” instantiations, in which a term of type $\forall
X.A$ is instantiated with the same type as witness. A _predicative_ fragment
of System F is one in which witnesses are restricted in such a way to avoid
such circular instantiations.

We will focus on three predicative fragments of System F, both in Church- and
Curry-style. The first is System ${\mathrm{F}_{1}}$, which is the fragment of
F in which witnesses are _quantifier-free_. The second is System
${\mathrm{F_{at}}}$, which is the fragment of F in which witnesses are
_atomic_ , that is, type variables. The third is system $\mathrm{ML}$ [41,
40], which essentially coincides with the _rank 1_ fragment of
${\mathrm{F}_{1}}$. For any type $A$, the rank $\mathsf{r}(A)$ is the maximum
number of nesting between $\Rightarrow$ and $\forall$, and is defined
inductively by $\mathsf{r}(X)=0$, $\mathsf{r}(A\Rightarrow
B)=\max\\{\mathsf{r}(A)+1,\mathsf{r}(B)\\}$ and $\mathsf{r}(\forall X_{1}\dots
X_{n}.A)=\mathsf{r}(A)+1$ (where $n>0$ and $A$ does not start with a
quantifier). To define $\mathrm{ML}$ (since type-checking is decidable in
$\mathrm{ML}$, we limit ourselves to Curry-style) one first has to enrich the
set of $\lambda$-terms with the $\mathsf{let}$-constructor, and add a rule

$\Gamma,x\mapsto A\vdash t:B$ $\Gamma\vdash u:A$ $\mathrm{let}$
$\Gamma\vdash\mathsf{let}\ x\ \mathsf{be}\ u\ \mathsf{in}\ t:B$

$\mathrm{ML}$ is the fragment of the resulting system in which typing rules
only contain judgements $\Gamma\vdash t:A$, where $\mathsf{r}(A)\leq 1$ and
for all $B\in\mathrm{Im}(\Gamma)$, $\mathsf{r}(B)\leq 1$.

Observe that in ${\mathrm{F}_{1}}$ one can encode $\mathsf{let}\ x\
\mathsf{be}\ u\ \mathsf{in}\ t$ by $(\lambda x.t)u$, so that the rule above
becomes derivable. This is not possible in $\mathrm{ML}$, due to the rank
restriction.

#### Impredicative and Predicative Encodings

It is well-known that sum and product types can be encoded inside System F by

$\displaystyle A\widetilde{+}B$ $\displaystyle=\forall X.(A\Rightarrow
X)\Rightarrow(B\Rightarrow X)\Rightarrow X$ $\displaystyle
A\widetilde{\times}B$ $\displaystyle=\forall X.(A\Rightarrow B\Rightarrow
X)\Rightarrow X$

where the type variable $X$ is fresh. The encoding of term constructors
$\iota_{i}(\cdot)$, $\langle\cdot,\cdot\rangle$ and term destructors
$\mathrm{Case}_{C}(\cdot,x^{A}.\cdot,x^{B}.\cdot)$ and $\pi_{i}(\cdot)$ is
given (in Church-style) by:

$\displaystyle\iota_{1}(t)$ $\displaystyle=\Lambda X.\lambda f^{A\Rightarrow
X}.\lambda g^{B\Rightarrow X}.ft$
$\displaystyle\qquad\mathrm{Case}_{C}(t,x^{A}.u,x^{B}.v)$
$\displaystyle=tC(\lambda x^{A}.u)(\lambda x^{B}.v)$
$\displaystyle\iota_{2}(t)$ $\displaystyle=\Lambda X.\lambda f^{A\Rightarrow
X}.\lambda g^{B\Rightarrow X}.gt$ $\displaystyle\qquad\pi_{1}(t)$
$\displaystyle=tA\lambda x^{A}.\lambda y^{B}.x$ $\displaystyle\langle
t,u\rangle$ $\displaystyle=\Lambda X.\lambda f^{A\Rightarrow B\Rightarrow
X}.ftu$ $\displaystyle\qquad\pi_{2}(t)$ $\displaystyle=tB\lambda x^{A}.\lambda
y^{B}.y$

At the level of provability, the encoding is _faithful_ : a type is inhabited
in the extension of System F with sum and product types iff the encoded type
is inhabited in System F. Moreover, the encoding of $\widetilde{+}$ satisfies
the _disjunction property_ : $A\widetilde{+}B$ is inhabited iff either $A$ or
$B$ are inhabited.

At the level of conversions, the encoding translates $\beta$-reduction rules
for sum and product types into $\beta$-reduction in F. Instead, the
$\eta$-rules for sums and products are not translated by the $\beta$\- and
$\eta$\- rules of System F. Yet, the equivalence generated by $\beta$\- and
$\eta$-rules is preserved by _contextual equivalence_ in System F (more on
this in Section 5).

The encoding of sum and product types is impredicative: the encoding of term
destructors requires witnesses of arbitrary complexity. Notably, given a term
$t$ of type $A\widetilde{+}B$, the term
$\mathrm{Case}_{A\widetilde{+}B}(t,x^{A}.\iota_{1}(x),x^{B}.\iota_{2}(x))$, of
type $A\widetilde{+}B$, has a circular instantiation of $A\widetilde{+}B$.

In [12] an alternative, predicative, encoding was defined within System
${\mathrm{F_{at}}}$. The fundamental observation is that the unrestricted
$\forall$E rule is derivable from the restricted one for the types of the form
$A\widetilde{+}B$ and $A\widetilde{\times}B$ (the authors call this phenomenon
_instantiation overflow_). In fact333We essentially follow here an encoding
from [9]., for any type $C$ of System F one can define contexts
$\mathsf{IO}^{+}_{C}[\ ]:A\widetilde{+}B\vdash(A\Rightarrow
C)\Rightarrow(B\Rightarrow C)\Rightarrow C$ and $\mathsf{IO}^{\times}_{C}[\
]:A\widetilde{\times}B\vdash(A\Rightarrow B\Rightarrow C)\Rightarrow C$ by
induction on $C$:

$\displaystyle\mathsf{IO}^{+}_{X}[\ ]$
$\displaystyle=\mathsf{IO}^{\times}_{X}[\ ]=[\ ]X$
$\displaystyle\mathsf{IO}^{+}_{C_{1}\Rightarrow C_{2}}[\ ]$
$\displaystyle=\lambda f^{A\Rightarrow C_{1}\Rightarrow C_{2}}.\lambda
g^{B\Rightarrow C_{1}\Rightarrow C_{2}}.\lambda
y^{C_{1}}.\mathsf{IO}^{+}_{C_{2}}[\ ](\lambda z^{A}.fzy)(\lambda z^{B}.gzy)$
$\displaystyle\mathsf{IO}^{\times}_{C_{1}\Rightarrow C_{2}}[\ ]$
$\displaystyle=\lambda f^{A\Rightarrow B\Rightarrow C_{1}\Rightarrow
C_{2}}.\lambda y^{C_{1}}.\mathsf{IO}^{+}_{C_{2}}[\ ](\lambda z^{A}\lambda
w^{B}.fzwy)$ $\displaystyle\mathsf{IO}^{+}_{\forall Y.C^{\prime}}[\ ]$
$\displaystyle=\lambda f^{A\Rightarrow\forall Y.C^{\prime}}.\lambda
g^{A\Rightarrow\forall Y.C^{\prime}}.\Lambda Y.\mathsf{IO}^{+}_{C^{\prime}}[\
](\lambda z^{A}.fzY)(\lambda z^{B}.gzY)$
$\displaystyle\mathsf{IO}^{\times}_{\forall Y.C^{\prime}}[\ ]$
$\displaystyle=\lambda f^{A\Rightarrow B\Rightarrow\forall
Y.C^{\prime}}.\Lambda Y.\mathsf{IO}^{+}_{C^{\prime}}[\ ](\lambda z^{A}.\lambda
w^{B}.fzwY)$

One can thus encode the type destructors as for F, by replacing the type
application $xC$ in $\mathrm{Case}_{C}(t,x^{A}.u,x^{B}.v)$ with either
$\mathsf{IO}^{+}_{C}[x]$ or $\mathsf{IO}^{\times}_{C}[x]$.

At the level of provability, this embedding is faithful when restricted to
simple types, i.e. for the intuitionistic propositional calculus (see [13]): a
simple type (possibly containing finite sums and products) is inhabited iff
its encoding is inhabited in ${\mathrm{F_{at}}}$. However, faithfulness does
not hold for the extension of ${\mathrm{F_{at}}}$ with sum and product types
(see [47]). In particular, one can construct types $C,D$ of F such that
$C\widetilde{+}D$ is inhabited in ${\mathrm{F_{at}}}$ while $C+D$ is not
inhabited in the extension of ${\mathrm{F_{at}}}$ with sums and products. This
also implies that the disjunction property fails for $C\widetilde{+}D$ in
${\mathrm{F_{at}}}$, since neither $C$ nor $D$ are inhabited.

Interestingly, at the level of conversions, this encoding is stronger than the
usual one: it translates not only $\beta$-reductions, but also the permutative
conversions and a restricted form of $\eta$-conversion for sums, into $\beta$
and $\eta$-reductions of ${\mathrm{F_{at}}}$ (see [11, 14, 9]).

##  3 Type Inhabitation

In this section we discuss type inhabitation in the systems
${\mathrm{F_{at}}}$ and ${\mathrm{F}_{1}}$. We briefly recall the
undecidability argument for (TI) in System F from [56], and observe that this
applies to ${\mathrm{F_{at}}}$ (a more detailed reconstruction can be found in
[51]).

The argument in [56] (which was later simplified in [8]) is based on an
embedding inside F of an undecidable fragment of first-order logic. We recall
the argument in a few more details, so that it will be clear that the same
argument shows the undecidability of type inhabitation in both
${\mathrm{F_{at}}}$ and ${\mathrm{F}_{1}}$.

We consider the $\Rightarrow,\forall$-fragment of _dyadic_ intuitionistic
first-order logic $\mathsf{DyIL_{\Rightarrow,\forall^{1}}}$, that is, in a
language with no function symbol and a finite number of at most binary
relation symbols. We consider sequents of the form $\Gamma\vdash\bot$ where
$\Gamma$ consists of three type of assumptions:

  1. i.

atomic formulas different from $\bot$;

  2. ii.

closed formulas of the form
$\forall\vec{\alpha}.(\varphi_{1}\Rightarrow\dots\Rightarrow\varphi_{n}\Rightarrow\psi)$,
where $\varphi_{1},\dots,\varphi_{n},\psi$ are atomic formulas and each
variable in $\psi$ occurs in some the $\varphi_{i}$;

  3. iii.

closed formulas of the form
$\forall\alpha(\forall\beta(p(\alpha,\beta)\Rightarrow\bot)\Rightarrow\bot)$.

We fix a finite number of distinguished type variables:

  * •

for each relation symbol $p$, three variables $p_{1},p_{2},p_{3}$;

  * •

five more variables $\spadesuit,\bullet,\circ_{1},\circ_{2},\star$.

We let, for any type $A$, $A^{\bullet}:=A\Rightarrow\bullet$, and we define,
for all types $A,B$:

$\displaystyle p_{AB}$ $\displaystyle=(A^{\bullet}\Rightarrow
p_{1})\Rightarrow(B^{\bullet}\Rightarrow p_{2})\Rightarrow p_{3}$
$\displaystyle p(A,B)$ $\displaystyle=p_{AB}\Rightarrow\star$

For any type $A$, we let $\mathcal{U}(A)$ be the set of all types
$(A^{\bullet}\Rightarrow
p_{i})\Rightarrow\circ_{1},A^{\bullet}\Rightarrow\circ_{2}$, where $i=1,2$.
Given a finite list of types $A_{1},\dots,A_{n}$, we let
$\mathcal{U}(A_{1},\dots,A_{n})\Rightarrow B$ be a shorthand for
$C_{1}\Rightarrow\dots\Rightarrow C_{k}\Rightarrow B$, where
$C_{1},\dots,C_{k}$ are the types in $\bigcup_{i}\mathcal{U}(A_{i})$.

Each formula $\varphi$ of $\mathsf{DyIL_{\Rightarrow,\forall^{1}}}$ is
translated into a type $\mathbin{\overline{\varphi}}$ as follows:

$\displaystyle\mathbin{\overline{p(\alpha_{i},\alpha_{j})}}$
$\displaystyle=p(X_{i},X_{j})\qquad\mathbin{\overline{\bot}}=\spadesuit$
$\displaystyle\mathbin{\overline{\varphi\Rightarrow\psi}}$
$\displaystyle=\mathbin{\overline{\varphi}}\Rightarrow\mathbin{\overline{\psi}}$
$\displaystyle\mathbin{\overline{\forall\alpha_{i}.\varphi}}$
$\displaystyle=\forall\vec{X}_{i}.(\mathcal{U}(X_{1},\dots,X_{n})\Rightarrow\mathbin{\overline{\varphi}})$

One can easily check the following by induction:

######  Proposition 3.1.

If $\varphi_{1},\dots,\varphi_{n}\vdash\varphi$ is provable in
$\mathsf{DyIL_{\Rightarrow,\forall^{1}}}$ and
$\alpha_{i_{1}},\dots,\alpha_{i_{k}}$ are the variables that occur in
$\mathrm{FV}(\varphi)$ but not in
$\mathrm{FV}(\varphi_{1},\dots,\varphi_{n})$, then
$x_{1}\mapsto\mathbin{\overline{\varphi}}_{1},\dots,x_{n}\mapsto\mathbin{\overline{\varphi}}_{n},\vec{y}\mapsto\mathcal{U}(X_{i_{1}},\dots,X_{i_{k}})\vdash
t:\mathbin{\overline{\varphi}}$ holds in ${\mathrm{F_{at}}}$ for some term
$t$.

The less trivial part is the following:

######  Theorem 3.2 ([56], Theorem 11.6.14).

If $\varphi_{1},\dots,\varphi_{n}$ satisfy i-iii, and
$x_{1}\mapsto\mathbin{\overline{\varphi}}_{1},\dots,x_{n}\mapsto\mathbin{\overline{\varphi}}_{n},\vec{y}\mapsto\mathcal{U}(X_{i_{1}},\dots,X_{i_{k}})\vdash
t:\spadesuit$ is deducible in System F, then
$\varphi_{1},\dots,\varphi_{n}\vdash\bot$ is provable in
$\mathsf{DyIL_{\Rightarrow,\forall^{1}}}$.

Since ${\mathrm{F_{at}}}$ and ${\mathrm{F}_{1}}$ are both fragments of F, we
can freely substitute them for System F in the statement of Theorem 3.2. Then,
together with Proposition 3.1 we deduce:

######  Corollary 3.1.

(TI) is undecidable in both ${\mathrm{F_{at}}}$ and ${\mathrm{F}_{1}}$.

######  Remark 3.1.

Although ${\mathrm{F_{at}}}$ and ${\mathrm{F}_{1}}$ are both undecidable, they
are not equivalent at the level of provability. For instance, the type
$(\forall X.X\Rightarrow Y)\Rightarrow(X\Rightarrow X)\Rightarrow Y$ is
inhabited in ${\mathrm{F}_{1}}$ (by the term $\lambda x^{\forall
X.X\Rightarrow Y}.\lambda y^{X\Rightarrow X}.x(X\Rightarrow X)y$), but not in
${\mathrm{F_{at}}}$ (as easily seen by a proof-search argument).

######  Remark 3.2.

The undecidability of the atomic fragment of (full) second-order
intuitionistic logic has been known since (at least) [55]. However, from this
one cannot deduce the undecidability of ${\mathrm{F_{at}}}$, due to the fact
that disjunction is not faithfully definable in ${\mathrm{F_{at}}}$ (see also
[47]).

######  Remark 3.3.

It is not difficult to see that System ${\mathrm{F_{at}}}$ is equivalent to a
first-order system, namely to the $\Rightarrow,\forall$-fragment
$\mathsf{1Mon}_{\Rightarrow,\forall}$ of _monadic_ first-order intuitionistic
logic in the language with no function symbol and a _unique_ monadic
predicate. The equivalence is given by an obvious bijection between formulas
and types given by $\widehat{p(\alpha_{i})}=X_{i}$,
$\widehat{\varphi\Rightarrow\psi}=\widehat{\varphi}\Rightarrow\widehat{\psi}$
and $\widehat{\forall\alpha_{i}.\varphi}=\forall X_{i}.\widehat{\varphi}$.
Hence, a consequence of Corollary 3.1 is that provability in
$\mathsf{1Mon}_{\Rightarrow,\forall}$ is undecidable. Provability in
extensions of $\mathsf{1Mon}_{\Rightarrow,\forall}$ with either finitely many
monadic predicates, or with disjunction, is known to be undecidable [19, 18].
To the best of our knowledge, the undecidability of
$\mathsf{1Mon}_{\Rightarrow,\forall}$ had not been observed before.

##  4 Typability and Type-checking

In usual implementations of polymorphic type systems the Church-style type
discipline is generally considered inconvenient, due to the heavy amount of
type annotations. Instead, Curry-style languages, for which a compiler can
(either completely or partially) reconstruct type annotations, are generally
preferred (two standard examples are the languages $\mathsf{ML}$ and
$\mathsf{Haskell}$). This is the reason why type-checking algorithms for
polymorphic type systems in Curry-style (or in some variants of Curry-style
with _partial_ type annotations [45]) have been extensively investigated [24,
26, 63, 18].

However, while $\mathrm{ML}$ admits a decidable type checking in Curry-style
(a main reason for its success), type checking has been shown to be
undecidable for System F and most of its variants (including the predicative
system ${\mathrm{F}_{1}}$ [18]), making the Curry-style version of such
systems impractical for implementation.

For the simply typed $\lambda$-calculus (and crucially also for
$\mathrm{ML}$), the type-checking problem can be reduced to _first-order
unification_ (FOU), that is, to the problem of unifying first-order terms (in
a language with a unique binary function symbol corresponding to
$\Rightarrow$). Typically, an application $tu:b$ will produce a first-order
equation of the form $a_{t}=a_{u}\Rightarrow b$, where $a_{t},a_{u}$ are
variables indicating the type of $t$ and the type of $u$, respectively. As FOU
is decidable, this suffices to show that type-checking is decidable in this
case.

In the case of polymorphism FOU is not sufficient to solve type-checking. In
fact, already in ${\mathrm{F}_{1}}$ one can type terms, like e.g. $\lambda
x.xx$, which contain _self-applications_. Using FOU, this term yields the
unsolvable equation $a_{x}=a_{x}\Rightarrow b$, showing that $\lambda x.xx$ is
not typable in either ${\mathrm{ST\lambda C}}$ or $\mathrm{ML}$. To type-check
System F programs one can replace FOU with either _semi-unification_ [24, 26]
or _second order unification_ (SOU) [45, 18]. Here we focus on the latter: in
SOU one tries to unify equations involving terms constructed from first-order
variables $a,b,c,\dots$ as well as second order variables
$\mathsf{F},\mathsf{G},\dots$. For instance, the term $\lambda x.xx$ above
yields the equations

$\displaystyle\mathsf{F}a$ $\displaystyle=(\mathsf{F}b)\Rightarrow\mathsf{G}$
(1)

where $\forall X.A=\forall X.\mathsf{F}X$ indicates the type of $x$, and the
variables $a,b$ encode the possible witnesses which permit to type $xx$ (in
Church-style one could indicate this with $\lambda x^{\forall
X.\mathsf{F}X}.((xa)^{\mathsf{F}a=\mathsf{F}b\Rightarrow\mathsf{G}}(xb)^{\mathsf{F}b})^{\mathsf{G}}$).
For instance, a (non-unique) solution to this problem is given by
$\mathsf{F}\mapsto\lambda x.x$, $\mathsf{G}\mapsto Z$, $a\mapsto Y\Rightarrow
Z$, $b\mapsto Y$.

Unfortunately, SOU is undecidable [22]. Moreover, one can encode restricted
(but still undecidable) variants of SOU in the type checking problem for
${\mathrm{F}_{1}}$ [18], showing that (TC) is undecidable for
${\mathrm{F}_{1}}$. A fundamental ingredient of these undecidability arguments
is the appeal to _variable cycles_ (see the discussion in [36]) like the one
in Eq. (1), that is, to unification problems from which one can deduce an
equation of the form $\mathsf{F}a_{1}\dots a_{n}=u[\mathsf{F}]$ equating a
second-order variable $\mathsf{F}$ with some term containing $\mathsf{F}$
itself.

Conversely, _acyclic_ SOU, that is, the problem of unifying SOU problems
containing no variable cycles, is decidable [36]. These observations can be
used to show that type-checking is actually decidable in ${\mathrm{F_{at}}}$.
In fact, a fundamental property of ${\mathrm{F_{at}}}$ (and a reason for its
very limited expressive power) is that any term typable in ${\mathrm{F_{at}}}$
is already typable in the simply-typed $\lambda$-calculus. Indeed, the
following is easily checked by induction:

######  Lemma 4.1.

If $\Gamma\vdash t:A$ is derivable in the Curry-style ${\mathrm{F_{at}}}$,
then $|\Gamma|\vdash t:|A|$ is derivable in the simply typed
$\lambda$-calculus, where $|A|$ is defined by $|X|=o$, $|A\Rightarrow
B|=|A|\Rightarrow|B|$, $|\forall X.A|=|A|$, and $|\Gamma|(x)=|\Gamma(x)|$.

An immediate consequence of Lemma 4.1 is that one cannot type $\lambda x.xx$
in ${\mathrm{F_{at}}}$ and, more generally, that any $\lambda$-term that would
give rise to a variable cycle cannot be typed in ${\mathrm{F_{at}}}$. Observe
that the converse does not hold: from the fact that $|\Gamma|\vdash t:|A|$
holds, one cannot deduce $\Gamma\vdash t:A$ (take for instance $t=x$,
$\Gamma(x)=X$ and $A=\forall X.X$).

However, these observations suggest that type checking for ${\mathrm{F_{at}}}$
can be decided by reasoning in two phases: to check if $\Gamma\vdash t:A$ is
derivable in ${\mathrm{F_{at}}}$, first check if $|\Gamma|\vdash t:|A|$ is
derivable in ${\mathrm{ST\lambda C}}$ using FOU; if this first step fails,
then the original problem must fail; if the first step succeeds, then the
original type-checking problem for ${\mathrm{F_{at}}}$ yields an instance of
(a suitable variant of) acyclic SOU, which must be decidable. By reasoning in
this way, one can thus establish:

######  Theorem 4.2.

(TC) for Curry-style ${\mathrm{F_{at}}}$ is decidable.

In App. A we describe in detail the decision algorithm for
${\mathrm{F_{at}}}$, which is based on a variant of second-order unification,
that we call _${\mathrm{F_{at}}}$ -unification_. The fundamental idea is to
consider SOU problems in a language with first-order _sequence variables_
$a,b,\dots$ and two kinds of second-order variables: _projection variables_
$\alpha,\beta,\dots$ and _type schemes_ $\mathsf{F},\mathsf{G},\dots$. The
intuition is that a term of the form $\alpha a_{1}\dots a_{n}$ describes a
(skolemized) witness; since the witnesses in ${\mathrm{F_{at}}}$ are type
variables, solving for $\alpha$ means associating it with either a constant
function or a projection. Instead, a term of the form
$\mathsf{F}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}$ stands for the application
of suitable witnesses $\mathfrak{a}_{1},\dots,\mathfrak{a}_{n}$ to some type
$\mathsf{F}$, hence solving for $\mathsf{F}$ means associating it with some
function $\lambda X_{1}\dots X_{n}.A(X_{1},\dots,X_{n})$, where
$A(X_{1},\dots,X_{n})$ is some type expression parametric on the type variable
$X_{1},\dots,X_{n}$. Hence, for example, checking if $\Gamma\vdash xy:\forall
Z.Z$ holds in ${\mathrm{F_{at}}}$, where $\Gamma(x)=\forall X.X\Rightarrow X$
and $\Gamma(y)=\forall Y.Y$, yields the equations

$\displaystyle\mathsf{F}X$ $\displaystyle=X\Rightarrow X$
$\displaystyle\qquad\mathsf{G}Y$ $\displaystyle=Y$
$\displaystyle\mathsf{F}(\alpha Z)$ $\displaystyle=\mathsf{G}(\beta
Z)\Rightarrow\mathsf{H}Z$ $\displaystyle\qquad\mathsf{H}Z$ $\displaystyle=Z$

which admit the solution $\mathsf{F}\mapsto\lambda X.X\Rightarrow X$,
$\mathsf{G},\mathsf{H}\mapsto\lambda X.X$ and $\alpha,\beta\mapsto\lambda
X.X$. Instead, checking if $\Gamma\vdash xy:\forall Z:Z$, where now
$\Gamma(x)=\forall X.X\Rightarrow X$ and $\Gamma(y)=Y$, yields the equations

$\displaystyle\mathsf{F}X$ $\displaystyle=X\Rightarrow X$
$\displaystyle\qquad\mathsf{G}$ $\displaystyle=Y$
$\displaystyle\mathsf{F}(\alpha Z)$
$\displaystyle=\mathsf{G}\Rightarrow\mathsf{H}Z$
$\displaystyle\qquad\mathsf{H}Z$ $\displaystyle=Z$

which have no solution (since one can deduce $Z=\mathsf{H}Z=Y$), showing that
(TC) fails in this case (although $|\Gamma|\vdash xy:|\forall Z.Z|$ holds in
the simply typed $\lambda$-calculus).

From the decidability of (TC) one can deduce the decidability of (T) by a
standard argument: we can reduce (T) to (TC) by showing that a type $A$ such
that
$\Gamma\vdash{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}:A$
holds exists iff $\Gamma\vdash(\lambda
xy.y){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}:\forall
X.X\Rightarrow X$ holds. In fact, if
$\Gamma\vdash{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}:A$
holds in ${\mathrm{F_{at}}}$, then from $\Gamma\vdash\lambda
xy.y:A\Rightarrow\forall X.(X\Rightarrow X)$ we deduce $\Gamma\vdash(\lambda
xy.y){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}:\forall
X.X\Rightarrow X$. Conversely, from $\Gamma\vdash(\lambda
xy.y){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}:\forall
X.X\Rightarrow X$, we deduce that there exists a type $A$ such that
$\Gamma\vdash\lambda xy.y:A\Rightarrow(X\Rightarrow X)$ and
$\Gamma\vdash{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}:A$
holds.

######  Corollary 4.1.

(T) for Curry-style ${\mathrm{F_{at}}}$ is decidable.

##  5 Equational Reasoning in System ${\mathrm{F_{at}}}$

As a consequence of Lemma 4.1 from the previous section, all terms which are
typable in Curry-style ${\mathrm{F_{at}}}$ are simply typable. In other words,
${\mathrm{F_{at}}}$ can be seen as a _type refinement_ system for
${\mathrm{ST\lambda C}}$, in the sense of [39]. In particular, as we show
below, the numerical functions which can be typed in ${\mathrm{F_{at}}}$ are
precisely the simply typable ones (i.e. the so-called _extended polynomials_
[54, 16]).

For this reason, investigating the typable terms of ${\mathrm{F_{at}}}$ might
seem not very interesting from a computational viewpoint. However, in this
section we show that studying such terms can be interesting for equational
reasoning. In fact, similarly to System F, standard notions of contextual
equivalence are stronger than $\beta\eta$-equivalence, and one can exploit
well-known techniques like _free theorems_ [62], to compute equivalences of
${\mathrm{F_{at}}}$-typable terms (which do not hold when viewing these terms
as typed in ${\mathrm{ST\lambda C}}$).

We first recall two standard notions of contextual equivalence:

######  Notation 1.

We let $\mathsf{Bool}=\forall X.X\Rightarrow X\Rightarrow X$ and
$\mathsf{Nat}=\forall X.(X\Rightarrow X)\Rightarrow(X\Rightarrow X)$. We let
$\mathbf{t}=\lambda xy.x$ and $\mathbf{f}=\lambda xy.y$ indicate the two
normal forms of type $\mathsf{Bool}$, and for all $n\in\mathbb{N}$, we let
$\mathbf{n}=\lambda fx.(f)^{n}x$ indicate the $n$-th Church numeral.

######  Definition 5.1 (contextual equivalence).

Let $F^{*}\in\\{{\mathrm{F_{at}}},\mathrm{ML},{\mathrm{F}_{1}},\mathrm{F}\\}$.
For all closed terms $t,u$ of type $A$ in $F^{*}$, we let

  * •

$t\simeq_{\mathsf{Bool}}^{F^{*}}u:A$ iff for any context $\mathtt{C}[\
]:A\vdash\mathsf{Bool}$ in $F^{*}$,
$\mathtt{C}[t]\simeq_{\beta\eta}\mathtt{C}[u]$;

  * •

$t\simeq_{\mathsf{Nat}}^{F*}u:A$ iff for any context $\mathtt{C}[\
]:A\vdash\mathsf{Nat}$ in $F^{*}$,
$\mathtt{C}[t]\simeq_{\beta\eta}\mathtt{C}[u]$.

It is easily seen that $\simeq_{\mathsf{Bool}}^{F^{*}}$ and
$\simeq_{\mathsf{Nat}}^{F^{*}}$ are congruences of the terms of $F^{*}$.
Moreover, in System F these two congruences coincide, due to the fact that the
identity relation
$\mathtt{id}:\mathsf{Nat}\Rightarrow\mathsf{Nat}\Rightarrow\mathsf{Bool}$ is
typable. Since this function is also typable in $\mathrm{ML}$, the same holds
for $\mathrm{ML}$ and ${\mathrm{F}_{1}}$. On the other hand, since the
identity relation is _not_ simply typable, we can deduce (see Lemma 5.4 below)
that it is not typable in ${\mathrm{F_{at}}}$. For this reason the congruences
$\simeq_{\mathsf{Bool}}^{{\mathrm{F_{at}}}}$ and
$\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}$ must be treated separately. In
what follows we will mostly focus on the latter, since the former identifies
distinct normal forms of type $\mathsf{Nat}$, which is not convenient for
obvious computational reasons.

######  Remark 5.1.

The typability of the identity relation $\mathtt{id}$ implies that any
extensional model must be _infinite_ , since for all $n\in\mathbb{N}$, the
interpretations of $\mathbf{n}$ and $\mathbf{n+1}$ cannot coincide. Instead,
it is not difficult to construct an extensional model of ${\mathrm{F_{at}}}$
in which any type is interpreted by a _finite_ set (to give an idea, let
$\mathcal{C}_{k}$ be a collection of sets of cardinality bounded by a fixed
$k\in\mathbb{N}$; one can let then $\llbracket X\rrbracket\in\mathcal{C}_{k}$,
$A\Rightarrow B=\llbracket B\rrbracket^{\llbracket A\rrbracket}$ and
$\llbracket\forall X.A\rrbracket=\prod_{S\in\mathcal{C}_{k}}\llbracket
A\rrbracket[X\mapsto S]$).

The so-called free theorems are a class of syntactic equations for typable
terms which can be justified by relying on either relational parametricity
[52] or dinaturality [3]. We let $t\approx u:A$ indicate that $t,u$ have type
$A$ in System F, and that the equivalence $t\simeq u$ can be deduced using
$\beta$-, $\eta$-rules, standard congruence rules (i.e. reflexivity, symmetry,
transitivity and context closure), as well as instances of free theorems for
System F.

Free theorems can be used to deduce contextual equivalence of
${\mathrm{F_{at}}}$-terms, thanks to the following:

######  Lemma 5.1 (free theorems in ${\mathrm{F_{at}}}$).

Let $t,u$ be terms of type $A$ in ${\mathrm{F_{at}}}$. If $t\approx u:A$,
where $t,u$ are seen as terms of System F, then
$t\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}u:A$.

###### Proof.

From $t\approx u:A$ it follows $t\simeq_{\mathsf{Nat}}^{\mathrm{F}}u:A$, since
$\simeq_{\mathsf{Nat}}^{\mathrm{F}}$ is the coarsest congruence not equating
normal forms of type $\mathsf{Nat}$. From
$t\simeq_{\mathsf{Nat}}^{\mathrm{F}}u:A$ we deduce
$t\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}u:A$, since any context in
${\mathrm{F_{at}}}$ is a context in F. ∎

We discuss below two applications of free theorems to study (CE) in
${\mathrm{F_{at}}}$.

#### Categorical Products and Coproducts

As mentioned in Section 2, the usual encoding of products and coproducts in
System F preserves $\beta$-equivalence but not $\eta$-equivalence. For this
reason, the encodings of $\times$ and $+$ do not form categorical products and
coproducts in System F up to $\beta\eta$-equivalence (more precisely, in the
syntactic category in which objects are the types of System F and arrows are
the typable terms up to $\simeq_{\beta\eta}$). Instead, it is well-known [50,
23, 60] that $\eta$-equivalence of $\times$ and $+$ is preserved in System F
up to free theorems: hence $\times$ and $+$ do form categorical products and
coproducts in System F up to $\simeq_{\mathsf{Nat}}^{\mathrm{F}}$ (more
precisely, in the syntactic category whose arrows are the typable terms up to
$\simeq_{\mathsf{Nat}}^{\mathrm{F}}$).

In a similar way, the predicative encodings of $\times$ and $+$ in
${\mathrm{F_{at}}}$, although preserving some restricted case of
$\eta$-equivalence, still do not form categorical products and coproducts in
${\mathrm{F_{at}}}$ up to $\simeq_{\beta\eta}$. We will show that they
similarly do form categorical products and coproducts in ${\mathrm{F_{at}}}$
up to $\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}$, as a consequence of the
application of free theorems.

For simplicity, we here only consider the case of $+$. However, our argument
scales straightforwardly to the encoding of all finite polynomial types, i.e.
of all types of the form $\sum_{i=1}^{k}\prod_{j=1}^{k_{i}}A_{ij}$ (see the
pre-print [47] for a more detailed discussion).

The fundamental step is showing that the impredicative and predicative
encodings are equivalent up to free theorems:

######  Lemma 5.2.

For all types $A,B,C$ and terms $x\mapsto A\vdash u:C$ and $x\mapsto B\vdash
v:C$, the equivalence $\mathsf{IO}^{+}_{C}[y](\lambda x.u)(\lambda
x.v)\approx\mathrm{Case}_{C}(y,x.u,x.v):C$ holds in System $\mathrm{F}$.

###### Proof.

The free theorem associated with the type $A\widetilde{+}B$ is the schematic
equation

$\mathrm{Case}_{E}(t_{1},x.\mathtt{C}[t_{2}],x.\mathtt{C}[t_{3}])\approx\mathtt{C}\Big{[}\mathrm{Case}_{D}(t_{1},x.t_{2},x.t_{3})\Big{]}$
(2)

where $t_{1}:A\widetilde{+}B$, $t_{2}[x:A]:D$, $t_{2}[x:B]:D$ and
$\mathtt{C}[\ ]:D\vdash E$. In fact, this equation is an instance of the
_dinaturality_ condition for the type $A\widetilde{+}B$ (see [50, 23, 49]).

We argue by induction on $C$:

  * •

if $C=Y$, then $\mathsf{IO}^{+}_{C}[y](\lambda x.u)(\lambda x.v)=yY(\lambda
x.u)(\lambda x.v)=\mathrm{Case}_{C}(y,x.u,x.v)$;

  * •

if $C=C_{1}\Rightarrow C_{2}$, then

$\displaystyle\mathsf{IO}^{+}_{C}[y](\lambda x.u)(\lambda x.v)$
$\displaystyle=\Big{(}\lambda fgz.\mathsf{IO}^{+}_{C_{2}}[y](\lambda
x.fxz)(\lambda x.gxz)\Big{)}(\lambda x.u)(\lambda x.v)$
$\displaystyle\stackrel{{\scriptstyle\text{[I.H.]}}}{{\approx}}\Big{(}\lambda
fgz.\mathrm{Case}_{C_{2}}(y,x.fxz,x.gxz)\Big{)}(\lambda x.u)(\lambda x.v)$
$\displaystyle\simeq_{\beta}\lambda z.\mathrm{Case}_{C_{2}}(y,x.uz,x.vz)$
$\displaystyle\approx\lambda z.\Big{(}\mathrm{Case}_{C}(y,x.u,x.v)\Big{)}z$
$\displaystyle\simeq_{\eta}\mathrm{Case}_{C}(y,x.u,x.v)$

where in the penultimate step we applied Eq. (2) with the context
$\mathtt{C}[\ ]=[\ ]z:C\vdash C_{2}$.

  * •

if $C=\forall Z.C^{\prime}$, then

$\displaystyle\mathsf{IO}^{+}_{C}[y](\lambda x.u)(\lambda x.v)$
$\displaystyle=\Big{(}\lambda fg.\Lambda
Z.\mathsf{IO}^{+}_{C^{\prime}}[y](\lambda x.fxZ)(\lambda x.gxZ)\Big{)}(\lambda
x.u)(\lambda x.v)$
$\displaystyle\stackrel{{\scriptstyle\text{[I.H.]}}}{{\approx}}\Big{(}\lambda
fg.\Lambda Z.\mathrm{Case}_{C^{\prime}}(y,x.fxZ,x.gxZ)\Big{)}(\lambda
x.u)(\lambda x.v)$ $\displaystyle\simeq_{\beta}\Lambda
Z.\mathrm{Case}_{C^{\prime}}(y,x.uZ,x.vZ)$ $\displaystyle\approx\Lambda
Z.\Big{(}\mathrm{Case}_{C}(y,x.u,x.v)\Big{)}Z$
$\displaystyle\simeq_{\eta}\mathrm{Case}_{C}(y,x.u,x.v)$

where in the penultimate step we applied Eq. (2) with the context
$\mathtt{C}[\ ]=[\ ]Z:C\vdash C^{\prime}$.

∎

######  Proposition 5.3.

$A\widetilde{+}B$ is a categorical coproduct in ${\mathrm{F_{at}}}$ up to
$\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}$.

###### Proof.

It suffices to check that the $\eta$-rule of the coproduct (see [29]) holds in
${\mathrm{F_{at}}}$. By translating this rule in F one obtains the equation

$y\approx\mathrm{Case}_{A\widetilde{+}B}(y,x.\iota_{1}(x),x.\iota_{2}(x)):A\widetilde{+}B$

which holds in F up to free theorems (see [50, 23, 60]). Using Lemma 5.2 we
thus deduce that $y\approx\mathsf{IO}^{+}_{A\widetilde{+}B}[y](\lambda
x.\iota_{1}(x))(\lambda x.\iota_{2}(x)):A\widetilde{+}B$ holds in F, and by
Lemma 5.1 we deduce
$y\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}\mathsf{IO}^{+}_{A\widetilde{+}B}[y](\lambda
x.\iota_{1}(x))(\lambda x.\iota_{2}(x)):A\widetilde{+}B$. ∎

#### Numerical Functions

We now consider the representable numerical functions, that is, the typable
terms of type
$\mathsf{Nat}\Rightarrow\dots\Rightarrow\mathsf{Nat}\Rightarrow\mathsf{Nat}$.
In this case we can strengthen Lemma 4.1:

######  Lemma 5.4.

For any $\beta$-normal $\lambda$-term $t$, $\vdash
t:\mathsf{Nat}\Rightarrow\dots\Rightarrow\mathsf{Nat}\Rightarrow\mathsf{Nat}$
holds in Curry-style ${\mathrm{F_{at}}}$ iff $\vdash
t:|\mathsf{Nat}|\Rightarrow\dots\Rightarrow|\mathsf{Nat}|\Rightarrow|\mathsf{Nat}|$
holds in ${\mathrm{ST\lambda C}}$.

###### Proof.

One direction follows from Lemma 4.1. For the converse one, let $t$ (which we
can suppose w.l.o.g. to be of the form $\lambda x_{1}\dots x_{k}.u$) be such
that $\vdash
t:|\mathsf{Nat}|\Rightarrow\dots\Rightarrow|\mathsf{Nat}|\Rightarrow|\mathsf{Nat}|$.
By letting $\mathsf{Nat}[X]=(X\Rightarrow X)\Rightarrow(X\Rightarrow X)$ we
deduce that $\\{x_{i}\mapsto\mathsf{Nat}[X]\\}\vdash u:\mathsf{Nat}[X]$ holds
in ${\mathrm{F_{at}}}$, and thus that $\\{x_{i}\mapsto\mathsf{Nat}\\}\vdash
u:\mathsf{Nat}[X]$ holds too, from which we conclude $\vdash
u:\mathsf{Nat}\Rightarrow\dots\Rightarrow\mathsf{Nat}\Rightarrow\mathsf{Nat}$.
∎

A consequence of Lemma 5.4 is that the representable numerical functions in
${\mathrm{F_{at}}}$ are precisely the extended polynomials, i.e. the smallest
class of functions arising from projections, constant functions, addition,
multiplication and the $\mathtt{iszero}$ function. Instead, it is well-known
that the predecessor function (which is not an extended polynomial) is typable
in $\mathrm{ML}$ [17] and, more generally, the representable functions of
$\mathrm{ML}$ are included in the class $\mathcal{E}_{3}$ of the Grzegorczyk
hierarchy [33].

Still, in both ${\mathrm{ST\lambda C}}$ and ${\mathrm{F_{at}}}$ the same
extended polynomial can be represented by different normal forms. For instance
the two normal forms $\lambda xyfz.x(yf)z$ and $\lambda xyfz.y(xf)z$ (encoding
the algorithms $n,m\mapsto\underbrace{m+\dots+m}_{n\text{ times}}$ and
$n,m\mapsto\underbrace{n+\dots+n}_{m\text{ times}}$) both represent the
multiplication function.

In System F, one can show that all primitive recursive functions are _uniquely
defined_ up to free theorems, that is, that for any two terms $t,u$
representing the same primitive recursive function, one can prove $t\approx u$
(see [48], Section 7.5). Using Lemma 5.1 we deduce then:

######  Lemma 5.5.

For all
$t,u:\mathsf{Nat}\Rightarrow\dots\Rightarrow\mathsf{Nat}\Rightarrow\mathsf{Nat}$
in $\mathrm{F}^{*}\in\\{{\mathrm{F_{at}}},\mathrm{ML},{\mathrm{F}_{1}}\\}$, if
for all $p_{1},\dots,p_{k}\in\mathbb{N}$,
$t\mathbf{p}_{1}\dots\mathbf{p}_{k}\simeq_{\beta\eta}u\mathbf{p}_{1}\dots\mathbf{p}_{k}:\mathsf{Nat}$,
then $t\simeq_{\mathsf{Nat}}^{\mathrm{F}^{*}}u$.

The problem $\mathrm{Eq}_{\mathcal{C}}$ of deciding $f=g$, where $f,g$ belong
to some subclass $\mathcal{C}$ of the primitive recursive functions, is well-
investigated. In particular, it is known that:

  * •

if $\mathcal{C}$ is the class of extended polynomials, then
$\mathrm{Eq}_{\mathcal{C}}$ is decidable [38];

  * •

if $\mathcal{C}$ contains projections, constants, +, $\times$ and bounded
multiplication, then $\mathrm{Eq}_{\mathcal{C}}$ is undecidable [31].

From these facts, using Lemma 5.5, we deduce then:

######  Proposition 5.6.

  * i.

The problem of deciding $\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}$ over
numerical functions in ${\mathrm{F_{at}}}$ is decidable.

  * ii.

The problem of deciding $\simeq_{\mathsf{Nat}}^{\mathrm{F}^{*}}$ over
numerical functions in $\mathrm{F}^{*}\in\\{\mathrm{ML},{\mathrm{F}_{1}}\\}$
is undecidable.

###### Proof.

i. is immediate from Lemma 5.4 and Lemma 5.5. To prove ii. it suffices to show
that the representable functions in $\mathrm{ML}$ are closed under bounded
multiplication. We show this fact in detail in App. B. ∎

An immediate corollary is that (CE) is undecidable in both $\mathrm{ML}$ and
${\mathrm{F}_{1}}$.

##  6 Contextual Equivalence is Undecidable

In this section we show that the congruences
$\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}$ and
$\simeq_{\mathsf{Bool}}^{{\mathrm{F_{at}}}}$ are both undecidable. To do this,
we will reduce the type inhabitation problem for a suitable extension of
${\mathrm{F_{at}}}$ to contextual equivalence. We discuss in some detail the
undecidability argument for $\simeq_{\mathsf{Bool}}^{{\mathrm{F_{at}}}}$, and
we postpone the similar argument for
$\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}$ to App. C.

Let ${\mathrm{F_{at}^{\clubsuit}}}$ be ${\mathrm{F_{at}}}$ extended with a
type constant $\clubsuit$ and a term constant $\star:\clubsuit$. It is not
difficult to see that the undecidability argument for (TI) from Section 3 also
applies to ${\mathrm{F_{at}^{\clubsuit}}}$.

Let ${\widetilde{\top}}:\forall X.X\Rightarrow X$ and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathsf{Id}}:={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\Lambda
X.\lambda x.x}$ be the unique closed $\beta$-normal term of type
$\widetilde{\top}$.

The fundamental idea will be to construct, for each type $A$ of
${\mathrm{F_{at}^{\clubsuit}}}$, two terms $t_{A},u_{A}$ of type
$(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}$ (where
$A^{*}=Y\Rightarrow A[Y/\clubsuit]$, for some fresh $Y$), such that
$t_{A}\simeq_{\mathsf{Bool}}^{{\mathrm{F_{at}}}}u_{A}$ holds in
${\mathrm{F_{at}}}$ iff $A$ is inhabited in ${\mathrm{F_{at}^{\clubsuit}}}$.

Let us fix a type $A$ of ${\mathrm{F_{at}^{\clubsuit}}}$, a variable $Y$ not
occurring free in $A$, and let $A^{*}=Y\Rightarrow A[Y/\clubsuit]$. We let
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}$
be the terms below:

$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\lambda
x.\mathbf{f}}\qquad{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}=\lambda
x.\mathsf{IO}^{+}_{\mathsf{Bool}}[\ ](\lambda x.\mathbf{t})(\lambda
x.\mathbf{f})$

In the following, for a term context $\mathtt{K}[\ ]$, we let $\mathtt{K}[\
]:A\vdash^{\Gamma}B$ be a shorthand for $\Gamma,x\mapsto A\vdash\mathtt{K}[\
]:B$.

We let $\mathbb{G}_{1}$-$\mathbb{G}_{4}$ be the families of term contexts
defined by mutual recursion as shown in Fig. 3. One can check that these
contexts cannot separate $u_{A}$ and $v_{A}$:

$\displaystyle\mathbb{G}_{1}:\qquad{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[\
]$
$\displaystyle::={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x_{i}}\mid{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[\
]Y{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}[\
]\mathtt{C}[\ ]}$
$\displaystyle\mathbb{G}_{2}:\qquad{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{D}}[\
]$
$\displaystyle::={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}z}(\Lambda
W.\lambda
w.{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{F}}[\
])\mid{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[\
]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}W}\mathtt{D}[\
]\mathtt{D}[\ ]$
$\displaystyle\mathbb{G}_{3}:\qquad{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[\
]$ $\displaystyle::=\mathbf{t}\mid\mathbf{f}\mid x(\Lambda Y.\lambda y.\lambda
z.{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{D}}[\
])$
$\displaystyle\mathbb{G}_{4}:\qquad{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{F}}[\
]$ $\displaystyle::=w\mid\mathtt{E}[\ ]W\mathtt{F}[\ ]\mathtt{F}[\ ]$

Figure 3: Contexts $\mathbb{G}_{1}$-$\mathbb{G}_{4}$.

######  Lemma 6.1.

  1. 1.

For all
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[\
]\in\mathbb{G}_{1}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]$.

  2. 2.

for all
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{D}}[\
]\in\mathbb{G}_{2}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{D}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{D}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}z_{i}\mathsf{Id}}$.

  3. 3.

for all
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[\
]\in\mathbb{G}_{3}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]$.

  4. 4.

for all
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{F}}[\
]\in\mathbb{G}_{4}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{F}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{F}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}w_{i}}$.

The key ingredient is a lemma stating that the families of contexts
$\mathbb{G}_{1}$-$\mathbb{G}_{4}$ are exhaustive precisely when $A$ is not
inhabited in ${\mathrm{F_{at}^{\clubsuit}}}$:

######  Lemma 6.2.

Let
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{x\mapsto
Z,x^{\prime}\mapsto Z}Z$ be a $\beta$-normal term context. Then either $A$ is
inhabited in ${\mathrm{F_{at}^{\clubsuit}}}$ or
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{1}$.

###### Proof.

We will prove the following claim: either there exists contexts
$\Gamma,\Theta,\Delta,\Sigma$, where

$\displaystyle\Gamma$ $\displaystyle=\\{x_{1}\mapsto
Z_{1},x^{\prime}_{1}\mapsto Z_{1},\dots,x_{p}\mapsto
Z_{p},x^{\prime}_{p}\mapsto Z_{p}\\}$ $\displaystyle\Theta$
$\displaystyle=\\{w_{1}\mapsto W_{1},\dots,w_{q}\mapsto W_{q}\\}$
$\displaystyle\Delta$ $\displaystyle=\\{y_{1}\mapsto A^{*}\Rightarrow
Y_{1},\dots,y_{r}\mapsto A^{*}\Rightarrow Y_{r}\\}$ $\displaystyle\Sigma$
$\displaystyle=\\{z_{1}\mapsto\widetilde{\top}\Rightarrow
Y_{1},\dots,z_{r}\mapsto\widetilde{\top}\Rightarrow Y_{r}\\}$

for some $p,q,r\in\mathbb{N}$ and variables
$Z_{1},\dots,Z_{p},W_{1},\dots,W_{q},Y_{1},\dots,Y_{r}$ pairwise distinct and
disjoint from $A$, and a context
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{H}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}A^{*}$,
or
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{1}$. If the main claim is true we can deduce the statement of
the lemma as follows: suppose
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\notin\mathbb{G}_{1}$. Then let $\theta$ be the substitution sending all
variables in $\Gamma,\Theta,\Delta,\Sigma$ plus $Y$ onto $\clubsuit$ and being
the identity on all other variables. Then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{H}\theta}[\
]:((\clubsuit\Rightarrow
A)\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma\theta,\Theta\theta,\Delta\theta,\Sigma\theta}:\clubsuit\Rightarrow
A$. Then we have
$\Gamma\theta,\Theta\theta,\Delta\theta,\Sigma\theta\vdash{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}:A$,
where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{H}\theta}[\lambda
x.\mathbf{t}]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\star}$
and we can conclude that
$\vdash{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t^{\prime}}:A$
holds where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t^{\prime}}$
is obtained from
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}$
by substituting the variables in $\Gamma$ and $\Theta$ by $\star$ and those in
$\Delta$ and $\Sigma$ by $\lambda x.\star$.

Let us prove the main claim. Suppose by contradiction that for no
$\Gamma,\Theta,\Delta,\Sigma$ there exists a context
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{H}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}A^{*}$.
We will show by simultaneous induction the following claims:

  1. 1.

for all $\Gamma,\Theta,\Delta,\Sigma$ as above, if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}Z_{i}$,
then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{1}$;

  2. 2.

for all $\Gamma,\Theta,\Delta,\Sigma$ as above, if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}Y_{i}$,
then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{2}$;

  3. 3.

for all $\Gamma,\Theta,\Delta,\Sigma$ as above, if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}\mathsf{Bool}$
and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]$ is an elimination context, then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{3}$;

  4. 4.

for all $\Gamma,\Theta,\Delta,\Sigma$ as above, if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}W_{i}$,
then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{4}$.

The main claim then follows from 1. by taking $\Gamma=\\{x\mapsto
Z,x^{\prime}\mapsto Z\\}$ and $\Theta=\Delta=\Sigma=\emptyset$.

We argue for each case separately:

  1. 1.

There exist two possibilities for
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]$:

    1. (a)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x_{i}}$,
hence
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{1}$;

    2. (b)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}Z\mathtt{K}_{1}[\
]\mathtt{K}_{2}[\ ]}$, where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}\mathsf{Bool}$
and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}_{i}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}Z$,
and where $\mathtt{K}^{\prime}[\ ]$ is an elimination context. By the
induction hypothesis then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]\in\mathbb{G}_{3},\mathtt{K}_{i}[\ ]\in\mathbb{G}_{1}$, hence
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{1}$.

  2. 2.

There exist three possibilities for
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{D}}[\
]$:

    1. (a)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}y_{i}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}}[\
]$, where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}A^{*}$,
but this case is excluded by the hypothesis;

    2. (b)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]=z_{i}(\Lambda W.\lambda
w.{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
])$, where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta\cup\\{w\mapsto
W\\},\Delta,\Sigma}W$ and where $W$ does not occur in
$\Gamma,\Theta,\Delta,\Sigma$. By the induction hypothesis then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]\in\mathbb{G}_{4}$, hence
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{2}$;

    3. (c)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]Y_{i}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}_{1}}[\
]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}_{2}}[\
]$, where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}\mathsf{Bool}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}_{i}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}Y_{i}$,
and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]$ is an elimination context. By the induction hypothesis this implies
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]\in\mathbb{G}_{3}$ and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}_{i}}\in\mathbb{G}_{2}$,
so we can conclude
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{2}$.

  3. 3.

If $\mathtt{K}[\ ]$ is an elimination context, then it must be
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]=x{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]$, where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma\cup\\{x_{1}\mapsto
Z^{\prime},x_{2}\mapsto
Z^{\prime\prime}\\},\Theta,\Delta,\Sigma}A^{*}\widetilde{+}\widetilde{\top}$.
Moreover, $\mathtt{K}^{\prime}$ must be of the form $\Lambda Y.\lambda
y.\lambda z.\mathtt{K}^{\prime\prime}[\ ]$, where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma\cup\\{x_{1}\mapsto
Z^{\prime},x_{2}\mapsto Z^{\prime\prime}\\},\Theta,\Delta\cup\\{y\mapsto
A^{*}\Rightarrow Y\\},\Sigma\cup\\{z\mapsto\widetilde{\top}\Rightarrow
Y\\}}Y$, and where $Y$ is distinct from all variables in
$\Gamma\cup\\{x_{1}\mapsto Z^{\prime},x_{2}\mapsto
Z^{\prime\prime}\\},\Theta,\Delta,\Sigma$; then by the induction hypothesis we
deduce
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime\prime}}[\
]\in\mathbb{G}_{2}$, and thus
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{3}$.

  4. 4.

There are two possible cases:

    1. (a)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]=w_{i}$, hence
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{4}$;

    2. (b)

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}W_{i}\mathtt{K}_{1}\mathtt{K}_{2}}$,
where
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}\mathsf{Bool}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}_{i}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\Gamma,\Theta,\Delta,\Sigma}W_{i}$
and $\mathtt{K}^{\prime}[\ ]$ is an elimination context. By the induction
hypothesis this implies
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]\in\mathbb{G}_{3}$ and $\mathtt{K}_{i}\in\mathbb{G}_{4}$, whence
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]\in\mathbb{G}_{4}$.

∎

######  Proposition 6.3.

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}\not\simeq_{\mathsf{Bool}}^{{\mathrm{F_{at}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}$
iff $A$ is inhabited in ${\mathrm{F_{at}^{\clubsuit}}}$.

###### Proof.

Suppose $\vdash t:A$ holds in ${\mathrm{F_{at}^{\clubsuit}}}$, then by letting
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t^{*}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\lambda
y.t}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}y}/{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\star}]$
we deduce
$\vdash{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t^{*}}:A^{*}$
and we can show
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}\not\simeq_{\mathsf{Bool}}^{{\mathrm{F_{at}}}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}$,
by letting
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]=x({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\iota_{1}(t^{*})})$,
since
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathbf{f}}$
and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]\simeq_{\beta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathsf{IO}^{+}_{\mathsf{Bool}}[\iota_{1}(t^{*})](\lambda
x.\mathbf{t})(\lambda
x.\mathbf{f})}\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(\lambda
x.\mathbf{t})t^{*}}\simeq_{\beta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathbf{t}}$.

Conversely, suppose $A$ is not inhabited in ${\mathrm{F_{at}^{\clubsuit}}}$.
Any context
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{\emptyset}\mathsf{Bool}$
can be written, up to $\eta$-equivalence, as
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\Lambda
Z.\lambda
x_{1}x_{2}.}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]$, with
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]:(A^{*}\widetilde{+}\widetilde{\top})\Rightarrow\mathsf{Bool}\vdash^{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x_{1}}\mapsto
Z,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x_{2}}\mapsto
Z}\mathsf{Bool}$. As we can suppose
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[\
]$ to be $\beta$-normal, by Lemma 6.2, it must be
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}^{\prime}}[\
]\in\mathbb{G}_{1}$. Hence, by Lemma 6.1 we deduce that
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{K}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]$.
∎

######  Theorem 6.4.

The congruences $\simeq_{\mathsf{Bool}}^{{\mathrm{F_{at}}}}$ and
$\simeq_{\mathsf{Nat}}^{{\mathrm{F_{at}}}}$ are both undecidable.

##  7 Conclusion

#### Related works

The literature on ML-polymorphism, both at theoretical and applicative level,
is vast. Several extensions of ML to account for first-class polymorphism
while retaining a decidable type-checking have been investigated, mostly
following two directions: first, that of considering type systems with
explicit type annotations (as the system $\mathsf{PolyML}$ [20]); second, that
of encoding first-class polymorphism in a ML-style system by means of
_coercions_ (as in System $\mathrm{Fc}$ [59] or in in
$\mathrm{ML}^{\mathrm{F}}$ [30]). In the last case, coherently with our
discussion on FOU and SOU, the price to pay to remain decidable is that self-
applications of $\lambda$-abstracted variables must come with explicit type
annotations. This approach is currently followed in the design of the Haskell
compiler, which supports first-class polymorphism.

Predicative restrictions of System F and their expressive power have been also
largely investigated [32, 33, 6]. For example, the numerical functions
representable in Leivant’s finitely stratified polymorphism are precisely
those at the 3rd level of Grzegorczyk’s hierarchy [33], and transfinitely
stratified systems have been shown to represent all primitive recursive
functions [6]. In [34] a system with expressive power comparable to System
${\mathrm{F_{at}}}$ is shown to characterize the polytime functions.

Research by Ferreira and her collaborators on System ${\mathrm{F_{at}}}$ has
mostly focused on predicative translations of intuitionistic logic and their
reduction properties [12, 11, 10]. As mentioned before, these translations
rely on the observation that for certain types the unrestricted
$\forall$E-rule is admissible in ${\mathrm{F_{at}}}$. The characterization of
the class of types satisfying this property is an open problem (a partial
characterization is described in [46]).

Another way to obtain interesting subsystems of System F is by restricting the
class of types which can be universally quantified (instead of the admissible
witnesses). For instance, the system in [2] forbids quantifier nestings, while
the system in [35] only allows quantification $\forall X.A$ when $X$ occurs at
depth at most 2 in $A$ (i.e. when $X$ occurs at most twice to the left of an
implication). Interestingly, both systems have the expressive power of Gödel’s
System T (which is not a first-order system).

Another kind of restrictions on the shape of types have been investigated by
the authors in [49, 48], motivated by ideas from the categorical semantics of
polymorphism [3]. The two resulting fragments $\mathrm{F}^{\kappa\leq
0},\mathrm{F}^{\kappa\leq 1}$ are equivalent, respectively, to the simply
typed $\lambda$-calculus with finite sums and products, and to its extension
with least and greatest fixpoints (in particular, (CE) is decidable in
$\mathrm{F}^{\kappa\leq 0}$).

Finally, polymorphism in _linear_ type systems has been investigated too.
Interestingly, (TI) [28, 27] and (CE) [43] remain undecidable even in this
case.

#### Future work

The main interest we found in investigating ${\mathrm{F_{at}}}$ was to shed
some new light on the source of undecidability of type-related properties for
full System F. Yet, one might well ask whether the decidability of type-
checking makes ${\mathrm{F_{at}}}$ a reasonable candidate for implementations.
Admittedly, our decision algorithm, which was only oriented to prove
decidability, is not very practical: checking failure is $\mathsf{coNP}$ with
respect to the number of type symbols. Yet, it does not seems unlikely that
more optimized algorithms can be developed.

By the way, given that the terms typable in ${\mathrm{F_{at}}}$ are simply
typable, would an implementation of atomic polymorphism be interesting at all?
In contrast with $\mathrm{ML}$, type-checking atomically polymorphic programs
is decidable at any rank. One could thus investigate extensions of
$\mathrm{ML}$ with first class atomic polymorphism (realistically, in presence
of other type constructors like e.g. some restricted version of dependent
types, see [64]).

A more interesting direction, suggested by our decision algorithm, would be to
investigate systems with full, impredicative, polymorphism, but obeying some
condition ensuring _acyclicity_ , so that TC (based on SOU) remains decidable.
One would thus retain some advantages of first-class polymorphism (e.g. the
modularity/genericity of programs) while admitting self-applications only in
“$\mathrm{ML}$-style” (or with explicit type annotations, as in
$\mathrm{ML}^{\mathrm{F}}$ [30]). For instance, a way to ensure acycliclity
might be to require that a polymorphic $\lambda$-abstracted variable be used
in an _affine_ way, i.e. at most once.

## References

  * [1] Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler.  Theorems for free for free: parametricity, with and without types.  In Proceedings of the ACM on Programming Languages, volume 1 of ICFP, page Article No. 39, New York, 2017.
  * [2] Thorsten Altenkirch and Thierry Coquand.  A finitary subsystem of the polymorphic $\lambda$-calculus.  In Samson Abramsky, editor, Typed Lambda Calculi and Applications, pages 22–28, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg.
  * [3] E.S. Bainbridge, Peter J. Freyd, Andre Scedrov, and Philip J. Scott.  Functorial polymorphism.  Theoretical Computer Science, 70:35–64, 1990.
  * [4] Henk Barendregt.  Lambda calculi with types.  In Handbook of Logic in Computer Science, pages 117–309. Oxford University Press, 1992.
  * [5] Henk Barendregt, Wil Dekkers, and Richard Statman.  Lambda calculus with types.  Perspectives in Logic. Cambridge University Press, 2013.
  * [6] Norman Danner and Daniel Leivant.  Stratified polymorphism and primitive recursion.  Mathematical Structures in Computer Science, 9(4):507–522, 1999\.
  * [7] Kosta Došen and Zoran Petrić.  The typed Böhm theorem.  Electronic Notes in Theoretical Computer Science, 50(2):117–129, 2001.
  * [8] Andrej Dudenhefner and Jakob Rehof.  A simpler undecidability proof for system F inhabitation.  In TYPES 2018, pages 2:1–2:11, 2018.
  * [9] José Espírito Santo and Gilda Ferreira.  A refined interpretation of intuitionistic logic by means of atomic polymorphism.  Studia Logica, 108(3):477–507, 2020.  URL: https://doi.org/10.1007/s11225-019-09858-1, doi:10.1007/s11225-019-09858-1.
  * [10] José Espírito Santo and Gilda Ferreira.  The Russell-Prawitz embedding and the atomization of universal instantiation.  Logic Journal of the IGPL, 07 2020.  jzaa025.
  * [11] Fernando Ferreira and Gilda Ferreira.  Commuting conversions vs. the standard conversions of the ”good” connectives.  Studia Logica, 92(1):63–84, 2009.
  * [12] Fernando Ferreira and Gilda Ferreira.  Atomic polymorphism.  Journal of Symbolic Logic, 78(1):260–274, 2013.
  * [13] Fernando Ferreira and Gilda Ferreira.  The faithfulness of Fat: a proof-theoretic proof.  Studia Logica, 103(6):1303–1311, 2015.
  * [14] Gilda Ferreira.  $\eta$-conversions of IPC implemented in atomic F.  Logic Journal of the IGPL, 25(2):115–130, 06 2016.
  * [15] Gilda Ferreira and Bruno Dinis.  Instantiation overflow.  Reports on Mathematical Logic, 51:15–33, 2016.
  * [16] Gilda Ferreira and Vasco T Vasconcelos.  The computational content of atomic polymorphism.  Logic Journal of the IGPL, 27(5):625–638, 12 2018.
  * [17] Steven Fortune, Daniel Leivant, and Michael O’Donnell.  The expressiveness of simple and second-order type structures.  Journal of the ACM, 30(1):151–185, January 1983.
  * [18] Ken-etsu Fujita and Aleksy Schubert.  The undecidability of type related problems in the type-free style system F with finitely stratified polymorphic types.  Information and Computation, 218:69–87, 2012.
  * [19] Dov M. Gabbay.  Semantical Investigations in Heyting’s Intuitionistic Logic, volume 148.  Springer Science + Business, Dordrecht, 1981.
  * [20] Jacques Garrigue and Didier Rémy.  Extending ml with semi-explicit higher-order polymorphism.  In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, pages 20–46, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.
  * [21] Paola Giannini and Simona Ronchi Della Rocca.  Characterization of typings in polymorphic type discipline.  In Proceedings of the 3-th Annual IEEE Symposium on Logic in Computer Science, pages 61–70, Edinburgh, 1988.
  * [22] Warren D. Goldfarb.  The undecidability of the second-order unification problem.  Theoretical Computer Science, 13(2):225–230, 1981.
  * [23] Ryu Hasegawa.  Categorical data types in parametric polymorphism.  Mathematical Structures in Computer Science, 4(1):71–109, 2009\.
  * [24] Fritz Henglein.  Polymorphic type inference and semi-unification.  PhD thesis, The State University of New Jersey, 1989.
  * [25] Roger J. Hindley.  The principal type scheme of an object in combinatory logic.  Transactions of the American Mathematical Society, 146:29–60, 1069\.
  * [26] Assaf J. Kfoury, Jerzy Tiuryn, and Paweł Urzyczyn.  The undecidability of the semi-unification problem.  Information and Computation, 102(1):83–101, 1993.
  * [27] Yves Lafont.  The undecidability of second order linear logic without exponentials.  The Journal of Symbolic Logic, 61(02):541–548, June 1996.  doi:10.2307/2275674.
  * [28] Yves Lafont and Andre Scedrov.  The Undecidability of Second Order Multiplicative Linear Logic.  Information and Computation, 125(1):46–51, February 1996.  doi:10.1006/inco.1996.0019.
  * [29] Joachim Lambek and Philip J. Scott.  Introduction to higher order categorical logic.  Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1988.
  * [30] Didier Le Botlan and Didier Rémy.  Mlf: Raising ml to the power of system f.  In Proc. of the International Conference on Functional Programming (ICFP ’03), pages 27–38, 2003.
  * [31] R. D. Lee.  Decidable classes of recursive equations.  PhD thesis, University of Leicester, 1969.
  * [32] Daniel Leivant.  Stratified polymorphism.  In LICS ’89. Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE, 1989.
  * [33] Daniel Leivant.  Finitely stratified polymorphism.  Information and Computation, 93(1):93–113, 1991.
  * [34] Daniel Leivant.  A foundational delineation of Poly-time.  Information and Computation, 110(2):391–420, 1994.
  * [35] Daniel Leivant.  Peano’s lambda calculus: the functional abstraction implicit in arithmetic.  In Logic, meaning and computation, Essays in Memory of Alonzo Church, volume 305 of Synthese Library, Studies in Epistemology, Logic, Methodology and Philosophy of Science, pages 313–329. Springer Netherlands, 2001\.
  * [36] Jordi Levy.  Decidable and undecidable second-order unification problems.  In Tobias Nipkow, editor, Rewriting Techniques and Applications, pages 47–60, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.
  * [37] M. H. Löb.  Embedding First Order Predicate Logic in Fragments of Intuitionistic Logic.  PhD thesis.
  * [38] Jan Małolepszy, Małgorzata Moczurad, and Marek Zaionc.  Schwichtenberg-style lambda definability is undecidable.  In Philippe de Groote and J. Roger Hindley, editors, Typed Lambda Calculi and Applications, pages 267–283, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg.
  * [39] Paul-André Melliès and Noam Zeilberger.  Functors are type refinement systems.  In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pages 3–16, New York, NY, USA, 2015. Association for Computing Machinery.
  * [40] R. Milner and L. Damas.  The principal type schemes for functional programs.  In Symposium on Principles of Programming Languages, ACM, 1982.
  * [41] Robin Milner.  A theory of type polymorphism in programming.  Journal of Computer and System Science, 17(3):248–375, 1978.
  * [42] Robin Milner.  The standard ml core language.  Polymorphism, 2(2), 1985.
  * [43] Le Than Dung Nguyen, Paolo Pistone, Thomas Seiller, and Lorenzo Tortora de Falco.  Finite semantics of polymorphism, complexity and the expressive power of type fixpoints.  https://hal.archives-ouvertes.fr/hal-01979009, 2019.
  * [44] Vincent Padovani.  Filtrage d’ordre supérieur.  PhD thesis, Université Paris 7, 1996.
  * [45] Frank Pfenning.  On the undecidability of partial polymorphic type reconstruction.  Fundamenta Informaticae, 19(1-2):185–199, 1993.
  * [46] Paolo Pistone.  Proof nets and the instantiation overflow property.  https://arxiv.org/abs/1803.09297, 2018.
  * [47] Paolo Pistone and Luca Tranchini.  The naturality of natural deduction II. some remarks on atomic polymorphism.  https://arxiv.org/abs/1908.11353, 2020.
  * [48] Paolo Pistone and Luca Tranchini.  The Yoneda Reduction of Polymorphic Types (extended version).  https://arxiv.org/abs/1907.03481, 2020.
  * [49] Paolo Pistone and Luca Tranchini.  The Yoneda Reduction of Polymorphic Types.  In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1–35:22, Dagstuhl, Germany, 2021. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.
  * [50] Gordon Plotkin and Martin Abadi.  A logic for parametric polymorphism.  In TLCA ’93, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 361–375. Springer Berlin Heidelberg, 1993.
  * [51] M Clarence Protin.  Type inhabitation of atomic polymorphism is undecidable.  Journal of Logic and Computation, 01 2021.  exaa090.
  * [52] John C. Reynolds.  Types, abstraction and parametric polymorphism.  In R.E.A. Mason, editor, Information Processing ’83, pages 513–523. North-Holland, 1983.
  * [53] Aleksy Schubert, Paweł Urzyczyn, and Konrad Zdanowski.  On the Mints hierarchy in first-order intuitionistic logic.  Logical Methods in Computer Science, 12(4:11):1–25, 2016.
  * [54] Helmut Schwichtenberg.  Definierbare funktionen im $\lambda$-kalkül mit typen.  Archiv für mathematische Logik und Grundlagenforschung, 17(3):113–114, 1975.
  * [55] S. K. Sobolev.  The intuitionistic propositional calculus with quantifiers.  Mathematical Notes of the Academy of Sciences of the USSR, 22(528-532), 1977.
  * [56] Morten Heine Sorensen and Pawel Urzyczyn.  Lectures on the Curry-Howard isomorphism, volume 149 of Studies in logic and the foundations of mathematics.  Elsevier Science, 2006.
  * [57] R. Statman.  Completeness, invariance and $\lambda$-definability.  The Journal of Symbolic Logic, 47(1):17–26, 1982.
  * [58] Richard Statman.  intuitionistic propositional logic is polynomial-space complete.  Theoretical Computer Science, 9(1):67–72, 1979.
  * [59] Marin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly.  System f with type equality coercions.  In TLDI ’07 Proceedings of the 2007 ACM SIGPLAN Internatinal workshop in Types in languages design and implementation, pages 53–66. ACM New York, 2007.
  * [60] Luca Tranchini, Paolo Pistone, and Mattia Petrolo.  The naturality of natural deduction.  Studia Logica, https://doi.org/10.1007/s11225-017-9772-6, 2017\.
  * [61] J. Voigtländer.  Proving correctness via free theorems: the caser of the destroy/build-rule.  In Proceedings of the ACM SIGPLAN symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 13–20, New York, 2008\. ACM press.
  * [62] Philip Wadler.  Theorems for free!  In Proceedings of the fourth international conference on functinoal programming languages and computer architecture - FPCA ’89, 1989.
  * [63] J. B. Wells.  Typability and type checking in System F are equivalent and undecidable.  Annals of Pure and Applied Logic, 98:111–156, 1998.
  * [64] Hongwei Xi and Frank Pfenning.  Dependent types in practical programming.  In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’99, pages 214–227, New York, NY, USA, 1999. Association for Computing Machinery.

##  Appendix A ${\mathrm{F_{at}}}$-unification

In this section we describe a decidable unification problem, that we call
${\mathrm{F_{at}}}$-unification, and we show that this problem captures type-
checking for ${\mathrm{F_{at}}}$.

#### A decidable second-order unification problem

We consider a second-order language composed out of three different sorts of
variables: _sequence variables_ $a,b,c,\dots$, _projection variables_
$\alpha^{n},\beta^{n},\gamma^{n},\dots$ and _second-order variables_
$\mathsf{F}^{n},\mathsf{G}^{n},\dots$ (where in the last two cases $n$
indicates the arity of the variable). The language includes expressions of
three sorts, noted $\langle*\rangle$, $*$ and $T(*)$; the expressions of each
type are defined by the grammars below:

$\displaystyle\mathfrak{a},\mathfrak{b},\mathfrak{c}$ $\displaystyle::=\langle
X_{1}\dots X_{n}\rangle\mid a\mid\alpha^{n}a_{1}\dots a_{n}$
$\displaystyle\qquad(\text{sort }\langle*\rangle)$ $\displaystyle\phi,\psi$
$\displaystyle::=X\mid\pi^{l}(\mathfrak{a})\mid\mathsf{F}^{n}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}\mid\Phi\Rightarrow\Psi$
$\displaystyle\qquad(\text{sort }*)$ $\displaystyle\Phi,\Psi$
$\displaystyle::=\forall a.\phi$ $\displaystyle\qquad(\text{sort }T(*))$

A _${\mathrm{F_{at}}}$ -unification problem_ is a pair $(U,E)$, where $U$ is a
set of equations of the form $t=u$ between expressions of type $*$, and $E$ is
a set of _constraints_ of the form $(\alpha:a)$ or $(a:k)$, where
$k\in\mathbb{N}$.

Given a ${\mathrm{F_{at}}}$-unification problem $(U,E)$, for all projection
variable $\alpha^{n}$ occurring in $U$, let $\deg(\alpha)$ indicate the
maximum value $u$ such that $\pi^{u}(\alpha^{n}a_{1}\dots a_{n})$ occurs in
$U$.

A _substitution_ for a ${\mathrm{F_{at}}}$-unification problem $(U,E)$ is
given by the following data:

  * •

for each sequence variable $a$, a natural number $k_{a}^{S}\in\mathbb{N}$;

  * •

for each projection variable $\alpha^{n}$, a pair $(k_{\alpha}^{S},S(\alpha))$
made of a natural number $k_{\alpha}^{S}\geq\deg(\alpha)$ and a sequence
$S(\alpha)=\langle S(\alpha)_{1},\dots,S(\alpha)_{k_{\alpha}^{S}}\rangle$,
where $S(\alpha)_{i}$ is either of the form $\lambda x_{1}.\dots.x_{n}.X$ or
of the form $\lambda x_{1}.\dots.x_{n}.\pi^{l}(x_{j})$, where $l$ is such
that, whenever $\pi^{u}(\alpha^{n}a_{1}\dots a_{n})$ occurs in $U$, $l\leq
k_{a_{j}}^{S}$;

  * •

for each second-order variable $\mathsf{F}^{n}$, a function $S(\mathsf{F})$ of
the form $\lambda\rho_{1}.\dots.\rho_{n}.A(\rho_{1},\dots,\rho_{n})$, where
$A(\rho_{1},\dots,\rho_{n})$ is given by the grammar

$A,B::=X\mid\pi^{l}(\rho_{i})\mid A\Rightarrow B\mid\forall X.A$

with $i\leq n$ and $l$ such that, if
$\mathsf{F}^{n}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}$ occurs in $U$, then
$l\leq k_{\mathfrak{a}_{i}}^{S}$ (where $k_{\mathfrak{a}}^{S}$ is $k$ if
$\mathfrak{a}=\langle X_{1},\dots,X_{k}\rangle$, is $k_{a}^{S}$ if
$\mathfrak{a}=a$, and is $k_{\alpha}^{S}$ if
$\mathfrak{a}=\alpha^{r}a_{1}\dots a_{r}$).

Given a substitution $S$, we define (1) for any expression $\mathfrak{a}$ of
sort $\langle*\rangle$, a sequence $S(\mathfrak{a})$ of type variables, (2)
for any expression $\phi$ of sort $*$, a type $S(\phi)$, and (3) for any
expression $\Phi$ of sort $T(*)$, a type $S(\Phi)$ as follows:

  * •

if $\mathfrak{a}=a$, $S(a)$ is a sequence of pairwise distinct variables
$\langle S(a)_{1},\dots,S(a)_{k_{a}}\rangle$ (chosen in such a way that if
$a\neq b$, $S(a)$ and $S(b)$ are disjoint);

  * •

if $\mathfrak{a}=\langle X_{1},\dots,X_{r}\rangle$, then
$S(\mathfrak{a})=\langle X_{1},\dots,X_{r}\rangle$;

  * •

if $\mathfrak{a}=\alpha^{n}a_{1}\dots a_{n}$, then $S(\mathfrak{a})=\langle
U_{1},\dots,U_{k_{\alpha}^{S}}\rangle$ where for all $i\leq k_{\alpha}^{S}$:

    * –

if $S(\alpha)_{i}=\lambda\vec{x}.X$, then $U_{i}=X$;

    * –

if $S(\alpha)_{i}=\lambda\vec{x}.\pi^{l}(x_{j})$, then $U_{i}=S(a_{j})_{l}$;

  * •

if $\phi=X$, then $S(\phi)=X$;

  * •

if $\phi=\pi^{l}(\mathfrak{a})$, then $S(\phi)=S(\mathfrak{a})_{l}$;

  * •

if $\phi=\mathsf{F}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}$, and
$S(\mathsf{F})=\lambda\vec{\rho}.A$, then $S(\phi)=A[\pi^{l}(\rho_{i})\mapsto
S(\mathfrak{a}_{i})_{l}]$;

  * •

if $\phi=\Phi\Rightarrow\Psi$, then $S(\phi)=S(\Phi)\Rightarrow S(\Psi)$;

  * •

if $\Phi=\forall a.\phi$, then $S(\Phi)=\forall S(a).S(\phi)$.

A substitution $S$ for $(U,E)$ is a _unifier_ of $(U,E)$ if the following
hold:

  1. 1.

for any equation $t=u\in U$, $S(t)=S(u)$ holds;

  2. 2.

for any constraint of the form $\alpha:a\in E$, $k_{a}^{S}=k_{\alpha}^{S}$;

  3. 3.

for any constraint of the form $a:k\in E$, $k_{a}^{S}=k$.

We let _$\mathtt{Fat}$ -$\mathtt{unification}$_ indicate the problem of
finding a unifier for a ${\mathrm{F_{at}}}$-unification problem. The rest of
this subsection is devoted to establish the following:

######  Theorem A.1.

$\mathtt{Fat}$-$\mathtt{unification}$ is decidable.

A ${\mathrm{F_{at}}}$-unification problem $(U,E)$ is in _normal form_ if if
contains no equation of the form
$\Phi_{1}\Rightarrow\Psi_{1}=\Phi_{2}\Rightarrow\Psi_{2}$. Any unification
problem can be put in normal form by repeatedly applying the following
simplification rule:

$U+\\{(\forall a_{1}.\phi_{1})\to(\forall b_{1}.\psi_{1})=(\forall
a_{2}.\phi_{2})\to(\forall b_{2}.\psi_{2})\\}$
$\big{(}U+\\{\phi_{1}=\phi_{2},\psi_{1}=\psi_{2}\\}\big{)}\big{[}a_{2}\mapsto
a_{1},b_{2}\mapsto b_{1}\big{]}$

Given a ${\mathrm{F_{at}}}$-unification problem in normal form $(U,E)$, we say
that an equation $t=u$ _can be deduced from $U$_ if $t=u$ can be deduced from
a finite set of equations in $U$ by applying standard first-order equality
rules. We say that two second-order variables $\mathsf{F},\mathsf{G}$ are
_equivalent_ (noted $\mathsf{F}\simeq\mathsf{G}$) if an equation of the form
$\mathsf{F}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}=\mathsf{G}\mathfrak{b}_{1}\dots\mathfrak{b}_{n}$
can be deduced from $U$; we say that $\mathsf{F}$ is _connected with
$\mathsf{G}$_ (noted $\mathsf{F}\leadsto\mathsf{G}$) if an equation of the
form $\mathsf{F}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}=\Phi\Rightarrow\Psi$,
where $\mathsf{U}$ occurs in $\Phi\Rightarrow\Psi$, can be deduced from $U$.
We say that $(U,E)$ has a _variable cycle_ if there exist variables
$\mathsf{F}_{1},\dots,\mathsf{F}_{k}$ such that
$\mathsf{F}_{1}\stackrel{{\scriptstyle\simeq}}{{\leadsto}}\mathsf{F}_{2}\stackrel{{\scriptstyle\simeq}}{{\leadsto}}\dots\stackrel{{\scriptstyle\simeq}}{{\leadsto}}\mathsf{F}_{n}\stackrel{{\scriptstyle\simeq}}{{\leadsto}}\mathsf{F}_{1}$
(where $\mathsf{F}\stackrel{{\scriptstyle\simeq}}{{\leadsto}}\mathsf{G}$ means
that $\mathsf{F}$ is connected with some variable equivalent to $\mathsf{G}$).

######  Lemma A.2.

Let $(U,E)$ be a unification problem in normal form. If $(U,E)$ has a variable
cycle, then it has no solution.

###### Proof.

To prove the lemma we show that any unification problem $(U,E)$ yields a
_first-order_ unification problem $U^{*}$ and that any unifier of $(U,E)$
yields a unifier of $U^{*}$. For the translation, we fix a constant $c$, and
we associate any second-order variable $\mathsf{F}$ with a first-order
variable $x_{\mathsf{F}}$; any expression is translated into a first order
expression by:

$\displaystyle\mathfrak{a}^{*}$ $\displaystyle=c$
$\displaystyle\mathsf{F}^{n}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}$
$\displaystyle=x_{\mathsf{F}}$ $\displaystyle(\Phi\Rightarrow\Psi)^{*}$
$\displaystyle=\Phi^{*}\Rightarrow\Psi^{*}$ $\displaystyle(\forall
a.\phi)^{*}$ $\displaystyle=\phi^{*}$

We finally let $U^{*}=\\{t^{*}=u^{*}\mid t=u\in U\\}$. Observe that if
$\mathsf{F}\simeq\mathsf{G}$ in $U$, then $x_{\mathsf{F}}=x_{\mathsf{G}}$ in
$U^{*}$, and if $\mathsf{F}\leadsto\mathsf{G}$ in $U$, then $U^{*}$ contains
an equation of the form $x_{\mathsf{F}}=t\Rightarrow u$, where
$x_{\mathsf{G}}$ occurs in $t\Rightarrow u$. Hence a variable cycle in $(U,E)$
induces a variable cycle in $U^{*}$.

For any substitution $S$ for $(U,E)$, we define a first-order substitution
$S^{*}$ as follows: given $\lambda\vec{\rho}.A$ we define $A^{*}$ by
$X^{*}=c$, $(\pi^{l}(\rho_{i}))^{*}=c$, $(A\Rightarrow B)^{*}=A^{*}\Rightarrow
B^{*}$ and $(\forall X.A)^{*}=A^{*}$. We let then
$S^{*}(x_{\mathsf{F}})=S(\mathsf{F})^{*}$.

One can easily check that if $S$ is a unifier for $(U,E)$, then $S^{*}$ is a
unifier of $U^{*}$. As a consequence, if $(U,E)$ has a variable cycle, so does
$U^{*}$, and by well-known facts about first-order unification, $U^{*}$ has no
unifier, and so neither $(U,E)$ does. ∎

Let us call a unification problem $(U,E)$ _simple_ if it contains no
expression of the form $\Phi\Rightarrow\Psi$. If $(U,E)$ has no variable
cycle, then it can be reduced to a simple unification problem by applying the
following rules:

$U+\\{\pi^{l}(\mathfrak{a})=\Phi\Rightarrow\Psi\\}$ $\\{X=Y\\}$
$U+\\{\mathsf{F}^{n}\mathfrak{a}_{1}^{1}\dots\mathfrak{a}_{n}^{1}=(\forall
c_{1}.\phi_{1})\Rightarrow(\forall
d_{1}.\psi_{1}),\dots,\mathsf{F}^{n}\mathfrak{a}_{1}^{r}\dots\mathfrak{a}_{n}^{r}=(\forall
c_{r}.\phi_{r})\Rightarrow(\forall d_{r}.\psi_{r})\\}$
$U\Big{[}\mathsf{F}^{n}\vec{\mathfrak{a}}\mapsto(\mathsf{F}_{1}^{n+1}\vec{\mathfrak{a}}c\Rightarrow\mathsf{F}_{2}^{n+1}\vec{\mathfrak{a}}d)\Big{]}+\left\\{\begin{matrix}\mathsf{F}_{1}^{n+1}\mathfrak{a}_{1}^{1}\dots\mathfrak{a}_{n}^{1}c_{1}=\phi_{1},\dots,\mathsf{F}_{1}^{n+1}\mathfrak{a}_{1}^{r}\dots\mathfrak{a}_{n}^{r}c_{r}=\phi_{r}\\\
\mathsf{F}_{2}^{n+1}\mathfrak{a}_{1}^{1}\dots\mathfrak{a}_{n}^{1}d_{1}=\psi_{1},\dots,\mathsf{F}_{2}^{n+1}\mathfrak{a}_{1}^{r}\dots\mathfrak{a}_{n}^{r}d_{r}=\psi_{r}\end{matrix}\right\\}$

Where in the first two rules we let $Y$ be any type variable distinct from
$X$, and in the last rule we suppose that $U$ contains no equation of the form
$\mathsf{F}^{n}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}=\Phi\Rightarrow\Psi$.
Observe that, by acycliclity, $\mathsf{F}$ cannot occur in either $\phi_{i}$
or $\psi_{i}$. One can argue by induction on the well-founded preorder
$\stackrel{{\scriptstyle\simeq}}{{\leadsto}}$ that one can eliminate all terms
of the form $\Phi\Rightarrow\Psi$ by applying a finite number of instances of
the rules above.

The last step to ensure decidability is the following:

######  Proposition A.3.

There is an algorithm that generates all unifiers of a simple unification
problem, if there exists any, and returns $\mathtt{failure}$ otherwise.

###### Proof.

We first describe an algorithm which generates non-deterministically all
unifiers. We will then show that the search space for unifiers can be
restricted to a finite one, allowing thus also to check if no unifier exists.

The algorithm is as follows:

  1. 1.

Proceed non-deterministically by applying the following rules:

    1. (a)

if $\pi^{j}(\alpha^{n}a_{1}\dots a_{n})=u$ occurs in $U$, then choose a
natural number $q$, set $S(\alpha)_{j}=\lambda\vec{x}.\pi^{q}(a_{j})$,
eliminate this equation and replace in all other equations any term of the
form $\alpha^{n}b_{1}\dots b_{n}$ with $\pi^{q}(b_{j})$;

    2. (b)

if $\pi^{j}(\alpha^{n}a_{1}\dots a_{n})=u$, then set $S(\alpha)_{j}=X$, where
$X$ is either a variable occurring in $U$ or a fresh variable, eliminate this
equation and replace in all other equations any term of the form
$\pi^{l}(\alpha^{n}b_{1}\dots b_{n})$ by $X$;

    3. (c)

if $\mathsf{F}^{n}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}=u$ is in $U$, then
choose a natural number $q$ and set
$S(\mathsf{F})=\lambda\vec{x}.\pi^{q}(x_{j})$, eliminate this equation and
replace in all other equations any term of the form
$\mathsf{F}^{n}\mathfrak{b}_{1}\dots\mathfrak{b}_{n}$ by
$\pi^{q}(\mathfrak{b}_{j})$;

    4. (d)

if $\mathsf{F}^{n}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}=u$ is in $U$, then set
$S(\mathsf{F})=\lambda\vec{x}.X$, where $X$ is either a variable already
occurring in $U$ or a fresh variable, eliminate this equation and replace in
all other equations any term of the form
$\mathsf{F}^{n}\mathfrak{b}_{1}\dots\mathfrak{b}_{n}$ by $X$.

  2. 2.

Observe that any rule eliminates one equation, so after a finite number of
steps one is left with only equations of the form $\mathfrak{a}=\mathfrak{b}$,
where $\mathfrak{a},\mathfrak{b}$ are either type variables or of the form
$\pi^{l}(b)$, for some sequence variable $b$. If from such equations one can
deduce either $X=Y$ for distinct type variables $X,Y$, or
$\pi^{l}(a)=\pi^{r}(b)$, where either $a\neq b$ or $a=b$ and $l\neq r$, then
return $\mathtt{local\ failure}$;

  3. 3.

otherwise, set $k_{a}^{S}$ any number greater or equal to all expression
$\pi^{l}(a)$ occurred during the computation, and set $k_{\alpha}^{S}$ is a
similar way. Adjust $k_{a}^{S},k_{\alpha}^{S}$, if possible, in order to
satisfy the constraints in $E$. If this is not possible (i.e. if $E$ contains
$(a:k)$ and an expression $\pi^{l}(a)$, with $l>k$, occurred in the
computation, or if $E$ further contains $(\alpha:a)$ and an expression
$\pi^{l}(\alpha^{r}a_{1}\dots a_{r})$, with $l>k$, occurred during the
computation), return $\mathtt{local\ failure}$. Otherwise, for all $l\leq
k_{\alpha}^{S}$ such that $\pi^{l}(a)$ never occurred, choose $S(\alpha)_{l}$
randomly;

  4. 4.

if some non-deterministic branch generated by steps 2. and 3. ends without
returning $\mathtt{local\ failure}$, then return $\mathtt{success}$.

It is clear that any succeeding path yields a unifier for $(U,E)$. Conversely,
if $S$ is a unifier of $(U,E)$, then one can easily see, by induction on the
number of equations of $U$, that $S$ is produced by some succeeding path of
the algorithm.

Now suppose that $S$ is a unifier and that $S$ is produced through a finite
number of computation steps $s_{1},\dots,s_{N}$, where
$N\leq\mathsf{card}(U)$. Let $K$ be the smallest natural number such that for
all sequence $\langle X_{1},\dots,X_{r}\rangle$ in $U$ and equation of the
form $\pi^{l}(\mathfrak{a})=\phi$ in $U$, $r,l\leq K$, and for all constraint
of the form $(a:k)$, $k\leq K$. Then we can replace each choice of a natural
number $q$ at steps 1a and 1c by some $q^{\prime}\leq K+N$ (in fact we need no
more than $N$ different values distinct from any index already occurring
somewhere in $U$).

Thus we can define a new algorithm which runs all (finitely many) computations
with search-space restricted to $K+N$, and returns $\mathtt{success}$ if one
of them succeeds, and returns $\mathtt{failure}$ if all of them return a
$\mathtt{local\ failure}$. ∎

#### Type-checking ${\mathrm{F_{at}}}$ by second-order unification

A _type-checking problem_ is a triple $(\Gamma,t,A)$ where $\Gamma$ is a term
context, $t$ is a $\lambda$-term with $FV(t)\subseteq\Gamma$ and $A$ is a
type. A _${\mathrm{F_{at}}}$ -solution_ of a type-checking problem is a type
derivation in ${\mathrm{F_{at}}}$ of $\Gamma\vdash t:A$. We wish to prove the
following:

######  Theorem A.4.

For any type-checking problem $(\Gamma,t,A)$, there exists a
${\mathrm{F_{at}}}$-unification problem $\mathbf{V}(\Gamma,t,A)$ such that
$(\Gamma,t,A)$ has a solution in ${\mathrm{F_{at}}}$ iff
$\mathbf{V}(\Gamma,t,A)$ has a unifier.

The first step is to associate with each term $t$ finite sets of sequence
variables, projection variables and second-order variables as follows (we
suppose that no variable occurs both free and bound in $t$, and that any bound
variable is bound exactly once):

  * •

with each variable $x$ in $t$, we associate two sequence variables
$a_{x},b_{x}$, a projection variable $\alpha^{1}_{x}$, and two second-order
variables $\mathsf{F}^{1}_{x},\mathsf{G}^{1}_{x}$;

  * •

with each subterm of $t$ of the form $uv$, we similarly associate two sequence
variables $a_{uv},b_{uv}$, a projection variable $\alpha_{uv}^{1}$ and two
second-order variables $\mathsf{F}^{2}_{uv},\mathsf{G}^{1}_{uv}$;

  * •

with each subterm of $t$ of the form $\lambda x.u$, we associate a sequence
variable $b_{\lambda x.u}$, and a second order variable
$\mathsf{G}^{1}_{\lambda x.t}$.

Given a set of equations $U$ and a sequence variable $a$ not occurring in $U$,
we let $Ua$ be the set of equations obtained by replacing all terms
$\alpha^{n}a_{1}\dots a_{n}$ by $\alpha^{n+1}a_{1}\dots a_{n}a$ and all term
$\mathsf{F}^{n}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}$ by
$\mathsf{F}^{n+1}\mathfrak{a}_{1}\dots\mathfrak{a}_{n}a$.

We define a set of equations $\mathbf{U}(t)$, by induction on $t$ as follows:

  * •

$\mathbf{U}(x)$ is formed by the equation

$\displaystyle\mathsf{F}_{x}(\alpha_{x}b_{x})$
$\displaystyle=\mathsf{G}_{x}b_{x}$

  * •

$\mathbf{U}(\lambda x.t)$ is formed by $\mathbf{U}(t)b_{\lambda x.t}$ plus the
equations

$\displaystyle\mathsf{G}_{\lambda x.t}b_{\lambda x.t}$ $\displaystyle=(\forall
a_{x}.\mathsf{F}_{x}a_{x}\vec{b}b_{\lambda x.t})\Rightarrow\forall
b_{t}.\mathsf{G}_{t}b_{t}b_{\lambda x.t}$

  * •

$\mathbf{U}(tu)$ is formed by $\mathbf{U}(t)b_{tu},\mathbf{U}(u)b_{tu}$ plus
the equations:

$\displaystyle\mathsf{G}_{t}b_{t}b_{tu}$ $\displaystyle=(\forall
b_{u}.\mathsf{G}_{u}b_{u}b_{tu})\Rightarrow(\forall
a_{tu}.\mathsf{F}_{tu}a_{tu}b_{tu})$
$\displaystyle\mathsf{F}_{tu}(\alpha_{tu}b_{tu})b_{tu}$
$\displaystyle=\mathsf{G}_{tu}b_{tu}$

We let
$\mathbf{V}(\Gamma,t,A)=(\mathbf{U}(\Gamma,t,A),\mathbf{E}(\Gamma,t,A))$,
where $\mathbf{U}(\Gamma,t,A)$ is the union of $\mathbf{U}(t)$ and all
equations $\forall a_{x}.\mathsf{F}_{x}=\Gamma(x)$ and $\forall
b_{t}.\mathsf{G}_{t}b_{t}=A$. $\mathbf{E}(\Gamma,t,A)$ is formed by all
constraints of the form $(\alpha_{x}:a_{x})$ and $(\alpha_{tu}:b_{t})$, as
well as all constraints of the form $(a_{x}:k)$, where $\Gamma(x)=\forall
X_{1}\dots X_{k}.C$, all constraints of the form $(b_{u}:0)$ where $t$
contains a subterm of the form $uv$, and the constraint $(b_{t},h)$, where
$A=\forall X_{1}\dots X_{h}.A^{\prime}$.

To show that solving $\mathbf{V}(\Gamma,t,A)$ is equivalent to checking if
$\Gamma\vdash t:A$, as in [21], we first define synthetic typing rules for
Curry-style ${\mathrm{F_{at}}}$ as shown in Fig. 4, where $A\preceq B$ holds
when $A=\forall X_{1}\dots X_{n}.A$ and $B=A[X_{1}\mapsto
Y_{1},\dots,X_{n}\mapsto Y_{n}]$.

$\begin{matrix}\ \\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.57222pt\hbox{\vbox{\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma(x)=A$}\hskip
4.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip 4.0pt\hbox{$A\preceq B$}\hskip
4.0pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to99.95013pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt$\vec{X}\notin FV(\Gamma)$}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
17.12453pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash
x:\forall\vec{X}:B$}\hskip 4.0pt}}}}}\ignorespaces\\\ \ \\\
\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.57222pt\hbox{\vbox{\hbox{\hskip 15.35243pt\hbox{\hskip
4.0pt\hbox{$\Gamma,x:A\vdash t:B$}\hskip
4.0pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to101.53435pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt$\vec{X}\notin
FV(\Gamma)$}}\vskip-2.8pt\nointerlineskip\hbox{\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash\lambda x.t:\forall\vec{X}.A\Rightarrow B$}\hskip
4.0pt}}}}\ignorespaces\\\ \ \\\
\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
24.57222pt\hbox{\vbox{\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash
t:A\Rightarrow B$}\hskip 4.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip
4.0pt\hbox{$\Gamma\vdash u:A$}\hskip 4.0pt}\hbox{\hskip
14.45377pt}\hbox{\hskip 4.0pt\hbox{$B\preceq C$}\hskip
4.0pt}}\vskip-2.8pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to182.66753pt{\xleaders\hrule\hfill}\lower 2.3pt\hbox{\hskip
3.0pt$\vec{X}\notin FV(\Gamma)$}}\vskip-2.8pt\nointerlineskip\hbox{\hskip
57.3407pt\hbox{\hbox{\hskip 4.0pt\hbox{$\Gamma\vdash
tu:\forall\vec{X}.C$}\hskip 4.0pt}}}}}\ignorespaces\\\ \ \\\ \end{matrix}$

Figure 4: Synthetic typing rules for Curry-style ${\mathrm{F_{at}}}$.

One can check by induction on $t$ that a synthetic type derivation of
$\Gamma\vdash t:A$ yields a unifier of $\mathbf{V}(\Gamma,t,A)$. Conversely,
we show that from a unifier $S$ for $\mathbf{V}(\Gamma,t,A)$ we can construct
a synthetic typing derivation of $\Gamma\vdash t:A$. We argue by induction on
$t$:

  * •

if $t=x$, then we have $\Gamma(x)=\forall X_{1}\dots
X_{N}.S(\mathsf{F}_{x})\vec{X}$, where $N=k_{a_{x}}^{S}$, $A=\forall
Y_{1}\dots Y_{P}.S(\mathsf{G}_{x})\vec{Y}$, where $P=k_{b_{x}}^{S}$, and
moreover,
$S(\mathsf{F}_{x})(S(\alpha_{x})_{1}\vec{Y})\dots(S(\alpha_{x})_{N}\vec{Y})=S(\mathsf{G}_{x})\vec{Y}$
(using the fact that $k_{\alpha_{x}}^{S}=k_{a_{x}}^{S}=N$). Observe that
$(S(\alpha_{x})_{j}\vec{Y})$ is a variable, and we deduce then that
$\Gamma(x)\preceq S(\mathsf{G}_{x})\vec{Y}$; since we can suppose that
$\vec{Y}$ does not occur in $\Gamma$, we deduce then that

$\Gamma(x)=\forall\vec{X}.S(\mathsf{F}_{x})\vec{X}$
$\forall\vec{X}.S(\mathsf{F}_{x})\vec{X}\preceq S(\mathsf{G}_{x})\vec{Y}$
$\vec{Y}\notin FV(\Gamma)$ $\Gamma\vdash x:A$

  * •

if $t=\lambda x.u$, then we have that $A=\forall X_{1}\dots X_{N}.(\forall
Y_{1}\dots Y_{P}.S(\mathsf{F}_{x})\vec{Y}\vec{X})\Rightarrow\forall Z_{1}\dots
Z_{Q}.S(\mathsf{G}_{u})\vec{Z}\vec{X}$, where $N=k_{b_{\lambda x.t}}^{S}$,
$P=k_{a_{x}}^{S}$, $Q=k_{b_{u}}^{S}$ and where we can suppose that the $X_{i}$
do not occur free in $\Gamma$; since since $\mathsf{U}(\lambda
x.t)=\mathsf{U}(t)a_{\lambda x.t}$ we deduce that $S$ unifies
$\mathbf{V}(\Gamma\cup\\{x:A_{1}\\},u,A_{2}))$. By I.H. we deduce then the
existence of a type derivation of $\Gamma,x:A_{1}\vdash u:A_{2}$, and since
the $X_{i}$ do not occur in $\Gamma$ we finally have

[I.H.] $\Gamma,x:A_{1}\vdash u:A_{2}$ $\vec{X}\notin FV(\Gamma)$ $\Gamma\vdash
t:A$

  * •

if $t=uv$, then we have that $A=\forall X_{1}\dots
X_{n}.S(\mathsf{G}_{uv})\vec{X}$, $S(\mathsf{G}_{u})\vec{X}=(\forall
Y_{1}\dots Y_{P}.S(\mathsf{G}_{v})\vec{Y}\vec{X})\Rightarrow(\forall
Z_{1}\dots Z_{Q}.S(\mathsf{F}_{uv})\vec{Z}\vec{X})$ and that
$S(\mathsf{F}_{uv})(S(\alpha_{uv})_{1}\vec{X})\dots(S(\alpha_{uv})_{N}\vec{X})\vec{X}=S(\mathsf{G}_{uv})\vec{X}$,
where $N=k_{b_{uv}}^{S}$, $P=k_{b_{u}}^{S}$ and $Q=k_{a_{uv}}^{S}$, and where
we use the fact that $k_{b_{u}}^{S}=0$. Moreover, for any choice of the
variables $\vec{X}$, we have that $S$ unifies $\mathbf{V}(\Gamma,u,(\forall
Y_{1}\dots Y_{P}.S(\mathsf{G}_{v})\vec{Y}\vec{X})\to\forall Z_{1}\dots
Z_{Q}.S(\mathsf{F}_{uv})\vec{Z}\vec{X})$ and $\mathbf{V}(\Gamma,v,\forall
Y_{1}\dots Y_{P}.S(\mathsf{G}_{u})\vec{Y}\vec{X})$; by choosing the $\vec{X}$
so that they do not occur free in $\Gamma$, using the I.H. and the fact that
$k_{\alpha_{uv}}^{S}=k_{a_{uv}}^{S}=Q$, we deduce then

[I.H.] $\Gamma\vdash u:(\forall Y_{1}\dots
Y_{P}.\mathsf{G}_{v}^{S}\vec{Y}\vec{X})\to(\forall Z_{1}\dots
Z_{Q}.S(\mathsf{F}_{uv})\vec{Z}\vec{X})$ [I.H.] $\Gamma\vdash v:\forall
Y_{1}\dots Y_{P}.S(\mathsf{G}_{v})\vec{Y}\vec{X}$ $\forall Z_{1}\dots
Z_{Q}.S(\mathsf{F}_{tu})\preceq S(\mathsf{G}_{tu})\vec{X}$ $\vec{X}\notin
FV(\Gamma)$ $\Gamma\vdash t:A$

##  Appendix B Bounded Multiplication in $\mathrm{ML}$

We show that the numerical functions representable in $\mathrm{ML}$ are closed
under bounded multiplication: if the function $g:\mathbb{N}\to\mathbb{N}$ is
representable, then also the function $f:\mathbb{N}\to\mathbb{N}$ defined by
$f(n)=\prod_{k\leq n}g(k)$ is representable.

The first step is to define an encoding of pairs inside ${\mathrm{ST\lambda
C}}$. Let $A,B$ be two simple types, and let $\langle
A,B\rangle:=(A\Rightarrow B\Rightarrow o)\Rightarrow o$. We let $\langle
t,u\rangle$ be the term $\lambda f.ftu$. We define the projections
$\mathsf{P}_{1}^{A}:\langle A,B\rangle\Rightarrow A$ and
$\mathsf{P}_{2}^{B}:\langle A,B\rangle\Rightarrow B$ by essentially following
the predicative encoding of products in ${\mathrm{F_{at}}}$. We first define a
term $\mathsf{T}^{C}:\langle A,B\rangle\Rightarrow(A\Rightarrow B\Rightarrow
C)\Rightarrow C$ by induction on a simple type $C$ as follows:

  * •

if $C=o$, then $\mathsf{T}^{C}=\lambda gh.gh$;

  * •

if $C=C_{1}\Rightarrow C_{2}$, then $\mathsf{T}^{A}=\lambda
ghz.\mathsf{T}^{A_{2}}g(\lambda ab.habz)$.

We finally let $\mathsf{P}_{1}^{A}:=\mathsf{T}^{A}\lambda xy.x$ and
$\mathsf{P}_{2}^{B}=\mathsf{T}^{B}\lambda xy.y$. This definition can be
straightforwardly extended to $n$-ary products $\langle
A_{1},\dots,A_{n}\rangle$, with projection functions
$\mathsf{P}_{i,n}^{A_{i}}:\langle A_{1},\dots,A_{n}\rangle\Rightarrow A_{i}$.

We furthermore exploit the following standard result (see [33]):

######  Lemma B.1.

For all $\beta$-normal term $t$, $\vdash
t:\mathsf{Nat}\Rightarrow\mathsf{Nat}$ holds in $\mathrm{ML}$ iff there exists
$k\in\mathbb{N}$, a term $t^{*}$ and simple types $A_{1},\dots,A_{k}$ such
that:

  * •

$\vdash
t^{*}:\mathsf{Nat}[A_{1}]\Rightarrow\dots\Rightarrow\mathsf{Nat}[A_{k}]\Rightarrow\mathsf{Nat}[o]$
holds in ${\mathrm{ST\lambda C}}$;

  * •

$t^{*}x\dots x\simeq_{\beta}tx$,

where $\mathsf{Nat}[A]=(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$.

Let $g:\mathbb{N}\to\mathbb{N}$ be a function represented in $\mathrm{ML}$ by
some term $t_{g}:\mathsf{Nat}\Rightarrow\mathsf{Nat}$. By Lemma B.1 we deduce
that there exist simple types $A_{1},\dots,A_{n}$ and a term $t^{*}_{g}$ such
that
$t^{*}_{g}:\mathsf{Nat}[A_{1}]\Rightarrow\dots\Rightarrow\mathsf{Nat}[A_{n}]\Rightarrow\mathsf{Nat}[o]$
in ${\mathrm{ST\lambda C}}$, and $t^{*}_{g}x\dots x\simeq_{\beta\eta}t_{g}x$.
Let now $f(n)=\prod_{k\leq n}g(k)$.

Let $C=\langle\mathsf{Nat}[A_{1}],\dots,\mathsf{Nat}[A_{n}]\rangle$ and
$D=\langle\mathsf{Nat}[o],C,\mathsf{Nat}[o]\rangle$. We define the term
$t_{f}$ by:

$t_{f}=\lambda x.\mathsf{P}_{1,3}^{\mathsf{Nat}[o]}\Big{(}x\big{(}\lambda
h.\langle v_{1}[h],v_{2}[h],v_{3}[h]\rangle\big{)}\langle
t^{*}_{g}\mathbf{0}\dots\mathbf{0},\langle\mathbf{0},\dots,\mathbf{0}\rangle,t_{g}^{*}\mathbf{0}\dots\mathbf{0}\rangle\Big{)}\
:\ \mathsf{Nat}[D]\Rightarrow\mathsf{Nat}[o]$

where

$\displaystyle v_{1}[h]$
$\displaystyle=(\mathsf{P}^{\mathsf{Nat}[o]}_{3,3}h)\cdot(\mathsf{P}_{1,3}^{\mathsf{Nat}[o]}h)$
$\displaystyle v_{2}[h]$
$\displaystyle=\left\langle\mathsf{P}_{1,n}^{\mathsf{Nat}[A_{1}]}(\mathsf{P}_{2,3}^{C}(h))+1,\dots,\mathsf{P}_{n,n}^{\mathsf{Nat}[A_{n}]}(\mathsf{P}_{2,3}^{C}(h))+1\right\rangle$
$\displaystyle v_{3}[h]$
$\displaystyle=t^{*}_{g}\Big{(}\mathsf{P}_{1,n}^{\mathsf{Nat}[A_{1}]}(\mathsf{P}_{2,3}^{C}(h))+1\Big{)}\dots\Big{(}\mathsf{P}_{n,n}^{\mathsf{Nat}[A_{n}]}(\mathsf{P}_{2,3}^{C}(h))+1\Big{)}$

Observe that $t_{f}\mathbf{n}$ computes the triple $\langle\prod_{k\leq
n}t_{g}\mathbf{k},\langle\mathbf{n},\dots,\mathbf{n}\rangle,t_{g}\mathbf{n}\rangle$
and then extracts its first element. Since $t_{f}$ has type
$\mathsf{Nat}[D]\Rightarrow\mathsf{Nat}[o]$ in ${\mathrm{ST\lambda C}}$, we
deduce, again by Lemma B.1, that $t_{f}$ has type
$\mathsf{Nat}\Rightarrow\mathsf{Nat}$ in $\mathrm{ML}$.

##  Appendix C Proofs from Section 6

###### Proof of Lemma 6.1.

  1. 1.

We must consider two cases:

    1. (a)

if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x_{i}}$,
then
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}x_{i}}$.

    2. (b)

if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}[\
]={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[\
]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}_{1}[\
]\mathtt{C}_{2}[\ ]}$, for some
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[\
]\in\mathbb{G}_{3}$ and $\mathtt{C}_{i}[\ ]\in\mathbb{G}_{1}$, then by the
induction hypothesis
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]$
and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}_{i}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u_{A}}]\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}v_{A}}]$,
so we can conclude.

  2. 2.

We must consider two cases:

    1. (a)

if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{D}}[\
]=z\Lambda W_{i}.\lambda
w_{i}.{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{F}}[\
]$ for some