A Mechanical Formalization of Higher-Ranked Polymorphic
Type Inference
JINXU ZHAO, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
TOM SCHRIJVERS, KU Leuven, Belgium
Modern functional programming languages, such as Haskell or OCaml, use sophisticated forms of type
inference. While an important topic in the Programming Languages research, there is little work on themechanization of the metatheory of type inference in theorem provers. In particular we are unaware of any
complete formalization of the type inference algorithms that are the backbone of modern functional languages.
This paper presents the first full mechanical formalization of the metatheory for higher-ranked polymorphic
type inference. The system that we formalize is the bidirectional type system by Dunfield and Krishnaswami(DK). The DK type system has two variants (a declarative and an algorithmic one) that have been manually
proven sound, complete and decidable. We present a mechanical formalization in the Abella theorem prover of
DK’s declarative type system with a novel algorithmic system. We have a few reasons to use a new algorithm.
Firstly, our new algorithm employs worklist judgments, which precisely capture the scope of variables andsimplify the formalization of scoping in a theorem prover. Secondly, while DK’s original formalization comeswith very well-written manual proofs, there are several details missing and some incorrect proofs, which
complicate the task of writing a mechanized proof. Despite the use of a different algorithm we prove the same
results as DK, although with significantly different proofs and proof techniques. Since such type inference
algorithms are quite subtle and have a complex metatheory, mechanical formalizations are an important
advance in type-inference research.
CCS Concepts: • Software and its engineering → Functional languages; Polymorphism; Formal language definitions.
Additional Key Words and Phrases: type inference, higher-rank polymorphism, mechanization
ACM Reference Format:
Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. A Mechanical Formalization of Higher-Ranked
Polymorphic Type Inference. Proc. ACM Program. Lang. 3, ICFP, Article 112 (August 2019), 29 pages. https://doi.org/10.1145/3341716

1

INTRODUCTION

Modern functional programming languages, such as Haskell or OCaml, use sophisticated forms oftype inference. The type systems of these languages are descendants of Hindley-Milner [Damas
and Milner 1982; Hindley 1969; Milner 1978], which was revolutionary at the time in allowing
type-inference to proceed without any type annotation. The traditional Hindley-Milner type system
Authors’ addresses: Jinxu Zhao, Department of Computer Science, The University of Hong Kong, Hong Kong, China,
jxzhao@cs.hku.hk; Bruno C. d. S. Oliveira, Department of Computer Science, The University of Hong Kong, Hong Kong,
China, bruno@cs.hku.hk; Tom Schrijvers, Department of Computer Science, KU Leuven, Leuven, Belgium, tom.schrijvers@
cs.kuleuven.be.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires
prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2019 Association for Computing Machinery.
2475-1421/2019/8-ART112
https://doi.org/10.1145/3341716

Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112

112:2

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

supports top-level implicit (parametric) polymorphism [Reynolds 1983]. With implicit polymorphism, type arguments of polymorphic functions are automatically instantiated. Thus implicit
polymorphism and the absence of type annotations mean that the Hindley-Milner type systemstrikes a great balance between expressive power and usability.
As functional languages evolved the need for more expressive power has motivated language
designers to look beyond Hindley-Milner. In particular one popular direction is to allow higherranked polymorphism where polymorphic types can occur anywhere in a type signature. An
important challenge is that full type inference for higher-ranked polymorphism is known to be
undecidable [Wells 1999]. Therefore some type annotations are necessary to guide type inference.
In response to this challenge several decidable type systems requiring some annotations have been
proposed [Dunfield and Krishnaswami 2013; Le Botlan and Rémy 2003; Leijen 2008; Peyton Joneset al. 2007; Serrano et al. 2018; Vytiniotis et al. 2008]. Two closely related type systems that support
predicative higher-ranked type inference were proposed by Peyton Jones et al. [Peyton Jones et al.
2007] and Dunfield and Krishnaswami [Dunfield and Krishnaswami 2013] (henceforth denoted
as DK). These type systems are popular among language designers and their ideas have been
adopted by several modern functional languages, including Haskell, PureScript [Freeman 2017]and Unison [Chiusano and Bjarnason 2015] among others. In those type systems type annotations
are required for polymorphic arguments of functions, but other type annotations can be omitted. A
canonical example (here written in Haskell) is:
hpoly = \(f :: forall a. a -> a) -> (f 1, f 'c')
The function hpoly cannot be type-checked in the Hindley-Milner type system. The type of hpolyis the rank-2 type: (forall a. a -> a) -> (Int, Char). Notably (and unlike Hindley-Milner)
the lambda argument f requires a polymorphic type annotation. This annotation is needed because
the single universal quantifier does not appear at the top-level. Instead it is used to quantify atype variable a used in the first argument of the function. Despite these additional annotations,
Peyton Jones et al. and DK’s type inference algorithms preserve many of the desirable properties
of Hindley-Milner. For example the applications of f implicitly instantiate the polymorphic typearguments of f.
Although type inference is important in practice and receives a lot of attention in academic
research, there is little work on mechanically formalizing such advanced forms of type inference intheorem provers. The remarkable exception is work done on the formalization of certain parts ofHindley-Milner type inference [Dubois 2000; Dubois and Menissier-Morain 1999; Garrigue 2015;
Naraschewski and Nipkow 1999; Urban and Nipkow 2008]. However there is still no formalizationof the higher-ranked type systems that are employed by modern languages like Haskell. This is at
odds with the current trend of mechanical formalizations in programming language research. In
particular both the POPLMark challenge [Aydemir et al. 2005] and CompCert [Leroy et al. 2012]
have significantly promoted the use of theorem provers to model various aspects of programming
languages. Today papers in various programming language venues routinely use theorem provers
to mechanically formalize: dynamic and static semantics and their correctness properties [Aydemir
et al. 2008], compiler correctness [Leroy et al. 2012], correctness of optimizations [Bertot et al. 2006],
program analysis [Chang et al. 2006] or proofs involving logical relations [Abel et al. 2018]. The
main argument for mechanical formalizations is a simple one. Proofs for programming languages
tend to be long, tedious and error-prone. In such proofs it is very easy to make mistakes that may
invalidate the whole development. Furthermore, readers and reviewers often do not have time tolook at the proofs carefully to check their correctness. Therefore errors can go unnoticed for along time. Mechanical formalizations provide, in principle, a natural solution for these problems.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:3

Theorem provers can automatically check and validate the proofs, which removes the burden ofchecking from both the person doing the proofs as well as readers or reviewers.
This paper presents the first fully mechanized formalization of the metatheory for higher-ranked
polymorphic type inference. The system that we formalize is the bidirectional type system by
Dunfield and Krishnaswami [2013]. We chose DK’s type system because it is quite elegant, welldocumented and it comes with detailed manually written proofs. Furthermore the system is adopted
in practice by a few real implementations of functional languages, including PureScript and Unison.
The DK type system has two variants: a declarative and an algorithmic one. The two variants havebeen manually proved to be sound, complete and decidable. We present a mechanical formalizationin the Abella theorem prover [Gacek 2008] for DK’s declarative type system using a different
algorithm. While our initial goal was to formalize both DK’s declarative and algorithmic versions,
we faced technical challenges with the latter, prompting us to find an alternative formulation.
The first challenge that we faced were missing details as well as a few incorrect proofs and lemmas
in DK’s formalization. While DK’s original formalization comes with very well written manual
proofs, there are still several details missing. These complicate the task of writing a mechanicallyverified proof. Moreover some proofs and lemmas are wrong and, in some cases, it is not clear
to us how to fix them. Despite the problems in DK’s manual formalization, we believe that these
problems do not invalidate their work and that their results are still true. In fact we have nothing
but praise for their detailed and clearly written metatheory and proofs, which provided invaluable
help to our own work. We expect that for most non-trivial manual proofs similar problems exist, so
this should not be understood as a sign of sloppiness on their part. Instead it should be an indicatorthat reinforces the arguments for mechanical formalizations: manual formalizations are error-prone
due to the multiple tedious details involved in them. There are several other examples of manual
formalizations that were found to have similar problems. For example, Klein et al. [Klein et al. 2012]mechanized formalizations in Redex for nine ICFP 2009 papers and all were found to have mistakes.
Another challenge was variable binding. Type inference algorithms typically do not rely simply on
local environments but instead propagate information across judgments. While local environments
are well-studied in mechanical formalizations, there is little work on how to deal with the complex
forms of binding employed by type inference algorithms in theorem provers. To keep track ofvariable scoping, DK’s algorithmic version employs input and output contexts to track informationthat is discovered through type inference. However modeling output contexts in a theorem prover
is non-trivial.
Due to those two challenges, our work takes a different approach by refining and extending
the idea of worklist judgments [Zhao et al. 2018], proposed recently to mechanically formalize analgorithm for polymorphic subtyping [Odersky and Läufer 1996]. A key innovation in our work
is how to adapt the idea of worklist judgments to inference judgments, which are not needed forpolymorphic subtyping, but are necessary for type-inference. The idea is to use a continuationpassing style to enable the transfer of inferred information across judgments. A further refinement to
the idea of worklist judgments is the unification between ordered contexts [Dunfield and Krishnaswami
2013; Gundry et al. 2010] and worklists. This enables precise scope tracking of free variables injudgments. Furthermore it avoids the duplication of context information across judgments inworklists that occurs in other techniques [Abel and Pientka 2011; Reed 2009]. Despite the use of adifferent algorithm we prove the same results as DK, although with significantly different proofs
and proof techniques. The calculus and its metatheory have been fully formalized in the Abella
theorem prover [Gacek 2008].
In summary, the contributions of this paper are:Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:4Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

Type variables
Types
Monotypes
Expressions
Contexts

a, b
A, B, C
τ,σ
e
Ψ

::=
::=
::=
::=

1 | a | ∀a. A | A → B
1|a |τ →σx | () | λx . e | e 1 e 2 | (e : A)
· | Ψ, a | Ψ, x : A

Fig. 1. Syntax of Declarative System• A fully mechanized formalization of type inference with higher-ranked types: Our
work presents the first fully mechanized formalization for type inference of higher ranked
types. The formalization is done in the Abella theorem prover [Gacek 2008] and it is available
online at https://github.com/JimmyZJX/TypingFormalization.
• A new algorithm for DK’s type system: Our work proposes a novel algorithm that implements DK’s declarative bidirectional type system. We prove soundness, completeness anddecidability.
• Worklists with inference judgments: One technical contribution is the support for inference judgments using worklists. The idea is to use a continuation passing style to enable thetransfer of inferred information across judgments.
• Unification of worklists and contexts: Another technical contribution is the unification
between ordered contexts and worklists. This enables precise scope tracking of variables injudgments, and avoids the duplication of context information across judgments in worklists.
2

OVERVIEWThis section starts by introducing DK’s declarative type system. Then it discusses several techniquesthat have been used in algorithmic formulations, and which have influenced our own algorithmic
design. Finally we introduce the novelties of our new algorithm. In particular the support for
inference judgments in worklist judgments, and a new form of worklist judgment that the unifies
ordered contexts and the worklists themselves.
2.1 DK’s Declarative System
Syntax. The syntax of DK’s declarative system [Dunfield and Krishnaswami 2013] is shown in
Figure 1. A declarative type A is either the unit type 1, a type variable a, a universal quantification∀a. A or a function type A → B. Nested universal quantifiers are allowed for types, but monotypes
τ do not have any universal quantifier. Terms include a unit term (), variables x, lambda-functions
λx . e, applications e 1 e 2 and annotations (e : A). Contexts Ψ are sequences of type variabledeclarations and term variables with their types declared x : A.
Well-formedness. Well-formedness of types and terms is shown at the top of Figure 2. The rules
are standard and simply ensure that variables in types and terms are well-scoped.
Declarative Subtyping. The bottom of Figure 2 shows DK’s declarative subtyping judgment
Ψ ⊢ A ≤ B, which was adopted from Odersky and Läufer [1996]. It compares the degree ofpolymorphism between A and B in DK’s implicit polymorphic type system. Essentially, if A canalways be instantiated to match any instantiation of B, then A is “at least as polymorphic as” B. We
also say that A is “more polymorphic than” B and write A ≤ B.
Subtyping rules ≤Var, ≤Unit and ≤→ handle simple cases that do not involve universal quantifiers. The subtyping rule for function types ≤→ is standard, being covariant on the return typeand contravariant on the argument type. Rule ≤∀R states that if A is a subtype of B in the context
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:5

