Kind Inference for Datatypes
NINGNING XIE, The University of Hong Kong, China
RICHARD A. EISENBERG, Bryn Mawr College, USA and Tweag I/O
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends
the expressive power of their type systems. With these features, the challenge of kind inference for datatypedeclarations has presented itself and become a worthy research problem on its own.
This paper studies kind inference for datatypes. Inspired by previous research on type-inference, we offer
declarative specifications for what datatype declarations should be accepted, both for Haskell98 and for a moreadvanced system we call PolyKinds, based on the extensions in modern Haskell, including a limited form ofdependent types. We believe these formulations to be novel and without precedent, even for Haskell98. These
specifications are complemented with implementable algorithmic versions. We study soundness, completenessand the existence of principal kinds in these systems, proving the properties where they hold. This work canserve as a guide both to language designers who wish to formalize their datatype declarations and also to
implementors keen to have principled inference of principal types.
CCS Concepts: • Theory of computation → Type theory; • Software and its engineering → Functional
languages; Polymorphism; Data types and structures.
Additional Key Words and Phrases: Haskell, Dependent Types
ACM Reference Format:
Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira. 2020. Kind Inference for Datatypes. Proc.
ACM Program. Lang. 4, POPL, Article 53 (January 2020), 28 pages. https://doi.org/10.1145/3371121

1

INTRODUCTION

Modern functional languages such as Haskell, ML, and OCaml come with powerful forms of type
inference. The global type-inference algorithms employed in those languages are derived fromthe Hindley-Milner type system (HM) [Damas and Milner 1982; Hindley 1969], with multiple
extensions. As the languages evolve, researchers also formalize the key aspects of type inference
for the new extensions. Common extensions of HM include higher-ranked polymorphism [Odersky
and Läufer 1996; Peyton Jones et al. 2007] and type-inference for GADTs [Peyton Jones et al. 2006],
which have both been formally studied thoroughly.
Most research work for extensions of HM so far has focused on forms of polymorphism (such assupport for impredicativity [Le Botlan and Rémy 2003; Leijen 2009; Rémy and Yakobowski 2008;
Serrano et al. 2018; Vytiniotis et al. 2008]), where type variables all have the same kind. In thesesystems, the type variables introduced by universal quantifiers and/or type declarations all standfor proper types (i.e., they have kind ⋆). In such a simplified setting, datatype declarations such as
Authors’ addresses: Ningning Xie, The University of Hong Kong, Department of Computer Science, Hong Kong, China,nnxie@cs.hku.hk; Richard A. Eisenberg, Bryn Mawr College, Department of Computer Science, Bryn Mawr, PA, USA,
Tweag I/O, rae@richarde.dev; Bruno C. d. S. Oliveira, The University of Hong Kong, Department of Computer Science,
Hong Kong, China, bruno@cs.hku.hk.
Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2020 Copyright held by the owner/author(s).
2475-1421/2020/1-ART53
https://doi.org/10.1145/3371121

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53

53:2

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveiradata Maybe a = Nothing | Just a pose no problem at all for type inference: with only one possible
kind for a, there is nothing to infer.
However, real-world implementations for languages like Haskell support a non-trivial kindlanguage, including kinds other than ⋆. Haskell98 accepts higher-kinded polymorphism [Jones 1995],
enabling datatype declarations such as data AppInt f = Mk (f Int). The type of constructor Mk
applies the type variable f to an argument Int. Accordingly, AppInt Bool would not work, as thetype Bool Int (in the instantiated type of Mk) is invalid. Instead, we must write something like
AppInt Maybe: the argument to AppInt must be suitable for applying to Int. In Haskell98, AppInt
has kind (⋆ → ⋆) → ⋆. For Haskell98-style higher-kinded polymorphism, Jones [1995] presents
one of the few extensions of HM that deals with a non-trivial language of kinds. His work addresses
the related problem of inference for constructor type classes, although he does not show directly
how to do inference for datatype declarations.
Modern Haskell1 has a much richer type and kind language compared to Haskell98. In recent
years, Haskell has seen a dramatic surge of new features that extend the expressive power ofalgebraic datatypes. Such features include GADTs, kind polymorphism [Yorgey et al. 2012] with
implicit kind arguments, and dependent kinds [Weirich et al. 2013], among others. With great power
comes great responsibility: now we must be able to infer these kinds, too. For instance, consider
these datatype declarations:data App f a = MkApp (f a)data T = MkT1 (App Maybe Int)
data Fix f= In (f (Fix f ))| MkT2 (App Fix Maybe) -- accept or reject?
Should the declaration for T be accepted or rejected? In a Haskell98 setting, the kind of App
is (⋆ → ⋆) → ⋆ → ⋆. Therefore T should be rejected, because in MkT2 the datatype App isapplied to Fix :: (⋆ → ⋆) → ⋆ and Maybe :: ⋆ → ⋆, which do not match the expected kinds ofApp. However, with kind polymorphism, T is accepted, because App has the more general kind∀k. (k → ⋆) → k → ⋆. With this kind, both uses of App in T are valid.
The questions we ask in this paper are these: Which datatype declarations should be accepted?
What kinds do accepted datatypes have? Surprisingly, the literature is essentially silent on thesequestions—we are unaware of any formal treatment of kind inference for datatype declarations.
Inspired by previous research on type inference, we offer declarative specifications for two
languages: Haskell98, as standardized [Peyton Jones 2003] (Section 3); and PolyKinds, a significant
fragment of modern Haskell (Section 6). These specifications are complemented with algorithmic
versions that can guide implementations (Sections 4 and 7). To relate the declarative and algorithmic
formulations we study various properties, including soundness, completeness, and the existence ofprincipal kinds (Sections 4.7, 5, and 7.6).
We offer the following contributions:• Kind inference for Haskell98: We formalize Haskell98’s datatype declarations, providing
both a declarative specification and syntax-driven algorithm for kind inference. We prove thatthe algorithm is sound and observe how Haskell98’s technique of defaulting unconstrained
kinds to ⋆ leads to incompleteness. We believe that ours is the first formalization of this
aspect of Haskell98. Its inclusion in this paper both sheds light on this historically important
language and also prepares us for the more challenging features of modern Haskell.
• Completeness for Haskell98 kind inference: To model the Haskell98 behavior of defaulting declaratively, and thus to achieve completeness, Section 5 proposes a variant of thedeclarative system that adapts the type parameters approach from Garcia and Cimini [2015].
• Kind inference for modern Haskell: We present a type and kind language that is unified
and dependently typed, modeling the challenging features for kind inference in modern
1 We consider the Glasgow Haskell Compiler’s implementation of Haskell, in version 8.8.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:3

Haskell. We include both a declarative specification (Section 6) and a syntax-driven algorithm(Section 7). The algorithm is proved sound, and we observe where and why completenessfails. In the design of our algorithm, we must choose between completeness and termination;
we favor termination but conjecture that an alternative design would regain completeness(Section 9). Unlike other dependently typed languages, we retain the ability to infer top-levelkinds instead of relying on compulsory annotations.
• Technical advances: This work introduces a number of technical innovations that appear
important in the implementation of type-inference for a dependently typed language. We
expect implementations to have developed these ideas independently, but this paper provides
their first known formalization. These innovations include promotion (Sections 4.6 and 7.4),
local scopes and moving (Section 7.4), and the quantification check (Section 7.2). In addition,
our kind-directed unification appears to risk divergence, yet we provide a subtle proof that it
is indeed terminating.
Our type systems are detailed, and many rules are elided to save space. The full judgments—andall proofs of stated lemmas and theorems—are provided in the technical supplement2 . In addition,
we have included there a detailed comparison of our work here to the GHC implementation. It is ourbelief that this study can help inform the design of principled inference algorithms for languages
beyond Haskell, as well as to guide the continued evolution of GHC’s kind inference algorithm.
2

OVERVIEWThis section gives an overview of our work. We start by contrasting kind inference with type
inference, and then summarize the key aspects of the two systems of datatypes that we develop.
2.1

Kind Inference in Haskell98

Haskell98’s kind language contains a constant (the kind ⋆) and kinds built from arrows (k 1 → k 2 ).
Kind inference for Haskell98 datatypes is thus closely related to type inference for the simply
typed λ-calculus (STLC). For example, consider a term + :: Int → Int → Int and a type constructor⊕ :: ⋆ → ⋆ → ⋆. At the term level, we infer that add a b = a + b yields add :: Int → Int → Int.
Similarly, we can create a datatype data Add a b = Add (a ⊕ b) and infer Add :: ⋆ → ⋆ → ⋆.
No principal types. Consider now the function definition k a = 1. In the STLC, there are infinitely
many (incomparable) types that can be assigned to k, including k :: Int → Int and k :: (Int →Int) → Int. Assuming there are no type variables, the STLC accordingly has no principal types.
An analogous datatype declaration is data K a = K Int. As with k, there are infinitely many
(incomparable) kinds that can be assigned to K , including K :: ⋆ → ⋆ and K :: (⋆ → ⋆) → ⋆.
Defaulting. Definitions like k (in STLC) or K (in Haskell98) do not have a principal type/kind,which raises the immediate question of what type/kind to infer. Haskell98 solves this problem
by using a defaulting strategy: if the kind of a type variable cannot be inferred, then it is defaulted
to ⋆. Therefore the kind of K in Haskell98 is ⋆ → ⋆. From the perspective of type inference,such defaulting strategy may seem somewhat ad-hoc, but due to the role that ⋆ plays at the typelevel it seems a defensible design for kind inference. Defaulting brings complications in writing adeclarative specification. We discuss this point further in Section 4.3.
2.2

Kind Inference in Modern GHC Haskell

The type and kind languages for modern GHC are unified (i.e., types and kinds are indistinguishable),dependently typed, and the kind system includes the ⋆ :: ⋆ axiom [Cardelli 1986; Weirich et al. 2013].
We informally use the word type or kind where we find it appropriate. Unlike Haskell98’s datatypes,
2 http://arxiv.org/abs/1911.06153.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:4

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira

whose inference problem is quite closely related to the well-studied inference problem for STLC,
type inference for various features in modern Haskell is not well-studied. While we are motivatedconcretely by Haskell, many of the challenges we face would be present in any dependently typed
language seeking principled type inference. We use the term PolyKinds to refer to the fragment ofmodern Haskell we model.3 We enumerate the key features of this fragment below.
Kind polymorphism and dependent types. Global type inference, in the style of Damas and Milner[1982], allows polymorphic kinds to be assigned to datatype definitions. For instance, reconsider
data K a = K Int. In PolyKinds, K can be given the kind K :: ∀{ k }. k → ⋆. This example shows oneof the interesting new features of PolyKinds over Haskell98: kind polymorphism [Yorgey et al. 2012].
The polymorphic kind is obtained via generalization, which is a standard feature in Damas-Milner
algorithms. Polymorphic types are helpful for recovering principal types, since they generalize
many otherwise incomparable monomorphic types.
System-F-based languages do not have dependent types. In contrast, PolyKinds supports dependent kinds such as data D :: ∀(k :: ⋆) (a :: k). K a → ⋆. There are two noteworthy aspects about thekind of D. Firstly, kind and type variables are typed: different type variables may have different
kinds. Secondly, the kinds of later variables can depend on earlier ones. In D, the kind of a depends
on k. Both typed variables and dependent kinds bring technical complications that do not exist in
many previous studies of type inference (e.g., [Peyton Jones et al. 2007; Vytiniotis et al. 2011]).
First-order unification with dependent kinds and typed variables. Although PolyKinds is dependently typed, its unification problem is remarkably first-order. This is in contrast to many otherdependently typed languages, where unification is usually higher-order [Andrews 1971; Huet 1973].
Since unification plays a central role in inference algorithms this is a crucial difference. Higher-orderunification is well-known to be undecidable in the general case [Goldfarb 1981]. As a consequence,
type-inference algorithms for most dependently typed languages make various trade-offs.
A key reason why unification can be kept as a first-order problem in PolyKinds is because thetype language does not include lambdas. Type-level lambdas have been avoided since the start in
Haskell, since they bring major challenges for (term-level) type inference [Jones 1995].
The unification problem for PolyKinds is still challenging, compared to unification for System-Flike languages: unification must be kind-directed, as first observed at the term level by Jones [1995].
Consider the following (contrived) example:
data X :: ∀a (b :: ⋆ → ⋆). a b → ⋆-- accepted
data Y :: ∀(c :: Maybe Bool). X c → ⋆ -- rejected
In X ’s kind, we discover a :: (⋆ → ⋆) → ⋆. When checking Y ’s kind, we must infer how to
instantiate X : that is, we must choose a and b so that a b unifies with Maybe Bool, which is c’s kind.
It is tempting to solve this with a 7→ Maybe and b 7→ Bool, but doing so would be ill-kinded, as aand Maybe have different kinds. Our unification thus features heterogeneous constraints [Gundry2013]. When solving a unification variable, we need to first unify the kinds on both sides.
Because unification recurs into kinds, and because types are undifferentiated from kinds, it mightseem that unification might not terminate. In Section 7.4 we show that the first-order unification
with heterogeneous constraints employed in PolyKinds is guaranteed to terminate.
Mutual and polymorphic recursion. Recursion and mutual recursion are omnipresent in datatypedeclarations. In PolyKinds, mutually recursive definitions will be kinded together and then get
generalized together. For example, both P and Q get kind ∀(k :: ⋆). k → ⋆.
3 Some of the features we model are slightly different in our presentation than they exist in GHC. The technical supplement

