Draft of 2016-09-30

Type checking through unification
Francesco Mazzoli1 and Andreas Abel2
1

FP Complete∗
<f@mazzo.li>
Gothenburg University
<andreas.abel@gu.se>

arXiv:1609.09709v1 [] 30 Sep 2016

2

Abstract
In this paper we describe how to leverage higher-order unification to type check a dependently
typed language with meta-variables. The literature usually presents the unification algorithm
as a standalone component, however the need to check definitional equality of terms while type
checking gives rise to a tight interplay between type checking and unification. This interplay
is a major source of complexity in the type-checking algorithm for existing dependently typed
programming languages. We propose an algorithm that encodes a type-checking problem entirely
in the form of unification constraints, reducing the complexity of the type-checking code by
taking advantage of higher order unification, which is already part of the implementation of
many dependently typed languages.
Keywords and phrases Dependent types, type checking, higher order unification, type reconstruction

1

Introduction

Theories with dependent types have been successfully exploited to design programming
languages and theorem provers, such as Agda [9], Idris [3], or Coq [2]. To make these
systems practical, the user is presented with a language much richer than the underlying
type theory, which will hopefully be small enough to gain confidence in the correctness of
the code that type checks it.
One common way to make a type theory palatable is extending it with meta-variables,
standing for yet to be determined terms, and solved by unification. Their usage in traditional
programming languages is confined to type inference, and thus traditionally they can stand
for types only. In dependently typed languages types can contain terms, and thus metavariables are usually extended to stand for any term in our language. A typical use case
for meta-variables is implicit arguments as introduced by Pollack [11], relieving the user of
having to write easily inferrable arguments to functions. For example, in Agda we can write
a safe head function which extracts the first element of a list, inferring both the type of the
elements and the length of the list:
head : {A : Set} → {n : Nat} → Vec A (1 + n) → A
head (x :: xs) = x

∗

The work presented in this paper was performed at the Chalmers University of Technology.

2

Type checking through unification

Here, Vec A n denotes a list of length n with elements of type A, and Set is the type of types.
The expression {A : Set} → {n : Nat} → ... binds two implicit arguments. When invoking
head, the type checker will insert two meta-variables standing for A and n and attempt to
solve them by inspecting the Vec argument that follows. Note that n is a value, while in
languages such ML and Haskell only types can be implicit.
The task of integrating meta-variables in a type-checking algorithm for dependent types
gives rise to complications. For example, consider the task of type checking
true : if α 6 2 then Bool else Nat,

where α is a yet to be determined (uninstantiated) meta-variable of type Nat. We want the
type of true to be Bool, but reduction is impeded by α. Thus, we cannot complete type
checking until α is instantiated.1 The problem lies in the fact that type checking dependent
types involves reducing terms to their normal forms, something that can be affected by
meta-variables, like in this case.
To solve issues like the one above, the only viable option—apart from refusing to solve
them—is to wait for the meta-variables that are affecting type checking to be instantiated,
and then resume. This gives rise to a sort of concurrency that makes reasoning about the
type checking algorithm arduous. In this paper, expanding on ideas developed in Agda [9]
and Epigram [7], we propose an algorithm that encodes a type-checking problem in a set
of unification constraints with a single traversal of the term to be checked. The generated
constraints can be solved effectively by the unification procedure already employed by Agda,
but our elaboration procedure is considerably simpler and shorter than Agda’s type-checking
code. This highlights an overlap in functionality between the type checker, which needs to
check that types and terms are of a certain shape; and the unifier, which checks the equality
of terms. Moreover, our algorithm lets us clearly separate concerns between type checking
and unification, making it easier to gain confidence on the elaboration procedure and then
experiment with various unification “backends”.
In the rest of the paper, we will explain the problem more clearly (Section 2). Then we
will introduce a simple type theory (Section 3) that will serve as a vector to explain our
algorithm in detail. In Section 4 we will give a specification to the unification procedure.
The algorithm itself is presented in Section 5, along with some of its properties. We will then
briefly discuss the performance and how the algorithm can be extended to support certain
popular language features (Section 6).
We have implemented the presented algorithm in a prototype, tog, which covers a subset
of Agda—every tog program is also a valid Agda program.2

2

The problem

In this section we will explain the challenges faced when type checking dependent types with
meta-variables. An Agda-like syntax will be used throughout the examples, please refer to
Appendix A for clarifications.
Coming back to the problem of type checking
true : BoolOrNat α,

given unistantiated meta-variable α and definition
1
2

Note that we cannot instantiate α without loss of generality, since both 0 and 1 are acceptable solutions.
The source code for tog is available at https://github.com/bitonic/tog.

F. Mazzoli and A. Abel

BoolOrNat : Nat → Set
BoolOrNat = λx → if x 6 2 then Bool else Nat

there are various tempting ways to approach the problem. The most conservative approach
is to stop type checking when faced with blocked terms (terms whose normalization is impeded by some meta-variables). However, this approach is unsatisfactory in many instances.
Consider
(true, refl) : BoolOrNat α × (α ≡ 0)

Where x ≡ y is the type inhabited by proofs that x is equal to y (propositional equality), and
refl is of type t ≡ t for any t (reflexivity). Type checking this pair will involve type checking
true : BoolOrNat α and then refl : α ≡ 0. If we give up on the first type-checking problem, we
will not examine the second, which will give us a solution for α (α := 0). After instantiating
α we can easily go back and successfully type check the first part. In general, we want to
attempt to type check as much as possible, and to instantiate as many meta-variables as
possible—as long as we do so without loss of generality, like in this case.
Another approach is to assume that blocked type-checking problems will eventually be
solved, and continue type checking. However, this road is dangerous since we need to be
careful not to generate ill-typed terms or invalid type-checking contexts, as noted by Norell
and Coquand [10]. Consider
test : (α ≡ 0) × (((x : BoolOrNat α) → BoolOrNat (1 + x)) → Nat)
test = (refl, λg → g true)