Ψ ⊢ A Well-formed declarative type
Ψ⊢1

a∈Ψ

wfd unitΨ⊢aΨ⊢A

wfd var

Ψ⊢B

Ψ⊢A→B

Ψ, a ⊢ A

wfd →Ψ ⊢ ∀a.Awfd ∀Ψ ⊢ e Well-formed declarative expression
x :A∈Ψ
Ψ⊢x

wfd tmvarΨ ⊢ e1Ψ ⊢ e2Ψ ⊢ e1 e2Ψ ⊢ ()

wfd tmunitΨ⊢A

wfd appΨ, x : A ⊢ eΨ ⊢ λx . eΨ⊢eΨ ⊢ (e : A)

wfd abs

wfd annoΨ ⊢ A ≤ B Declarative subtypinga∈ΨΨ⊢a ≤a

≤Var

Ψ⊢1≤1

Ψ⊢τ

Ψ ⊢ [τ /a]A ≤ BΨ ⊢ ∀a. A ≤ B

≤Unit

≤∀L

Ψ ⊢ B 1 ≤ A1

Ψ ⊢ A2 ≤ B 2

Ψ ⊢ A1 → A2 ≤ B 1 → B 2
Ψ, b ⊢ A ≤ B
Ψ ⊢ A ≤ ∀b. B

≤→

≤∀R

Fig. 2. Declarative Well-formedness and Subtyping

Ψ, a, where a is fresh in A, then A ≤ ∀a. B. Intuitively, if A is more general than ∀a. B (where theuniversal quantifier already indicates that ∀a. B is a general type), then A must instantiate to [τ /a]Bfor every τ .
The most interesting rule is ≤∀L. If some instantiation of ∀a. A, [τ /a]A, is a subtype of B,
then ∀a. A ≤ B. The monotype τ we used to instantiate a is guessed in this declarative rule, but
the algorithmic system does not guess and defers the instantiation until it can determine themonotype deterministically. The fact that τ is a monotype rules out the possibility of polymorphic(or impredicative) instantiation. However this restriction ensures that the subtyping relation remains
decidable. Allowing an arbitrary type (rather than a monotype) in rule ≤∀L is known to give riseto an undecidable subtyping relation [Tiuryn and Urzyczyn 1996]. Peyton Jones et al. [2007] also
impose the restriction of predicative instantiation in their type system. Both systems are adopted
by several practical programming languages.
Note that when we introduce a new binder in the premise, we implicitly pick a fresh one. Thisapplies to rules such as wfd∀, wfd abs, ≤∀R, throughout the whole text.
Declarative Typing. The bidirectional type system, shown in Figure 3, has three judgments. The
checking judgment Ψ ⊢ e ⇐ A checks expression e against the type A in the context Ψ. The
synthesis judgment Ψ ⊢ e ⇒ A synthesizes the type A of expression e in the context Ψ. The
application judgment Ψ ⊢ A • e ⇒⇒ C synthesizes the type C of the application of a function oftype A (which could be polymorphic) to the argument e.
Many rules are standard. Rule DeclVar looks up term variables in the context. Rules Decl1I
and Decl1I⇒ respectively check and synthesize the unit type. Rule DeclAnno synthesizes theannotated type A of the annotated expression (e : A) and checks that e has type A. Checking an
expression e against a polymorphic type ∀a. A in the context Ψ succeeds if e checks against A inthe extended context (Ψ, a). The subsumption rule DeclSub depends on the subtyping relation, andchanges mode from checking to synthesis: if e synthesizes type A and A ≤ B (A is more polymorphic
than B), then e checks against B. If a checking problem does not match any other rules, this rule
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:6

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

Ψ⊢e ⇐AΨ⊢e ⇒AΨ ⊢ A • e ⇒⇒ Ce checks against input type A.
e synthesizes output type A.
Applying a function of type A to e synthesizes type C.

(x : A) ∈ ΨΨ⊢x ⇒AΨ⊢AΨ⊢e ⇐AΨ ⊢ (e : A) ⇒ A

DeclAnno

Ψ, a ⊢ e ⇐ AΨ ⊢ e ⇐ ∀a. A

Decl∀IΨ, x : A ⊢ e ⇐ BΨ ⊢ λx . e ⇐ A → BΨ ⊢ e1 ⇒ A

DeclVarDecl→IΨ ⊢ A • e 2 ⇒⇒ C

Ψ ⊢ e1 e2 ⇒ CΨ⊢e ⇒AΨ⊢A≤B

Ψ⊢e ⇐BΨ ⊢ () ⇐ 1
Ψ⊢τ

Decl1I

DeclSubΨ ⊢ () ⇒ 1

Ψ ⊢ [τ /a]A • e ⇒⇒ C

Ψ ⊢ ∀a. A • e ⇒⇒ C
Ψ⊢σ →τ

Decl∀AppΨ, x : σ ⊢ e ⇐ τΨ ⊢ λx . e ⇒ σ → τ
Decl→E

Decl1I⇒

Decl→I⇒Ψ⊢e ⇐AΨ ⊢ A → C • e ⇒⇒ C

Decl→App

Fig. 3. Declarative Typing

can be applied to synthesize a type instead and then check whether the synthesized type entails
the checked type. Lambda abstractions are the hardest construct of the bidirectional type system todeal with. Checking λx . e against function type A → B is easy: we check the body e against B in
the context extended with x : A. However, synthesizing a lambda-function is a lot harder, and thistype system only synthesizes monotypes σ → τ .
Application e 1 e 2 is handled by Rule Decl→E, which first synthesizes the type A of the function
e 1 . If A is a function type B → C, Rule Decl→App is applied; it checks the argument e 2 against B
and returns type C. The synthesized type of function e 1 can also be polymorphic, of the form ∀a. A.
In that case, we instantiate A to [τ /a]A with a monotype τ using according to Rule Decl→I⇒. If[τ /a]A is a function type, Rule Decl→App proceeds; if [τ /a]A is another universal quantified type,
Rule Decl→I⇒ is recursively applied.
Overlapping Rules. Some of the declarative rules overlap with each other. Declarative subtyping
rules ≤∀L and ≤∀R both match the conclusion Ψ ⊢ ∀a. A ≤ ∀a. B. In such case, choosing ≤∀R firstis always better, since we introduce the type variable a to the context earlier, which gives more
flexibility on the choice of τ . The declarative typing rule DeclSub overlaps with both Decl∀I and
Decl→I. However, we argue that more specific rules are always the best choices, i.e. Decl∀I and
Decl→I should have higher priority than DeclSub. We will come back to this topic in Section 4.2.
2.2

DK’s Algorithm

DK’s algorithm version revolves around their notion of algorithmic context.
Algorithmic Contexts

Γ, ∆, Θ ::=· | Γ, a | Γ, x : A | Γ, αD | Γ, αD = τ | Γ, ▶αDIn addition to the regular (universally quantified) type variables a, the algorithmic context also
contains existential type variables αD. These are placeholders for monotypes τ that are still to be
determined by the inference algorithm. When the existential variable is “solved”, its entry in thecontext is replaced by the assignment αD = τ . A context application on a type, denoted by [Γ]A,substitutes all solved existential type variables in Γ with their solutions on type A.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:7

All algorithmic judgments thread an algorithmic context. They have the form Γ ⊢ . . . ⊣ ∆, whereΓ is the input context and ∆ is the output context: Γ ⊢ A ≤ B ⊣ ∆ for subtyping, Γ ⊢ e ⇐ A ⊣ ∆for type checking, and so on. The output context is a functional update of the input context thatrecords newly introduced existentials and solutions.
Solutions are incrementally propagated by applying the algorithmic output context of a previous
task as substitutions to the next task. This can be seen in the subsumption rule:Γ ⊢e ⇒A⊣ΘΘ ⊢ [Θ]A ≤ [Θ]B ⊣ ∆Γ ⊢e ⇐B ⊣∆DK_Sub

The inference task yields an output context Θ which is applied as a substitution to the types A and
B before performing the subtyping check to propagate any solutions of existential variables thatappear in A and B.
Markers for scoping. The sequential order of entries in the algorithmic context, in combination
with the threading of contexts, does not perfectly capture the scoping of all existential variables.
For this reason the DK algorithm uses scope markers ▶αD in a few places. An example is given in
the following rule:Γ, ▶αD, αD ⊢ [Dα /a]A ≤ B ⊣ ∆, ▶αD, ΘΓ ⊢ ∀a. A ≤ B ⊣ ∆DK_≤∀LTo indicate that the scope of αD is local to the subtyping check [Dα /a]A ≤ B, the marker is pushed
onto its input stack and popped from the output stack together with the subsequent part Θ, which
may refer to αD. (Remember that later entries may refer to earlier ones, but not vice versa.) This way
αD does not escape its scope.
At first sight, the DK algorithm would seem a good basis for mechanization. After all it comeswith a careful description and extensive manual proofs. Unfortunately, we ran into several obstacles
that have prompted us to formulate a different, more mechanization-friendly algorithm.
Broken Metatheory. While going through the manual proofs of DK’s algorithm, we found several
problems. Indeed, two proofs of lemmas—Lemma 19 (Extension Equality Preservation) and Lemma
14 (Subsumption)— wrongly apply induction hypotheses in several cases. Fortunately, we havefound simple workarounds that fix these proofs without affecting the appeals to these lemmas.
More seriously, we have also found a lemma that simply does not hold: Lemma 29 (Parallel
Admissibility)1 . See Appendix for a detailed explanation and counterexample. This lemma is acornerstone of the two metatheoretical results of the algorithm, soundness and completeness withrespect to the declarative system. In particular, both instantiation soundness (i.e. a part of subtyping
soundness) and typing completeness directly require the broken lemma. Moreover, Lemma 54(Typing Extension) also requires the broken lemma and is itself used 13 times in the proof of typing
soundness and completeness. Unfortunately, we have not yet found a way to fix this problem.
Complex Scoping and Propagation. Besides the problematic lemmas in DK’s metatheory, there
are other reasons to look for an alternative algorithmic formulation of the type system that is moreamenable to mechanization. Indeed, two aspects that are particularly challenging to mechanize are
the scoping of universal and existential type variables, and the propagation of the instantiationof existential type variables across judgments. DK is already quite disciplined on these accounts,
in particular compared to traditional constraint-based type-inference algorithms like Algorithm
1 Ningning Xie found the issue with Lemma 29 in 2016 while collaborating with the second author on an earlier attempt tomechanically formalize DK’s algorithm. The authors acknowledged the problem after we contacted them through email.
Although they briefly mentioned that it should be possible to use a weaker lemma instead they did not go into details.

Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:8Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

W [Milner 1978] which features an implicit global scope for all type variables. Indeed, DK uses its
explicit and ordered context Γ that tracks the relative scope of universal and existential variables
and it is careful to only instantiate existential variables in a well-scoped manner.
Moreover, DK’s algorithm carefully propagates instantiations by recording them into the context
and threading this context through all judgments. While this works well on paper, this approach isstill fairly involved and thus hard to reason about in a mechanized setting. Indeed, the instantiations
have to be recorded in the context and are applied incrementally to each remaining judgment inturn, rather than immediately to all remaining judgments at once. Also, as we have mentioned above,the stack discipline of the ordered contexts does not mesh well with the use of output contexts;
explicit marker entries are needed in two places to demarcate the end of an existential variable’s
scope. Actually we found a scoping issue related to the subsumption rule DK_Sub, which mightcause existential variables to leak across judgments. In Section 5.1 we give a detailed discussion.
The complications of scoping and propagation are compelling reasons to look for anotheralgorithm that is easier to reason about in a mechanized setting.
2.3