outlines the differences. These minor differences do not affect the applicability of our work to improving the GHC
implementations, but they may affect the ability to test our examples in GHC.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:5

data P a = MkP (Q a)data Q a = MkQ (P a)
The recursion is simple here: all recursive occurrences are at the same type. In existing typeinference algorithms, such recursive definitions are well understood and do not bring considerable
complexity to type inference. However, we must also consider polymorphic recursion as in Poly:
data Poly :: ∀k. k → ⋆data Poly k = C1 (Poly Int) | C2 (Poly Maybe)This example includes a kind signature, meaning that we must check the kind of the datatype, notinfer it. In the definition of Poly, the type Poly Int requires an instantiation k 7→ ⋆, while the type
Poly Maybe requires an instantiation of k 7→ (⋆ → ⋆). These differing instantiations cause thedeclaration to be polymorphic recursive.
PolyKinds deals with such cases of polymorphic recursion, which also appear at the term level—
for example, when writing recursive functions over GADTs or nested datatypes [Bird and Meertens
1998]. Polymorphic recursion is known to render type-inference undecidable [Henglein 1993].
Furthermore, most existing formalizations of type inference avoid the question entirely, either by
not modeling recursion at all or not allowing polymorphic recursion. Our PolyKinds system has
full support for polymorphic recursion, implemented directly without the use of a fix operator.
Polymorphic recursion is allowed only on datatypes with a kind signature; other datatypes aretreated as monomorphic during inference.
Visible kind application. PolyKinds lifts visible type application (VTA) [Eisenberg et al. 2016],
whereby we can explicitly instantiate a function call, as in id @Bool True, to kinds, giving us
visible kind application (VKA). Following the design of VTA, we distinguish specified variables frominferred variables. As described by Eisenberg et al. [2016, Section 3.1], only specified variables canbe instantiated via VKA. Instantiation of variables is inferred when no explicit kind application is
given. To illustrate, consider data T :: ∀a b. a b → ⋆. Here, a and b are specified variables. Because
their order is given, explicit instantiation of a must happen before b. For example, T @Maybe
instantiates a to Maybe. On the other hand, the kind of a and b can be generalized to a :: k → ⋆ andb :: k. Elaborating the kind of T , we write T :: ∀{ k :: ⋆} (a :: k → ⋆) (b :: k). a b → ⋆. The variable k
is inferred and is not available for instantiation with VKA. This split between specified and inferredvariables supports predictable type inference: if the variables invented by the compiler (e.g., k)were available for instantiation, then we have no way of knowing what order to instantiate them.
Open kind signatures and generalization order. Echoing the design of Haskell, PolyKinds supports
open kind signatures. We say a signature is closed if it contains no free variables (e.g., data T ::∀a. a →⋆). Otherwise, it is open (e.g., data Q :: ∀(a :: (f b)) (c :: k). f c → ⋆). Free variables (in this case, f ,b, k) will be generalized over. We have a decision to make: in which order do we generalize thefree variables? This question is non-trivial, as there can be dependency between the variables. We
infer k :: ⋆, f :: k → ⋆, b :: k. Even though f and b appear before k, their kinds end up depending
on k and we must quantify k before f and b. Inferring this order is a challenge: we cannot know
the correct order before completing inference. We thus introduce local scopes, which are sets ofvariables that may be reordered. Since the ordering is not fixed by the programmer, these variables
are considered inferred, not specified, with respect to VKA.
Existential quantification. PolyKinds supports existentially quantified variables on datatypeconstructors. This is useful, for example, to model GADTs. Given data T1 = ∀a. MkT1 a, we get
MkT1 :: ∀(a :: ⋆). a → T1. The type of the data constructor declaration can also be generalized.
Given data P1 :: ∀(a :: ⋆). ⋆, from data T2 = MkT2 P1, we infer MkT2 :: ∀{ a :: ⋆}. P1 @a → T2,
where P1 is elaborated to P1 @a with a generalized as an inferred variable.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:6

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveirai

programpgm
datatype decl. T
data c’tor decl. Deexpression

FFF

rec Ti ; pgm | ejdata T ai i = Dj
D τi ipolytype
monotype
kind

σ
τ
κ

F ∀ai : κ i i .τF Int | a | T | τ1 τ2 |→F ⋆ | κ1 → κ2

F...

term context
type context

Ψ
Σ

F
F

• | Ψ, D : σ• | Σ, a : κ | Σ,T : κΣ; Ψ ⊢pgm pgm : σ(Typing Program)
pgm-dtpgm-expr

Σ ′ = Σ, Ti : κ i