Type checking the definition test will involve checking that its type is a valid type, and that
its body is well typed. Checking the former will involve making sure that
BoolOrNat α = Nat

since we know that the type of x must be Nat, given that x is used as an argument of
(1+) : Nat → Nat.3
If we assume that the type is valid, we will proceed and type check the body pairwise.
Type checking the first element—a proof by reflexivity that α is equal to 0—will instantiate
α to 0, and then we will be faced with
(λg → g true) : ((x : Bool) → BoolOrNat (1 + x)) → Nat

Note that the type is ill-typed,4 violating the usual invariants present when type checking—
namely the fact that when we make progress we always generate well-typed terms. Worse,
to type check we will instantiate x with 0, ending up with BoolOrNat (1 + true). With some
effort we can exploit this problem to make the type checker loop, and thus type checking
will be undecidable.
As mentioned in the introduction, at the heart of the problem lies the fact that to type
check we need to reduce terms to their weak head normal form. If reduction is impeded

3

4

Note that checking that an equality type is a well-formed type does not involved checking that the
equated things are equal—4 ≡ 5 is a valid type. In this instance while α ≡ 0 appears in the type for
test, this does not mean that α will be unified with 0 when type checking the type. However, type
checking its proof refl : α ≡ 0 will.
x, of type Bool, appears as an argument to the function (1+).

3

4

Type checking through unification

by meta-variables, we cannot proceed. To overcome this problem, Norell proposed to define
type checking as an elaboration procedure:5 given the problem of type checking t against A
in context Γ, type checking will produce a term u that approximates t:
JΓ ⊢ t : AK

u

u is an approximation of t in the sense that it it can be turned into t by instantiating certain
meta-variables—if a subterm of t cannot be type checked a placeholder meta-variable will be
put in its place, an type checking that subterm will be postponed. Type checking will also
consist in making sure that, once the postponed type-checking problems can be solved, the
placeholder meta-variables will be instantiated accordingly with the corresponding omitted
subterm of t (possibly instantiated further).
For instance, when type checking the type of test, we’ll have
J· ⊢ ((x : BoolOrNat α) → BoolOrNat (1 + x)) → Nat : SetK
((x : BoolOrNat α) → BoolOrNat β) → Nat

Since we cannot type check
x : BoolOrNat α ⊢ 1 + x : Nat

a fresh meta-variable β of type Nat in context x : BoolOrNat α replaces 1 + x. Then, when
checking the body of test, we will check it against the approximated type generated above.
When α is instantiated, we can resume checking that BoolOrNat α = Nat, and if we are
successful, instantiate β := 1 + x. This will prevent us from running into problems when type
checking the body, since when we do instantiate α to 0, we do not have 1 + x later: instead,
β is in its place, preserving the well-typedness of the type.
The Agda system, as described in Norell’s thesis, currently implements this elaboration
interleaving type checking and unification, using some fairly delicate machinery. Our contribution is to describe a type-checking problem entirely in terms of unification constraints,
thus simplifying the algorithm. This highlights an overlap in functionality between the type
checker, which needs to check that types and terms are of a certain shape, and the unifier,
which checks the equality of terms: we are using the unifier as an engine to pattern match
on types, with taking meta-variables into account. Moreover, separating the unifier from the
type checker makes it easy easy to experiment with different unification “backends” used by
the same type checking “frontend”.

3

The type theory

To illustrate the type-checking algorithm we will make use of a dependent type theory with
booleans and one universe. Its syntax is shown in Figure 1.

3.1

Terms and types

Terms and types inhabit the same syntactic class. We usually denote terms with t, u, and
v; and types with A, B, and C . The theory is designed to be the simplest fragment that
presents the problems described in Section 2. For this reason we include a universe Set

5

Norell was following a long tradition of elaborating user syntax when working with type theories, see
Section 7.1 for more details.

F. Mazzoli and A. Abel

5

x, y, z
α, β, γ

-- Variables
-- Meta-variables

-- Types/terms
A, B, C , t, u, v
::= Set
| Bool | true | false
| (x : A) → B | λx → t
| n

-----

n

-- Neutral terms
::= h
| nt
| if n /x.A then t else u
::= x | α

h

Type of types
Booleans
Dependent functions
Neutral term

-- Head
-- Function application
-- Bool elimination
-- Neutral term heads

Γ, ∆ ::= · | Γ, x : A

-- Contexts

Σ, Ξ ::= · | Σ, α : A

-- Signatures

θ, η ::= · | θ, α := t

-- Meta-variable substitutions

Figure 1 Syntax

and means of computing with booleans, so that we can write functions from booleans to
types—otherwise meta-variables can never prevent us from knowing how a type looks like.
The typing rules and algorithms presented in this paper can be extended to a richer theory,
as we have done for our implementation, which includes implicit arguments, user defined
inductive data types and records, and propositional equality.

3.2

Neutral terms, substitutions, and term application

Terms are always kept in β-normal form. Terms headed by a variable or meta-variable are
called neutral, the others canonical. Variable and meta-variable substitution immediately
restore the β-normal form as soon as the substitution is performed, a technique known as
hereditary substitution [13]. Substituting a term u for a head h, i.e., a variable x or metavariable α, is written t[h := u ], reading “substitute u for h in t”. The rules for substitution
are not relevant to the paper and are shown in Appendix B. The appendix also defines rules
to eliminate redexes that substitution might generate, to restore the β-normal form.

3.3

Contexts and signatures

Most operations are done under a context (denoted by Γ or ∆), that stores the types of free
variables; and a signature (denoted by Σ or Ξ), that stores the type of meta-variables. We
tacitly assume that no duplicate names are present in contexts and signatures. We often
make use of a global signature Σ throghout the rules, if there is no need for the rules to carry
it explicitely since it is never changed. Note that a signature contains only closed types for
the meta-variables—we do not make use of an explicit representation of meta-variables in
context. This is for the sake of simplicity, since we do not present our unification algorithm
in detail, where the contextual representation would be most convenient. Throughout the
paper, we will use Γ → A to indicate the function type formed by all the types in Γ as the