Judgment Lists

To avoid the problem of incrementally applying a substitution to remaining tasks, we can findinspiration in the formulation of constraint solving algorithms. For instance, the well-known
unification algorithm by Martelli and Montanari [1982] decomposes the problem of unifying two.
.
terms s = t into a number of related unification problems between pairs of terms si = ti . These
smaller problems are not tackled independently, but kept together in a set S. The algorithm itself istypically formulated as a small-step-style state transition system S ↣ S ′ that rewrites the set ofunification problems until it is in solved form or until a contradiction has been found. For instance,
the variable elimination rule is written as:.

.

x = t, S ↣ x = t, [t/x]Si f x < t and x ∈ S

Because the whole set is explicitly available, the variable x can be simultaneously substituted.
In the above unification problem, all variables are implicitly bound in the same global scope.
Some constraint solving algorithms for Hindley-Milner type inference use similar ideas, but are
more careful tracking the scopes of variables [Pottier and Rémy 2005]. However they have separate
phases for constraint generation and solving. Recent unification algorithms for dependently-typed
languages are also more explicit about scopes. For instance, Reed [2009] represents a unification
problem as ∆ ⊢ P where P is a set of equations to be solved and ∆ is a (modal) context. Abel andPientka [2011] even use multiple contexts within a unification problem. Such a problem is denoted∆ ⊩ K where the meta-context ∆ contains all the typings of meta-variables in the constraint set
K . The latter consists of constraints like Ψ ⊢ M = N : C that are equipped with their individual
context Ψ. While accurately tracking the scoping of regular and meta-variables, this approach is
not ideal because it repeatedly copies contexts when decomposing a unification problem, and later
it has to substitute solutions into these copies.
2.4

Single-Context Worklist Algorithm for Subtyping

In recent work, Zhao et al. [2018] have shown how to mechanize a variant of DK’s subtyping
algorithm and shown it correct with respect to DK’s declarative subtyping judgment. This approachovercomes some problems in DK’s formulation by using a worklist-based judgment of the formΓ⊢Ω
where Ω is a worklist (or sequence) of subtyping problems of the form A ≤ B. The judgment isdefined by case analysis on the first element of Ω and recursively processes the worklist until
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:9

it is empty. Using both a single common ordered context Γ and a worklist Ω greatly simplifies
propagating the instantiation of type variables in one subtyping problem to the remaining ones.
Unfortunately, this work does not solve all problems. In particular, it has two major limitations
that prevent it from scaling to the whole DK system.
Scoping Garbage. Firstly, the single common ordered context Γ does not accurately reflect thetype and unification variables currently in scope. Instead, it is an overapproximation that steadily
accrues variables, and only drops those unification variables that are instantiated. In other words,
Γ contains “garbage” that is no longer in scope. This complicates establishing the relation with thedeclarative system.
No Inference Judgments. Secondly, and more importantly, the approach only deals with a judgment
for checking whether one type is the subtype of another. While this may not be so difficult to adapt
to the checking mode of term typing Γ ⊢ e ⇐ A, it clearly lacks the functionality to support theinference mode of term typing Γ ⊢ e ⇒ A. Indeed, the latter requires not only the communicationof unification variable instantiations from one typing problem to another, but also an inferred type.
2.5

Algorithmic Type Inference for Higher-Ranked Types: Key Ideas

Our new algorithmic type system builds on the work above, but addresses the open problems.
Scope Tracking. We avoid scoping garbage by blending the ordered context and the worklist intoa single syntactic sort Γ, our algorithmic worklist. This algorithmic worklist interleaves (type andterm) variables with work like checking or inferring types of expressions. The interleaving keeps
track of the variable scopes in the usual, natural way: each variable is in scope of anything in frontof it in the worklist. If there is nothing in front, the variable is no longer needed and can be popped
from the worklist. This way, no garbage (i.e. variables out-of-scope) builds up.
Algorithmic judgment chainω::= A ≤ B | e ⇐ A | e ⇒a ω | A • e ⇒⇒a ω

Algorithmic worklist
Γ ::= · | Γ, a | Γ, αD | Γ, x : A | Γ ⊩ ωFor example, suppose that the top judgment of the following worklist checks the identity function
against ∀a. a → a:Γ ⊩ λx . x ⇐ ∀a. a → a
To proceed, two auxiliary variables a and x are introduced to help the type checking:Γ, a, x : a ⊩ x ⇐ awhich will be satisfied after several steps, and the worklist becomes
Γ, a, x : a
Since the variable declarations a, x : a are only used for a judgment already processed, they can besafely removed, leaving the remaining worklist Γ to be further reduced.
Our worklist can be seen as an all-in-one stack, containing variable declarations and subtyping/typing judgments. The stack is an enriched form of ordered context, and it has a similar variablescoping scheme.
Inference Judgments. To express the DK’s inference judgments, we use a novel form of work
entries in the worklist: our algorithmic judgment chains ω. In its simplest form, such a judgment
chain is just a check, like a subtyping check A ≤ B or a term typecheck e ⇐ A. However, thenon-trivial forms of chains capture an inference task together with the work that depends on its
outcome. For instance, a type inference task takes the form e ⇒a ω. This form expresses that weneed to infer the type, say A, for expression e and use it in the chain ω by substituting it for theProc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:10Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

placeholder type variable a. Notice that such a binds a fresh type variable for the inner chain ω,
which behaves similarly to the variable declarations in the context.
Take the following worklist as an example
αD ⊩ (λx . x ) () ⇒a a ≤ αD, x : αD, βD ⊩ αD ≤ βD ⊩ βD ≤ 1
There are three (underlined) judgment chains in the worklist, where the first and second judgment
chains (from the right) are two subtyping judgments, and the third judgment chain, (λx . x ) () ⇒aa ≤ αD, is a sequence of an inference judgment followed by a subtyping judgment.
The algorithm first analyses the two subtyping judgments and will find the best solutions
αD = βD = 1 (please refer to Figure 5 for detailed derivations). Then we substitute every instance of αD
and βD with 1, so the variable declarations can be safely removed from the worklist. Now we reduce
the worklist to the following state· ⊩ (λx . x ) () ⇒a a ≤ 1, x : 1
which has a term variable declaration as the top element. After removing the garbage term variabledeclaration from the worklist, we process the last remaining inference judgment (λx . x ) () ⇒ ?,with the unit type 1 as its result. Finally the last judgment becomes 1 ≤ 1, a trivial base case.
3

ALGORITHMIC SYSTEM

This section introduces a novel algorithmic system that implements DK’s declarative specification.
The new algorithm extends the idea of worklists proposed by Zhao et al. [2018] in two ways. Firstly,
unlike Zhao et al. [2018]’s worklists, the scope of variables is precisely tracked and variables do notescape their scope. This is achieved by unifying algorithmic contexts and the worklists themselves.
Secondly, our algorithm also accounts for the type system (and not just subtyping). To deal withinference judgments that arise in the type system we employ a continuation passing style to enable
the transfer of inferred information across judgments in a worklist.
3.1

Syntax and Well-Formedness

Figure 4 shows the syntax and well-formedness judgments used by the algorithm. Similarly to thedeclarative system the well-formedness rules are unsurprising and merely ensure well-scopedness.
Existential Variables. The algorithmic system inherits the syntax of terms and types from thedeclarative system. It only introduces one additional feature. In order to find unknown types τin the declarative system, the algorithmic system extends the declarative types A with existential
D They behave like unification variables, but their scope is restricted by their position
variables αD, β.
in the algorithmic worklist rather than being global. Any existential variable αD should only besolved to a type that is well-formed with respect to the worklist to which αD has been added. The
point is that the monotype τ , represented by the corresponding existential variable, is always wellformed under the corresponding declarative context. In other words, the position of αD’s reflects thewell-formedness restriction of τ ’s.
Judgment Chains. Judgment chains ω, or judgments for short, are the core components of ouralgorithmic type-checking. There are four kinds of judgments in our system: subtyping (A ≤ B),
checking (e ⇐ A), inference (e ⇒a ω) and application inference (A • e ⇒⇒a ω). Subtyping andchecking are relatively simple, since their result is only success or failure. However both inference
and application inference return a type that is used in subsequent judgments. We use a continuationpassing-style encoding to accomplish this. For example, the judgment chain e ⇒a (a ≤ B) contains
two judgments: first we want to infer the type of the expression e, and then check if that type
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:11

Existential variablesαD, βD

Algorithmic types

A, B, C::=

Algorithmic judgment chainω::= A ≤ B | e ⇐ A | e ⇒a ω | A • e ⇒⇒a ω

Algorithmic worklist

Γ::=

1 | a | ∀a. A | A → B | αD
· | Γ, a | Γ, αD | Γ, x : A | Γ ⊩ ωΓ ⊢ A Well-formed algorithmic type
Γ⊢1

wf_unita∈ΓΓ⊢awf_varαD ∈ ΓΓ ⊢ αDΓ⊢A

wf_exvar

Γ⊢B

Γ⊢A→B

wf_→

Γ, a ⊢ AΓ ⊢ ∀a.Awf_∀Γ ⊢ e Well-formed algorithmic expression
x :A∈Γ
Γ⊢x

wf_tmvarΓ ⊢ e1Γ ⊢ ()Γ ⊢ e2Γ ⊢ e1 e2Γ, x : A ⊢ e

wf_tmunitΓ⊢A

wf_appΓ ⊢ λx . eΓ ⊢eΓ ⊢ (e : A)

wf_abswf_annoΓ ⊢ ω Well-formed algorithmic judgment
Γ⊢A

Γ⊢B

Γ⊢A≤B
Γ ⊢e

Γ, a ⊢ ωΓ ⊢ e ⇒a ω

Γ ⊢e

wf≤

Γ ⊢e ⇐A
Γ⊢A

wf⇒

Γ⊢A

wf⇐

Γ, a ⊢ ωΓ ⊢eΓ ⊢ A • e ⇒⇒a ω

wf⇒⇒

wf Γ Well-formed algorithmic worklist
wf ·

wf·

wf Γ
wf Γ, awf Γ

wfa

wf Γ, αD

wfαD

wf Γ

Γ⊢A

wf Γ, x : A

wfof

wf Γ

Γ⊢ω

wf Γ ⊩ ω

wfω

Fig. 4. Extended Syntax and Well-Formedness for the Algorithmic System

is a subtype of B. The unknown type of e is represented by a type variable a, which is used as aplaceholder in the second judgment to denote the type of e.
Worklist Judgments. Our algorithm has a non-standard form. We combine traditional contexts
and judgment(s) into a single sort, the worklist Γ. The worklist is an ordered collection of bothvariable bindings and judgments. The order captures the scope: only the objects that come aftera variable’s binding in the worklist can refer to it. For example, [·, a, x : a ⊩ x ⇐ a] is a valid
worklist, but [· ⊩ x ⇐ a, x : a, a] is not (the underlined symbols refer to out-of-scope variables).
Hole Notation. We use the syntax Γ[ΓM ] to denote the worklist ΓL , ΓM , ΓR , where Γ is the worklist
ΓL , •, ΓR with a hole (•). Hole notations with the same name implicitly share the same structure
D means
ΓL and ΓR . A multi-hole notation splits the worklist into more parts. For example, Γ[Dα ][β]
D
Γ1 , αD, Γ2 , β, Γ3 .
3.2

Algorithmic System

The algorithmic typing reduction rules, defined in Figure 5, have the form Γ −→ Γ ′. The reduction
process treats the worklist as a stack. In every step it pops the first judgment from the worklist for
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:12

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