Σ; Ψ ⊢ e : σiΣ ′ ⊢dt Ti { ΨiiΣ ′; Ψ, Ψi ⊢pgm pgm : σiΣ; Ψ ⊢pgm e : σΣ ⊢dt T { ΨiΣ; Ψ ⊢pgm rec Ti ; pgm : σ(Typing Datatype Decl.)

dt-declΣ, ai : κ i i ⊢dc i Dj { τj(T : κ i → ⋆) ∈ ΣT aijjΣ ⊢dt data T ai i = Dj { D j : ∀ai : κ i i .τjjiΣ ⊢τdc D { τ ′(Typing Data Constructor Decl.)

dc-declΣ ⊢ τi → τ : ⋆kiΣ ⊢τdc D τi i { τi i → τΣ ⊢k τ : κ(Kinding)
k-app

k-var

k-tcon(a : κ) ∈ Σ(T : κ) ∈ Σ

k-nat

k-arrowΣ ⊢k a : κΣ ⊢k T : κΣ ⊢k Int : ⋆Σ ⊢k →: ⋆ → ⋆ → ⋆Σ ⊢k τ1 : κ 1 → κ 2 Σ ⊢k τ2 : κ 1
Σ ⊢k τ1 τ2 : κ 2

Fig. 1. Declarative specification of Haskell98 datatype declarations

2.3

Desirable Properties for Kind Inference

One goal in writing this paper is to provide concrete, principled guidance to implementors ofdependently typed languages, such as GHC/Haskell. It is thus important to be able to describe
our inference algorithm as sound and complete against a declarative specification. This declarative
specification is what we might imagine a programmer to have in her head as she programs. Thissystem should be designed with a minimum of low-level detail and a minimum of surprises. It isthen up to an algorithm to live up to the expectations set by the specification. The algorithm issound when all programs it accepts are also accepted by the specification; it is complete when all
programs accepted by the specification are accepted by the algorithm.
Why choose the particular set of features described here? Because they lead to interestingkind inference challenges. We have found that the features above are sufficient in exploring kindinference in modern Haskell. We consider unformalized extensions in Section 8.
3

DATATYPES IN HASKELL98

We begin our formal presentation with Haskell98. The fragment of the syntax of Haskell98 thatconcerns us appears at the top of Figure 1, including datatype declarations, types, kinds, and contexts.
The metavariable e refers to expressions, but we do not elaborate the details of expressions’ syntax
or typing rules here. A program pgm is a sequence of groups (defined below) of datatype declarations
T , followed by an expression e. We write τ1 → τ2 as an abbreviation for (→) τ1 τ2 .
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

3.1

53:7

Groups and Dependency Analysis

Users are free to write declarations in any order: earlier declarations can depend on later ones inthe same compilation unit. However, any kind-checking algorithm must process the declarations in
dependency order. Complicating this is that type declarations may be mutually recursive. A formal
analysis of this dependency analysis is not enlightening, so we consider it to be a preprocessing stepthat produces the grammar in Figure 1. This dependency analysis breaks up the (unordered) raw
input into mutually recursive groups (potentially containing just one declaration), and puts thesein dependency order. We use the term group to describe a set of mutually recursive declarations.
3.2

Declarative Typing Rules

The declarative typing rules are in Figure 1. There are no surprises here; we review these rules
briefly. The top judgment is Σ; Ψ ⊢pgm pgm : σ . Its rule pgm-dt extends the input type context
Σ with kinds for the datatype declarations to form Σ ′, which is used to check both the datatypei
declarations and the rest of the program. In rule pgm-dt, we implicitly extract the names T fromithe declarations T (and use this abuse of notation throughout our work, relating T to T and Dto D). The kinds are guessed for an entire group all at once: they are added to the context before
looking at the declarations. This is needed because the declarations in the group refer to one another.
Guessing the right answer is typical of declarative type systems. The algorithmic system presented
in Section 4 provides a mechanism for an implementation. Although there is no special judgmentiifor typing a group of mutually recursive datatypes, we use Σ ⊢grp rec Ti { κ i i ; Ψi to denote thatithe kinding results of datatype declarations are κ i i , and the output term contexts are Ψi .
Declarations are checked with Σ ⊢dt T { Ψ. This uses the guessed kinds to process the data
constructors of a declaration, producing a term context Ψ with the data constructors and theirtypes. The rule dt-decl ensures that the datatype has an appropriate kind in the context and thenchecks data constructors using the ⊢dc judgment. These checks are done in a type context extended
with bindings for the type variables ai i , where each ai has a kind extracted from the guessed kindof the datatype T . The subscript on the ⊢dc judgment is the return type of the constructors, whosetypes are easily checked by rule dc-decl. The kinding judgment Σ ⊢k τ : κ is standard.
4

KIND INFERENCE FOR HASKELL98

We now present the algorithmic system for Haskell98. Of particular interest is the defaulting rule
(Section 4.3), which means that these rules are not complete with respect to the declarative system.
4.1

SyntaxThe top of Figure 2 describes the syntax of kinds and contexts in the algorithmic system for
Haskell98. The differences from the declarative system are highlighted in gray. Kinds are extended
with unification kind variables αb. Algorithmic contexts are also extended with unification kindvariables, either unsolved (bα ) or solved (bα = κ). Although the grammar for algorithmic term
contexts Γ appears identical to that of declarative contexts, note that the grammar for κ has been
extended; accordingly, algorithmic contexts Γ might include kinds with unification variables, while
declarative contexts Ψ do not. This approach of recording unification variables and their solutions in
the contexts is inspired by Gundry et al. [2010] and Dunfield and Krishnaswami [2013]. Importantly,
an algorithmic context is an ordered list, which enforces that given ∆1 , αb = κ, ∆2 , the kind κ mustb βb = αb. Complete
be well-formed under ∆1 . This rules out solutions like αb = αb → ⋆ or αb = β,contexts Ω are contexts with all unification variables solved.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:8

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveirakindκterm context
Γtype context∆, Θcomplete type context ΩΩ; Γ ⊩pgm pgm : σF ⋆ | κ 1 → κ 2 | αb
F • | Γ, D : σ
F • | ∆, a : κ | ∆,T : κ | ∆, αb | ∆, αb = κF • | Ω, a : κ | Ω,T : κ | Ω, αb = κ(Typing Program)a-pgm-dtia-pgm-expr

Θi ⊩dt Ti { Γi ⊣ Θi+1[Ω]Ω; [Ω]Γ ⊢ e : σΩ; Γ ⊩pgm e : σiΘ1 = Ω, αbi , Ti : αbiiΘn+1 −→→ Ω′Ω; Γ ⊩pgm rec Ti

i ∈1..niΩ ′; Γ, Γi ⊩pgm pgm : σ; pgm : σ∆ ⊩dt T { Γ ⊣ Θ(Typing Datatype Decl.)

a-dt-decl(T : κ) ∈ ∆ii∆, αbi ⊩u [∆]κ ≈ (bα i → ⋆) ⊣ Θ1 , αbi = κ i∆ ⊩ data T ai = Djdt∆ ⊩τdc D { τ ′ ⊣ Θij ∈1..niΘj , ai : κ i i ⊩dc i Dj { τj ⊣ Θj+1 , ai : κ i i
T aij{ D j : ∀ai : κ i .τj ⊣ Θn+1

a-dc-decli(Typing Data Constructor Decl.)∆ ⊩k τi i → τ : ⋆ ⊣ Θ∆ ⊩τdc D τi i { τi i → τ ⊣ ΘFig. 2. Algorithmic program typing in Haskell98

We use a hole notation for inserting or replacing declarations in the middle of a context. ∆[Θ]means that ∆ is of the form ∆1 , Θ, ∆2 . To reduce clutter, when we have ∆[bα ], we also use only
∆ to refer to the same context. If we have ∆[b
α ] = ∆1 , αb, ∆2 , then ∆[b
α = κ] = ∆1 , αb = κ, ∆2 .
This notation allows multiple holes: ∆[Θ1 ][Θ2 ] means that ∆ is of the form ∆1 , Θ1 , ∆2 , Θ2 , ∆3 . For
b is ∆1 , αb, ∆2 , β,b ∆3 . Critically, αb appears before β.
bexample, ∆[b
α ][β]
Since type contexts carry solutions for unification variables, we use contexts as substitutions:[∆]κ applies ∆ to kind κ. Applying ∆ substitutes all solved unification variables in its argument
idempotently. If under a complete context Ω, a kind κ is well-formed, then [Ω]κ contains nounification variables and is thus a well-formed declarative kind. For term contexts, [∆]Γ applies∆ to each kind in Γ. Similarly, if under Ω, a term context Γ is well-formed, then [Ω]Γ gives backa declarative term context. The notation [Ω]∆ applies a complete context Ω to ∆. We apply Ω tothe kind of type variables and type constructors in ∆ and remove the binding of solved unification
variables from ∆. The full definition of context substitution is in the technical supplement. As above,[Ω]∆ is a declarative type context.
4.2

Algorithmic Typing Rules

Figure 2 presents the typing rules for programs, datatype declarations and data constructor declarations. As this work focuses on the problem of kind inference of datatypes, we reduce theexpression typing to the declarative system (rule a-pgm-expr); note that the contexts used there
are declarative, as explained above. For type-checking a group of mutually recursive datatypes(rule a-pgm-dt), we first assign each type constructor a unification variable αb, and then type-check(⊩dt ) each datatype definition (Section 4.4), producing the context Θn+1 . Then we default (Section 4.3)
all unsolved unification variables with ⋆ using Θn+1 −→→ Ω, and continue with the rest of the
program. Defaulting here means that the constraints of one group do not propagate to the restof the program; accordingly, the input context of ⊩pgm is always a complete context. Echoing theProc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

jKind Inference for Datatypes

53:9
i

i

notation for the declarative system, we write Ω ⊩grp rec Ti { κ i i ; Γi ⊣ Θ to denote that theresults of type-checking a group of datatype declarations are the kinds κ i i , the output term contextsiΓi , and the final output type context Θ.
4.3

Defaulting

One of the key properties of datatypes in Haskell98 is the defaulting rule. In a datatype definition,
if a type parameter is not fully determined by the definitions in its mutually recursive group, it isdefaulted to have kind ⋆.
→). An algorithmic context ∆ is defaulted to a complete context Ω,Definition 4.1 (Defaulting, −→written ∆ −→→ Ω by replacing all unsolved unification variables αb in ∆ with αb = ⋆.
To understand how this rule affects code in practice, consider the following definitions:data Q1 a = MkQ1 -- Q1 :: (⋆ → ⋆)data P1 a = MkP1 P2 -- P1 :: (⋆ → ⋆) → ⋆data Q2 = MkQ2 (Q1 Maybe) -- rejected
data P2 = MkP2 (P1 Maybe) -- accepted
One might think that the result of checking Q1 and Q2 would be the same as checking P1 and P2.
However, this is not true. Q1 and Q2 are not mutually recursive: they will not be in the same group
and are checked separately. In contrast, P1 and P2 are mutually recursive and are checked together.
This difference leads to the rejection of Q2: after kinding Q1, the parameter a is defaulted to ⋆, andthen Q1 Maybe fails to kind check. Our algorithm is a faithful model of datatypes in Haskell98, andthis rejection is exactly what the step Θn+1 −→→ Ω (in rule a-pgm-dt) brings.
Other design alternatives. One alternative design is to default in rule a-pgm-expr instead ofrule a-pgm-dt, as shown in rule a-pgm-expr-alt. This means constraints in one group propagate
to other groups, but not to expressions. Then Q2 above is accepted.
∆ −→→Ω[Ω]Ω; [Ω]Γ ⊢ e : σ
a-pgm-expr-alt∆; Γ ⊩pgm e : σ
A second alternative is that defaulting happens at the very end of type-checking a compilation unit.
In this scenario, we wait to commit to the kind of a datatype until checking expressions. Now we
can accept the following program, which would otherwise be rejected. However, this strategy does
not play along well with modular design, as it takes an extra action at a module boundary.
data Q1 a = MkQ1
mkQ1
= MkQ1 :: Q1 Maybe
In the rest of this section, we stay with the standard, doing defaulting as portrayed in Figure 2.
4.4

Checking Datatype Declarations

The judgment ∆ ⊩dt T { Γ ⊣ Θ checks the datatype declaration T under the input context ∆,returning a term context Γ and an output context Θ. Its rule a-dt-decl first gets the kind κ of thethe type constructor from the context. It then assigns a fresh unification variable αb to each typei

parameter. The expected kind of the type constructor is αbi → ⋆. The rule then unifies κ withi

αbi → ⋆. Before unification, we apply the context to κ; unification (Section 4.6) requires its inputs
to be inert with respect to the context substitution. Our implementation of unification guarantees
that all the αbi will be solved, as reflected in the rule a-dt-decl. The type parameters are added
to the context to type check each data constructor. Checking the data constructor Dj returns its
itype τj and the context Θj+1 , ai : αbi . Note that each output context must be of this form as no new
entries are added to the end of the context during checking individual data constructors. We canthen generalize the type τj over type parameters, returning Θn+1 as the result context.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:10Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira∆ ⊩k τ : κ ⊣ Θ(Kinding)
a-k-tcona-k-var(T : κ) ∈ ∆a-k-arrow∆ ⊩ →: ⋆ → ⋆ → ⋆ ⊣ ∆k(a : κ) ∈ ∆a-k-nat∆⊩ T :κ ⊣∆∆ ⊩ Int : ⋆ ⊣ ∆k∆ ⊩k a : κ ⊣ ∆ka-k-app∆ ⊩k τ1 : κ 1 ⊣ Θ1

Θ1 ⊩k τ2 : κ 2 ⊣ Θ2

Θ2 ⊩kapp [Θ2 ]κ 1 • [Θ2 ]κ 2 : κ 3 ⊣ Θ∆ ⊩k τ1 τ2 : κ 3 ⊣ Θ∆ ⊩kapp κ 1 • κ 2 : κ ⊣ Θ(Application Kinding)a-kapp-arrowa-kapp-kuvar∆[b
α 1 , αb2 , αb = αb1 → αb2 ] ⊩u αb1 ≈ κ ⊣ Θ∆ ⊩u κ 1 ≈ κ ⊣ Θ∆[bα ] ⊩kapp αb • κ : αb2 ⊣ Θ∆ ⊩kapp κ 1 → κ 2 • κ : κ 2 ⊣ Θ∆ ⊩u κ 1 ≈ κ 2 ⊣ Θ(Kind Unification)a-u-arrow∆ ⊩ κ 1 ≈ κ 3 ⊣ Θ1

Θ1 ⊩ [Θ1 ]κ 2 ≈ [Θ1 ]κ 4 ⊣ Θuua-u-refl∆⊩ κ ≈κ ⊣∆∆ ⊩ κ1 → κ2 ≈ κ3 → κ4 ⊣ Θuua-u-kvarR

a-u-kvarLprpr∆ ⊩αb κ ⇝ κ 2 ⊣ Θ[bα]∆ ⊩αb κ ⇝ κ 2 ⊣ Θ[bα]∆[bα ] ⊩u αb ≈ κ ⊣ Θ[bα = κ2 ]∆[b
α ] ⊩u κ ≈ αb ⊣ Θ[bα = κ2 ]pr∆ ⊩αb κ 1 ⇝ κ 2 ⊣ Θ(Promotion)a-pr-arrow

a-pr-starpr∆ ⊩αb ⋆ ⇝ ⋆ ⊣ ∆a-pr-kuvarLb α ] ⊩pr βb ⇝ βb ⊣ ∆[β][bb α]∆[β][bαbpr∆ ⊩αb κ 1 ⇝ κ 3 ⊣ ∆1prpr

∆1 ⊩αb [∆1 ]κ 2 ⇝ κ 4 ⊣ Θ∆ ⊩αb κ 1 → κ 2 ⇝ κ 3 → κ 4 ⊣ Θa-pr-kuvarRb ⊩pr βb ⇝ βb1 ⊣ ∆[βb1 , αb][βb = βb1 ]∆[bα ][β]
αbFig. 3. Algorithmic kinding, unification and promotion in Haskell98.

The data constructor declaration judgment ∆ ⊩τdc D { τ ′ ⊣ Θ type-checks a data constructor,
by simply checking that the expected type τi i → τ is well-kinded.
4.5

Kinding

The algorithmic kinding ∆ ⊩k τ : κ ⊣ Θ is given in Figure 3. Most rules are self-explanatory. For
applications (rule a-k-app), we synthesize the type for an application τ1 τ2 , where τ1 and τ2 havekinds κ 1 and κ 2 , respectively. The hard work is delegated to the application kinding judgment.
Application kinding ∆ ⊩kapp κ 1 •κ 2 : κ ⊣ Θ says that, under the context ∆, applying an expressionof kind κ 1 to an argument of kind κ 2 returns the result kind κ and an output context Θ. We require
the invariants that [∆]κ 1 = κ 1 and [∆]κ 2 = κ 2 . Therefore, if the kind is a unification variable αb(rule a-kapp-kuvar), we know it must be an unsolved unification variable. Since we know κ 1 must
be a function kind, we solve αb using αb1 → αb2 , unify αb1 with the argument kind κ, and return αb2 .
Note that the unification variables αb1 and αb2 are inserted in the middle of the context ∆; this allows
us to remove the type variables from the end of the context in rule a-dt-decl and also plays acritical role in maintaining unification variable scoping in the more complicated system we analyze
later. If the kind of the function is not a unification variable, it must surely be a function kind
κ 1 → κ 2 (rule a-kapp-arrow), so we unify κ 1 with the known argument kind κ, returning κ 2 .
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

4.6

53:11

Unification

The unification judgment ∆ ⊩u κ 1 ≈ κ 2 ⊣ Θ is given in Figure 3. The elaborate style of thisjudgment (and its helper judgment ⊩pr ) is overkill for Haskell98, but this design sets us up well tounderstand unification in the presence of our PolyKinds system, later. We require the preconditions
that [∆]κ 1 = κ 1 and [∆]κ 2 = κ 2 , so that every time we encounter a unification variable, we know
it is unsolved. Rule a-u-refl is our base case, and rule a-u-arrow unifies the components of thearrow types. When unifying αb ≈ κ (rule a-u-kvarL), we cannot simply set αb to κ, as κ might
include variables bound to the right of αb. Instead, we need to promote (⊩pr ) κ.
Promotion. The crucial observation of ⊩pr is that the relative order between unification variables
does not matter for solving a constraint. Consider unifying αb, βb ⊩u αb ≈ βb → ⋆. We cannot set
αb = βb → ⋆, as this is ill-scoped. However, the constraint is solvable, as one solution context canb
be βb1 , αb = βb1 → ⋆, βb = βb1 . In other words, although βb → ⋆ contains an out-of-scope variable β,bbb
we can solve the constraint by introducing a fresh in-scope variable β 1 and setting β = β 1 .
pr
The promotion judgment ∆ ⊩αb κ 1 ⇝ κ 2 ⊣ Θ captures this observation. The judgment says
that, under the context ∆, we promote the kind κ 1 , yielding κ 2 , so that κ 2 is well-formed in theprefix context of αb, while retaining [Θ]κ 1 = [Θ]κ 2 . At a high-level, ⊩pr looks for free variablesin κ 1 . Kind constants are always well-formed (rule a-pr-star). Variables bound to the left of αbin ∆ are unaffected (rule a-pr-kuvarL), as they are already well-formed. In rule a-pr-kuvarR, aunification variable βb bound to the right of αb in ∆ is replaced by a fresh variable introduced to αb’s
left. Promotion is a partial operation, as it requires βb either to be to the right or to the left of αb.
There is yet another possibility: if βb = αb, then no rule applies. This is a desired property, as theβb = αb case exactly corresponds to the “occurs-check” in a more typical presentation of unification.
By preventing promoting αb to the left of αb, we prevent the possibility of an infinite substitution
when applying an algorithmic context. It is this promotion algorithm that guarantees that all the αbiwill be solved in rule a-dt-decl: those variables will appear to the right of the unification variable
invented in rule a-pgm-dt and will be promoted (and thus solved).
Returning to the ⊩u judgment, rule a-u-kvarL first promotes the kind κ, yielding κ 2 , so that κ 2 iswell-formed in the prefix context of αb. We can then set αb = κ 2 in the concluding context. Rule a-ub either rule a-u-kvarL andkvarR is symmetric to rule a-u-kvarL. Note that when unifying αb ≈ β,rule a-u-kvarR could be tried; an implementation can arbitrarily choose between them.
4.7

Soundness and Completeness

The main theorem of soundness is for program typing:
Theorem 4.2 (Soundness of ⊩pgm ). If Ω ok, and Ω ⊩ectx Γ, and Ω; Γ ⊩pgm pgm : σ , then [Ω]Ω; [Ω]Γ ⊢pgm
pgm : σ .
This lemma statement refers to judgments Ω ok and Ω ⊩ectx Γ; these basic well-formedness
checks are given in the technical supplement. Because the declarative judgment ⊢pgm requires
declarative contexts, we write [Ω]Ω and [Ω]Γ in the conclusion, applying the complete algorithmic
context Ω as a substitution to form a declarative context, free of unification variables.
The statement of completeness relies on the definition of context extension ∆ −→ Θ. The judgment
captures a process of information increase. The formal definition of context extension is given in
the technical supplement, and its treatment is as in Dunfield and Krishnaswami [2013]. Intuitively,
context extension preserves all information in ∆, and may increase the information by adding
or solving more unification variables. In all the algorithmic judgments, the output context is anextension of the input context.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:12

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira

We prove that our system is complete only up to checking a group of datatype declarations.
ii

Theorem 4.3 (Completeness of ⊩grp ). Given Ω ok, if [Ω]Ω ⊢grp rec Ti { κ i i ; Ψi , then there exists
i
i
i
i
i
i
κ i′ , Γi , Θ, and Ω ′, such that Ω ⊩grp rec Ti { κ i′ ; Γi ⊣ Θ, where Θ −→ Ω ′, and [Ω ′]κ i′ = κ i , andi

Ψi = [Ω ′]Γi .
The theorem statement uses the notational convenience for checking groups, defined in Section 3.2 and Section 4.2. The theorem states that for every possible declarative typing for a group,
the algorithmic typing results can be extended to support the declarative typing.
Unfortunately, the typing program judgment ⊢pgm is incomplete, as our algorithm models defaulting, while the declarative system does not. (For example, the Q1/Q2 example of Section 4.3
is accepted by the declarative system but rejected by both GHC and our algorithmic system.) As
straightforward as the defaulting rule may seem, it is surprisingly hard to model in a declarative
system. We remedy this in the next section.
5

TYPE PARAMETERS, PRINCIPAL KINDS AND COMPLETENESS IN HASKELL98

We have seen that our judgments for checking programs ⊢pgm and ⊩pgm do not support completeness,because the declarative system cannot easily model the defaulting rule given in Section 4.3. In thissection, we introduce kind parameters, inspired by type parameters in Garcia and Cimini [2015],
and relate the defaulting rule to principal kinds to recover completeness.
5.1

Type Parameters

Consider the datatype data App f a = MkApp (f a) again. The parameter a in this example can beof any kind, including ⋆, ⋆ → ⋆, or others. To express this polymorphism without introducing firstclass polymorphism, we endow the declarative system with a set of kind parameters. Importantly,
kind parameters live only in our reasoning; users are not allowed to write any kind parameters inthe source. We amend the definition of kinds in Figure 1 as follows.
kind parameter P
kind
κ

∈
KParamF ⋆ | κ1 → κ2 | P

Kind parameters are uninterpreted kinds: there is no special treatment of kind parameters in thetype system. Think of them as abstract, opaque kind constants. Kind parameters are eliminatedby substitutions S, which map kind parameters to kinds, and homomorphically work on kinds
themselves. For example, App can be assigned kind (P → ⋆) → P → ⋆. By substituting for P,
we can get, for example, (⋆ → ⋆) → ⋆ → ⋆. Indeed, from (P → ⋆) → P → ⋆ we can get allother possible kinds of App. This leads to the definition of principal kinds for a group; and to theproperty that for every well-formed group, there exists a list of principal kinds.
Definition 5.1 (Principal Kind in Haskell98 with Kind Parameters). Given a context Σ, a groupii
rec Ti , and a list of kinds κ i i , we say that the κ i i are principal kinds of Σ and rec Ti , denoted as
i
i
i
i
i
i
Σ ⊢ rec Ti {p κ i i , if Σ ⊢grp rec Ti { κ i i ; Ψi , and whenever Σ ⊢grp rec Ti { κ i′ ; Ψi′ holds,iithere exists some substitution S, such that S(κ i ) = κ i′ and S(Ψi ) = Ψi′ .
ii
Theorem 5.2 (Principality of Haskell98 with Kind Parameters). If Σ ⊢grp rec Ti { κ i i ; Ψi , theniiithere exists some κ i′ such that Σ ⊢ rec Ti { p κ i′ .
5.2

Principal Kinds and Defaulting

Using the notion of kind parameters, we can now incorporate defaulting into the declarative
specification of Haskell98. To this end, we define the defaulting kind parameter substitution S ⋆ :Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:13

Definition 5.3 (Defaulting Kind Parameter Substitution). Let S ⋆ ∈ KParam → κ denote thesubstitution that substitutes all kind parameters to ⋆.
Using S ⋆ , we can rewrite rule pgm-dt. Noteworthy is the fact that kind parameters only live in the
middle of the derivation (in the κ i ), but never appear in the results S ⋆ (κ i ).
iΣ ⊢grp rec Ti { κ i i ; Ψi

i

i

i

i

Σ, Ti : S ⋆ (κ i ) ; Ψ, S ⋆ (Ψi ) ⊢pgm pgm : σΣ ⊢ rec Ti { p κ i i

pgm-dtPi

Σ; Ψ ⊢pgm rec Ti ; pgm : σ
5.3

Completeness

The two versions of defaulting (the one above and ∆ −→→ Ω of Section 4.2) are equivalent. This
fact is embodied in the following theorem, stating that the algorithmic system is complete withrespect to the declarative system with kind parameters.
Theorem 5.4 (Completeness of ⊩pgm with Kind Parameters). Given algorithmic contexts Ω, Γ, anda program pgm, if [Ω]Ω; [Ω]Γ ⊢pgm pgm : σ , then Ω; Γ ⊩pgm pgm : σ .
6

DECLARATIVE SYNTAX AND SEMANTICS OF POLYKINDS

Having set the stage for kind inference for datatypes in Haskell98, we now present the declarative
PolyKinds system. Our syntax is given at the top of Figure 4. Compared to Haskell98, programs
pgm now include datatype signatures S. Data constructor declarations D support existential quantification. Types and kinds are collapsed into one level; σ and K are now synonymous metavariables
and allow prenex polymorphism, where variables in a kind binder ϕ can optionally have kindannotations. Monotypes τ and κ allow visible kind applications τ1 @τ2 . Elaborated types µ, η are
the result of elaboration, which decorates source types to make them fully explicit. This is done
so that checking equality of elaborated types is straightforward. The syntax for elaborated types
contains inferred polymorphism ∀{ϕ c }.µ, where complete free kind binders ϕ c have all variables
annotated. Elaborated monotypes ρ and ω share the same syntax as monotypes. We informally use
only ρ or ω for elaborated monotypes.
6.1

Groups and Dependency Analysis

Decomposition of signatures and definitions allows a more fine-grained control of dependency
analysis. If T has a signature, and S depends on T , then we can kind-check S without inspecting
the definition of T , because we know the kind of T . In other words, S only depends on the signatureof T , not the definition of T . The complete dependency analysis rule, inspired by Jones [1999,
Section 11.6.3], is:Definition 6.1 (Dependency Analysis in PolyKinds).
(i) If the signature/definition of T1 mentions T2 , then:(a) if T2 has a signature, the signature/definition of T1 depends on the signature of T2 ;(b) otherwise, the signature/definition of T1 depends on the definition of T2 .
(ii) A definition depends on its signature.
To avoid a type that mentions itself in its own kind, we disallow self-dependency or mutual
dependency involving signatures. For example, a group data T1 :: T2 a → ⋆; data T2 :: T1 → ⋆is rejected, lest T1 be assigned type ∀(a :: T1). T2 a → ⋆. In other words, signatures do not form
groups: they are always processed individually. Moreover, the definition of a datatype which has asignature does not join others in a group, as according to Definition 6.1, there will be no dependency
from datatypes on it. This simplifies the kinding procedure, as we will see in the coming section.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:14

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveirai

sig S; pgm | rec Ti ; pgm | edata T : σjdata T ai i = Dj
∀ϕ.D τi i

programdatatype signature
datatype decl.
data constructor decl.

pgm
S
T
D

F
F
F
F

type, kindmonotype, monokind
elaborated type, kindσ, Kτ , κ, ρ, ωµ, ηF ∀ϕ. σ | τF ⋆ | Int | a | T | τ1 τ2 | τ1 @τ2 |→F ∀{ϕ c }.µ | ∀ϕ c . µ | ρ

term context
Ψtype context
Σkind binder list
ϕcomplete kind binder list ϕ c

F
F
F
F

• | Ψ, D : µ• | Σ, a : ρ | Σ,T : η• | ϕ, a | ϕ, a : κ• | ϕ c, a : ρ

Σ; Ψ ⊢pgm pgm : σ(Typing Program)
pgm-dt-ttS

pgm-sig

Σ ⊢sig S { T : ηΣ,T : η; Ψ ⊢pgm pgm : µ(T : η) ∈ ΣΣ; Ψ ⊢pgm sig S; pgm : µΣ ⊢dt T { Ψ1Σ; Ψ, Ψ1 ⊢pgm pgm : µ

Σ; Ψ ⊢pgm rec T ; pgm : µ

pgm-dt-ttiΣ, ϕ ic ⊢ela ωi : ⋆i

ϕ ic ∈ Q(ωi )

i

i

i

Σ, ∪ϕ ic , Ti : ωi ⊢dt Ti { Ψi

i
i

i
i

i gen

Σ, ∪ϕ ic , Ti : ωi ⊢ϕ c Ψi { Ψi′iΣ, Ti : ∀{ϕ ic }.ωi ; Ψ, Ψi′[Ti 7→ Ti @ϕ ic ] ⊢pgm pgm : σiiΣ; Ψ ⊢pgm rec Ti ; pgm : σΣ ⊢sig S { T : η(Typing Signature)

sig-tt⌉σ ⌈ϕ ∈ Q(σ )ϕ 1c ∈ Q(∀ϕ c . η)Σ, ϕ 1c ⊢k ∀ϕ. σ : ⋆ { ∀ϕ c . η|ϕ | = |ϕ c |Σ ⊢sig data T : σ { T : ∀{ϕ 1c }.∀{ϕ c }.η
Σ ⊢dt T { Ψ(Typing Datatype Decl.)

dt-tt(T : ∀{ϕ 1c }.∀ϕ 2c . ω i i → ⋆) ∈ ΣjΣ, ϕ 1c , ϕ 2c , ai : ωi i ⊢dc(T @ϕ 1c @ϕ 2c ai i )jjΣ ⊢dt data T ai i = Dj { D j : ∀{ϕ 1c }.∀ϕ 2c . ∀ai : ω i i .µ jΣ ⊢dcρ D { µgen

(Typing Data Constructor Decl.)Σ ⊢ϕ c Ψ1 { Ψ2

Dj { µ j(Generalization)

gen

dc-tt

ϕ c ∈ Q(µ\Σ,τi i )Σ, ϕ c ⊢k ∀ϕ.τi i → ρ : ⋆ { µ

i
c
Σ ⊢dc
ρ ∀ϕ.D τi { ∀{ϕ }.µϕ c , ϕ ic ∈ Q(µ i )
gen

i

i

Σ ⊢ϕ c D i : µ i { D i : ∀{ϕ c , ϕ ic }.µ iiFig. 4. Declarative specification of PolyKinds

6.2

Checking Programs

The declarative typing rules appear in Figure 4. The judgment Σ; Ψ ⊢pgm pgm : σ checks the
program. From now on we omit the typing rule for expressions in programs, which is essentiallythe same as in Haskell98. Rule pgm-sig processes kind signatures by elaborating and generalizing
the kind, then adding it to the context Σ. The helper judgment Σ ⊢sig S { T : η checks a kind
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:15

Σ ⊢inst µ 1 : η ⊑ ω { µ 2(Instantiation)
inst-forallΣ ⊢ela ρ : ω1

inst-reflΣ ⊢inst µ : ω ⊑ ω { µΣ ⊢kc σ ⇐ ω { µΣ ⊢inst µ 1 @ρ : η[a 7→ ρ] ⊑ ω 2 { µ 2Σ ⊢inst µ 1 : ∀a : ω 1 .η ⊑ ω2 { µ 2(Kind Checking)kc-subΣ ⊢k σ : η { µ 1Σ ⊢inst µ 1 : η ⊑ ω { µ 2Σ ⊢kc σ ⇐ ω { µ 2Σ ⊢k σ : η { µ(Kinding)
ktt-appktt-starΣ ⊢k τ1 : η 1 { ρ 1Σ ⊢inst ρ 1 : η 1 ⊑ (ω1 → ω2 ) { ρ 2Σ ⊢k ⋆ : ⋆ { ⋆Σ ⊢kc τ2 ⇐ ω1 { ρ 3Σ ⊢k τ1 τ2 : ω2 { ρ 2 ρ 3
ktt-foralli

ktt-kappΣ ⊢k κ 1 : ∀a : ω.η { ρ 1Σ ⊢kc κ 2 ⇐ ω { ρ 2Σ ⊢ela ω : ⋆Σ ⊢k κ 1 @κ 2 : η[a 7→ ρ 2 ] { ρ 1 @ρ 2

Σ, a : ω ⊢kc σ ⇐ ⋆ { µΣ ⊢k ∀a.σ : ⋆ { ∀a : ω.µΣ ⊢ela µ : η(Elaborated Kinding)ela-appela-kappΣ ⊢ela ρ 1 : ω 1 → ω2

Σ ⊢ela ρ 2 : ω 1

Σ ⊢ela ρ 1 ρ 2 : ω2

Σ ⊢ela ρ 1 : ∀a : ω.η

Σ ⊢ela ρ 2 : ωΣ ⊢ela ρ 1 @ρ 2 : η[a 7→ ρ 2 ]Fig. 5. Selected rules for declarative kind-checking in PolyKinds

signature data T : σ . First, it uses ⌉σ ⌈ to ensure σ returns ⋆: ⌉σ ⌈ simply traverses over arrows
and foralls, checking that the final kind of σ is ⋆. Then, as σ may be an open kind signature, it
extracts the free kind variables ϕ ∈ Q(σ ), where Q(σ ) is the set of all well-formed orderings ofthe free variables (transitively looking into variables’ kinds) of σ ; thus, ϕ is one such ordering. As
discussed in Section 2.2, variables in ϕ are inferred so we accept any relative order, as long as itfeatures the necessary dependency between the variables. Then the rule tries to elaborate (⊢k ) the
kind ∀ϕ. σ , where ϕ and ϕ c have the same length (|ϕ | = |ϕ c |). As the elaborated result ∀ϕ c . η canbe further generalized, we bring the free variables ϕ 1c ∈ Q(∀ϕ c . η) into scope when elaborating.
The concluding output is T : ∀{ϕ 1c }.∀{ϕ c }.η. As an example, consider a kind signature ∀a.b → ⋆.
We have ϕ = b, ϕ c = b : ⋆, and ϕ 1c = c : ⋆, and the final kind is ∀{c : ⋆}.∀{b : ⋆}.∀(a : c).b → ⋆.
We see in this one example the three sources of quantified variables, always in this order: variables
arising from generalization (c), from implicit quantification (b), and from explicit quantification (a).
Returning to the ⊢pgm judgment, rule pgm-dt-ttS checks a datatype definition that has a kindsignature. It ensures that the signature has already been checked, by fetching the kind informationin the context using (T : η) ∈ Σ. Then it checks the datatype declaration, and gathers the output
term context to check the rest of the program. Rule pgm-dt-tt, as in Haskell98, guesses kinds ωifor each datatype Ti and puts Ti : ωi in the context before looking at the declarations. The majordifference from Haskell98 is that kinds can be generalized after the group is checked. We use ϕ ic
to denote the free variables in each kind ωi . After the recursive group is typed, we generalize thekind of each type constructor as well as the type of its data constructors. To generalize the type ofdata constructors, we use the ⊢gen judgment. Rule gen generalizes every data constructor in thecontext, where ϕ c are free type variables of its corresponding type constructor, and ϕ ic are free typevariables specific to the data constructor. Returning to rule pgm-dt-tt, note that since the kinds oftype constructors are generalized, the occurrences of the type constructors now require more type
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:16

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira

arguments. Therefore in Ψi′, we substitute Ti with Ti @ϕ ic , where Ti is applied to all the variables
bound in ϕ ic .
The judgment of checking datatype declarations Σ ⊢dt T { Ψ has only rule dt-tt, which
expands on the rule in Haskell98, to support top-level polymorphism for the kind of T .
Rule dc-tt supports existential variables ϕ. Moreover, the elaborated type µ of ∀ϕ.τi i → ρ canbe further generalized over ϕ c . Note that ϕ c (via a small abuse of notation in the rule) excludes freevariables in τi and Σ.
6.3

Checking Kinds

The kinding judgment ⊢k appears in Figure 5. For space reasons, we present only selected rules.
Kinding Σ ⊢k σ : η { µ infers the type σ to have kind η, and it elaborates σ to µ. The kinding rules
are built upon the axiom Σ ⊢k ⋆ : ⋆ { ⋆ (rule ktt-star). While this axiom is known to violate
logical consistency, as Haskell is already logically inconsistent because of its general recursion, we
do not consider it as an issue here. Rule ktt-app concerns applications τ1 τ2 . It first infers the kindof τ1 to be η 1 . The kind η 1 can be a polymorphic kind headed by a ∀, though it is expected to be afunction kind. Thus the rule uses ⊢inst to instantiate η 1 to ω1 → ω2 . The instantiation judgmentΣ ⊢inst µ 1 : η ⊑ ω { µ 2 instantiates a kind η to a monokind ω, where if µ 1 has kind η then µ 2
has kind ω. After instantiation, rule ktt-app checks (⊢kc ) the argument τ2 against the expectedargument kind ω1 . The kind checking judgment ⊢kc simply delegates the work to kinding andinstantiation. Rule ktt-kapp checks visible kind applications. Note in the return kind η, the variable
a is substituted by the elaborated argument ρ 2 . Rule ktt-foralli elaborates an unannotated type∀a.σ to ∀a : ω.µ, where ω is an elaborated kind (⊢ela ) guessed for a.
The stand-alone elaborated kinding judgment ⊢ela type-checks elaborated types. As all necessary
instantiation has been done, type-checking for elaborated types is easy. For example, rule ela-app
concerns applications ρ 1 ρ 2 . Compared to rule ktt-app, here ρ 1 has an arrow kind, and takes exactly
the kind of ρ 2 . All judgments output well-formed elaborated types, as the following lemma states:
Lemma 6.2 (Type Elaboration). We have: (1) if Σ ⊢k σ : η { µ, then Σ ⊢ela µ : η; (2) if Σ ⊢kc σ ⇐η { µ, then Σ ⊢ela µ : η; (3) if Σ ⊢ela µ 1 : η, and Σ ⊢inst µ 1 : η ⊑ ω { µ 2 , then Σ ⊢ela µ 2 : ω.
7

KIND INFERENCE FOR POLYKINDS

We now describe the algorithmic counterpart of the PolyKinds system. Figure 6 presents the syntax
of kinds and contexts in the algorithmic system for PolyKinds. Elaborated monotypes are extended
with unification variables αb. Echoing the algorithm for Haskell98, type contexts are extended withunification variables, which now have kinds (bα : ω and αb : ω = ρ). Also added to contexts are
local scopes {∆}. These are special type contexts, where variables can be reordered. Recall the kind∀(a :: (f b)) (c :: k). f c → ⋆ in Section 2, where f and b appear before k, but end up depending on
k. In which order should we put f , b and k in the algorithmic context to kind-check the signature?
We cannot have a correct order before completing inference. Therefore, we put them into a local
scope, knowing we can reorder the variables during kind-checking according to the dependency
information. The well-formedness judgment for local scopes requires them to be well-scoped,
leading to the fact that ∆, {∆ ′ } is well-formed iff ∆, ∆ ′ is. The marker ▶D , subscripted by the nameof a data constructor, is used only in and explained with rule a-dc-tt.
7.1

Algorithmic Program Typing

The algorithmic typing rules appear in Figure 6. The judgment Ω; Γ ⊩pgm pgm : µ checks the
program. The rule a-pgm-sig and rule a-pgm-dt-ttS correspond directly to the declarative rules.
Note that as the datatype declaration in rule a-pgm-dt-ttS already has a signature, the output type
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:17

F ⋆ | Int | a | T | ρ 1 ρ 2 | ρ 1 @ρ 2 |→| αb
F • | Γ, D : µ
F • | ∆, a : ω | ∆,T : η∆, αb : ω | ∆, αb : ω = ρ | ∆, {∆ ′ } | ∆, ▶D|
F • | Ω, a : ω | Ω,T : η | Ω, αb : ω = ρ | Ω, {Ω ′ } | Ω, ▶D
F • | ϕbc , αb : κ

ρ, ω
Γ
∆, Θ

elaborated monotype
term context
type context

complete type context Ωkind binder listϕbcΩ; Γ ⊩pgm pgm : µ(Typing Program)(T : η) ∈ ΩΩ ⊩dt T { Γ1 ⊣ ΩΩ; Γ, Γ1 ⊩pgm pgm : µ

a-pgm-dt-ttS

a-pgm-sigΩ ⊩sig S { T : ηΩ,T : η; Γ ⊩pgm pgm : µΩ; Γ ⊩pgmΩ; Γ ⊩pgm rec T ; pgm : µ

sig S; pgm : µ

a-pgm-dt-tti

Θ1 = Ω, αbi : ⋆ , Ti : αbiiΘi ⊩dt Ti { Γi ⊣ Θi+1

i

i
i
gen
c
c
′
b
Θn+1 ⊩ϕ c ([Θn+1 ](Γi [ ϕ i 7→ ϕ i ])) { Γi
i
i
i
i
i
c
c
c
α i )[ ϕbi 7→ ϕ i ]) ; Γ, Γi′[Ti 7→ Ti @ϕ ic ] ⊩pgm pgm : µΩ, Ti : ∀{ϕ i }.(([Θn+1 ]bi ∈1..nΩ; Γ ⊩pgm rec Ti; pgm : µiϕbic = unsolved([Θn+1 ]bαi )Ω ⊩sig S { T : η(Typing Signature)

a-sig-ttiai = fkv(σ )Ω, {bα i : ⋆, ai : αbi } ⊩ σ : ⋆ { η ⊣ ∆⌉σ ⌈ic
ϕ 1 = scoped_sort(ai : [∆]bαi )ϕb2c = unsolved(∆)∆ ,→ ai iΩ ⊩sig data T : σ { T : ∀{ϕ 2c }.((∀{ϕ 1c }.[∆]η)[ϕb2c 7→ ϕ 2c ])ik∆ ⊩dt T { Γ ⊣ Θ(Typing Datatype Decl.)

a-dt-tt(T : ∀{ϕ 1c }.∀ϕ 2c . ω) ∈ ∆ii∆, ϕ 1c , ϕ 2c , αbi : ⋆ ⊩u [∆]ω ≈ (bα i → ⋆) ⊣ Θ1 , ϕ 1c , ϕ 2c , αbi : ⋆ = ω i

Θj , ϕ 1c , ϕ 2c , ai : ωi i ⊩dc(T @ϕ 1c @ϕ 2c ai i )∆ ⊩dt data T ai i = Dj

j ∈1..n

Dj { µ j ⊣ Θj+1 , ϕ 1c , ϕ 2c , ai : ωi i

i

j

j

{ D j : ∀{ϕ 1c }.∀ϕ 2c . ∀ai : ωi i .µ j ⊣ Θn+1

∆ ⊩dc
ρ D { µ ⊣Θ(Typing Data Constructor Decl.)
a-dc-tt∆, ▶D ⊩k ∀ϕ.(τi i → ρ) : ⋆ { µ ⊣ Θ1 , ▶D , Θ2

ϕbc = unsolved(Θ2 )

i
c
c
bc
∆ ⊩dc
ρ ∀ϕ.D τi { ∀{ϕ }.(([Θ2 ]µ)[ϕ 7→ ϕ ]) ⊣ Θ1

Fig. 6. Algorithmic program typing in PolyKinds

context remains unchanged. Rule a-pgm-dt-tt concerns a group (without kind signatures). Like in
Haskell98, it first assigns a fresh unification variable αbi : ⋆ as the kind of each type constructor, andthen type-checks each datatype declaration, yielding the output context Θn+1 . Unlike Haskell98
which then uses defaulting, here from each αbi we get their unsolved unification variables ϕbic andgeneralize the kind of each type constructor as well as the type of each data constructor. The
unsolved(∆) metafunction simply extracts a set of free unification variables in ∆, with their kinds
substituted by ∆. Before generalization, we apply Θn+1 to the results so all solved unification
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:18Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira

variables get substituted away. We use the notation ϕbic 7→ ϕ ic to mean that all unification variables
in ϕbic are replaced by fresh type variables in ϕ ic . The algorithmic generalization judgment ⊩gencorresponds straightforwardly to the declarative rule, and thus is included only in the technicalsupplement. Though they appear daunting, the extended contexts used in the last premise to thisrule are unsurprising: they just apply the relevant substitutions (the solved unification variables inΘn+1 , the replacement of unification variables with fresh proper type variables ϕbic 7→ ϕ ic , and thegeneralization of the kinds of the group of datatypes Ti 7→ Ti @ϕ ic ).
The judgment Ω ⊩sig S { T : η type-checks a signature definition. We get all free variables in σusing fkv(σ ) and assign each variable ai a kind αbi : ⋆. Those variables are put into a local scope tokind-check σ . Then, we use scoped_sort—a standard topological sort—to return an ordering of thevariables that respects dependencies. Finally, we substitute away solved unification variables in the
result kind µ and generalize over the unsolved variables ϕb2c in ∆. As ϕb2c is generalized outside ϕ 1c ,we use the quantification check ∆ ,→ ai i (Section 7.2) to ensure the result kind is well-ordered.
Rule a-dt-tt is a straightforward generalization of rule a-dt-decl to polymorphic kinds. HereT can have a polymorphic kind from kind signatures.
Rule a-dc-tt checks a data constructor declaration. It first puts a marker into the context before
kinding. After kinding, it substitutes away all the solved unification variables to the right of themarker, and generalizes over all unsolved unification variables to the right of the marker. The factthat the context is ordered gives us precise control over variables that need generalization.
7.2

The Quantification Check

Ill-ordered kinds are rejected. Consider the following example:
data Proxy :: ∀k. k → ⋆data Relate :: ∀a (b :: a). a → Proxy b → ⋆data T :: ∀(a :: ⋆) (b :: a) (c :: a) d. Relate b d → ⋆Proxy just gives us a way to write a type whose kind is not ⋆. The Relate τ1 τ2 type forces the kindof τ2 to depend on that of τ1 , giving rise to the unusual dependency in T . The definition of T thenintroduces a, b, c and d. The kinds of a, b and c are known, but the kind of d must be inferred; callb Naïvely,b where βb :: a. There are no further constraints on β.
it αb. We discover that αb = Proxy β,b
we would generalize over β, but that would be disastrous, as a is locally bound. Instead, we must
reject this definition, as our declarative specification always puts inferred variables (such as thetype variable βb would become if generalized) before other ones.
The quantification-checking metafunction ∆ ,→ ϕ, defined as fkv(unsolved(∆)) ♯ ϕ, ensures that
free variables in unsolved(∆) are disjoint (♯) with ϕ, so that we can safely generalize unsolved(∆)
outside ϕ.4
7.3

Kinding

Figure 7 presents the selected rules for kinding judgment ⊩k , along with the auxiliary judgments.
Most rules correspond directly to their declarative counterparts. For applications τ1 τ2 , rule aktt-app first synthesizes the kind of τ1 to be η 1 , then uses ⊩kapp to type-check τ2 . The judgment∆ ⊩kapp (ρ 1 : η) • τ : ω { ρ 2 ⊣ Θ is interpreted as, under context ∆, applying the type ρ 1 ofkind η to the type τ returns kind ω, the elaboration result ρ 2 , and an output context Θ. When
η 1 is polymorphic (rule a-kapp-tt-forall), we instantiate it with a fresh unification variable.
Rule a-ktt-foralli checks a polymorphic type. We assign a unification variable as the kind of a,bring αb : ⋆, a : αb into scope to check the body against ⋆, yielding the output context ∆2 , a : αb, ∆3 .
4 See also the alternative design in the technical supplement.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:19∆ ⊩inst µ 1 : η ⊑ ω { µ 2 ⊣ Θ(Instantiation)
a-inst-forall

a-inst-refl∆ ⊩u ω1 ≈ ω 2 ⊣ Θ∆, αb : ω 1 ⊩inst µ 1 @b
α : η[a 7→ αb] ⊑ ω 2 { µ 2 ⊣ Θ∆ ⊩inst µ : ω 1 ⊑ ω 2 { µ ⊣ Θ∆ ⊩inst µ 1 : ∀a : ω1 .η ⊑ ω 2 { µ 2 ⊣ Θ∆ ⊩kc σ ⇐ ω { µ ⊣ Θ(Kind Checking)a-kc-sub∆ ⊩k σ : η { µ 1 ⊣ ∆1

∆1 ⊩inst µ 1 : [∆1 ]η ⊑ [∆1 ]ω { µ 2 ⊣ ∆2

∆ ⊩kc σ ⇐ ω { µ 2 ⊣ ∆2
∆ ⊩k σ : η { µ ⊣ Θ(Kinding)
a-ktt-app∆ ⊩k τ1 : η 1 { ρ 1 ⊣ ∆1

a-ktt-star∆ ⊩k ⋆ : ⋆ { ⋆ ⊣ ∆∆1 ⊩kapp (ρ 1 : [∆1 ]η 1 ) • τ2 : ω { ρ ⊣ Θ∆ ⊩k τ1 τ2 : ω { ρ ⊣ Θ

a-ktt-foralli∆, αb : ⋆, a : αb ⊩kc σ ⇐ ⋆ { µ ⊣ ∆2 , a : αb, ∆3∆3 ,→ a∆ ⊩ ∀a.σ : ⋆ { ∀a : αb.[∆3 ]µ ⊣ ∆2 , unsolved(∆3 )k∆ ⊩kapp (ρ 1 : η) • τ : ω { ρ 2 ⊣ Θa-kapp-tt-arrow(Application Kinding)a-kapp-tt-forall∆ ⊩kc τ ⇐ ω1 { ρ 2 ⊣ Θ∆, αb : ω1 ⊩kapp (ρ 1 @b
α : η[a 7→ αb]) • τ : ω { ρ ⊣ Θ∆ ⊩kapp (ρ 1 : ω1 → ω2 ) • τ : ω2 { ρ 1 ρ 2 ⊣ Θ∆ ⊩kapp (ρ 1 : ∀a : ω1 .η) • τ : ω { ρ ⊣ Θ

a-kapp-tt-kuvar∆1 , αb1 : ⋆, αb2 : ⋆, αb : ω = (bα 1 → αb2 ), ∆2 ⊩kc τ ⇐ αb1 { ρ 2 ⊣ Θ∆1 , αb : ω, ∆2 ⊩kapp (ρ 1 : αb) • τ : αb2 { ρ 1 ρ 2 ⊣ Θ∆ ⊩ela µ : η(Elaborated Kinding)a-ela-kappa-ela-app∆ ⊩ela ρ 1 : ω1 → ω 2∆ ⊩ela ρ 2 : ω1

∆ ⊩ela ρ 1 ρ 2 : ω2

∆ ⊩ela ρ 1 : ∀a : ω.η

∆ ⊩ela ρ 2 : ω∆ ⊩ela ρ 1 @ρ 2 : η[a 7→ [∆]ρ 2 ]Fig. 7. Selected rules for algorithmic kinding in PolyKinds

As a goes out of the scope in the conclusion, we need to drop a in the concluding context. To
make sure that dropping a outputs a well-formed context, we substitute away all solved unification
variables in ∆3 for the return kind, and keep only unsolved(∆3 ), which are ensured (∆3 ,→ a) tohave no dependency on a.
In the algorithmic elaborated kinding judgment ∆ ⊩ela µ : η, we keep the invariant: [∆]η = η.
That is why in rule a-ela-app we substitute a with [∆]ρ 2 .
Instantiation (⊩inst ) contains the only entry to unification (rule a-inst-refl).
7.4

Unification

The judgments of unification and promotion are excerpted in Figure 8. Most rules are naturalextensions of those in Haskell98. Full rules are in the technical supplement.
pr
Promotion. The promotion judgment ∆ ⊩αb ω1 ⇝ ω2 ⊣ Θ is extended with kind annotations forunification variables. As our unification variables have kinds now, rule a-pr-kuvarR-tt must alsob so that βb1 : ρ 1 in the context is well-formed. Promotion now has a newpromote the kind of β,Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:20Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira∆ ⊩u ω 1 ≈ ω2 ⊣ Θ(Unification)a-u-app∆ ⊩u ρ 1 ≈ ρ 3 ⊣ ∆1

a-u-refl-tt∆ ⊩u ω ≈ ω ⊣ ∆∆1 ⊩u [∆1 ]ρ 2 ≈ [∆1 ]ρ 4 ⊣ Θ∆ ⊩u ρ 1 ρ 2 ≈ ρ 3 ρ 4 ⊣ Θ

a-u-kvarL-tt
pr∆ ⊩αb ρ 1 ⇝ ρ 2 ⊣ Θ1 , αb : ω1 , Θ2

Θ1 ⊩ela ρ 2 : ω2

Θ1 ⊩u [Θ1 ]ω1 ≈ ω 2 ⊣ Θ3

∆ ⊩u αb ≈ ρ 1 ⊣ Θ3 , αb : ω 1 = ρ 2 , Θ2

a-u-kvarL-lo-tt∆1 , ∆2 ++mv αb : ω1 { ΘΘ1 , {Θ2 } ⊩ela ρ 2 : ω 2pr∆[{Θ}] ⊩αb ρ 1 ⇝ ρ 2 ⊣ Θ1 , {Θ2 , αb : ω1 , Θ3 }, Θ4
Θ1 , {Θ2 } ⊩u [Θ1 , Θ2 ]ω1 ≈ ω2 ⊣ Θ5 , {Θ6 }∆[{∆1 , αb : ω1 , ∆2 }] ⊩u αb ≈ ρ 1 ⊣ Θ5 , {Θ6 , αb : ω 1 = ρ 2 , Θ3 }, Θ4pr∆ ⊩αb ω 1 ⇝ ω2 ⊣ Θ(Promotion)a-pr-kuvarR-ttpr∆ ⊩αb [∆]ρ ⇝ ρ 1 ⊣ Θ[bα ][βb : ρ]a-pr-tvarprpr∆[a][bα ] ⊩αb a ⇝ a ⊣ ∆[a][bα]∆1 ++mv ∆2 { Θa-mv-empty• ++mv ∆ { ∆∆[bα ][βb : ρ] ⊩αb βb ⇝ βb1 ⊣ Θ[βb1 : ρ 1 , αb][βb : ρ = βb1 ]a-mv-kuvarvars(ω) ♯ dom(∆2 )∆1 ++mv ∆2 { Θαb : ω, ∆1 ++mv ∆2 { αb : ω, Θ(Moving)¬(vars(ω) ♯ dom(∆2 ))∆1 ++mv ∆2 , αb : ω { Θa-mv-kuvarM

αb : ω, ∆1 ++mv ∆ { ΘFig. 8. Selected rules for unification, promotion, and moving in PolyKinds

failure mode: it cannot move proper quantified type variables. In rule a-pr-tvar, the variable amust be to the left of αb.
Unfortunately, now we cannot easily tell whether promoting is terminating. In particular, theconvergence of promotion in Haskell98 is built upon the obvious fact that the size of the kind being
promoted always gets smaller from the conclusion to the hypothesis. However, rule a-pr-kuvarRtt breaks this invariant, as the judgment recurs into the kinds of unification variables, and the sizeof the kinds may be larger than the unification variables. As shown in Section 7.5, we prove that
promotion is terminating.
Unification. The unification judgment ∆ ⊩u ω1 ≈ ω 2 ⊣ Θ for PolyKinds features heterogeneous
constraints. Recall the definition of X and Y discussed in Section 2.2. When unifying αb βb with
Maybe Bool, setting αb =Maybe and βb =Bool results in ill-kinded results. This suggests that whensolving a unification variable, we need to first unify the kinds of both sides, as shown in rule a-ukvarL-tt. When unifying αb with ρ 1 , we first promote ρ 1 , yielding ρ 2 . Now ρ 2 must be well-formed
under Θ1 , so we can get its kind ω1 . We then unify the kinds of both sides. If everything succeeds,
we set αb : ω1 = ρ 2 . Under this rule, the unification αb βb ≈Maybe Bool would be rejected correctly.
Rule a-u-kvarL-lo-tt is essentially the same as rule a-u-kvarL-tt, but deals with unification
variables in a local scope. We thus need an extra step to move αb towards the end of the local scope.
Local scopes and moving. As we have mentioned, a local scope can be reordered as long as thecontext is well-formed. Consider unifying {bα : ⋆, a : ⋆, b : αb, c : ⋆} ⊩u αb ≈ a. We see that a is not
well-formed under the context before αb, and thus we cannot rewrite αb : ⋆ with αb = a : ⋆. However,
we can reorder the context to put αb to the right of a. In fact, to maximize the prefix context of αb,
we can move αb to the end of the context, yielding {a : ⋆, c : ⋆, αb : ⋆, b : αb}. As b depends on αb, b isalso moved to the end of the context. The final context is now {a : ⋆, c : ⋆, αb : ⋆ = a, b : αb}.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:21

The moving judgment ∆1 ++mv ∆2 { Θ reorders the context, by appending ∆2 to the end of ∆1 ,yielding Θ. As we have emphasized, reordering must preserve a well-formed context. Therefore,
every term that depends on ∆2 (rule a-mv-kuvarM) needs to be placed at the end, along with ∆2 .
In rule a-u-kvarL-lo-tt, we begin by reordering the local scope to put αb as far to the right as
possible. The rest of the rule is essentially the same as rule a-u-kvarL-tt: the added complication
stems from the need to keep track of what bindings in the context are a part of the current local
scope.
7.5

Termination

Now the challenge is to prove that our unification algorithm terminates, which relies on theconvergence of the promotion algorithm. Next, we first discuss the termination of unification, andthen move to the more complicated proof for promotion. Let ⟨∆⟩ denote the number of unsolved
unification variables in ∆.
prLemma 7.1 (Promotion Preserves ⟨∆⟩). If ∆ ⊩αb ω 1 ⇝ ω 2 ⊣ Θ, then ⟨∆⟩ = ⟨Θ⟩.
Lemma 7.2 (Unification Makes Progress). If ∆ ⊩u ω1 ≈ ω2 ⊣ Θ, then either Θ = ∆, or ⟨Θ⟩ < ⟨∆⟩.
Now we measure unification ∆ ⊩u ω1 ≈ ω2 ⊣ Θ using the lexicographic order of the pair(⟨∆⟩, |ω1 |), where |ω1 | computes the standard size of ω1 . We prove the pair always gets smallerfrom the conclusion to the hypothesis. Formally, assuming promotion terminates, we have
Theorem 7.3 (Unification Terminates). Given a context ∆ ok, and kinds ρ 1 and ρ 2 , where [∆]ρ 1 = ρ 1 ,and [∆]ρ 2 = ρ 2 , it is decidable whether there exists Θ such that ∆ ⊩u ρ 1 ≈ ρ 2 ⊣ Θ.
We are not yet done, since Theorem 7.3 depends on the convergence of promotion. As observedin rule a-pr-kuvarR, the size of the type being promoted increases from the conclusion to the
hypothesis. Worse, the context never decreases. How do we prove promotion terminates? The crucial
observation for rule a-pr-kuvarR is that, when we move from the conclusion to the hypothesis,
we also move from a unification variable to its kind. Since the kind is well-formed under the prefix
context of the variable, we are somehow moving leftward in the context.
To formalize the observation, we define the dependency graph of a context.
Definition 7.4 (Dependency Graph). The dependency graph of a context ∆ is a directed graph where:(1) Nodes are all type variables and unsolved unification variables of ∆, and the terminal symbols⋆, → and Int.
(2) Edges indicate the dependency from a type to its substituted kind. For example, if αb : ω, thenthere is a directed edge from αb to all the nodes appearing in [∆]ω.
As an illustration, consider the context ∆ = αb : ⋆, αb1 : ⋆, αb2 : ⋆ = αb1 , αb3 : ⋆ → αb2 , whose
dependency graph is given in Figure 9a (the reader is advised to ignore the color for now). There areseveral notable properties. First, as long as the context is well-formed, the graph is acyclic except
for the self-loop of ⋆ and →. Second, solved unification variables never appear in the graph. The
kind of αb3 depends on αb2 , which is already solved by αb1 , so the dependency goes from αb3 to αb1 .
Now let us consider how promotion works in terms of the dependency graph, by trying tounify ∆ ⊩u αb ≈ αb3 Int. We start by promoting αb3 Int. The derivation of the promotion is given at
the bottom of Figure 9. We omit some details via (· · · ) as promoting constants (⋆,→ and Int) is
trivial. At the top of Figure 9 we give the dependency graph at certain points in the derivation,
where the part being promoted is highlighted in gray. At the beginning we are at Figure 9a. For
αb3 , by rule a-pr-kuvarR, we first promote the kind of αb3 , which is (after context application)⋆ → αb1 (Figure 9b). As ⋆ and → are always well-formed, we then promote αb1 whose kind is theProc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:22

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira

αb3

→

αb3

αb3

αb1

αb

⋆

Int

→

αb1

αb

⋆

Int

(b) Promote ⋆ → αb1(a) Promote αb3 Int

→

βb2

βb1

αb

⋆

Int

(c) Solve αb1 = βb1

→

βb1

αb

⋆

Int

(d) Solve αb3 = βb2

Θ1 = βb1 : ⋆ , αb : ⋆, αb1 : ⋆ = βb1 , αb2 : ⋆ = αb1 , αb3 : ⋆ → αb2
Θ2 = βb1 : ⋆, βb2 : ⋆ → βb1 , αb : ⋆, αb1 : ⋆ = βb1 , αb2 : ⋆ = αb1 , αb3 : ⋆ → αb2 = βb2pr∆ ⊩αb ⋆ ⇝ ⋆ ⊣ ∆···pr∆ ⊩αb αb1 ⇝ βb1 ⊣ Θ1

9ba-pr-kuvarR

9ca-pr-apppr∆ ⊩αb ⋆ → αb1 ⇝ ⋆ → βb1 ⊣ Θ1pr
∆ ⊩αb αb3 ⇝ βb2 ⊣ Θ2

9aa-pr-kuvarR9dpr∆ ⊩αb αb3 Int ⇝ αb2 Int ⊣ Θ2···
a-pr-app

Fig. 9. Example of dependency graphwell-formed ⋆. Now we create a fresh variable βb1 : ⋆, and solve αb1 with βb1 (Figure 9c). Note since
αb1 is solved, the dependency from αb3 goes to βb1 . Finally, we create a fresh variable βb2 with kind
⋆ → βb1 , and solve αb3 with βb2 (Figure 9d). Going back to unification, we solve αb = βb2 Int.
We have several key observations. First, when we move from Figure 9a to Figure 9b via rule apr-kuvarR, we are actually moving from the current node (bα 3 ) to its adjacent nodes (⋆, →, and αb1 ).
In other words, we are going down in this graph. Moreover, promotion terminates immediately attype constants, so we never fall into the trap of loop. Further, when we solve variables with freshones (Figure 9c and Figure 9d), the shape of the graph never changes.
With all those in mind, we conclude that the promotion process goes top-down via rule a-prkuvarR in the dependency graph until it terminates at types that are already well-formed. Based on
this conclusion, we can formally prove that promotion terminates.
Theorem 7.5 (Promotion Terminates). Given a context ∆[b
α ] ok, and a kind ρ 1 with [∆]ω1 = ω1 , itpris decidable whether there exists Θ such that ∆ ⊩αb ω1 ⇝ ω2 ⊣ Θ.
7.6

Soundness, Completeness and Principality

We prove our algorithm is sound:
Theorem 7.6 (Soundness of ⊩pgm ). If Ω; Γ ⊩pgm pgm : µ, then [Ω]Ω; [Ω]Γ ⊢pgm pgm : [Ω]µ.
Unfortunately, we lose completeness. Recall the example in Section 7.2. This definition of T isrejected by the algorithmic quantification check as the kind of d cannot be determined. However,the declarative system can guess correctly, e.g., Proxy b or Proxy c. Unfortunately, different choices
lead to incomparable kinds for T . Thus we argue such programs must be rejected.
Nevertheless, if the user explicitly writes down d :: Proxy b or d :: Proxy c, then the program will
be accepted by the algorithm. Thus, we conjecture that if all local dependencies are annotated by
the user, we can regain completeness. This, however, is a bit annoying to users, because it meansthat we cannot accept definitions like the one below, even though the dependency is clear.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:23

data Eq :: ∀k. k → k → ⋆data P :: ∀k (a :: k) b. Eq a b → ⋆We do not consider the incompleteness as a problematic issue in practice, as this scenario isquite contrived and (we expect) will rarely occur “in the wild”. See more discussion of this point in
Section 9.
Although the algorithm is incomplete, we offer the following guarantee: if the algorithm accepts
a definition, then that definition has a principal kind, and the algorithm infers the principal kind.
Definition 7.7 (Kind Instantiation). Under context Σ, a kind η = ∀{ϕ 1 }.∀ϕ 2 .ω1 , where ϕ’s can be
empty, instantiates to ω, denoted as Σ ⊢ η ⊑ ω, if ω1 [ϕ 1 7→ ρ 1 ][ϕ 2 7→ ρ 2 ] = ω for some ρ 1 and ρ 2 .
The relation is embedded in Σ ⊢inst µ 1 : η ⊑ ω { µ 2 (Figure 5), where we ignore µ 1 and µ 2 .
Definition 7.8 (Partial Order of Kinds in PolyKinds). Under context Σ, a kind η 1 is more generalthan η 2 , denoted as Σ ⊢ η 1 ⪯ η 2 , if for all ω such that Σ ⊢ η 2 ⊑ ω, we have Σ ⊢ η 1 ⊑ ω.
To understand the definition, consider that if the program type-checks under T : η 2 , then it must
type-check under T : η 1 , as T : η 1 can be instantiated to all monokinds that T : η 2 is used at.
Now we lift the definition of ⊩grp to be the generalized result of kinds and contexts.
Theorem 7.9 (Principality of ⊩grp ). If Ω ⊩grp rec Ti
iii
rec Ti { η i′ ; Ψi holds, we have [Ω]Ω ⊢ [Ω]η i ⪯ η i′.

ii{ η i i ; Γi , then whenever [Ω]Ω ⊢grp

This result echoes the result in the term-level type inference algorithm for Haskell ([Vytiniotis
et al. 2011, Section 6.5]): our algorithm does not infer every kind acceptable by the declarative
system, but the kinds it does infer are always the best (principal) ones.
8

LANGUAGE EXTENSIONS

We have seen that the PolyKinds system incorporates many features and enjoys desirable properties.
In this section, we discuss how the PolyKinds system can be extended with more related language
features. The technical supplement contains a few more, less impactful extensions.
8.1

Higher-Rank Polymorphism

The system can be extended naturally to support higher-rank polymorphism [Dunfield and Krishnaswami 2013; Peyton Jones et al. 2007]. With higher-rank polymorphism, every type can have apolymorphic kind. For example, data constructor declarations become ∀ϕ.D σi i instead of ∀ϕ.D τi i .
Unfortunately, higher-rank polymorphism breaks principality. Consider:data Q1 :: ∀k 1 k 2 . k 1 → ⋆data Q2 :: (∀(k 1 : ⋆) (k 2 : k 1 ). k 1 → ⋆) → ⋆First, we modify the definition of partial order of kinds (Definition 7.8) to state that one kindis more general than another if it can be instantiated to all polykinds that the other kind canbe instantiated to. Now consider the kind of Q1, which under the algorithm is generalized to∀{ k3 :⋆} (k 1 :⋆) (k 2 : k3). k 1 → ⋆. In Theorem 7.9, we guarantee that this kind is a principal kind as
it can be instantiated to all monokinds that other possible kinds for Q1, e.g., ∀(k 1 ::⋆) (k 2 ::k 1 ). k 1 → ⋆,can be instantiated to. However, under the new definition, ∀{ k3 :: ⋆} (k 1 :: ⋆) (k 2 :: k3). k 1 → ⋆is no longer more general than ∀(k 1 :: ⋆) (k 2 :: k 1 ). k 1 → ⋆, as there is no way to instantiate theformer to the latter. To see why we need to modify the definition at all, consider the rank-2 kind of
Q2, which expects exactly an argument of kind ∀(k 1 :: ⋆) (k 2 :: k 1 ). k 1 → ⋆.
We do not consider the absence of principality in the setting of higher-rank polymorphism
to be a severe issue in practice, for two reasons: to our knowledge, higher-rank polymorphism
for datatypes is not heavily used; and it may be possible to recover principality through the use
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:24

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveiraof a more generous type-subsumption relation. Currently, GHC (and our model of it) does notsupport first-class type-level abstraction (i.e., Λ in types) [Jones 1995]. This means that we cannot
introduce new variables (also called skolemization [Peyton Jones et al. 2007, Section 4.6.2]) in
an attempt to equate one type with another. Returning to the example above, we could massage∀{ k3 :: ⋆} (k 1 :: ⋆) (k 2 :: k3). k 1 → ⋆ to ∀(k 1 :: ⋆) (k 2 :: k 1 ). k 1 → ⋆ if we could abstract over the
k 1 in the target type. Recent advances in type-level programming in Haskell [Kiss et al. 2019]suggest we may be able to add first-class abstraction, meaning that type-subsumption can use bothinstantiation and skolemization. We conjecture that this development would recover principal
types.
8.2

Generalized Algebraic Datatypes (GADTs)

The focus of this work has been on uniform datatypes, where every constructor’s type matches
exactly the datatype head: this fact allows us to easily choose the subscript to the ⊢dc judgment
in, e.g., rule dt-tt. Programmers in modern Haskell, however, often use generalized algebraic
datatypes [Peyton Jones et al. 2006; Xi et al. 2003]. There are two impacts of adding these, both ofwhich we found surprising.
Equality constraints. The power of GADTs arises from how they encode local equality constraints.
Any GADT can be rewritten to a uniform datatype with equality constraints [Vytiniotis et al. 2011,
Section 4.1]. For example, we can rewrite data G a where MkG :: G Bool to be data G a = (a ∼Bool) ⇒ MkG, where ∼ describes an equality constraint. For our purposes of doing kind inference,these equality constraints are uninteresting: the ∼ operator simply relates two types of the samekind and can be processed as any polykinded type constructor would be. Modeling constraints tothe left of a ⇒ similarly would add a little clutter to our rules, but would offer no real challenges.
The unexpected simplicity of adding GADTs to our system arises from a key fact: we do notever allow pattern-matching. A GADT pattern-match brings a local equality assumption into scope,
which would influence the unification algorithm. However, as pattern matching does not happen
in the context of datatype declarations, we avoid this wrinkle here.
Syntax. The implementation of GADTs in GHC has an unusual syntax: data G a where MkG ::a → G Int. The surprising aspect of this syntax is that the two as above are different: the a in theheader is unrelated to the a in the data constructor. This seemingly inconsequential design choicemakes kind inference for GADTs very challenging, as constructors have no way to refer back to
the datatype parameters. Given that this aspect of GADTs is a quirk of GHC’s design—and is notrepeated in other languages that support GADTs—we remark here that it is odd and perhaps should
be remedied. For the details, please see the technical supplement.
8.3

Type Families

Type families [Chakravarty et al. 2005] are, effectively, type-level functions. Kind inference of typefamilies thus can be designed much like type inference for ordinary functions. However, as they canhave dependency, the complications we describe in this paper would arise here, too. In particular,
unification would have to be kind-directed, as we have described. The current syntax for closed
type families [Eisenberg et al. 2014] shares the same scoping problem as the syntax for GADTs, so
our arguments above apply to closed type families equally.
The challenge with type families is that they indeed do pattern-matching, and thus (in concert
with GADTs) can bring local equalities into scope. A full analysis of the ramifications here is beyond
the scope of this paper, but we believe the literature on type inference in the presence of local
equalities would be helpful. Principal among these is the work of Vytiniotis et al. [2011], but Gundry[2013] and Eisenberg [2016] also approach this problem in the context of dependent types.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

9

53:25

RELATED WORKThe Glasgow Haskell Compiler. The systems we present here are inspired by the algorithms
implemented in GHC. However, our goal in the design of these systems is to produce a sound and(nearly) complete pair of specification and implementation, not simply to faithfully record what is
implemented. We have identified ways that the GHC implementation can improve in the future. For
example, GHC quantifies over local scopes as specified where we believe they should be inferred;
and the tight connection in our system between unification and promotion may improve upon
GHC’s approach, which separates the two. The details of the relationship between our work and
GHC (including a myriad of ways our design choices differ in small ways from GHC’s) appear in
the technical supplement.
Unification with dependent types. While full higher-order unification is undecidable [Goldfarb
1981], the pattern fragment [Miller 1991] is a well-known decidable fragment. Much literature [Abeland Pientka 2011; Gundry and McBride 2013; Reed 2009] is built upon the pattern fragment.
Unification in a dependently typed language features heterogeneous constraints. To prove correctness, Reed [2009] used a weaker invariant on homogeneous equality, typing modulo, which statesthat two sides are well typed up to the equality of the constraint yet to be solved. Gundry and
McBride [2013] observed the same problem, and use twin variables to explicitly represent the same
variable at different types, where twin variables are eliminated once the heterogeneous constraint
is solved. In both approaches the well-formedness of a constraint depends on other constraints.
Cockx et al. [2016] proposed a proof-relevant unification that keeps track of the dependencies
between equations. Different from their approaches, our algorithm unifies the kinds when solving
unification variables. This guarantees that our unification always outputs well-formed solutions.
Ziliani and Sozeau [2015] present the higher-order unification algorithm for CIC, the base logic
of Coq. They favor syntactic equality by trying first-order unification, as they argue the first-ordersolution gives the most natural solution. However, they omit a correctness proof for their algorithm.
Coen [2004] also considers first-order unification, but only the soundness lemma is proved. Different
from their systems, our system is based on the novel promotion judgment, and correctness including
soundness and termination is proved.
The technique of suspended substitutions [Eisenberg 2016; Gundry and McBride 2013] is widelyadopted in unification algorithms. Our system provides a design alternative, our quantification check.
Choosing between suspended substitutions and the quantification check is a user-facing language
design decision, as suspended substitutions can accept some more programs. The quantification
check means that the kind of a locally quantified variable a must be fully determined in a’s scope;
it may not be influenced by usage sites of the construct that depends on a. Suspended substitutions
relax this restriction. We conjecture that suspended substitutions can yield a complete algorithm.
However, that mechanism is complex. Moreover, unification based on suspended substitutions
is only decidable for the pattern fragment. Our system, in contrast, avoids all the complication
introduced by suspended substitutions through its quantification check. Our unification terminates
for all inputs, preserving backward compatibility to Hindley-Milner-style inference. Although we
reject the definition of T (Section 7.2), we can solve more constraints outside the pattern fragment.
We conjecture that those constraints are much more common than definitions like T . Suspended
substitutions often come with a pruning process [Abel and Pientka 2011], which produces a valid
solution before solving a unification variable. Our promotion process has a similar effect.
Homogeneous kind-preserving unification. Jones [1995] proposed a homogeneous kind-preserving
unification between two types. Kinds κ are defined only as ⋆ or κ 1 → κ 2 . As the kind system ismuch simpler, kind-preserving unification ≈κ is simply subscripted by the kind, and working out
the kinds is straightforward. Our unification subsumes Jones’s algorithm.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:26

Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira

Type inference in Haskell. Type inference in Haskell is inspired by Damas and Milner [1982] andPottier and Rémy [2005], extended with various type features, including higher rank polymorphism [Peyton Jones et al. 2007] and local assumptions [Schrijvers et al. 2009; Simonet and Pottier
2007; Vytiniotis et al. 2011], among others. However, none of these works describe an inference
algorithm for datatypes, nor do they formalize type variables of varying kinds or polymorphic
recursion.
Dependent Haskell. Our PolyKinds system merges types and kinds, a key feature of Dependent
Haskell (DH) [Eisenberg 2016; Gundry 2013; Weirich et al. 2013, 2017]. There is ongoing work
dedicated to its implementation [Xie and Eisenberg 2018]. The most recent work by Weirich et al.
[2019] integrates roles [Breitner et al. 2016] with dependent types. Our work is the first presentationof unification for DH, and our system may be useful in designing DH’s term-level type inference.
Context extension. Our approach of recording unification variables and their solutions in thecontexts is inspired by Gundry et al. [2010] and Dunfield and Krishnaswami [2013]. Gundry and
McBride [2013] applied the approach to unification in dependent types, where the context also
records constraints; constraints also appear in context in Eisenberg [2016]. Further, we extend thecontext extension approach with local scopes, supporting groups of order-insensitive variables.
Polymorphic recursion. Mycroft [1984] presented a semi-algorithm for polymorphic recursion. Jim[1996] and Damiani [2003] studied typing rules for recursive definitions based on rank-2 intersection
types. Comini et al. [2008] studied recursive definitions in a type system that corresponds to theabstract interpreter in Gori and Levi [2002, 2003]. Our system does not infer polymorphic recursion;
instead, we exploit kind annotations to guide the acceptance of polymorphic recursion.
Constraint-solving approaches. Many systems (e.g. [Pottier and Rémy 2005]) adopt a modular
presentation of type inference, which consists of a constraint generator and a constraint solver. For
simplicity, we have presented an eager unification algorithm instead of using a separate constraint
solver. However, we believe changing to a constraint-solving approach should not change any ofour main results. Section B.1 of the technical supplement considers this point further.
10

CONCLUSION

We have presented the first known, detailed account of kind inference for datatypes, codifying
the inference both from the early days of Haskell and the Haskell of today. For the former, we canprove soundness and completeness using the technique of kind parameters. For the latter, we havedescribed a sound algorithm for inferring types even in the presence of dependency, allowing users
to infer datatype kinds instead of merely checking them. The algorithm is incomplete in obscure
scenarios (Section 7.2), a conscious design decision in order to retain termination.
There are several ways we could extend this work. The most obvious is to include other constructs
in our approach. However, even with only datatypes formalized, we see this work as sturdy enoughto aim at implementation. A primary motivation for starting this work was shortcomings in GHC’s
current kind inference algorithm and results, yet we had no principled way of improving it. Having
completed this research, we now feel encouraged to attack this practical problem afresh and apply
what we have learned. We further believe that our approach to inference will be useful to designers
and implementors of other dependently typed languages, as they share many of the same challenges
as GHC, both in processing datatypes and in type-checking ordinary expressions.
ACKNOWLEDGMENTS
We thank the anonymous reviewers for their helpful comments. This work has been sponsored by
the Hong Kong Research Grant Council projects number 17210617 and 17209519. This material isbased upon work supported by the National Science Foundation under Grant No. 1704041.
Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

Kind Inference for Datatypes

53:27

REFERENCES
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.
P. B. Andrews. 1971. Resolution in type Theory. Journal of Symbolic Logic 36 (1971), 414–432.
Richard S. Bird and Lambert Meertens. 1998. Nested datatypes. In LNCS 1422: Proceedings of Mathematics of Program
Construction, Johan Jeuring (Ed.). Springer-Verlag, Marstrand, Sweden, 52–67. http://www.cs.ox.ac.uk/people/richard.
bird/online/BirdMeertens98Nested.pdf
Joachim Breitner, Richard A Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2016. Safe zero-cost coercions for
Haskell. Journal of Functional Programming 26 (2016).
L. Cardelli. 1986. A polymorphic lambda-calculus with Type:Type. Technical Report 10. SRC.
Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. 2005. Associated type synonyms. In Proceedings of theTenth ACM SIGPLAN International Conference on Functional Programming (ICFP ’05). ACM, New York, NY, USA, 241–253.
https://doi.org/10.1145/1086365.1086397
Jesper Cockx, Dominique Devriese, and Frank Piessens. 2016. Unifiers as equivalences: proof-relevant unification of
dependently typed data. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming(ICFP 2016). ACM, New York, NY, USA, 270–283. https://doi.org/10.1145/2951913.2951917
Claudio Sacerdoti Coen. 2004. Mathematical knowledge management and interactive theorem proving. Ph.D. Dissertation.
University of Bologna, 2004. Technical Report UBLCS 2004-5.
Marco Comini, Ferruccio Damiani, and Samuel Vrech. 2008. On polymorphic recursion, type systems, and abstract
interpretation. In International Static Analysis Symposium. Springer, 144–158.
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). ACM, New York, NY, USA, 207–212.
https://doi.org/10.1145/582153.582176
Ferruccio Damiani. 2003. Rank 2 intersection types for local definitions and conditional expressions. ACM Transactions on
Programming Languages and Systems (TOPLAS) 25, 4 (2003), 401–451.
Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rankpolymorphism. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13).
ACM, New York, NY, USA, 429–442. https://doi.org/10.1145/2500365.2500582
Richard A Eisenberg. 2016. Dependent types in haskell: Theory and practice. Ph.D. Dissertation. University of Pennsylvania.
Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. 2014. Closed type families withoverlapping equations. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL ’14). ACM, New York, NY, USA, 671–683. https://doi.org/10.1145/2535838.2535856
Richard A Eisenberg, Stephanie Weirich, and Hamidhasan G Ahmed. 2016. Visible type application. In European Symposiumon Programming. Springer, 229–254.
Ronald Garcia and Matteo Cimini. 2015. Principal type schemes for gradual programs. In Proceedings of the 42nd Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). ACM, New York, NY, USA,
303–315. https://doi.org/10.1145/2676726.2676992
Warren D Goldfarb. 1981. The undecidability of the second-order unification problem. Theoretical Computer Science 13, 2(1981), 225–230.
Roberta Gori and Giorgio Levi. 2002. An experiment in type inference and verification by abstract interpretation. In
International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 225–239.
Roberta Gori and Giorgio Levi. 2003. Properties of a type abstract interpreter. In International Workshop on Verification,
Model Checking, and Abstract Interpretation. Springer, 132–145.
Adam Gundry and Conor McBride. 2013. A tutorial implementation of dynamic pattern unification. Unpublished draft(2013).
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. ACM, 43–54.
Adam Michael Gundry. 2013. Type inference, Haskell and dependent types. Ph.D. Dissertation. University of Strathclyde.
Fritz Henglein. 1993. Type inference with polymorphic recursion. ACM Trans. Program. Lang. Syst. 15, 2 (April 1993),
253–289. https://doi.org/10.1145/169701.169692
J. Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969),
29–60.
G. Huet. 1973. A unification algorithm for typed lambda calculus. Theoretical Computer Science 1, 1 (1973), 27–57.
Trevor Jim. 1996. What are principal typings and what are they good for?. In Proceedings of the 23rd ACM SIGPLAN-SIGACT
symposium on Principles of programming languages. ACM, 42–53.
Mark P Jones. 1995. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal offunctional programming 5, 1 (1995), 1–35.

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.

53:28Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. OliveiraMark P. Jones. 1999. Typing Haskell in Haskell. In Proceedings of the 1999 Haskell Workshop (Haskell ’99), Erik Meijer (Ed.).
Paris, France, pp. 9–22. University of Utrecht Technical Report UU-CS-1999-28.
Csongor Kiss, Susan Eisenbach, Tony Field, and Simon Peyton Jones. 2019. Higher-order type-level programming in Haskell.
In Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP 2019). ACM.
Didier Le Botlan and Didier Rémy. 2003. MLF: Raising ML to the Power of System F (ICFP ’03). 12.
Daan Leijen. 2009. Flexible types: robust type inference for first-class polymorphism. In Proceedings of the 36th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’09). ACM, New York, NY, USA, 66–77.
https://doi.org/10.1145/1480881.1480891
Dale Miller. 1991. Unification of simply typed lambda-terms as logic programming. (1991).
Alan Mycroft. 1984. Polymorphic type schemes and recursive definitions. In International Symposium on Programming.
Springer, 217–228.
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). ACM, New York, NY, USA, 54–67. https://doi.org/10.1145/237721.237729
Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press.
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.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. 2006. Simple unification-based type
inference for GADTs. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming(ICFP ’06). ACM, New York, NY, USA, 50–61. https://doi.org/10.1145/1159803.1159811
François Pottier and Didier Rémy. 2005. The essence of ML type inference. Advanced Topics in Types and Programming
Languages (2005).
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. ACM, 49–56.
Didier Rémy and Boris Yakobowski. 2008. From ML to MLF: Graphic type constraints with efficient type inference. In
Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). ACM, New York,NY, USA, 63–74. https://doi.org/10.1145/1411204.1411216
Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann, and Dimitrios Vytiniotis. 2009. Complete and decidable type
inference for GADTs. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP’09). ACM, New York, NY, USA, 341–352. https://doi.org/10.1145/1596550.1596599
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).
ACM, New York, NY, USA, 783–796. https://doi.org/10.1145/3192366.3192389
Vincent Simonet and François Pottier. 2007. A constraint-based approach to guarded algebraic data types. ACM Transactions
on Programming Languages and Systems (TOPLAS) 29, 1 (2007), 1.
Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn (X) Modular type inferencewith local assumptions. Journal of functional programming 21, 4-5 (2011), 333–412.
Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. 2008. FPH: First-class polymorphism for Haskell (ICFP’08). 12.
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. 2019. A Role for dependent types in
Haskell. Proc. ACM Program. Lang. 3, ICFP, Article 101 (July 2019), 29 pages. https://doi.org/10.1145/3341705
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. 2013. System FC with Explicit Kind Equality. In Proceedings of the
18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). ACM, New York, NY, USA, 275–286.
https://doi.org/10.1145/2500365.2500599
Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A Eisenberg. 2017. A specification for
dependent types in Haskell. In Proceedings of the 22th ACM SIGPLAN International Conference on Functional Programming(ICFP ’17). ACM.
Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In Proceedings of the 30th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’03). ACM, New York, NY, USA, 224–235.
https://doi.org/10.1145/604131.604150
Ningnign Xie and Richard A Eisenberg. 2018. Coercion Quantification. In Haskell Implementors’ Workshop.
Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães.
2012. Giving Haskell a Promotion. In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and
Implementation (TLDI ’12). ACM, New York, NY, USA, 53–66. https://doi.org/10.1145/2103786.2103795
Beta Ziliani and Matthieu Sozeau. 2015. A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading.
In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). ACM, New
York, NY, USA, 179–191. https://doi.org/10.1145/2784731.2784751

Proc. ACM Program. Lang., Vol. 4, No. POPL, Article 53. Publication date: January 2020.