6

Type checking through unification

Γ ⊢ Set : Set

Γ ⊢ Bool : Set

Γ ⊢ true : Bool

Γ ⊢ false : Bool

Γ ⊢ A : Set Γ, x : A ⊢ B : Set
Γ, x : A ⊢ t : B
Γ ⊢ n ⇒ A Γ ⊢ A ≡ B : Set
Γ⊢n:B
Γ ⊢ (x : A) → B : Set
Γ ⊢ λx → t : (x : A) → B
Figure 2 Σ; Γ ⊢ t : A Type checking canonical terms

x :A∈Γ
Γ⊢x⇒A
Γ ⊢ n ⇒ Bool

α:A ∈ Σ
Γ⊢α⇒A

Γ ⊢ n ⇒ (x : A) → B
Γ⊢t :A
Γ ⊢ n t ⇒ B[x := t]

Γ, x : Bool ⊢ A : Set
Γ ⊢ t : A[x := true]
Γ ⊢ u : A[x := false]
Γ ⊢ if n /x.A then t else u ⇒ A[x := n]

Figure 3 Σ; Γ ⊢ n ⇒ A Type inference for neutral terms

domains and terminating with A, and t Γ to indicate the term formed by t applied to all
the variables in Γ. Moreover, every mention of a context and a signature is assumed to be
valid according to the rules in Figure 5 and 4.
Throughout the paper, we will also concatenate whole contexts and signatures, e.g. Σ, Ξ.

3.4

Well-typed terms

The bidirectional typing checking rules are shown in figures 2 and 3. The type of neutral
terms can be inferred, while canonical terms are checked. Our type theory includes a universe
Set equipped with an inconsistent typing rule Set : Set for the sake of simplicity, but our
presentation can be extended with stratified universes.
Finally, definitional equality of terms (needed to define the typing rules) is specified in
figures 7 and 8. The conversion rules are performed in a type-directed way, so that it can
respect the η-laws of functions.

3.5

Meta-variable substitutions

We specify typed meta-variable substitutions, a construct that will be useful to give a specification to our unification algorithm. A meta-variable substitution θ from Σ to Ξ gives
an instantiation to each meta-variable in Σ. The meta-variables in the instantiations are
scoped over a new signature Ξ. The validity rule shown in figure 6 makes sure that the
meta-variables instantiations are well-typed with respect to their type.
Applying a substitution θ to a term t amounts to substitute each meta-variable for its
instantiation in θ, as specified in appendix B. Moreover, if the substitution is valid, if we
have Σ; Γ ⊢ t : A and Ξ ⊢ θ : Σ, we will have that
Ξ; θΓ ⊢ θt : θA,

where applying a substitution to a context amounts to applying it to all the types it contains.
Like with contexts and signatures, we will use , to also concatenate meta-variable substitutions. So for example if we have Ξ ⊢ θ : Σ and Ξ ⊢ η : Σ′ , we have that Ξ ⊢ (θ, η) : (Σ, Σ′ ).

F. Mazzoli and A. Abel

⊢Σ
⊢·

7

Σ; · ⊢ A : Set
⊢ Σ, α : A

Σ⊢Γ
Σ; Γ ⊢ A : Set
Σ ⊢ Γ, x : A

Σ⊢·

Figure 4 ⊢ Σ Well-formed signatures

Figure 5 Σ ⊢ Γ Well-formed contexts

for all (α : A) ∈ Σ, α := t ∈ θ and Ξ; · ⊢ t : θA
Ξ⊢θ:Σ
Figure 6 Ξ ⊢ θ : Σ Well-formed meta-variable substitutions

Γ ⊢ Set ≡ Set : Set

Γ ⊢ Bool ≡ Bool : Set

Γ ⊢ false ≡ false : Bool
Γ, x : A ⊢ f x ≡ g x : B
Γ ⊢ f ≡ g : (x : A) → B

Γ ⊢ true ≡ true : Bool

Γ ⊢ A1 ≡ A2 : Set Γ, x : A1 ⊢ B1 ≡ B2 : Set
Γ ⊢ (x : A1 ) → B1 ≡ (x : A2 ) → B2 : Set
Γ ⊢ n ≡ n′ ⇒ A
Γ ⊢ A ≡ B : Set
Γ ⊢ n ≡ n′ : B

Figure 7 Σ; Γ ⊢ t ≡ u : A Definitional equality of canonical terms

Γ ⊢ n ≡ n ′ ⇒ (x : A) → B
Γ ⊢ t ≡ t′ : A
Γ ⊢ n t ≡ n ′ t ′ ⇒ B[x := n]

Γ⊢h⇒A
Γ⊢h≡h⇒A

Γ ⊢ n ≡ n ′ ⇒ Bool
Γ, x : Bool ⊢ A ≡ A : Set
Γ ⊢ t ≡ t ′ : A[x := true]
Γ ⊢ u ≡ u ′ : A[x := false]
Γ ⊢ if n /x.A then t else u ≡ if n ′ /x.A′ then t ′ else u ′ ⇒ A[x := n]
′

Figure 8 Σ; Γ ⊢ n ≡ n ′ ⇒ A Definitional equality of neutral terms

8

Type checking through unification

4

Unification

In this section we will give a specification for the unification algorithm that we will need to
solve the constraints generated by elaboration.

4.1

Unification constraints

The input for the unification algorithm are heterogeneous constraints of the form
Γ ⊢ t : A = u : B.

Such a constraint is well formed if we have that Γ ⊢ t : A and Γ ⊢ u : B. As we will see in
Section 5, it is crucial for the constraints to be heterogeneous for the elaboration procedure
to work as we intend to.
A constraint is solved if we have that Γ ⊢ A ≡ B : Set and Γ ⊢ t ≡ u : A. This means
that to solve a constraint the unifier will have to establish definitional equality of both the
types and the terms.