Γ −→ Γ ′Γ, a −→1 ΓΓ reduces to Γ ′.
Γ, αD −→2 ΓΓ, x : A −→3 ΓΓ ⊩ 1 ≤ 1 −→4 ΓΓ ⊩ a ≤ a −→5 ΓΓ ⊩ αD ≤ αD −→6 ΓΓ ⊩ A1 → A2 ≤ B 1 → B 2 −→7 Γ ⊩ A2 ≤ B 2 ⊩ B 1 ≤ A1
Γ ⊩ ∀a. A ≤ B −→8 Γ, αD ⊩ [Dα /a]A ≤ B

when B , ∀a. B ′Γ ⊩ A ≤ ∀b. B −→9 Γ, b ⊩ A ≤ B
Γ[Dα ] ⊩ αD ≤ A → B −→10 [D
α 1 → αD2 /Dα ](Γ[Dα 1 , αD2 ] ⊩ αD1 → αD2 ≤ A → B)
when αD < FV (A) ∪ FV (B)Γ[Dα ] ⊩ A → B ≤ αD −→11 [D
α 1 → αD2 /Dα ](Γ[Dα 1 , αD2 ] ⊩ A → B ≤ αD1 → αD2 )when αD < FV (A) ∪ FV (B)D ⊩ αD ≤ βD −→12 [DD α ][])
Γ[Dα ][β]
α /β](Γ[DD ⊩ βD ≤ αD −→13 [DD α ][])
Γ[Dα ][β]
α /β](Γ[DD ⊩ a ≤ βD −→14 [a/β](Γ[a][])D
Γ[a][β]D ⊩ βD ≤ a −→15 [a/β](Γ[a][])D
Γ[a][β]D ⊩ 1 ≤ βD −→16 [1/β](Γ[])
DΓ[β]D ⊩ βD ≤ 1 −→17 [1/β](Γ[])
DΓ[β]Γ ⊩ e ⇐ B −→18 Γ ⊩ e ⇒a a ≤ Bwhen e , λx . e ′ and B , ∀a. B ′Γ ⊩ e ⇐ ∀a. A −→19 Γ, a ⊩ e ⇐ AΓ ⊩ λx . e ⇐ A → B −→20 Γ, x : A ⊩ e ⇐ B
Γ[Dα ] ⊩ λx . e ⇐ αD −→21 [D
α 1 → αD2 /Dα ](Γ[Dα 1 , αD2 ], x : αD1 ⊩ e ⇐ αD2 )Γ ⊩ x ⇒a ω −→22 Γ ⊩ [A/a]ω

when (x : A) ∈ ΓΓ ⊩ (e : A) ⇒a ω −→23 Γ ⊩ [A/a]ω ⊩ e ⇐ A
Γ ⊩ () ⇒a ω −→24 Γ ⊩ [1/a]ω
DΓ ⊩ λx . e ⇒a ω −→25 Γ, αD, βD ⊩ [Dα → β/a]ω,x : αD ⊩ e ⇐ βDΓ ⊩ e 1 e 2 ⇒a ω −→26 Γ ⊩ e 1 ⇒b (b • e 2 ⇒⇒a ω)Γ ⊩ ∀a. A • e ⇒⇒a ω −→27 Γ, αD ⊩ [Dα /a]A • e ⇒⇒a ωΓ ⊩ A → C • e ⇒⇒a ω −→28 Γ ⊩ [C/a]ω ⊩ e ⇐ A
Γ[Dα ] ⊩ αD • e ⇒⇒a ω −→29 [D
α 1 → αD2 /Dα ](Γ[Dα 1 , αD2 ] ⊩ αD1 → αD2 • e ⇒⇒a ω)
Fig. 5. Algorithmic Typing

Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:13processing and possibly pushes new judgments onto the worklist. The syntax Γ −→∗ Γ ′ denotes
multiple reduction steps.

Γ −→∗ Γ−→∗ idΓ −→ Γ1Γ1 −→∗ Γ ′Γ −→∗ Γ ′−→∗ step

In the case that Γ −→∗ · this corresponds to successful type checking.
Please note that when a new variable is introduced in the right-hand side worklist Γ ′, we implicitly
pick a fresh one, since the right-hand side can be seen as the premise of the reduction.
Rules 1-3 pop variable declarations that are essentially garbage. That is variables that are out of
scope for the remaining judgments in the worklist. All other rules concern a judgment at the frontof the worklist. Logically we can discern 6 groups of rules.
1. Algorithmic subtyping. We have six subtyping rules (Rules 4-9) that are similar to theirdeclarative counterparts. For instance, Rule 7 consumes a subtyping judgment and pushes twoback to the worklist. Rule 8 differs from declarative Rule ≤∀L by introducing an existential variable
αD instead of guessing the monotype τ instantiation. Each existential variable is later solved to a
monotype τ with the same context, so the final solution τ of αD should be well-formed under Γ.
Worklist Variable Scoping. Rules 8 and 9 involve variable declarations and demonstrate how our
worklist treats variable scopes. Rule 8 introduces an existential variable αD that is only visible tothe judgment [Dα /a]A ≤ B. Reduction continues until all the subtyping judgments in front of αD aresatisfied. Finally we can safely remove αD since no occurrence of αD could have leaked into the leftpart of the worklist. Moreover, the algorithm garbage-collects the αD variable at the right time: itleaves the environment immediately after being unreferenced completely for sure.
Example. Consider the derivation of the subtyping judgment (1 → 1) → 1 ≤ (∀a. 1 → 1) → 1:
· ⊢ (1 → 1) → 1 ≤ (∀a. 1 → 1) → 1−→7 · ⊩ 1 ≤ 1 ⊩ ∀a. 1 → 1 ≤ 1 → 1−→8 · ⊩ 1 ≤ 1, αD ⊩ 1 → 1 ≤ 1 → 1−→7 · ⊩ 1 ≤ 1, αD ⊩ 1 ≤ 1 ⊩ 1 ≤ 1−→4 · ⊩ 1 ≤ 1, αD ⊩ 1 ≤ 1−→4 · ⊩ 1 ≤ 1, αD−→2 · ⊩ 1 ≤ 1−→4 ·First, the subtyping of two function types is split into two judgments by Rule 7: a covariant subtyping
on the return type and a contravariant subtyping on the argument type. Then we apply Rule 8 toreduce the ∀ quantifier on the left side. The rule introduces an existential variable αD to the context(even though the type ∀a. 1 → 1 does not actually refer to the quantified type variable a). In thefollowing 3 steps we satisfy the judgment 1 → 1 ≤ 1 → 1 by Rules 7, 4 and 4.
Now the existential variable αD, introduced before but still unsolved, is at the top of the worklist
and Rule 2 garbage-collects it. The process is carefully designed within the algorithmic rules: when
αD is introduced earlier by Rule 8, we foresee the recycling of αD after all the judgments (potentially)requiring αD have been processed. Finally Rule 4 reduces one of the base cases and finishes thesubtyping derivation.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:14

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

2. Existential decomposition. Rules 10 and 11 are algorithmic versions of Rule ≤→; they bothpartially instantiate αD to function types. The domain αD1 and range αD2 of the new function typeare not determined: they are fresh existential variables with the same scope as αD. We replace αD in
the worklist with αD1 , αD2 . To propagate the instantiation to the rest of the worklist and maintainwell-formedness, every reference to αD is replaced by αD1 → αD2 . The occurs-check condition prevents
divergence as usual. For example, without it αD ≤ 1 → αD would diverge.
3. Solving existentials. Rules 12-17 are base cases where an existential variable is solved. They
all remove an existential variable and substitute the variable with its solution in the remaining
worklist. Importantly the rules respect the scope of existential variables. For example, Rule 12 statesthat an existential variable αD can be solved with another existential variable βD only if βD occurs afterαD.
One may notice that the subtyping relation for simple types is just equivalence, which is true
according to the declarative system. The DK’s system works in a similar way.
4. Checking judgments. Rules 18-21 deal with checking judgments. Rule 18 is similar to
DeclSub, but rewritten in the continuation-passing-style. The side conditions e , λx . e ′ andB , ∀a. B ′ prevent overlap with Rules 19, 20 and 21; this is further discussed at the end of thissection. Rules 19 and 20 adapt their declarative counterparts to the worklist style. Rule 21 is a special
case of Decl → I, dealing with the case when the input type is an existential variable, representing
a monotype function as in the declarative system (it must be a function type, since the expression
λx . e is a function). The same instantiation technique as in Rules 10 and 11 applies. The declarative
checking rule Decl1I does not have a direct counterpart in the algorithm, because Rules 18 and 24
can be combined to give the same result.
Rule 21 Design Choice. The addition of Rule 21 is a design choice we have made to simplify
the side condition of Rule 18 (which avoids overlap). It also streamlines the algorithm and themetatheory as we now treat all cases where we can see that an existential variable should beinstantiated to a function type (i.e., Rules 10, 11, 21 and 29) uniformly.
The alternative would have been to omit Rule 21 and drop the condition on e in Rule 18. The
modified Rule 18 would then handle Γ ⊩ λx . e ⇐ αD and yield Γ ⊩ λx . e ⇒a a ≤ αD, which would befurther processed by Rule 25 to Γ, βD1 , βD2 ⊩ βD1 → βD2 ≤ αD, x : βD1 ⊩ e ⇐ βD2 . As a subtyping constraint
between monotypes is simply equality, βD1 → βD2 ≤ αD must end up equating βD1 → βD2 with αD andthus have the same effect as Rule 21, but in a more roundabout fashion.
In comparison, DK’s algorithmic subsumption rule has no restriction on the expression e, andthey do not have a rule that explicitly handles the case λx . e ⇐ αD. Therefore the only way to checka lambda function against an existential variable is by applying the subsumption rule, which further
breaks into type inference of a lambda function and a subtyping judgment.
5. Inference judgments. Inference judgments behave differently compared with subtyping andchecking judgments: they return a type instead of only accepting or rejecting. For the algorithmic
system, where guesses are involved, it may happen that the output type of an inference judgment
refers to new existential variables, such as Rule 25. In comparison to Rule 8 and 9, where newvariables are only referred by the sub-derivation, Rule 25 introduces variables αD, βD that affect theremaining judgment chain. This rule is carefully designed so that the output variables are boundby earlier declarations, thus the well-formedness of the worklist is preserved, and the garbage will
be collected at the correct time. By making use of the continuation-passing-style judgment chain,
inner judgments always share the context with their parent judgment.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:15Rules 22-26 deal with type inference judgments, written in continuation-passing-style. When an
inference judgment succeeds with type A, the algorithm continues to work on the inner-chain ω
by assigning A to its placeholder variable a. Rule 23 infers an annotated expression by changing
into checking mode, therefore another judgment chain is created. Rule 24 is a base case, where theunit type 1 is inferred and thus passed to its child judgment chain. Rule 26 infers the type of an
application by firstly inferring the type of the function e 1 , and then leaving the rest work to an
application inference judgment, which passes a, representing the return type of the application, tothe remainder of the judgment chain ω.
Rule 25 infers the type of a lambda expression by introducing αD, βD as the input and output typesof the function, respectively. After checking the body e under the assumption x : αD, the return
type might reflect more information than simply αD → βD through propagation when existential
variables are solved or partially solved. The variable scopes are maintained during the process:the assumption of argument type (x : αD) is recycled after checking against the function body;
D are only visible in the remaining chain
the existential variables used by the function type (Dα , β)
D[D
α → β/a]ω.
The recycling process of Rule 25 differs from DK’s corresponding rule significantly,
and we further discuss the differences in Section 5.1.
6. Application inference judgments. Finally, Rules 27-29 deal with application inference
judgments. Rules 27 and 28 behaves similarly to declarative rules Decl∀App and Decl → App. Rule
29 instantiates αD to the function type αD1 → αD2 , just like Rules 10, 11 and 21.
Example. Figure 6 shows a sample derivation of the algorithm. It checks the application (λx . x ) ()against the unit type. According to the algorithm, we apply Rule 18 (subsumption), changing toinference mode. Type inference of the application breaks into two steps by Rule 26: first we infer
the type of the function, and then the application inference judgment helps to determine the return
type. In the following 5 steps the type of the identity function, λx . x, is inferred to be αD → αD:checking the body of the lambda function (Rule 25), switching from check mode to inference mode
(Rule 18), inferring the type of a term variable (Rule 22), solving a subtyping between existential
variables (Rule 12) and garbage collecting the term variable x (Rule 3).
After that, Rule 28 changes the application inference judgment to a check of the argument against
the input type αD and returns the output type αD. Checking () against the existential variable αD solves
αD to the unit type 1 through Rules 18, 24 and 16. Immediately after αD is solved, the algorithm
replaces every occurrence of αD with 1. Therefore the worklist remains 1 ≤ 1, which is finished off
by Rule 4. Finally, the empty worklist indicates the success of the whole derivation.
In summary, our type checking algorithm accepts (λx . x ) () ⇐ 1.
Non-overlapping and Deterministic Reduction. An important feature of our algorithmic rules isthat they are directly implementable. Indeed, although written in the form of reduction rules, they
do not overlap and are thus deterministic.
Consider in particular Rules 8 and 9, which correspond to the declarative rules ≤∀L and ≤∀R.
While those declarative rules both match the goal ∀a. A ≤ ∀b. B, we have eliminated this overlap in
the algorithm by restricting Rule 8 (B , ∀a. B ′) and thus always applying Rule 9 to ∀a. A ≤ ∀b. B.
Similarly, the declarative rule DeclSub overlaps highly with the other checking rules. Its algorithmic counterpart is Rule 18. Yet, we have avoided the overlap with other algorithmic checking
rules by adding side-conditions to Rule 18, namely e , λx . e ′ and B , ∀a. B ′.
These restrictions have not been imposed arbitrarily: we formally prove that the restrictedalgorithm is still complete. In Section 4.2 we discuss the relevant metatheory, with the help of anon-overlapping version of the declarative system.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:16

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers· ⊩ (λx . x ) () ⇐ 1−→18 · ⊩ (λx . x ) () ⇒a a ≤ 1−→26 · ⊩ (λx . x ) ⇒b (b • () ⇒⇒a a ≤ 1)−→25 ·, αD, βD ⊩ αD → βD • () ⇒⇒a a ≤ 1, x : αD ⊩ x ⇐ βD−→18 ·, αD, βD ⊩ αD → βD • () ⇒⇒a a ≤ 1, x : αD ⊩ x ⇒b b ≤ βD−→22 ·, αD, βD ⊩ αD → βD • () ⇒⇒a a ≤ 1, x : αD ⊩ αD ≤ βD−→12 ·, αD ⊩ αD → αD • () ⇒⇒a a ≤ 1, x : αD−→3 ·, αD ⊩ αD → αD • () ⇒⇒a a ≤ 1−→28 ·, αD ⊩ αD ≤ 1 ⊩ () ⇐ αD−→18 ·, αD ⊩ αD ≤ 1 ⊩ () ⇒a a ≤ αD−→24 ·, αD ⊩ αD ≤ 1 ⊩ 1 ≤ αD−→16 · ⊩ 1 ≤ 1−→4 ·Fig. 6. A Sample Derivation for Algorithmic TypingΩ

Declarative worklist::=· | Ω, a | Ω, x : A | Ω ⊩ ω

Γ⇝Ω
Ω⇝Ω

⇝Ω

Ω ⊢τ

Γ instantiates to Ω.
Ω, [τ /Dα ]Γ ⇝ ΩΩ, αD, Γ ⇝ Ω⇝DαFig. 7. Declarative Worklists and Instantiation

4

METATHEORYThis section presents the metatheory of the algorithmic system presented in the previous section.
We show that three main results hold: soundness, completeness and decidability. These three results
have been mechanically formalized and proved in the Abella theorem prover [Gacek 2008].
4.1

Declarative Worklist and Transfer

To aid formalizing the correspondence between the declarative and algorithmic systems, we
introduce the notion of a declarative worklist Ω, defined in Figure 7. A declarative worklist Ω has
the same structure as an algorithmic worklist Γ, but does not contain any existential variables αD.
Worklist instantiation. The relation Γ ⇝ Ω expresses that the algorithmic worklist Γ can beinstantiated to the declarative worklist Ω, by appropriately instantiating all existential variables αDin Γ with well-scoped monotypes τ . The rules of this instantiation relation are shown in Figure 7
too. Rule ⇝D
α replaces the first existential variable with a well-scoped monotype and repeats theprocess on the resulting worklist until no existential variable remains and thus the algorithmic
worklist has become a declarative one. In order to maintain well-scopedness, the substitution isapplied to all the judgments and term variable bindings in the scope of αD.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:17∥Ω∥

Judgment erasure.
∥·∥=·∥Ω, a∥ = ∥Ω∥, a∥Ω, x : A∥ = ∥Ω∥, x : A∥Ω ⊩ ω ∥ = ∥Ω∥Ω −→ Ω ′Declarative transfer.

Ω, a −→ ΩΩ, x : A −→ ΩΩ ⊩ A ≤ B −→ Ω

when ∥Ω∥ ⊢ A ≤ BΩ ⊩ e ⇐ A −→ Ω

when ∥Ω∥ ⊢ e ⇐ AΩ ⊩ e ⇒a ω −→ Ω ⊩ [A/a]ω

when ∥Ω∥ ⊢ e ⇒ AΩ ⊩ A • e ⇒⇒a ω −→ Ω ⊩ [C/a]ω

when ∥Ω∥ ⊢ A • e ⇒⇒ C

Fig. 8. Declarative Transfer

Observe that the instantiation Γ ⇝ Ω is not deterministic. From left to right, there are infinitely
many possibilities to instantiate an existential variable and thus infinitely many declarative worklists
that one can get from an algorithmic one. In the other direction, any valid monotype in Ω can be
abstracted to an existential variable in Γ. Thus different Γ’s can be instantiated to the same Ω.
Lemmas 4.1 and 4.2 generalize Rule ⇝D
α from substituting the first existential variable to substituting any existential variable.
Lemma 4.1 (Insert). If ΓL , [τ /Dα ]ΓR ⇝ Ω and ΓL ⊢ τ , then ΓL , αD, ΓR ⇝ Ω.
Lemma 4.2 (Extract). If ΓL , αD, ΓR ⇝ Ω , then there exists τ s.t. ΓL ⊢ τ and ΓL , [τ /Dα ]ΓR ⇝ Ω.
Declarative transfer. Figure 8 defines a relation Ω −→ Ω ′, which transfers all judgments in the
declarative worklists to the declarative type system. This relation checks that every judgment
entry in the worklist holds using a corresponding conventional declarative judgment. The typing
contexts of declarative judgments are recovered using an auxiliary erasure function ∥Ω∥ 2 . The
erasure function simply drops all judgment entries from the worklist, keeping only variable andtype variable declarations.
4.2

Non-Overlapping Declarative System

DK’s declarative system, shown in Figures 2 and 3, has a few overlapping rules. In contrast, ouralgorithm has removed all overlap; at most one rule applies in any given situation. This discrepancy
makes it more difficult to relate the two systems.
To simplify matters, we introduce an intermediate system that is still declarative in nature, but
has no overlap. This intermediate system differs only in a few rules from DK’s declarative system:(1) Restrict the shape of B in the rule ∀L subtyping rule:
B , ∀b. B ′Ψ⊢τΨ ⊢ [τ /a]A ≤ BΨ ⊢ ∀a. A ≤ B∀L ′2 In the proof script we do not use the erasure function, for the declarative system and well-formedness judgments

automatically fit the non-erased declarative worklist just as declarative contexts.

Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:18

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

Ψ′ ≤ Ψ
·≤·CtxSubEmpty

Ψ′ ≤ Ψ
Ψ ′, a ≤ Ψ, a

CtxSubTyVar

Ψ′ ≤ Ψ

Ψ ⊢ A′ ≤ AΨ ′, x : A′ ≤ Ψ, x : A

CtxSubTmVar

Fig. 9. Context Subtyping(2) Drop the redundant rule Decl1I, which can be easily derived by a combination of DeclSub,
Decl1I⇒ and ≤Unit:Ψ ⊢ () ⇒ 1

Decl1I⇒Ψ⊢1≤1Ψ ⊢ () ⇐ 1≤Unit
DeclSub(3) Restrict the shapes of e and A in the subsumption rule DeclSub:e , λx . e ′A , ∀a. A′Ψ⊢e ⇒AΨ⊢A≤B

Ψ⊢e ⇐B

DeclSub ′The resulting declarative system has no overlapping rules and more closely resembles the algorithmic system, which contains constraints of the same shape.
We have proven soundness and completeness of the non-overlapping declarative system withrespect to the overlapping one to establish their equivalence. Thus the restrictions do not change
the expressive power of the system. Modification (2) is relatively easy to justify, with the derivation
given above: the rule is redundant and can be replaced by a combination of three other rules.
Modifications (1) and (3) require inversion lemmas for the rules that overlap. Firstly, Rule ∀Loverlaps with Rule ∀R for the judgment Ψ ⊢ ∀a. A ≤ ∀b. B. The following inversion lemma for Rule
∀R resolves the overlap:
Lemma 4.3 (Invertibility of ∀R). If Ψ ⊢ A ≤ ∀a. B then Ψ, a ⊢ A ≤ B.
The lemma implies that preferring Rule ∀R does not affect the derivability of the judgment.
Therefore the restriction B , ∀b. B ′ in ∀L′ is valid.
Secondly, Rule DeclSub overlaps with both Decl∀I and Decl→I. We have proven two inversion
lemmas for these overlaps:
Lemma 4.4 (Invertibility of Decl∀I). If Ψ ⊢ e ⇐ ∀a. A then Ψ, a ⊢ e ⇐ A.
Lemma 4.5 (Invertibility of Decl→I). If Ψ ⊢ λx . e ⇐ A → B then Ψ, x : A ⊢ e ⇐ B.
These lemmas express that applying the more specific rules, rather than the more general rule
DeclSub, does not reduce the expressive power.
The proofs of the above two lemmas rely on an important property of the declarative system, thesubsumption lemma. To be able to formulate this lemma, Figure 9 introduces the context subtyping
relation Ψ ≤ Ψ ′. Context Ψ subsumes context Ψ ′ if they bind the same variables in the same order,
but the types A of the term variables x in the former are subtypes of types A′ assigned to thoseterm variables in the latter. Now we can state the subsumption lemma:
Lemma 4.6 (Subsumption). Given Ψ ′ ≤ Ψ:(1) If Ψ ⊢ e ⇐ A and Ψ ⊢ A ≤ A′ then Ψ ′ ⊢ e ⇐ A′;(2) If Ψ ⊢ e ⇒ B then there exists B ′ s.t. Ψ ⊢ B ′ ≤ B and Ψ ′ ⊢ e ⇒ B ′;(3) If Ψ ⊢ A • e ⇒⇒ C and Ψ ⊢ A′ ≤ A, then there exists C ′ s.t. Ψ ⊢ C ′ ≤ C and Ψ ′ ⊢ A′ • e ⇒⇒ C ′.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:19This lemma expresses that any derivation in a context Ψ has a corresponding derivation in any
context Ψ ′ that it subsumes.
We have tried to follow DK’s manual proof of this lemma, but we discovered several problems intheir reasoning that we have been unable to address. Fortunately we have found a different way toprove the lemma. The details of this issue can be found in Appendix.
Three-Way Soundness and Completeness Theorems. We now have three systems that can be
related: DK’s overlapping declarative system, our non-overlapping declarative system, and ouralgorithmic system. We have already established the first relation, that the two declarative systems
are equivalent. In what follows, we will establish the soundness of our algorithm directly against
the original overlapping declarative system. However, we have found that showing completenessof the algorithm is easier against the non-overlapping declarative system. Of course, as a corollary,it follows that our algorithm is also complete with respect to DK’s declarative system.
4.3

Soundness

Our algorithm is sound with respect to DK’s declarative system. For any worklist Γ that reduces
successfully, there is a valid instantiation Ω that transfers all judgments to the declarative system.
Theorem 4.7 (Soundness). If wf Γ and Γ −→∗ ·, then there exists Ω s.t. Γ ⇝ Ω and Ω −→∗ ·.
The proof proceeds by induction on the derivation of Γ −→∗ ·. Interesting cases are those
involving existential variable instantiations, including Rules 10, 11, 21 and 29. Applications ofLemmas 4.1 and 4.2 help analyse the full instantiation of those existential variables. For example,
when αD is solved to αD1 → αD2 in the algorithm, applying the Extract lemma gives two instantiations
αD1 = σ and αD2 = τ . It follows that αD = σ → τ , which enables the induction hypothesis andfinishes the corresponding case. Some immediate corollaries which show the soundness for specificjudgment forms are:Corollary 4.8 (Soundness, single judgment form). Given wf Γ:(1) If Γ ⊩ A ≤ B −→∗ ·then there exist A′, B ′, Ω s.t. Γ ⊩ A ≤ B ⇝ Ω ⊩ A′ ≤ B ′ and ∥Ω∥ ⊢ A′ ≤ B ′;(2) If Γ ⊩ e ⇐ A −→∗ ·then there exist A′, Ω s.t. Γ ⊩ e ⇐ A ⇝ Ω ⊩ e ⇐ A′ and ∥Ω∥ ⊢ e ⇐ A′;(3) If Γ ⊩ e ⇒a ω −→∗ · for any ωthen there exists Ω, ω ′, A s.t. Γ ⇝ Ω and ∥Ω∥ ⊢ e ⇒ A;
(4) If Γ ⊩ A • e ⇒⇒a ω −→∗ · for any ωthen there exists Ω, ω ′, A′, C s.t. Γ ⊩ A•e ⇒⇒a ω ⇝ Ω ⊩ A′ •e ⇒⇒a ω ′ and ∥Ω∥ ⊢ A′ •e ⇒⇒ C.
4.4

CompletenessThe completeness of our algorithm means that any derivation in the declarative system has analgorithmic counterpart. We explicitly relate between an algorithmic context Γ and a declarative
context Ω to avoid potential confusion.
Theorem 4.9 (Completeness). If wf Γ and Γ ⇝ Ω and Ω −→∗ ·, then Γ −→∗ ·.
We prove completeness by induction on the derivation of Ω −→∗ · and use the non-overlapping
declarative system. Since the declarative worklist is reduced judgment by judgment (shown in
Figure 8), the induction always analyses the first judgment by a small step. As the algorithmic
system introduces existential variables, a declarative rule may correspond to multiple algorithmic
rules, and thus we analyse each of the possible cases.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:20

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

Most cases are relatively easy to prove. The Insert and Extract lemmas are applied when thealgorithm uses existential variables, but transferred to a monotype for the declarative system, suchas Rules 6, 8, 10, 11, 12-17, 21, 25, 27 and 29.
Algorithmic Rules 10 and 11 require special treatment. When the induction reaches the ≤→case, the first judgment is of shape A1 → A2 ≤ B 1 → B 2 . One of the corresponding algorithmic
judgments is αD ≤ A → B. However, the case analysis does not imply that αD is fresh in A and B,
therefore Rule 10 cannot be applied and the proof gets stuck. The following lemma helps us out
in those cases: the success in declarative subtyping indicates the freshness of αD in A and B in its
corresponding algorithmic judgment. In other words, the declarative system does not accept infinite
types. A symmetric lemma holds for A → B ≤ αD.
Lemma 4.10 (Prune Transfer for Instantiation). If (Γ ⊩ αD ≤ A → B) ⇝ (Ω ⊩ C ≤ A1 → B 1 )and ∥Ω∥ ⊢ C ≤ A1 → B 1 , then αD < FV (A) ∪ FV (B).
The following corollary is derived immediately from Theorem 4.9.
Corollary 4.11 (Completeness, single judgment form). Given wf Γ containing no judgments:(1) If Ω ⊢ A′ ≤ B ′ and Γ ⊩ A ≤ B ⇝ Ω ⊩ A′ ≤ B ′then Γ ⊩ A ≤ B −→∗ ·;(2) If Ω ⊢ e ⇐ A′ and Γ ⊩ e ⇐ A ⇝ Ω ⊩ e ⇐ A′
then Γ ⊩ e ⇐ A −→∗ ·;(3) If Ω ⊢ e ⇒ A and Γ ⊩ e ⇒a 1 ≤ 1 ⇝ Ω ⊩ e ⇒a 1 ≤ 1then Γ ⊩ e ⇒a 1 ≤ 1 −→∗ ·;(4) If Ω ⊢ A′ • e ⇒⇒ C and Γ ⊩ A • e ⇒⇒a 1 ≤ 1 ⇝ Ω ⊩ A′ • e ⇒⇒a 1 ≤ 1then Γ ⊩ A • e ⇒⇒a 1 ≤ 1 −→∗ ·.
4.5

Decidability

Finally, we show that our algorithm is decidable:
Theorem 4.12 (Decidability). Given wf Γ, it is decidable whether Γ −→∗ · or not.
Our decidability proof is based on a lexicographic group of induction measures⟨|Γ|e , |Γ|⇔ , |Γ|∀, |Γ|αD, |Γ|→ + |Γ|⟩ on the worklist Γ. Formal definitions of these measures can befound in the Appendix. The first two, | · |e and | · |⇔ , measure the total size of terms and the totaldifficulty of judgments, respectively. In the latter, check judgments count for 2, inference judgments
for 1 and function inference judgments for 3. Another two measures, | · |∀ and | · |→ , count the total
number of universal quantifiers and function types, respectively. Finally, | · |αD counts the numberof existential variables in the worklist, and | · | is simply the length of the worklist.
It is not difficult to see that all but two algorithmic reduction rules decrease the group of measures.
(The result of Rule 29 could be directly reduced by Rule 28, which decreases the measures.) The
two exceptions are Rules 10 and 11. Both rules increase the number of existential variables without
decreasing the number of universal quantifiers. However, they are both immediately followed byRule 7, which breaks the subtyping problem into two smaller problems of the form αD ≤ A andA ≤ αD which we call instantiation judgments.
We now show that entirely reducing these smaller problems leaves the worklist in a state with an
overall smaller measure. Our starting point is a worklist Γ, Γi where Γi are instantiation judgments.
Γi := · | Γi , αD ≤ A | Γi , A ≤ αD where αD < FV (A) ∪ FV (Γi )Fully reducing these instantiation judgments at the top of the worklist has a twofold impact. Firstly,
new entries may be pushed onto the worklist which are not instantiation judgments. This only
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:21Γ ⇀ Γ′Γ⇀Γ

⇀ id|A|∀ = 0

ΓL , [A/Dα ]ΓR ⇀ Γ ′ΓL , αD, ΓR ⇀ Γ ′Γ updates to Γ ′.
⇀ solveΓL , αD, ΓR ⇀ Γ ′ΓL , ΓR ⇀ Γ ′⇀ αDFig. 10. Worklist Update

happens when Γi contains a universal quantifier that is reduced by Rule 8 or 9. The new entries
then are of the form Γ≤ :
Γ≤ := · | Γ≤ , a | Γ≤ , αD | Γ≤ , A ≤ B
Secondly, reducing the instantiation judgments may also affect the remainder of the worklist Γ,
by solving existing existentials and introducing new ones. This worklist update is captured in the
update judgment Γ ⇀ Γ ′ defined in Figure 10. For instance, an existential variable instantiation,
ΓL , αD, ΓR ⇀ ΓL , αD1 , αD2 , [D
α 1 → αD2 /D
α ]ΓR , can be derived as a combination of the three rules that define
the update relation.
The good news is that worklist updates do not affect the three main worklist measures:
Lemma 4.13 (Measure Invariants of Worklist Extension). If Γ ⇀ Γ ′ then |Γ|e = |Γ ′ |e and|Γ|⇔ = |Γ ′ |⇔ and |Γ|∀ = |Γ ′ |∀ .
Moreover, we can characterize the reduction of the instantiation judgments as follows.
Lemma 4.14 (Instantiation Decidability). For any well-formed algorithmic worklist (Γ, Γi ):1) If |Γi |∀ = 0, then there exists Γ ′s.t. (Γ, Γi ) −→∗ Γ ′ and |Γ ′ |αD = |Γ|αD − |Γi | and Γ ⇀ Γ ′.
2) If |Γi |∀ > 0, then there exist Γ ′, Γ≤s.t. (Γ, Γi ) −→∗ (Γ ′, Γ≤ ) and |Γ≤ |∀ = |Γi |∀ − 1 and Γ ⇀ Γ ′.
Hence, reducing the instantiation judgment prefix Γi either decreases the number of universal
quantifiers or eliminates one existential variable per instantiation judgment. The proof of thislemma proceeds by induction on the measure 2 ∗ |Γi |→ + |Γi | of the instantiation judgment list Γi .
Let us go back to the whole algorithm and summarize our findings. The decidability theorem
is shown through a lexicographic group of induction measures ⟨|Γ|e , |Γ|⇔ , |Γ|∀, |Γ|αD, |Γ|→ + |Γ|⟩which is decreased by nearly all rules. In the exceptional case that the measure does not decrease
immediately, we encounter an instantiation judgment at the top of the worklist. We can thenmake use of Lemma 4.14 to show that |Γ|αD or |Γ|∀ decreases when that instantiation judgment isconsumed or partially reduced. Moreover, Lemma 4.13 establishes that no higher-priority measurecomponent increases. Hence, in the exceptional case we have an overall measure decrease too.
Combining all three main results (soundness, completeness and decidability), we conclude thatthe declarative system is decidable by means of our algorithm.
Corollary 4.15 (Decidability of Declarative Typing). Given wf Ω, it is decidable whetherΩ −→∗ · or not.
4.6