4.2

Unification algorithm specification

A unification algorithm takes a signature and set of constraints, and attempts to solve them
by instantiating meta-variables. Thus, unification rules will be of the form
Σ, C

Ξ, θ

Where Σ and C are the input signature and constraints, and Ξ and θ are the output signature
and substitution, such that Ξ ⊢ θ : Σ. If the substitution solves all the constraints we have
that
Ξ

θC.

Note that unification might make no progress at all, and just return Σ and the identity
substitution.

4.3

A suitable unification algorithm

Higher order unification in the context of dependently typed languages is still a poorly
understood topic, and we do not have the space to discuss it in depth here. The basis
for most of the unification algorithms employed in such languages is pattern unification, as
introduced by Miller [8]. However in modern languages such as Agda or Coq there are factors
complicating this process. The main inconvenience, as already mentioned in Section 1, is the
fact that we cannot always know if a constraint is solvable, since solving other constraints
might enable us to solve the current one. A algorithm that takes care of handling constraints
under these assumptions is usually called dynamic.
However, another issue when unifying terms in these type theories is that definitional
equality (specified by conversion rules such as the ones presented in this paper) often includes η-laws for functions and product types, and possibly other type-directed conversion
rules. For this reason our constraints equate typed expressions.6 Note that the types in the
constraints are only needed so that we can abide by the η laws.
6

We also have the constraints to equate the types too, but this is only for brevity: if that wasn’t the case,
all we would have to do is to convert each Γ ⊢ t : A = u : B into {Γ ⊢ A : Set = B : Set, Γ ⊢ t : A = u : B }.

F. Mazzoli and A. Abel

Ideally, to solve the heterogeneous constraints, a heterogeneous pattern unification algorithm is needed, such as the one described in chapter 4 of Adam Gundry’s thesis [5].
However, in our prototype, we have found that implementing such an algorithm is impractical for performance reasons.7 In practice, a homogeneous pattern unification algorithm
like the one employed in the Agda system works well enough in many of the examples that
we have analysed. In this context, a heterogeneous constraint Γ ⊢ t :A = u :B is converted to
two homogeneous constraints, Γ ⊢ A = B : Set and Γ ⊢ t = u : A. Some bookkeeping will be
needed to ensure that the constraint equating the types is solved before attempting the one
equating the terms, so that Γ ⊢ t = u : A is considered only when it is well-formed—when
we know that A ≡ B.

5

Type checking through unification

As mentioned in Section 2, our algorithm will elaborate a type-checking problem into a
well-typed term and a set of unification constraints. Given some type-checking problem
Σ; Γ ⊢ t : A, the algorithm will elaborate it into a term u and constraints C, along with an
extended signature Ξ—since the elaboration process will add new meta-variables.
The algorithm is specified using rules of the form
JΣ; Γ ⊢ t : AK

Ξ, u, C,

such that:
Ξ is an extension of Σ;
u is well typed: Ξ; Γ ⊢ u : A;
C is a set of well formed unification constraints;
if unification produces a signature Ξ′ and substitution Ξ′ ⊢ θ : Ξ such that Ξ′ θC, we
have that Ξ′ ; θΓ ⊢ θt ≡ θu : θA. In other words, solving all the constraints restores
definitional equality between the original term t and the original term u.
The main idea is to infer what the type must look like based on the term, and generate
constraints that make sure that, if the constraints can be solved, that will be the case. For
example, if faced with problem
Σ; Γ ⊢ true : A,

we know that A must be Bool. However, A might be a type stuck on a meta-variable, as
discussed in Section 2. At the same time, we want the elaboration procedure to immediately
return a well-typed term. The heterogeneous constraints let us do just that: we will create
a new meta-variable of type A in Γ, and use that as the elaborated term. Moreover we will
return a constraint equating the newly created meta-variable to true:
JΣ; Γ ⊢ true : AK
(Σ, α : Γ → A), α Γ, {Γ ⊢ true : Bool = α Γ : A}

Note how we respect the contract of elaboration—the elaborated term is well-typed, the
constraint is well-formed—without making any commitment on the shape of A.
For a more complicated example, consider the type-checking problem

7

Specifically, the need to typecheck meta-variable instantiations and retry if they are ill-typed is particularly taxing.

9

10

Type checking through unification

Σ; Γ ⊢ λx → t : A.

We know that A needs to be a function type, but we do not know what the domain and
codomain types are yet. To get around this problem we will add new meta-variables to the
signature acting as the domain and codomain, then elaborate the body using those, and
follow the same technique illustrated above to return a well-typed term by adding a new
meta-variable:
-- Add meta-variables for the domain (β) and codomain (γ):
Σ1 := Σ, β : Γ → Set, γ : Γ → (x : β) → Set
-- Elaborate the body of the abstraction:
JΣ1 ; Γ, x : β ⊢ t : γ Γ xK
Σ2 , u, C
-- Add meta-variable that we will return as the elaborated term:
Σ3 := Σ2 , α : Γ → A
-- Return the appropriate constraint equating the abstracted elaborated body to the new
-- meta-variable, together with the constraints generated from elaborating the body:
JΣ; Γ ⊢ λx → t : AK
Σ4 ,
α Γ,
{Γ ⊢ (λx → u) : (x : β Γ) → γ Γ x = α Γ : A} ∪ C