Abella and Proof Statistics

We have chosen the Abella (v2.0.7-dev 3 ) proof assistant [Gacek 2008] to develop our formalization.
Abella is designed to help with formalizations of programming languages, due to its built-in support
3 We use a development version because the developers just fixed a serious bug that accepts a simple proof of false, which

also affects our proof. Specifically, our scripts compile against commit 92829a of Abella’s GitHub repository.

Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:22

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

Table 1. Statistics for the proof scripts

File(s)SLOC#Theorems

Description

olist.thm, nat.thm
typing.thm
decl.thmorder.thm
alg.thm

311
245
226
235
679

57
7
33
27
80

trans.thm

616

53

declTyping.thm

909

70

soundness.thm
depth.thm
dcl.thmcompleteness.thm
inst_decidable.thm
decidability.thm
smallStep.thm

1,107
206
380
1,124
837
983
119

78
14
12
61
45
57
2

Basic data structures
Declarative & algorithmic system, debug examples
Basic declarative properties
The | · |∀ measure; decl. subtyping strengthening
Basic algorithmic properties
Worklist instantiation and declarative transfer;
Lemmas 4.1, 4.2
Non-overlapping declarative system;
Lemmas 4.3, 4.4, 4.5, 4.6
Soundness theorem; aux. lemmas on transfer
The | · |→ measure; Lemma 4.10
Non-overlapping declarative worklist
Completeness theorem; aux. lemmas and relations
Other worklist measures; Lemma 4.14
Decidability theorem and corollary
The equivalence between big-step and small-step