Note how the use of heterogeneous equality is crucial if we want to avoid to ever commit
to the types having a particular shape, while having all the constraints to be well-formed
immediately.
Every rule in full algorithm is going to follow the general pattern that emerged above:
(a) Elaborate sub-terms, adding meta-variables to have types to work with;
(b) Add a meta-variable serving as the elaborated term, say α;
(c) Return a constraint equating α to a term properly constructed using the elaborated
subterms; together with the constraints returned by elaborating said subterms.
For brevity we present the full algorithm using an abbreviated notation that implicitely
threads the signatures (Σ, Σ1 , Σ2 , and Σ3 in the example above) across rules. We will also use
the macro Fresh(_, _) to add new meta-variables in a context, such that α := Fresh(Γ, A)
is equivalent to Ξ := Σ, α : Γ → A, and successive appearances of α are automatically applied
to Γ, and where Σ and Ξ are the old and new signature—which are, as said, implicitly
threaded. Finally, we implicitly collect the constraints generated when elaborating the
subterms, and implicitly add a meta-variable that stands for the elaborated term, together
with an appropriate constraint—steps (b) and (c) in the process described above.8 For
example, the rule to elaborate abstractions, explained before, will be shown as
β := Fresh(Γ, Set)
γ := Fresh(Γ, x : β, Set)
JΓ, x : β ⊢ t : γK
u
JΓ ⊢ λx → t : AK
(λx → u) : (x : β) → γ
The complete algorithm is shown in figure 9. They are remarkably similar to the typing rules, however instead of matching directly on the type we expect we match through
constraints.
8

In our Haskell implementation, the elaboration is a state and writer monad over the signature and the
constraint set, respectively.

F. Mazzoli and A. Abel

JΓ ⊢ Set : AK

JΓ ⊢ false : AK

11

Set : Set

JΓ ⊢ Bool : AK

Bool : Set

JΓ ⊢ true : AK

true : Bool

JΓ ⊢ A : SetK
A′
Γ, x : A′ ⊢ B : Set
B′
JΓ ⊢ (x : A) → B : S K
(x : A′ ) → B ′ : Set

false : Bool

β := Fresh(Γ, Set)
γ := Fresh(Γ, x : β, Set)
JΓ, x : β ⊢ t : γK
u
JΓ ⊢ λx → t : AK
(λx → u) : (x : β) → γ

x :A∈Γ
JΓ ⊢ xK
x :A

β := Fresh(Γ, Set)
γ := Fresh(Γ, x : β, Set)
JΓ ⊢ n : (x : β) → γK
t
JΓ ⊢ u : βK
v
JΓ ⊢ n u : AK
t v : γ[x := v]

α:A ∈Σ
JΓ ⊢ αK
α:A

JΓ, x : Bool ⊢ B : SetK
B′
JΓ ⊢ n : BoolK
t
′
′
JΓ ⊢ u : B [x := true]K
u
JΓ ⊢ v : B ′ [x := false]K
v′
JΓ ⊢ if n /x.B then u else v : AK
if t /x.B ′ then u ′ else v ′ : B ′ [x := t]
Figure 9 JΣ; Γ ⊢ t : AK

Ξ, u, C Elaboration

The rules can easily be turned into an algorithm which pattern matches on the term and
decides how to proceed.9 Naturally the algorithm can still fail if it encounters an out of
scope meta-variable or variable, although in real systems scope checking is usually performed
beforehand.

5.1

Examples

We will explore how the algorithm works by going through various common situations. The
reader can experiment using the mentioned tog tool, passing the -d ’elaborate’ commandline flag to have it to print out the generated constraints. A wealth of examples are present
in the repository. We will assume the usage of pattern unification to solve constraints when
examining the examples.

5.1.1

A simple problem

Let’s take type-checking problem
·; · ⊢ true : Bool.

The algorithm will return the triple
α : Bool, α, {· ⊢ true : Bool = α : Bool }

The constraint is immediately solvable, yielding the substitution α := true, which will restore
definitional equality between the elaborated term and true.

5.1.2

An ill-typed problem

Now for something that should fail. Given
9

Our implementation can be found at https://github.com/bitonic/tog/blob/master/src/Tog/Elaborate.hs.

12

Type checking through unification

add : Nat → Nat → Nat,

we want to solve
·; x : Nat ⊢ add x : Nat.

The algorithm will return the triple
Σ, ζ x, C where
Σ = α : Nat → Nat, β : (x : Nat) → Nat → Set, γ : (x : Nat) → α x,
δ : (x : Nat) → (y : α x) → β x y, ζ : Nat → Nat
C = {x : Nat ⊢ δ x (γ x) : β x (γ x) = ζ x : Nat,
x : Nat ⊢ add : Nat → Nat → Nat = δ x : (y : α x) → β x y,
x : Nat ⊢ x : Nat = γ x : α x }

While looking scary at first, the meaning of the meta-variables and constraints is easy to
interpret, keeping in mind that we generate one constraint per subterm (including the top
level term).
At the top level, we elaborate the two subterms add and x. We know that add must be a
function type, since it is applied to something; and that the type of x must match the type
of the domain of said function type. Thus, two meta-variables are created to represent the
domain and codomain—α and β. Then, add and x are elaborated with said types, which in
turn requires the addition of γ and δ, serving as elaborated terms. These are the ingredients
for the second and third constraint. Finally, the elaborated δ (representing add) is applied to
γ (representing x), and equated to a new meta-variable ζ, which is the result of the top-level
elaboration.
The constraints reflect the fact that the term is ill-typed: β is equated both to Nat (in
the first constraint), and to Nat → Nat, in the second constraint. Thus, unification will fail.

5.1.3

An unsolvable problem

Finally, let’s go back to an example which cannot immediately be solved in its entirety:
α : Nat; · ⊢ (true, 0) : BoolOrNat α × Nat.

The desired outcome for this problem is to type check the second element of the pair, 0;
but “suspend” the type checking of the first element by replacing refl with a meta-variable.
Running the type-checking problem through the elaboration procedure yields
Σ, ζ x, C where
Σ = β : Set, γ : Set, δ : β, ζ : γ, ι : BoolOrNat α × Nat
C = {· ⊢ (δ, ζ) : β × γ = ι : BoolOrNat α × Nat,
· ⊢ 0 : Nat = ζ : γ,
· ⊢ true : Bool = δ : β }

The second and third constraints regard the two sub-problems individually, and are solvable
yielding the substitution
β := Bool, δ := true, γ := Nat, ζ := 0,

and leaving us with

F. Mazzoli and A. Abel

13

· ⊢ (true, 0) : Bool × Nat = ι : BoolOrNat α × Nat.

At this point the unifier will be able to substitute ι with a pair
· ⊢ (true, 0) : Bool × Nat = (ξ, 0) : BoolOrNat α × Nat.

Now solving the constraint amounts to solve
· ⊢ true : Bool = ξ : BoolOrNat α,

but the unifier is not going to be able to make progress, since substituting ξ for true will
leave the constraint ill-formed. Thus, the final result of the elaboration and unification will
be (ξ, 0), which is all we could hope for.

5.2

Some properties

◮ Lemma 1 (Well-formedness and functionality of elaboration). Let ⊢ Σ and Σ ⊢ Γ.
1. There uniquely exist a signature Ξ, constraints C, a term t ′ , and a type A such that
JΣ; Γ ⊢ tK

Ξ | C ⊢ t′ ⇒ A

and Ξ; Γ ⊢ A : Set.
2. If Σ; Γ ⊢ A : Set, then there uniquely exist a signature Ξ, constraints C, and a term t ′
such that
JΣ; Γ ⊢ t ⇐ AK

Ξ | C ⊢ t′.

In both cases, Ξ is necessarily an extension of Σ and all the outputs are well-formed, meaning
⊢ Ξ and Ξ; Γ ⊢ t ′ : A and Ξ; Γ ⊢ C.
Proof. By induction on t.

◭

◮ Lemma 2 (Soundness of elaboration).
If one of
JΣ; Γ ⊢ tK
Ξ | C ⊢ t′ ⇒ A
JΣ; Γ ⊢ t ⇐ AK
Ξ | C ⊢ t′

and there is some well-typed meta substitution Σ′ ⊢ θ : Ξ that solves the constraints, i.e.,
Σ′ θC, then
Σ′ , θΓ ⊢ θt ≡ θt ′ : θA.

Proof. By induction on term t.

◭

◮ Lemma 3 (Strong soundness of elaboration).
1. If
JΣ; Γ ⊢ tK

Ξ | C ⊢ t′ ⇒ A

and there is some closing untyped substitution σ such that dom(σ) ⊇ dom(Ξ) and ⊢ σ : Σ
and σΓ ⊢ σA : Set and σ solves the untyped constraints, then
σΓ ⊢ σt ≡ σt ′ : σA.

14

Type checking through unification

2. If
JΣ; Γ ⊢ t ⇐ AK

Ξ | C ⊢ t′

and there is some closing untyped substitution σ : Ξ that is well-typed for Σ, i.e, ⊢ σ : Σ
and solves the untyped constraints, i.e., σC, then
σΓ ⊢ σt ≡ σt ′ : σA.

Proof. By induction on term t.
Case Abstraction λx → t
[[(Σ, α : (Γ → Set)); (Γ, x : (α Γ)) ⊢ t]]
Ξ | C ⊢ t′ ⇒ B
[[Σ; Γ ⊢ (λx → t)]]
Ξ | C ⊢ (λx → t′ ) ⇒ ((x : α Γ) → B)
By assumption ⊢ σ : Σ and σΓ ⊢ σ((x : α Γ) → B) : Set, which by inversion gives
us σΓ ⊢ (σα) Γ : Set and σ(Γ, x : α Γ) ⊢ σB : Set. Thus ⊢ σα : (σΓ → Set) and
⊢ σ : (Σ, α : (Γ → Set)). By induction hypothesis, σΓ, x : σ(α Γ) ⊢ σt = σt′ : σB, thus by
the ξ rule for equality, σΓ ⊢ σ(λx → t) = σ(λx → t′ ) : σ((x:α Γ) → B).
Case Application t u
[[Σ; Γ ⊢ u]]
Σ1 | C 1 ⊢ u ′ ⇒ A
[[Σ1 , β : ((Γ, x:A) → Set); Γ, x:A ⊢ t ⇐ ((x:A) → β Γ x)]]
[[Σ; Γ ⊢ t u]]
Σ 2 | C 1 ∪ C 2 ⊢ t′ u ′ ⇒ β Γ u ′

Σ 2 | C 2 ⊢ t′

By the first induction hypothesis, σΓ ⊢ σu = σu′ : σA. By the second induction hypothesis
◭
◮ Lemma 4 (Completeness of elaboration). Let us assume a term t and a wellformed signature Σ and Σ ⊢ Γ and a second signature Ξ and a substitution Ξ ⊢ θ : Σ such that
Ξ; θΓ ⊢ θt : C .
1. Then
JΣ; Γ ⊢ tK

(Σ, Σ′ ) | C ⊢ t ′ ⇒ B

and there exists a substitution θ′ such that
Ξ ⊢ (θ, θ′ ) : (Σ, Σ′ )
Ξ (θ, θ′ )C
Ξ; θΓ ⊢ C = (θ, θ′ )B : Set
Ξ; θΓ ⊢ θt = (θ, θ′ )t ′ : C .

2. Further, if Σ; Γ ⊢ A : Set and Ξ; θΓ ⊢ θA = C : Set, then
JΣ; Γ ⊢ t ⇐ AK

(Σ, Σ′ ) | C ⊢ t ′

and there exists a substitution θ′ such that
Ξ ⊢ (θ, θ′ ) : (Σ, Σ′ )
Ξ (θ, θ′ )C
Ξ; θΓ ⊢ θt = (θ, θ′ )t ′ : C .

F. Mazzoli and A. Abel

15

In other words, if it’s possible to instantiate some meta-variables to make t well-typed, then
all the constraints generated by the elaboration procedure are solvable.
Proof. By induction on t.

◭