Total

7,977

596

(60 definitions in total)

for variable binding and the λ-tree syntax [Miller 2000], which is a form of HOAS. Nominal variables,or ∇-quantified variables, are used as an unlimited name supply, which supports explicit freshness
control and substitutions. Although Abella lacks packages, tactics and support for modules, its
higher-order unification and the ease of formalizing substitution-intensive relations are very helpful.
While the algorithmic rules are in a small-step style, the proof script rewrites them into a big-stepstyle for easier inductions. In addition, we do prove the equivalence of the two representations.
Statistics of the Proof. The proof script consists of 7,977 lines of Abella code with a total of 60
definitions and 596 theorems. Figure 1 briefly summarizes the contents of each file. The files arelinearly dependent due to limitations of Abella.
5

DISCUSSION

This section discusses some insights that we gained from our work and contrasts the scoping
mechanisms we have employed with those in DK’s algorithm. We also discuss a way to improve theprecision of their scope tracking. Furthermore we discuss and sketch an extension of our algorithmwith an elaboration to a target calculus, and discuss an extension of our algorithm with scoped
type variables [Peyton Jones and Shields 2004].
5.1

Contrasting Our Scoping Mechanisms with DK’s

A nice feature of our worklists is that, simply by interleaving variable declarations and judgment
chains, they make the scope of variables precise. DK’s algorithm deals with garbage collecting
variables in a different way: through type variable or existential variable markers (as discussed
in Section 2.2). Despite the sophistication employed in DK’s algorithm to keep scoping precise,
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:23

there is still a chance that unused existential variables leak their scope to an output context andaccumulate indefinitely. For example, the derivation of the judgment (λx . x ) () ⇐ 1 is as follows. . . x ⇒ αD . . .

. . . αD ≤ βD. . .

D x : αD ⊢ x ⇐ βD ⊣ Γ1 , x : αD
Γ, αD, β,. . . () ⇐ αD . . .

Γ ⊢ λx . x ⇒ αD → βD ⊣ Γ1

Γ1 ⊢ αD → αD • () ⇒⇒ αD ⊣ Γ2

Γ ⊢ (λx . x ) () ⇒ αD ⊣ Γ2

Γ2 ⊢ 1 ≤ 1 ⊣ Γ2

Γ ⊢ (λx . x ) () ⇐ 1 ⊣ Γ, αD = 1, βD = αD
D and Γ2 := (Γ, αD = 1, βD = αD) solves both αD and β.
D
where Γ1 := (Γ, αD, βD = αD) solves β,
If the reader is not familiar with DK’s algorithm, he/she might be confused about the inconsistenttypes across judgment. As an example, (λx . x ) () synthesizes αD, but the second premise of thesubsumption rule uses 1 for the result. This is because a context application [Γ, αD = 1, βD = αD]D
α =1happens between the premises.
The existential variables αD and βD are clearly not used after the subsumption rule, but according to
the algorithm, they are kept in the context until some parent judgment recycles a block of variables,or to the very end of a type inference task. In that sense, DK’s algorithm does not control thescoping of variables precisely.
Two rules we may blame for not garbage collecting correctly are the inference rule for lambda
functions and an application inference rule:D x : αD ⊢ e ⇐ βD ⊣ ∆, x : αD, ΘΓ, αD, β,Γ ⊢ λx . e ⇒ αD → βD ⊣ ∆DK_→I⇒

Γ, αD ⊢ [Dα /a]A • e ⇒⇒ C ⊣ ∆Γ ⊢ ∀a. A • e ⇒⇒ C ⊣ ∆DK_∀App

In contrast, Rule 25 of our algorithm collects the existential variables right after the second judgment
chain, and Rule 27 collects one existential variable similarly:DΓ ⊩ λx . e ⇒a ω −→25 Γ, αD, βD ⊩ [Dα → β/a]ω,x : αD ⊩ e ⇐ βDΓ ⊩ ∀a. A • e ⇒⇒a ω −→27 Γ, αD ⊩ [Dα /a]A • e ⇒⇒a ω
It seems impossible to achieve a similar outcome in DK’s system by only modifying these tworules. Taking DK_→I⇒ as an example, the declaration or solution for αD and βD may be referred toby subsequent judgments. Therefore leaving αD and βD in the output context is the only choice, when
the subsequent judgments cannot be consulted.
To fix the problem, one possible modification is on the algorithmic subsumption rule, as garbage
collection for a checking judgment is always safe:Γ, ▶αD⊢ e ⇒ A ⊣ ΘΘ ⊢ [Θ]A ≤ [Θ]B ⊣ ∆, ▶αD, ∆ ′Γ ⊢e ⇐B ⊣∆DK_Sub

Here we employ the markers in a way they were originally not intended for. We create a dummy
fresh existential αD and add a marker to the input context of the inference judgment. After thesubtyping judgment is processed we look for the marker and drop everything afterwards. We pick
this rule because it is the only one where a checking judgment calls an inference judgment. That isthe point where our algorithm recycles variables—right after a judgment chain is satisfied. After
applying this patch, to the best of our knowledge, DK’s algorithm behaves equivalently to ouralgorithm in terms of variable scoping. However, this exploits markers in a way they were notintended to be used and seems ad-hoc.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:24

5.2

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

Elaboration

Type-inference algorithms are often extended with an associated elaboration. For example, for
languages with implicit polymorphism, it is common to have an elaboration to a variant of System
F [Reynolds 1983], which recovers type information and explicit type applications. Therefore anatural question is whether our algorithm can also accommodate such elaboration. While ouralgorithmic reduction does not elaborate to System F, we believe that it is not difficult to extend
the algorithm with a (type-directed) elaboration. We explain the rough idea as follows.
Since the judgment form of our algorithmic worklist contains a collection of judgments, elaboration expressions are also generated as a list of equal length to the number of judgments (notjudgment chains) in the worklist. As usual, subtyping judgments translate to coercions (denoted byf and represented by System F functions), all three other types of judgments translate to terms in
System F (denoted by t).
Let Φ be the elaboration list, containing translated type coercions and terms:
Φ ::= · | Φ, f | Φ, t
Then the form of our algorithmic judgment becomes:
Γ ,→ Φ
We take Rule 18 as an example, rewriting small-step reduction in a relational style,Γ ⊩ e ⇒a a ≤ B ,→ Φ, f , tΓ ⊩ e ⇐ B ,→ Φ, f t

Translation_18

As is shown in the conclusion of the rule, a checking judgment at the top of the worklist corresponds
to a top element for elaboration. The premise shows that one judgment chain may relate to morethan one elaboration elements, and that the outer judgment, being processed before inner ones,
elaborates to the top element in the elaboration list.
Moreover, existential variables need special treatment, since they may be solved at any point,
or be recycled if not solved within their scopes. If an existential variable is solved, we not only
propagate the solution to the other judgments, but also replace occurrences in the elaboration list. If
an existential variable is recycled, meaning that it is not constrained, we can pick any well-formed
monotype as its solution. The unit type 1, as the simplest type in the system, is a good choice.
5.3

Lexically-Scoped Type Variables

We have further extended the type system with support for lexically-scoped type variables [Peyton Jones and Shields 2004]. Our Abella formalization for this extension proves all the metatheory
we discuss in Section 4.
From a practical point of view, this extension allows the implementation of a function to refer totype variables from its type signature. For example,(λx . λy. (x : a)) : ∀a b. a → b → a
has an annotation (x : a) that refers to the type variable a in the type signature. This is not asurprising feature, since the declarative system already accepts similar programs
Ψ, a ⊢ e ⇐ AΨ ⊢ ∀a. AΨ ⊢ e ⇐ ∀a. A

Decl∀IΨ ⊢ (e : ∀a. A) ⇒ ∀a. A

DeclAnno

The main issue is the well-formedness condition. Normally Ψ ⊢ (e : A) follows from Ψ ⊢ e andΨ ⊢ A. However, when A = ∀a. A′, the type variable a is not in scope at e, therefore Ψ ⊢ e is not
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:25derivable. To address the problem, we add a new syntactic form that explicitly binds a type variable
simulatenously in a function and its annotation.
Expressionse::=. . . | Λa. e : A

This new type-lambda syntax Λa. e : A actually annotates its body e with ∀a. A, while making avisible inside the body of the function. The well-formedness judgments are extended accordingly:
Ψ, a ⊢ eΨ, a ⊢ AΨ ⊢ Λa. e : A

wfd ΛΓ, a ⊢ eΓ, a ⊢ AΓ ⊢ Λa. e : A

wf_Λ

Corresponding rules are introduced for both the declarative system and the algorithmic system:
Ψ, a ⊢ A Ψ, a ⊢ e ⇐ AΨ ⊢ Λa. e : A ⇒ ∀a. A

DeclΛ

Γ ⊩ Λa. e : A ⇒b ω −→30 Γ ⊩ [(∀a. A)/b]ω, a ⊩ e ⇐ A
In practice, programmers would not write the syntax Λa. e : A directly. The ScopedTypeVariables
extension of Haskell is effective only when the type signature is explicitly universally quantified(which the compiler translates into an expression similar to Λa. e : A); otherwise the programmeans the normal syntax e : ∀a. A and may not later refer to the type variable a.
We have proven all three desired properties for the extended system, namely soundness, completeness and decidability.
6

RELATED WORK

Throughout the paper we have already discussed much of the closest related work. In this section
we summarize the key differences and novelties, and we discuss some other related work.
Predicative Higher-Ranked Polymorphism Type Inference Algorithms. Higher-ranked polymorphism is a convenient and practical feature of programming languages. Since full type-inference
for System F is undecidable [Wells 1999], various decidable partial type-inference algorithms weredeveloped. The declarative system of this paper, proposed by Dunfield and Krishnaswami [2013], ispredicative: ∀’s only instantiate to monotypes. The monotype restriction on instantiation is considered reasonable and practical for most programs, except for those that require sophisticated formsof higher-order polymorphism. In those cases, the bidirectional system accepts guidance throughtype annotations, which allow polymorphic types. Such annotations also improve readability ofthe program, and are not much of a burden in practice.
DK’s algorithm is shown to be sound, complete and decidable in 70 pages of manual proofs.
Though carefully written, some of the proofs are incorrect (see discussion in Appendix ), which
creates difficulties when formalizing them in a proof assistant. In their follow-up work Dunfield
and Krishnaswami [2019] enrich the bidirectional higher-rank system with existentials and indexed
types. With a more complex declarative system, they developed a proof of over 150 pages. It iseven more difficult to argue its correctness for every single detail within such a big development.
Unfortunately, we find that their Lemma 26 (Parallel Admissibility) appears to have the same issue
as lemma 29 in Dunfield and Krishnaswami [2013]: the conclusion is false. We also discuss the issue
in more detail in Appendix.
Peyton Jones et al. [2007] developed another higher-rank predicative bidirectional type system.
Their subtyping relation is enriched with deep skolemisation, which is more general than ours
and allows more valid relations. In comparison to DK’s system, they do not use the application
inference judgment, resulting in a complicated mechanism for implicit instantiation taken care by
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:26

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