(Σ, Σ′ ) | C ⊢ t ′ ⇒ A′ , then
◮ Corollary 5 (Simple inference). If Σ; Γ ⊢ t : A and JΣ; Γ ⊢ tK
all the constraints in C are solvable by some substitution Σ ⊢ θ′ : Σ′ and Σ; Γ ⊢ A = θ′ A′ : Set.
Proof. From Completeness with Ξ = Σ and identity substitution θ.

◭

◮ Corollary 6 (Simple checking). If Σ; Γ ⊢ t : A and JΣ; Γ ⊢ t ⇐ AK
all the constraints in C are solvable.

(Σ, Σ′ ) | C ⊢ t ′ , then

Proof. From Completeness with Ξ = Σ and identity substitution θ.

◭

5.2.1

Effectiveness

While the properties above guarantee establish some basic results about the algorithm, they
are all also satisfied by the very useless elaboration algorithm
JΣ; Γ ⊢ t : AK

(Σ, α : Γ → A, β : Γ → Set), α Γ, {Γ ⊢ α Γ : A = t : β Γ}.

However, the intent of the developed algorithm is to be as effective, when used with pattern
unification, as the current techniques to type check dependent types with meta-variables.
To achieve this, it has been designed so that the generated constraints fall in the pattern
fragment when existing type checkers would be able to make progress, and by testing the
algorithm “in the wild” with existing Agda programs we have found it effective in practice.
For instance, if we did not keep our terms in β-normal form, we could not elaborate applications into constraints falling into the pattern fragment, due to the fact that we cannot
reliably infer the type of the function.
However, future work should involve a formal characterization of completeness in the
context of type checkers for dependent types with meta-variables, and a proof that our
algorithm is indeed complete.

6

Additional remarks

6.1

Additional features

In this section we will briefly sketch how to fit popular features into the framework described.
The general idea is to do everything which doesn’t require normalization in the elaboration
procedure, and the rest into the unifier.

6.1.1

Implicit arguments

We have already implemented a restricted form of implicit arguments, which we call “type
schemes” in line with ML terminology. Type schemes allow the user to define a number of
implicit arguments in top-level definitions, for example the already mentioned
head : {A : Set} → {n : Nat} → Vec A (1 + n) → A.

, before even
Under this scheme, every occurrence of head is statically replaced with head
elaborating—we do it while scope checking. However this is obviously limited, since we can
only have implicit arguments before any explicit ones and only for top-level definitions.

16

Type checking through unification

We want to enable a more liberal placement of implicit arguments. This is achieved in
Agda by allowing implicit arguments in all types, and in any many positions. The details of
the implementation are still in flux in Agda itself, but the core idea is to type-check function
application and abstractions bidirectionally, by first looking at the type and inserting implicit
arguments if needed. So elaborating t u where t : {x : A} → (y : B) → C will result in t u.
Similarly, elaborating t : {x : A} → B will result in λ{x } → t, where {x } binds an implicit
arguments.
We are exploring two ways to integrate this kind of mechanism in our framework:
Mimic the bidirectional type-checking performed in Agda and similar systems closely, by
adding a new kind of constraint for function application and abstraction which waits on
the type to have a rigid head, that is to say a type not blocked on a meta-variable.
Alternatively, force all implicit arguments to appear before an explicit one (with the
exception of type schemes), and always include an implicit arguments in →-types.10
Multiple implicit arguments will then be handled by one implicit argument carrying a
tuple.
We are currently implementing the latter proposal, since it is simpler to describe and to
implement, although only using it will tell if it is practical.11

6.1.2

Type classes

Type classes, as employed by Haskell, were introduced to handle overloaded operators in
programming languages [12]. Other similar structures include canonical structures in Coq.
In short, type classes let the user specify a collection of methods that can be implemented
for a specific type. For example, the type class identifying monoid is defined as
class Monoid a where
mempty : a
mappend : a → a → a
-- Monoid instance for list
instance Monoid [a ] where
mempty = [ ]
-- Empty list
mappend = (+
+) -- Concatenation
-- Monoid instance for pairs of monoids
instance (Monoid a, Monoid b) ⇒ Monoid (a, b) where
mempty = (mempty, mempty)
mappend (x1 , y1 ) (x2 , y2 ) = (x1 ‘mappend‘ x2 , y1 ‘mappend‘ y2 )

Type classes are a form of type-directed name resolution, and thus cannot be resolved at
elaboration time—we might need to instantiate meta-variables before being able to resolve
the right method. To integrate it in our framework we have to include type-classes into
our unification procedure. Luckily, this is exactly what the authors of the theorem prover
Matita accomplished using what they dubbed unification hints [1]. Briefly, the unifier is
given “hints” on how to solve problems that it cannot resolve by itself, and such hints are
repeatedly tried if unification fails.

10

Note that the restriction of having implicit arguments always paired with explicit ones is being planned
in Agda too, to make the automatic insertion of implicit arguments more predictable.
11
A more thorough proposal is available at https://github.com/bitonic/tog/wiki/Implicit-Arguments.

F. Mazzoli and A. Abel

Similar to type-classes, overloaded constructors are a feature introduced by Agda, that
lets the user define multiple data constructors with the same name. When such an overloaded constructor is used, its type must be determined by the type we are type checking
it against. It is easy to see how this problem is essentially the same as resolving the right
type class instance when encountering one of its methods—the type-class being “data types
with the same constructors”, the instances being the data-types, and the methods being the
constructors—, and thus we plan to implement this feature using unification hints as well.

6.2

Performance

One reason for concern is that our algorithm generates more constraints than ordinary typechecking algorithms. However, as already remarked, our algorithm generates a number of
constraints and meta-variables which is linear in the size of the input term. Moreover, we
would expect the unifier to spend little time solving the trivial constraints which are normally
handled by the type-checker directly.
In the examples we have collected, we have found that this is the case, and the run time
is dominated by unification filling in implicit arguments which can become very large. More
specifically, most of the time is spent dealing with η-expansion, which we plan to improve
in the future.

7

Conclusion

We have presented an algorithm that leverages the unifier, an important part of already
existing dependently typed programming languages and theorem provers, to greatly simplify
the process of type checking. The expressivity of higher-order unification lets us specify the
type-rules concisely. Moreover, we have clearly separated type checking from unification,
allowing for greater modularity.
We have implemented the ideas presented in the tog, covering a large subset of the Agda
languages. We are currently in the process of improving tog to get narrow the gap between
its capabilities and Agda.

7.1

Acknowledgements and related work

This work is a continuation of the work by Norell & Coquand [10], which describes how
Agda deals with issues that we presented. In fact, the algorithm described here is a simpler
re-implementation of what they specified.
The other main inspiration came from a discussion with Adam Gundry about how Epigram 2 deals with type checking in the presence of meta-variables. The propositional equality
Epigram 2 is powerful enough to represent constraints stuck on some meta-variable as an
unfinished equality proof. Thus, the unifier, when given a constraint Γ ⊢ t : A = u : B
produces a—possibly unfinished—proof that Γ ⊢ t : A ≡ u : B, where here ≡ denotes Epigram’s heterogeneous propositional equality. This proof can be used to “transport” terms
on one side of the equation to the other. From this discussion I realised that such a powerful
equality was not needed to implement a similar system.
The already cited work on Matita [1] convinced us further that isolating “dynamic”
procedures in the unifier is a good idea.
Finally, our work follows a long tradition of separating elaboration of the user syntax into
a core type theory, and the type-checking of such theory. As far as we know this line of work

17

18

Type checking through unification

Set[h := t]

Set

Bool[h := t]

Bool

true[h := t]

A[h := t]
A′
B[h := t]
B′
((x : A) → B)[h := t]
(x : A′ ) → B ′
h[h := t]

t

n[h := t]

w

h 6≡ h ′
h [h := t]
h′

true

u[h := t]
(λx → u)[h := t]
n[h := t]

′

v
u[h := t]
(n u)[h := t]

A[h := t]
A′
u[h := t]
u′
v[h := t]
′
′
′
if w /x.A then u else v
w′
(if n /x.A then u else v)[h := t]
w′

Figure 10 u[h := t]
terms

u ′ and n[h := t]

false[h := t]

u′
v′

false

u′
λx → u ′
v u′

v′

v′

u Hereditary substitution into canonical and neutral

goes back at least to Coquand and Huet’s “Constructive Engine” [6], with its separation
between the “concrete” user syntax and the internal “abstract” syntax.
Moreover, we’d like to thank Andrea Vezzosi, Nils Anders Danielsson, Conor McBride,
and Bas Spitters for the useful input.

A

Syntax and types used in examples

Throughout the examples we use a syntax close to the one in Agda and Haskell. Some
details regarding the syntax:
type and data constructors are shown in a sans serif font;
new meta-variables are introduced using underscores ( );
binary operators are referred to with parentheses, e.g. (+);
implicit arguments are indicated by curly braces;
definitions can be defined by pattern matching.
We use some standard types, namely:
Set : Set—Set is the type of all types, and its type is Set itself;
Bool : Set, inhabited by true and false;
Nat : Set, representing the natural numbers, introduced by number literals (1, 2, etc.);
(≡):{A:Set} → A → A → Set, the identity type; inhabited by refl:{A:Set} → {x :A} →
x ≡ x.

B

Substitution and term elimination

Figure 10 show the rules to substitute a term u for a head h, which can be a variable x or a
meta-variable α. Substituting (n u)[h := t] into proper neutral terms n t might (in case the
head of n is h) generate redexes, which are eliminated by invocations of the term elimination
judgment t u
v and if t /x.A then u else v
t, whose rules are given respectively in
Figure 11 and Figure 12. Term elimination in turn invokes substitution when the eliminated
term is a λ-abstraction.
While we use explicit names in our rules, we do not address issues related to α-renaming
here. In our prototype substitution is implemented using de Bruijn indices [4].

F. Mazzoli and A. Abel

19

t[x := u]
(λx → t) u
Figure 11 t u

t′
t′

v Application elimination

(if true /x.A then t else u)
Figure 12 if t /x.A then u else v

t

(if false /x.A then t else u)

u

t Bool elimination

References
1
2
3
4

5
6
7
8
9

10
11
12

13

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Hints in
unification. In Theorem Proving in Higher Order Logics, pages 84–98. Springer, 2009.
Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development,
Coq’Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.
Edwin Brady. Idris, a general-purpose dependently typed programming language: Design
and implementation. Journal of Functional Programming, 23(05):552–593, 2013.
Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool
for automatic formula manipulation, with application to the church-rosser theorem. In
Indagationes Mathematicae (Proceedings), volume 75, pages 381–392. Elsevier, 1972.
Adam Gundry. Type Inference, Haskell and Dependent Types. PhD thesis, Department of
Computer and Information Sciences, University of Strathclyde, 2013.
Gérard Huet. The constructive engine. A Perspective in Theoreticak Computer Science,
pages 38–69, 1989.
Conor McBride and James McKinna. The view from the left. Journal of Functional
Programming, 14(1):69–111, 2004.
Dale Miller. Unification under a mixed prefix. J. Symb. Comput., 14(4):321–358, October
1992.
Ulf Norell. Towards a practical programming language based on dependent type theory.
PhD thesis, Department of Computer Science and Engineering, Chalmers University of
Technology, SE-412 96 Göteborg, Sweden, 2007.
Ulf Norell and Catarina Coquand. Type checking in the presence of meta-variables. Unpublished draft, 2007.
Robert Pollack. Implicit syntax. Informal Proceedings of First Workshop on Logical Frameworks, Antibes, May 1990.
Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL ’89, pages 60–76, New York, NY, USA, 1989. ACM.
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical
framework i: Judgments and properties. Technical report, DTIC Document, 2003.