the unification process for the algorithm. A manual proof is given, showing that the algorithm issound and complete with respect to their declarative specification.
In a more recent work, Xie and Oliveira [2018] proposed a variant of a bidirectional type
inference system for a predicative system with higher-ranked types. Type information flows fromarguments to functions with an additional application mode. This variant allows more higherorder typed programs to be inferred without additional annotations. Following the new mode,
the let-generalization of the Hindley-Milner system is well supported as a syntactic sugar. The
formalization includes some mechanized proofs for the declarative type system, but all proofs
regarding the algorithmic type system are manual.
Impredicative Higher-Ranked Polymorphism Type Inference Algorithms. Impredicative System F
allows instantiation with polymorphic types, but unfortunately its subtyping system is alreadyundecidable [Tiuryn and Urzyczyn 1996]. Works on partial impredicative type-inference algorithms [Le Botlan and Rémy 2003; Leijen 2008; Vytiniotis et al. 2008] navigate a variety of design
tradeoffs for a decidable algorithm. As a result, such algorithms tend to be more complicated, andthus less adopted in practice. Recent work proposed Guarded Impredicative Polymorphism [Serrano
et al. 2018], as an improvement on GHC’s type inference algorithm with impredicative instantiation. They make use of local information in n-ary applications to infer polymorphic instantiations
with a relatively simple specification and unification algorithm. Although not all impredicative
instantiations can be handled well, their algorithm is already quite useful in practice.
Mechanical Formalization of Polymorphic Subtyping. In all previous work on type inference forhigher-ranked polymorphism (predicative and impredicative) discussed above, proofs and metatheory for the algorithmic aspects are manual. The only partial effort on mechanizing algorithmic
aspects of type inference for higher-ranked types is the Abella formalization of polymorphic subtyping by Zhao et al. [2018]. The judgment form of worklist Γ ⊢ Ω used in the formalization
simplifies the propagation of existential variable instantiations. However, the approach has two
main drawbacks: it does not collect unused variable declarations effectively; and the simple form of
judgment cannot handle inference modes, which output types. The new worklist introduced in thispaper inherits the simplicity of propagating instantiations, but overcomes both of the issues by
mixing judgments with declarations and using the continuation-passing-style judgment chains.
Furthermore, we formalize the complete bidirectional type system by Dunfield and Krishnaswami[2013], whereas Zhao et al. only formalize the subtyping relation.
Mechanical Formalizations of Other Type-Inference Algorithms. Since the publication of the
POPLMark challenge [Aydemir et al. 2005], many theorem provers and packages provide new
methods for dealing with variable binding [Aydemir et al. 2008; Chlipala 2008; Urban 2008]. Moreand more type systems are formalized with these tools. However, mechanizing certain algorithmic
aspects, like unification and constraint solving, has received very little attention and is still challenging. Moreover, while most tools support local (input) contexts in a neat way, many practical
type-inference algorithms require more complex binding structures with output contexts or various
forms of constraint solving procedures.
Algorithm W, as one of the classic type inference algorithms for polymorphic type systems,
has been manually proven to be sound and complete with respect to the Hindley-Milner typesystem [Damas and Milner 1982; Hindley 1969; Milner 1978]. After around 15 years, the algorithm was formally verified by Naraschewski and Nipkow [1999] in Isabelle/HOL [Nipkow et al.
2002]. The treatment of new variables was tricky at that time, while the overall structure follows
the structure of Damas’s manual proof closely. Later on, other researchers [Dubois 2000; Dubois
and Menissier-Morain 1999] formalized algorithm W in Coq [The Coq development team 2017].
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:27

Nominal techniques [Urban 2008] in Isabelle/HOL have been developed to help programming
language formalizations, and are used for a similar verification [Urban and Nipkow 2008]. Moreover, Garrigue [Garrigue 2015] mechanized a type inference algorithm, with the help of locallynameless [Charguéraud 2012], for Core ML extended with structural polymorphism and recursion.
Ordered Contexts in Type Inference. Gundry et al. [Gundry et al. 2010] revisit algorithm W andpropose a new unification algorithm with the help of ordered contexts. Similar to DK’s algorithm,
information of meta variables flow from input contexts to output contexts. Not surprisingly, its
information increase relation has a similar role to DK’s context extension. Our algorithm, in contrast,
eliminates output contexts and solution records (Dα = τ ), simplifying the information propagation
process through immediate substitution by collecting all the judgments in a single worklist.
The Essence of ML Type Inference. Constraint-based type inference is adopted by Pottier and Rémy
[2005] for ML type systems, which do not employ higher-ranked polymorphism. An interesting
feature of their algorithm is that it keeps precise scoping of variables, similarly to our approach.
Their algorithm is divided into constraint generation and solving phases (which are typical of
constraint-based algorithms). Furthermore an intermediate language is used to describe constraints
and their constraint solver utilizes a stack to track the state of the solving process. In contrast, ouralgorithm has a single phase, where the judgment chains themselves act as constraints, thus noseparate constraint language is needed.
Lists of Judgments in Unification. Some work [Abel and Pientka 2011; Reed 2009] adopts asimilar idea to this paper in work on unification for dependently typed languages. Similarly
to our work the algorithms need to be very careful about scoping, since the order of variabledeclarations is fundamental in a dependently typed setting. Their algorithms simplify a collectionof unification constraints progressively in a single-step style. In comparison, our algorithm mixes
variable declarations with judgments, resulting in a simpler judgment form, while processing
them in a similar way. One important difference is that contexts are duplicated in their unification
judgments, which complicates the unification process, since the information of each local context
needs to be synchronized. Instead we make use of the nature of ordered context to control thescopes of unification variables. While their algorithms focus only on unification, our algorithm
also deals with other types of judgments like synthesis. A detailed discussion is in Section 2.3.
7

CONCLUSION

In this paper we have provided the first mechanized formalization of type inference for higherranked polymorphism. This contribution is made possible by a new type inference algorithm for
DK’s declarative type system that incorporates two novel mechanization-friendly ideas. Firstly,
we merge the traditional type context with the recently proposed concept of judgment chains,to accurately track variable scopes and to easily propagate substitutions. Secondly, we use acontinuation-passing style to return types from the synthesis mode to subsequent tasks.
We leave extending our algorithm with elaboration to future work, as well as investigating
whether the problems we have found in DK’s manual proofs for their algorithm can be addressed.
ACKNOWLEDGMENTS
We sincerely thank the anonymous reviewers for their insightful comments. Ningning Xie foundthe issue with Lemma 29 in DK’s formalization that we reported on this article. This work has beensponsored by the Hong Kong Research Grant Council projects number 17210617 and 17258816, andby the Research Foundation - Flanders.
Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

112:28

Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers

REFERENCES
Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark.
2018. POPLMark Reloaded: Mechanizing Proofs by Logical Relations. Submitted to the Journal of functional programming(2018).
Andreas Abel and Brigitte Pientka. 2011. Higher-order dynamic pattern unification for dependent types and records. In
International Conference on Typed Lambda Calculi and Applications. Springer, 10–26.
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. 2008. Engineering Formal
Metatheory. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL ’08).
Brian E Aydemir, Aaron Bohannon, Matthew Fairbairn, J Nathan Foster, Benjamin C Pierce, Peter Sewell, Dimitrios
Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized metatheory for the masses:
The POPLmark challenge. In The 18th International Conference on Theorem Proving in Higher Order Logics.
Yves Bertot, Benjamin Grégoire, and Xavier Leroy. 2006. A Structured Approach to Proving Compiler Optimizations Basedon Dataflow Analysis. In Proceedings of the 2004 International Conference on Types for Proofs and Programs (TYPES’04).
Bor-Yuh Evan Chang, Adam Chlipala, and George C. Necula. 2006. A Framework for Certified Program Analysis and Its
Applications to Mobile-code Safety. In Proceedings of the 7th International Conference on Verification, Model Checking, andAbstract Interpretation (VMCAI’06).
Arthur Charguéraud. 2012. The Locally Nameless Representation. Journal of Automated Reasoning 49, 3 (01 Oct 2012),
363–408.
Paul Chiusano and Runar Bjarnason. 2015. Unison. http://unisonweb.org
Adam Chlipala. 2008. Parametric Higher-order Abstract Syntax for Mechanized Semantics. In Proceedings of the 13th ACM
SIGPLAN International Conference on Functional Programming (ICFP ’08).
Luis Damas and Robin Milner. 1982. Principal Type-schemes for Functional Programs. In Proceedings of the 9th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’82).
Catherine Dubois. 2000. Proving ML type soundness within Coq. Theorem Proving in Higher Order Logics (2000), 126–144.
Catherine Dubois and Valerie Menissier-Morain. 1999. Certification of a type inference tool for ML: Damas–Milner within
Coq. Journal of Automated Reasoning 23, 3 (1999), 319–346.
Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and Easy Bidirectional Typechecking for Higher-rank
Polymorphism. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13).
Joshua Dunfield and Neelakantan R. Krishnaswami. 2019. Sound and Complete Bidirectional Typechecking for Higher-rank
Polymorphism with Existentials and Indexed Types. Proc. ACM Program. Lang. 3, POPL, Article 9 (Jan. 2019), 28 pages.
Phil Freeman. 2017. PureScript. http://www.purescript.org/
Andrew Gacek. 2008. The Abella Interactive Theorem Prover (System Description). In Proceedings of IJCAR 2008 (Lecture
Notes in Artificial Intelligence).
Jacques Garrigue. 2015. A certified implementation of ML with structural polymorphism and recursive types. Mathematical
Structures in Computer Science 25, 4 (2015), 867–891.
Adam Gundry, Conor McBride, and James McKinna. 2010. Type Inference in Context. In Proceedings of the Third ACM
SIGPLAN Workshop on Mathematically Structured Functional Programming (MSFP ’10).
Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematicalsociety 146 (1969), 29–60.
Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon
Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. 2012. Run Your Research: On the Effectiveness of Lightweight
Mechanization. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL ’12). 285–296.
Didier Le Botlan and Didier Rémy. 2003. MLF: Raising ML to the Power of System F. In Proceedings of the Eighth ACM
SIGPLAN International Conference on Functional Programming (ICFP ’03).
Daan Leijen. 2008. HMF: Simple Type Inference for First-class Polymorphism. In Proceedings of the 13th ACM SIGPLAN
International Conference on Functional Programming (ICFP ’08).
Xavier Leroy et al. 2012. The CompCert verified compiler. Documentation and userâĂŹs manual. INRIA Paris-Rocquencourt(2012).
Alberto Martelli and Ugo Montanari. 1982. An Efficient Unification Algorithm. ACM Trans. Program. Lang. Syst. 4, 2 (April
1982), 258–282.
Dale Miller. 2000. Abstract Syntax for Variable Binders: An Overview. In CL 2000: Computational Logic (Lecture Notes in
Artificial Intelligence).
Robin Milner. 1978. A theory of type polymorphism in programming. Journal of computer and system sciences 17, 3 (1978),348–375.

Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference

112:29Wolfgang Naraschewski and Tobias Nipkow. 1999. Type inference verified: Algorithm W in Isabelle/HOL. Journal ofAutomated Reasoning 23, 3 (1999), 299–318.
Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle/HOL: a proof assistant for higher-order logic. Vol. 2283.
Springer Science & Business Media.
Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL ’96).
Simon Peyton Jones and Mark Shields. 2004. Lexically-scoped type variables. (2004). http://research.microsoft.com/enus/um/people/simonpj/papers/scoped-tyvars/ Draft.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical type inference for arbitraryrank types. Journal of functional programming 17, 1 (2007), 1–82.
François Pottier and Didier Rémy. 2005. Advanced Topics in Types and Programming Languages. The MIT Press, Chapter
The Essence of ML Type Inference, 387–489.
Jason Reed. 2009. Higher-order Constraint Simplification in Dependent Type Theory. In Proceedings of the Fourth International
Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP ’09).
John C Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. Information Processing (1983), 513–523.
Alejandro Serrano, Jurriaan Hage, Dimitrios Vytiniotis, and Simon Peyton Jones. 2018. Guarded Impredicative Polymorphism.
In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018).
The Coq development team. 2017. The Coq proof assistant. https://coq.inria.fr/
Jerzy Tiuryn and Pawel Urzyczyn. 1996. The subtyping problem for second-order types is undecidable. In Proceedings 11th
Annual IEEE Symposium on Logic in Computer Science.
Christian Urban. 2008. Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning 40, 4 (2008), 327–356.
Christian Urban and Tobias Nipkow. 2008. Nominal verification of algorithm W. From Semantics to Computer Science. Essaysin Honour of Gilles Kahn (2008), 363–382.
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2008. FPH: First-class Polymorphism for Haskell. In
Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08).
Joe B Wells. 1999. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied
Logic 98, 1-3 (1999), 111–156.
Ningning Xie and Bruno C. d. S. Oliveira. 2018. Let Arguments Go First. In Programming Languages and Systems, Amal
Ahmed (Ed.). Springer International Publishing, Cham, 272–299.
Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. Formalization of a Polymorphic Subtyping Algorithm. In ITP(Lecture Notes in Computer Science), Vol. 10895. Springer, 604–622.

Proc. ACM Program. Lang., Vol. 3, No. ICFP, Article 112. Publication date: August 2019.