Equality Proofs and Deferred Type Errors
A Compiler Pearl
Dimitrios Vytiniotis

Simon Peyton Jones

Microsoft Research, Cambridge{dimitris,simonpj}@microsoft.com

Abstract
The Glasgow Haskell Compiler is an optimizing compiler that expresses and manipulates first-class equality proofs in its intermediate language. We describe a simple, elegant technique that exploits
these equality proofs to support deferred type errors. The techniquerequires us to treat equality proofs as possibly-divergent terms; weshow how to do so without losing either soundness or the zerooverhead cost model that the programmer expects.
Categories and Subject Descriptors D.3.3 [Language Constructs
and Features]: Abstract data types; F.3.3 [Studies of Program
Constructs]: Type structure
General Terms Design, Languages
Keywords Type equalities, Deferred type errors, System FC

1.

Introduction

In a compiler, a typed intermediate language provides a firm place
to stand, free from the design trade-offs of a complex source language. Moreover, type-checking the intermediate language provides a simple and powerful consistency check on the earlier stagesof type inference and other optimizing program transformations.
The Glasgow Haskell Compiler (GHC) has just such an intermediate language. This intermediate language has evolved in the last
few years from System F to System FC (Sulzmann et al. 2007;
Weirich et al. 2011) to accommodate the source-language featuresof GADTs (Cheney and Hinze 2003; Peyton Jones et al. 2006;
Sheard and Pasalic 2004) and type families (Chakravarty et al.
2005; Kiselyov et al. 2010); and from System FC to System F↑C , acalculus now fully equipped with kind polymorphism and datatype
promotion (Yorgey et al. 2012).
The principal difference between System F and System F↑C is that,together with type information, System F↑C carries equality proofs:

evidence that type equality constraints are satisfied. Such proofs
are generated during the type inference process and are useful for
type checking System F↑C programs. However, once type checkingof the F↑C program is done, proofs – very much like types – can beJosé Pedro Magalhães
Utrecht University
jpm@cs.uu.nl

completely (and statically) erased, so that they induce no runtime
execution or allocation overhead.
Proof assistants and dependently typed languages (Bove et al. 2009;
Norell 2007; The Coq Team) adopt a similar design with staticallyerasable proofs, including ones that go beyond equality to more
complex program properties. However, there is one important difference: in proof assistants the proof language is the computation
language, always a side-effect free and terminating language thatguarantees logical consistency of the proofs. On the other hand,in System F↑C the computation language includes partial functions
and divergent terms. To ensure logical consistency, F↑C keeps theequality proof language as a syntactically separate, consistent-byconstruction set of equality proof combinators.
In this paper we investigate the opportunities and challenges ofblurring the rigid proof/computation boundary, without threatening
soundness, by allowing “proof-like” first-class values to be returned
from ordinary (even divergent or partial) computation terms. We
make the following contributions:• The proofs-as-values approach opens up an entirely new pos-sibility, that of deferring type errors to runtime. A common
objection to static type systems is that the programmer wants
to be able to run a program even though it may contain some
type errors; after all, the execution might not encounter the error. Recent related work (Bayne et al. 2011) makes a convincing case that during prototyping or software evolution programmers wish to focus on getting part of their code right, without
first having to get all of it type-correct. Deferring type errors
seems to be just the right mechanism to achieve this. Our new
approach gives a principled way in which such erroneous programs can be run with complete type safety (Sections 3 and 5).
• The key to the almost effortless shift to proofs-as-values isbased on a simple observation: System F↑C , with the recent addition of kind polymorphism (Yorgey et al. 2012), already allows
us to define within the system an ordinary first-class type fortype equality (Section 4). As such, we can have ordinary values of that type, that are passed to or returned from arbitrary(even partial or divergent) terms. Moreover, deferring type errors aside, there are other compelling advantages of proofs-asvalues in an evidence-passing compiler, as we outline in Section 6.
• Most functional programmers think of types as static objects,

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
ICFP’12, September 9–15, 2012, Copenhagen, Denmark.
Copyright © 2012 ACM 978-1-4503-1054-3/12/09. . . $10.00

with zero run-time overhead, and they expect the same of proofs
about types. Treating type equality proofs as values seriously
undermines this expectation. In Section 7 we address this challenge and show how the optimizer of GHC, with no changes
whatsoever, can already eliminate the cost of equality proofs –except in corner cases where it would be wrong to do so.

Everything we describe is fully implemented. As far as we know,
GHC is the first, and only, widely-used optimizing compiler thatmanipulates first-class proofs. We describe this paper as a “pearl”
because it shows a simple and elegant way in which the apparentlyesoteric notion of a “proof object” can be deployed to solve a verypractical problem.

2.

The opportunity: deferring type errors

Suppose you type this Haskell term into the interactive read-evalprint prompt in GHCi:
ghci> fst (True, ’a’ && False)
This term does not “go wrong” when evaluated: you might expect
to just get back the result True from projecting the first componentof the pair. But in a statically typed language like Haskell you get
the type error:
Couldn’t match ‘Bool’ with ‘Char’In the first argument of ‘(&&)’, namely ’a’This behaviour is fine for programs that are (allegedly) finished, butsome programmers would much prefer the term to evaluate to True
when doing exploratory programming. After all, if the error is ina bit of the program that is not executed, it is doing no harm! In
particular, when refactoring a large program it is often useful to beable to run parts of the completed program, but type errors prevent
that. What we want is to defer type errors until they matter. We havemore to say about motivation and related work in Section 8.
As we shall see, System F↑C allows us to offer precisely this behaviour, without giving up type safety. Here is an interactive session
with ghci -fdefer-type-errors:
ghci> let foo = (True, ’a’ && False)
Warning: Couldn’t match ‘Bool’ with ‘Char’
ghci> :type foo(Bool, Bool)ghci> fst foo
Trueghci> snd foo
Runtime error: Couldn’t match ‘Bool’ with ‘Char’
Notice that:• The definition of foo produced a warning (rather than an error),but succeeds in producing an executable binding for foo.
• Since type checking of foo succeeded it has a type, which canbe queried with :type to display its type, (Bool, Bool).
• The term fst foo typechecks fine, and also runs fine, returning

True.
• The term snd foo also typechecks fine, and runs; however theevaluation aborts with a runtime error giving exactly the sameerror as the original warning.
That is, the error message is produced lazily, at runtime, when andonly when the requirement for Char and Bool to be the same typeis encountered.
2.1

How deferring type errors works, informally

GHC’s type inference algorithm works in two stages: first we generate type constraints, and then we solve them (Vytiniotis et al.
2011). In addition, inference elaborates the Haskell source term to
an explicitly typed F↑C term, that includes the types and proofs (“evidence” in GHC jargon) computed by the constraint solver.

In the previous example, during type inference for the sub-term’a’ && False we generate a type equality constraint, written
Char ∼ Bool. Usually the constraint solver would immediately reject such a constraint as insoluble, but with -fdefer-type-errors
we take a different course: we generate “evidence” for Char ∼Bool, but ensure that if the (bogus) evidence is ever evaluated itbrings the program to a graceful halt. More concretely, here is theF↑C term that we generate for foo:
foo = let (c : Char ∼ Bool) = error "Couldn’t..."in (True, (cast ’a’ c) && False)
The elaborated foo contains a lazy binding of an evidence variable
c of type Char ∼ Bool to a call to error. The latter is a built-in
Haskell constant, of type ∀a . String → a, that prints its argument
string and brings execution to a halt.
When we evaluate fst foo the result is True; but if we evaluate
snd foo, we must evaluate the result of (&&), which in turn evaluates its first argument, cast ’a’ c. The cast forces evaluation of c,and hence triggers the runtime error. Note that the exact placementof coercions, and thus which errors get deferred, depends on the internals of the type inference process; we discuss this in more detailin Section 5.4.
There is something puzzling about binding variable c with the type
Char ∼ Bool. The evidence variable c is supposed to be boundto a proof witnessing that Char and Bool are equal types, but isnevertheless bound to just a term, and in fact a crashing term,
namely error! How can we then ensure soundness, and how can weget statically erasable proofs? It turns out that the type Char ∼ Boolis almost but not quite the type of a proof object. To explain how
this works, we move on to present some more details on GHC’s
typed intermediate language, System F↑C .

3.

The F↑C language

System F↑C is a polymorphic and explicitly typed language, whose
syntax is given in Figure 1. Our presentation closely follows themost recent work on F↑C Yorgey et al. (2012), and we will not repeat
operational semantics and type soundness results; instead, we refer
the reader to Yorgey et al. (2012) for the details.
A quick glance at Figure 1 will confirm that the term language e
is mostly conventional, explicitly-typed, lambda calculus, with letbindings, literals (l), data constructors (K), and case expressions.
In addition, the language includes type and kind polymorphism:
type (Λa:η.e) and kind (Λχ.e) abstractions, and type (e ϕ) andkind (e κ) applications, respectively. Some motivation for kind
abstractions and applications comes from previous work but, as weshall see in Section 6.2, kind polymorphism will play a key role
here as well.
The distinctive feature of F↑C is the use of coercions, γ. A coercion γof type τ ∼# ϕ is nothing more than a proof of type equality between
the types ϕ and τ. Contrary to the notation used in Section 2.1 andin previous presentations of System F↑C notice that we use symbol∼# instead of ∼ for coercion types, and Constraint# rather thanConstraint for their kind – this is for a good reason that will become
evident in Section 4.2.
The term (e . γ) is a cast that converts a term e of type τ to one oftype ϕ, when γ : τ ∼# ϕ. Once again, this is deliberately different
than the cast term that appeared in Section 2.1, as we discuss in
Section 4.2. The only other place where a coercion γ may appear
in the term language is in an application (e γ), so coercions are not
first-class values. Dually, one can abstract over such coercions witha coercion abstraction λ (c:τ ∼# ϕ) . e.

Termse, u ::=
|
|
|
|
|
p
::=
Types
ϕ, σ , τ, υ

x | l | λ x:σ .e | e u
Λa:η.e | e ϕ | Λχ.e | e κ
λ c:τ.e | e γ
K | case e of p → u
let x:τ = e in ue.γ
K c:τ x:τΓ `tm e : τType/kind polymorphism
Coercion abs/app

Γ` x:τ
Γ, (x:σ ) `tm e : τΓ `ty σ : ?

Cast
Patterns

Γ `tm λ x:σ .e : σ → τ
::=
|
|
|
|
|
|

a
H
F
ϕ1 ϕ2
ϕκ
∀a:η.ϕ∀χ.τ

Variables
Constants
Type functions
Application
Kind application
Polymorphic types
Kind-polymorphic types

T
(→)
(∼# )

Datatypes
Arrow
Primitive equality type

χ |?|κ →κ∀χ.κ
Constraint#

Polymorphic kinds
Kind of static proofs

Coercion values
γ, δ
::=
|
|
|
|
|

c
γ1 γ2
hϕi
γ1 ; γ2sym γ...

Variables
Application
Reflexivity
Transitivity
Symmetry
Other coercion forms

Environments
Γ, ∆
::=
bnd
::=
|
|
|
|
|
|
Notation
Tκτ
≡
α →α
≡
≡
3

· | Γ, bnd
χa:ηc : σ ∼# ϕx:σ
T : ∀χ.κ → ?
K : ∀χ (a:ηa ).τ → T χ a...
T κ1 . . . κm τ1 . . . τn
α1 → . . . → αn → α
for α either κ or τ

initial (closed) environment(∼# ) : ∀χ.χ → χ → Constraint#

The syntax of coercions themselves (γ in Figure 1) includes coercion variables, constructors for reflexivity, transitivity, and symmetry, as well as other constructors (such as lifting type equalities overdata constructors) that we do not need to discuss in this paper.
The well-formedness judgement for terms appears in Figure 2
and is mostly conventional. In particular, the rules for coercion
abstraction and application (ECA BS and ECA PP) mirror those forterms (EA BS and EA PP). The rule for case expressions (EC ASE) isalso standard but notice that it allows us to bind coercion variables,
as well as term variables, in a pattern.

Γ `tm K : σ

EA BSECA BSΓ `tm e : (σ1 ∼# σ2 ) → τΓ `co γ : σ1 ∼# σ2Γ `k η
Γ, (a:η) `tm e : τΓ `tm Λa:η.e : ∀a:η.τ
Γ, χ `tm e : τΓ `tm Λχ.e : ∀χ.τETABS

EK ABSΓ, (x:σ ) `tm u : σΓ, (x:σ ) `tm e : τΓ `tm let x:σ = u in e : τ

EL ET

EA PP

Γ `tm e u : τΓ `tm λ c:σ .e : σ → τΓ `tm e γ : τEC ONΓ `tm e : σ → τΓ `tm u : σΓ, (c:σ ) `tm e : τΓ `ty σ : Constraint#

ECA PPΓ `tm e : ∀a:η.τ
Γ `ty ϕ : ηΓ `tm e ϕ : τ[ϕ/a]Γ `tm e : ∀χ.τΓ `k κ
Γ `tm e κ : τ[κ/χ]Γ `tm e : τΓ `co γ : τ ∼# ϕ
Γ `tm e . γ : ϕΓ `tm e : T κ σ
For each branch K x:τ → u(K:∀χ (a:ηa ).σ1 ∼# σ2 → τ → T χ a) ∈ Γ0
ϕi = τi [κ/χ][σ /a]ϕ1i = σ1i [κ/χ][σ /a]ϕ2i = σ2i [κ/χ][σ /a] Γ, c:ϕ1 ∼ ϕ2 x:ϕ `tm u : σKind variable
Type variable
Coercion variable
Term variable
Data type
Data constructor
Type families etc.

Figure 1: Syntax of System FC (excerpt)

3.1

EVAR

tm

Type constants
H
::=
|
|
Kinds
κ, η
::=
|
|

Γ0

(K:σ ) ∈ Γ0(x:τ) ∈ Γ

Γ `tm case e of K (c:σ1 ∼# σ2 ) (x:τ) → u : σ

ETA PP

EKA PPEC AST

EC ASE

Figure 2: Well-formed terms

values (∀a:η.ϕ) and the type of kind-polymorphic values (∀χ.τ).
The type constants H include data constructors (T ), and the function constructor (→) as well as the equality constructor (∼# ). The
well-formedness judgement for types appears in Figure 3.
What should the kind of ∼# be? We mentioned previously that wewould like to classify any type τ ∼# σ as having kind Constraint# ,but the kind of τ and σ can be any kind whatsoever. This indicatesthat ∼# should be given the polymorphic kind:∀χ.χ → χ → Constraint#This kind, made valid because the syntax of kinds κ includes kindpolymorphism, is recorded in the initial environment Γ0 (bottom of
Figure 1). Well-formedness of kinds (Γ `k κ), for this presentation,amounts to well-scoping, so we omit the details from Figure 3. As
a convention, we write τ ∼# ϕ to mean (∼# ) κ τ ϕ in the rest of
this paper, where the kind κ of τ and ϕ is clear from the context.
Finally, notice that well-formed arrow types1 are allowed to accept
an argument which is either Constraint# or ?, to account for coercion or term abstraction, but may only return ?, hence disallowing
any functions to return a value of type τ ∼# ϕ. However, as we will

Types, kinds, and kind polymorphism

The type language of System F↑C includes variables and constants,
type and kind application, as well as the type of type-polymorphic

1

For simplicity of presentation we do not include a binding for (→) in
the initial environment Γ0 , hence only allowing fully applied arrow types,
unlike Haskell.

The cast converts the type of the result from [Int ] to [a]2 . The
coercion sym [c] is evidence for (or a proof of) the equality of thesetypes, lifting c (of type a ∼# Int) over lists ([c], of type [a] ∼# [Int ]),before applying symmetry. We urge the reader to consult Sulzmann
et al. (2007) and Weirich et al. (2011) for more examples andintuition.

Γ `ty τ : κ(a : η) ∈ Γ(T : κ) ∈ Γ
TVAR

ty

Γ `ty T : κΓ` a:η

Γ `ty τ1 : κ1 Γ `ty τ2 : ?
κ1 ∈ {?,Constraint# }Γ `ty τ1 → τ2 : ?
Γ `ty τ1 : κ1 → κ2Γ `ty τ2 : κ1
Γ `ty τ1 τ2 : κ2
Γ, (a:η) `ty τ : ?
Γ `k η
ty

TA PP

TDATA

A final remark: we will be presenting and discussing a number ofF↑C programs in the rest of the paper. For readability purposes wewill sometimes omit type or kind applications in F↑C terms whenthese types or kinds are obvious from the context, making thesyntax appear less verbose.

TA RR

Γ `ty τ : ∀χ.κΓ `k η
Γ `ty τ η : κ[η/χ]TKA PP

4.
TA LL

Γ ` ∀a:η.τ : ?

Γ `ty ∀χ.τ : ?

TKA LLΓ `co γ : σ1 ∼# σ2...
Γ `k κ
...

Figure 3: Well-formed types and coercions
see in Section 4, a function can well return terms that contain such
coercions.
3.2

Two forms of equalityΓ, χ `ty τ : ?

F↑C datatypes with coercions

In F↑C , coercions can appear as arguments to data constructors,

a feature that is particularly useful for representing generalized
algebraic datatypes (GADTs) (Peyton Jones et al. 2006). Consider
this source Haskell program which defines and uses a GADT:
data T a whereT1 :: Int → T Int
T2 :: a → T af :: T a → [a]f (T1 x) = [x + 1]
f (T2 v) = [ ]main = f (T1 4)
In F↑C , we regard the GADT data constructor T1 as having the type:
T1 : ∀a . (a ∼# Int) → Int → T a
So T1 takes three arguments: a type argument to instantiate a, a
coercion witnessing the equality between a and Int, and a value oftype Int. Here is the F↑C version of main:
main = f Int (T1 Int hInti 4)
The coercion argument has kind Int ∼# Int, for which the evidence
is just hInti (reflexivity). Similarly, pattern-matching on T1 binds
two variables: a coercion variable, and a term variable. Here is theF↑C elaboration of function f :f = Λ(a : ?) . λ (x : T a) .
case x ofT1 (c : a ∼# Int) (n : Int)→ (Cons (n + 1) Nil) . sym [c]T2 v → Nil

In Section 2 we sketched how to use type-equality evidence to support deferred type errors, using σ ∼ τ as the type of equality evidence. Then in Section 3 we introduced our intermediate language,
System F↑C , in which explicit coercions of type σ ∼# τ represent evidence for the equality of two types. The distinction between (∼)
and (∼# ) is crucial: it allows us to to marry a sound, erasable language of proofs with the potentially-unsound ability to have terms
that compute proofs, as we discuss in this section.
4.1

The tension

Types have a very valuable property that programmers take for
granted: they give strong static guarantees, but they carry no runtime overhead. This zero-overhead guarantee is formally justified
by an erasure property: we can erase all the types before runningthe program, without changing the result.
Can we offer a similar guarantee for coercions? Yes, we can. System F↑C is carefully designed so that coercion abstractions, coercion
applications, and casts, are all statically erasable, just like type abstractions and applications.
But this statement is manifestly in tension with our approach todeferred type errors. Consider once more the F↑C termlet (c : Char ∼ Bool) = error "Couldn’t match..."in snd (True, (cast ’a’ c) && False)
Obviously we cannot erase the binding of c and the cast, leaving
snd (True, ’a’ && False), because the latter will crash. So it seems
that insisting on complete erasure of equalities kills the idea ofdeferring type errors stone dead!
4.2

The two equalities

We now present our resolution of this tension. We have carefully
maintained a distinction between• (∼# ), the type of primitive coercions γ in F↑C , which are fully

erasable, and• (∼), type of evidence generated by the type inference engine,which cannot be erased.
However (∼) is not some magical built-in device. Rather, we candefine it as a perfectly ordinary GADT (like the one we havealready seen in Section 3.2), thus:
data a ∼ b whereEq# :: (a ∼# b) → a ∼ b
2 We informally use Haskell’s notation [τ ] for the type list of τ, and Consand Nil as its constructors.

This definition introduces a new algebraic data type constructor(∼), belonging in the T syntactic category of Figure 1. It hasexactly one data constructor Eq# , whose (important) argument isa static equality proof. Readers familiar with proof assistants ortype theory will immediately recognize in the definition of (∼) thetype used traditionally in such systems to internalize definitional
equality as a type (e.g. refl_equal in Coq).
Like (∼# ), the data type (∼) is polymorphically kinded:∼ : ∀χ . χ → χ → ?
Eq# : ∀χ . ∀(a : χ) (b : χ) . (a ∼# b) → (a ∼ b)

5.

With F↑C in hand we can now explain in more detail the mechanismof deferring type errors. We begin by sketching a little more about
the type inference process.
5.1

cast : ∀(a b : ?) . a → (a ∼ b) → b
cast = Λ(a b : ?) . λ (x : a) . λ (eq : a ∼ b) .
case eq of Eq# (c : a ∼# b) → x . c
Each use of cast forces evaluation of the coercion, via the case
expression and, in the case of a deferred type error, that is what
triggers the runtime failure.
Just as cast is a lifted version of ., we can lift all the coercion
combinators from the (∼# ) type to (∼). For example:
mkRefl :: ∀χ . ∀(a : χ) . a ∼ a
mkRefl = Λχ . Λ(a : χ) . Eq# χ a a hai
mkSym :: ∀χ . ∀(a b : χ) . (a ∼ b) → (b ∼ a)mkSym = Λχ . Λ(a b : χ) . λ (c : a ∼ b) .
case c of Eq# c → Eq# χ b a (sym c)
The relationship between (∼) and (∼# ) is closely analogous to thatbetween Int and Int# , described twenty years ago in our implementation of arithmetic in GHC (Peyton Jones and Launchbury 1991).
Concretely, here is GHC’s implementation of addition on Int:
data Int = I# Int#
plusInt :: Int → Int → Int
plusInt x y = case x of I# x0 →case y of I# y0 → I# (x0 +# y0 )An Int is an ordinary algebraic data type with a single constructor
I# (the ‘#’ is not special; it is just part of the constructor name). This
constructor has a single argument, of type Int# , which is the typeof unboxed integers, a honest-to-goodness 32-bit integer value justlike C’s int. Finally (+# ) is the machine 32-bit addition instruction.
We may summarise the relationships thus:• A value of type Int, or σ ∼ τ, is always heap-allocated; it isalways represented by a pointer to the heap-allocated object;
and the object can be a thunk.
• A value of type Int# , or σ ∼# τ is never heap-allocated; and it

cannot be a thunk. There is no bottom value of type Int# , orσ ∼# τ; we say that they are unlifted types.
• The plusInt function lifts the primitive addition +# from Int#

to Int, by explicitly evaluating and unboxing its arguments; andthe function mkSym works in just the same way.
The main difference between Int# and a ∼# b is that the fomer
is represented by a 32-bit unboxed value, whereas the latter has
a structure that is irrelevant for the execution of a program, and canbe represented by a zero-bit value, or entirely erased — it comes tothe same thing in the end.

Type inference by constraint generation

GHC’s type inference algorithm works in two stages (Vytiniotis
et al. 2011):• Step 1: traverse the syntax tree of the input Haskell term, gen-erating type constraints together with an elaborated term3 in
System F↑C .

As with τ ∼# σ we usually omit the kind application in τ ∼ σ as asyntactic convenience.
The key point is that if γ : σ ∼# τ, then a value Eq# γ is an
ordinary term, built with the data constructor Eq# , and having typeσ ∼ τ. Given the GADT (∼) we can define the function cast thattakes such a term-level equality witness and casts a value between
equivalent types:

Type inference and deferral of type errors• Step 2: solve the constraints, creating F↑C bindings that give

evidence for the solution.

For example, consider the term show xs, where xs : [Int ], andshow : ∀a . Show a ⇒ a → String. In Step 1 we generate:
Elaborated term:
Constraint:

show [Int ] d6 xs
d6 : Show [Int ]The elaborated term looks much like the original except that show
is now applied to a type argument [Int ] (corresponding to the “∀a”
in show’s type) and an evidence argument d6 (corresponding to the“Show a ⇒” in its type). The constraint is given a fresh name,d6 in this example, which is mentioned in the elaborated term.
Afficionados of Haskell’s type-class system will recognise d6 asshow’s dictionary argument: it is simply a tuple of functions, themethods of the Show class.
When Step 1 is complete, the constraint solver solves the generated
constraints, producing evidence bindings:
d6 : Show [Int ] = $dShowList Int $dShowInt
Here the solver has constructed a dictionary for Show [Int ], using
the dictionary-construction functions that arise from the instancedeclarations of the class Show:$dShowInt : Show Int$dShowList : ∀a . Show a → Show [a]Finally, the evidence bindings are wrapped around the term in a let
to make an executable term:
let d6 = $dShowList Int $dShowInt
in show [Int ] d6 xs
5.2

Equality constraints

This is all quite conventional. Somewhat less conventionally (butfollowing the French school of type inference (Pottier and Rémy2005)) GHC generates equality constraints as well as type-classconstraints. We simplified the show example; in reality GHC generates the following:
Elaborated term:
Constraints:

show α d6 (cast xs c5 )d6 : Show α
c5 : [Int ] ∼ αWhen instantiating show’s type in Step 1, the constraint generator
does not yet know that it will be applied to the type [Int ], so
instead it creates a fresh unification variable α, and uses that toinstantiate show’s type. Later, when checking show’s argument x, it
must ensure that show’s argument type α is equal to the actual typeof xs, namely [Int ]. It ensures this (eventual) equality by generating
3 In reality we first generate an elaborated term by decorating the Haskell

source term, and then desugar it, but we will ignore that extra step here.

an equality constraint c5 : [Int ] ∼ α, again with an arbitrary freshname c5 which names the evidence for the equality. Lastly, inthe elaborated term, we use the cast term cast xs c5 to convert
xs into a term of type α. Notice that c5 ’s type [Int ] ∼ α uses
the boxed equality (∼) rather than the primitive F↑C equality (∼# )(Section 4.2).

• The technique makes elegant use of laziness. In a call-by-value

language, a strict binding of c in Section 2.1 would be evaluatedby the call fst foo, or even when foo is bound, and it would obviate the entire exercise if that evaluation triggered the runtime
error! Nevertheless, the idea can readily be adapted for call-byvalue, by simply making (∼) into a sum type:
data a ∼ b whereEq# :: (a ∼# b) → a ∼ b
Error :: String → a ∼ b

In Step 2, the constraint solver has a little extra work to do: as well
as solving the constraints and giving bindings for the evidence variables, it must also produce bindings for the unification variables. In
our running example, the solution to the constraints looks like this:αc5 : [Int ] ∼ αd6 : Show [Int ]===The solver decided to eliminate α by substituting [Int ] for α,
the first of the above bindings. The equality c5 now witnesses
the vacuous equality [Int ] ∼ [Int ], but it must still be given abinding, here mkRefl [Int ]. (Recall that mkRefl was introduced in
Section 4.2.)
Actually, as a matter of efficiency, in our real implementation theconstraint generator solves many simple and immediately-soluble
equalities (such as α ∼ [Int ]) “on the fly” using a standard unification algorithm, rather than generating an equality constraint to besolved later. But that is a mere implementation matter; the implementation remains faithful to the semantics of generate-and-solve.
Moreover, it certainly cannot solve all equalities in this way, because of GADTs and type families (Vytiniotis et al. 2011).
5.3

Now, the “evidence” for an erroneous type constraint would be
an Error value, and evaluating that is fine. We simply need toadjust cast to deal with the Error case:[Int ]
mkRefl [Int ]$dShowList Int $dShowInt

cast = Λ(a b : ?) . λ (x : a) . λ (eq : a ∼ b) .
case eq of
Eq# (c : a ∼# b) → x . cError s → error s• The technique works uniformly for all type constraints, notonly for equality ones. For example, in Section 5.1, suppose
there was no instance for Show [Int ]. Then the constraint d6 :Show [Int ] would be insoluble, so again we can simply emit awarning and bind d6 to an error thunk. Any program that needs
the evidence for d6 will now fail; those that don’t, won’t.
• We can defer all type errors in terms, but not kind errors intypes. For example, consider
data T = MkT (Int Int)f (MkT x) = x

Deferring type errors made easy

In a system generating equality proofs using the (∼) datatype,which has values that can be inhabited by ordinary terms, it is delightfully easy to support deferred type errors. During constraint
generation, we generate a type-equality constraint even for unifications that are manifestly insoluble. During constraint solving, instead of emitting an error message when we encounter an insoluble constraint, we emit a warning, and create a value binding forthe constraint variable, which binds it to a call to error, applied tothe error message string that would otherwise have been emitted atcompile time. And that’s all there is to it.
It is worth noting several features of this implementation technique:• Each F↑C term given above is a well-typed F↑C term, even thoughsome are generated from a type-incorrect Haskell term. Of
course it can fail at run-time, but it does so in a civilized way,by raising an exception, not by causing a segmentation fault,
or performing (&&) of a character and a boolean. You might
consider that a program that fails at runtime in this way is not
well-typed, in Milner’s sense of “well typed programs do notgo wrong”. But Haskell programs can already “go wrong” inthis way — consider (head [ ]) for example — so matters arecertainly no worse than in the base language.
In short, we have merely deferred the type errors to runtime; wehave not ignored them!

• Deferring type errors is not restricted to interpreted expressions

typed at the interactive GHCi prompt. You can compile any
module with -fdefer-type-errors and GHC will produce
a compiled binary, which can be linked and run.
• There is no reflection involved, nor run-time type checking.

Indeed there is no runtime overhead whatsoever: the programruns at full speed unless it reaches the point where a runtime
error is signalled, in which case it halts. (This claim assumes
the optimisations described in Section 7.)

The type Int Int simply does not make sense – applying Int to
Int is a kind error, and we do not have a convenient way to deferkind errors, only type errors.
5.4

The placement of errors

Since many different parts of a program may contribute to a typeerror, there may be some non-determinism about how delayed adeferred type error will be. Suppose that upper : [Char ] → [Char ],and consider the term:
upper [True, ’a’]
There are two type incompatibilities here. First, the boolean Trueand character ’a’ cannot be in the same list. Second, the function
upper expects a list of characters but is given a list with a boolean
in it. Here is one possible elaboration:
Elaborated term:
Constraints:

upper [cast True c7 , ’a’]
c7 : Bool ∼ Char

But the program could also be elaborated in another way:
Elaborated term:
Constraints:

upper (cast [True, cast ’a’ c8 ] c9 )c8 : Char ∼ Boolc9 : [Bool] ∼ [Char ]In this case, type inference has cast ’a’ to Bool using c8 , so that it
can join True to form a list of Bool; and then cast the list [Bool]
to [Char ] using c9 to make it compatible with upper. The two
elaborated programs have slightly different runtime behaviour. If
the term is bound to tm, then head (tail tm) will run successfully(returning ’A’) in the first elaboration, but fail with a runtime error
in the second.
We might hope that the type inference engine inserts as few casts as
possible, and that it does so as near to the usage site as possible. Infact this turns out to be the case, because the type inference engine

uses the (known) type of upper to type-check its argument, expecting the result to be of type [Char ]. This idea of “pushing down” theexpected type into an expression, sometimes called bidirectionalor local type inference (Pierce and Turner 2000), is already implemented in GHC to improve the quality of error messages; see
Peyton Jones et al. (2007, Section 5.4) for details. Although it is aheuristic, and not a formal guarantee, the mechanism localises thecasts very nicely in practice.
Nevertheless, the bottom line is that the dynamic semantics of a
type-incorrect program depends on hard-to-specify implementation
details of the type inference algorithm. That sounds bad! But wefeel quite relaxed about it:• The issue arises only for programs that contain errors. Typecorrect programs have their usually fully-specified semantics.

are treated uniformly with type-class constraints and implicitparameter constraints; anywhere a class constraint can appear,
an equality constraint can appear, and vice versa. Class constraints
and implicit-parameter constraints definitely cannot be erased: bydesign their evidence carries a runtime value. Treating some constraints as non-erasable values and others (the equalities) as typelike, erasable constructs, led to many annoying special cases in thetype inference and source-to-F↑C elaboration of Haskell programs.
The most troublesome example of this non-uniformity arises whentreating Haskell’s superclasses. Consider the declaration
class (a ∼ F b, Eq a) ⇒ C a b where . . .
Here Eq a is a superclass of C a b, meaning that from evidence forC a b one can extract evidence for Eq a. Concretely this extraction
is witnessed by a field selector:• Regardless of the precise placement of coercions, the elaborated

sc2 : C a b → Eq aprogram is type correct. This is not a soundness issue.
• The imprecision of dynamic semantics is no greater a short-coming than the lack of a formal specification of the precise
type error message(s) produced by a conventional type inference engine for a type-incorrect program. And yet no compiler
or paper known to us gives a formal specification of what typeerrors are produced for a type-incorrect program.
That said, it is interesting to reflect on approaches that might tighten
up the specification, and we do so in Section 9.
5.5

Summary

There are many reasons why evidence-based type elaboration, using constraint generation and subsequent constraint solving, is desirable (Vytiniotis et al. 2011):

which takes a dictionary (i.e. record of values) for C a b and picks
out the Eq a field. In just the same way one should be able to extractevidence for a ∼ F b, which suggests a selector function with typesc1 : C a b → (a ∼ F b)
Before we distinguished (∼) and (∼# ) we could not write thisfunction because there simply is no such function in F↑C ; indeed
the type C a b → (a ∼# F b) is not even well kinded in Figure 3.
There is a good reason for this: dictionaries can be recursively
defined and can diverge (Lämmel and Peyton Jones 2005), so theselector function may diverge when evaluating its arguments – but
the type a ∼# F b cannot represent divergence, because that would
be unsound.
The tension is readily resolved by (∼); the type of sc1 is wellformed and its definition looks something like this:• It is expressive, readily accommodating Haskell’s type classes,

sc1 = Λab . λ (d : C a b) .
case d ofMkC (c : a ∼# F b) (eq : Eq a) . . . → Eq# c

implicit parameters, and type families.
• It is modular. The constraint generator accepts a very large in-put language (all of Haskell), so it has many cases, but eachcase is very simple. In contrast, the constraint solver accepts avery small input language (the syntax of constraints) but embodies a complex solving algorithm. Keeping the two separate
is incredibly wonderful.
• It is robust: for example it does not matter whether the con-straint generator traverses the term left-to-right or right-to-left:
the resulting constraint is the same either way.
• Neither the constraint generator nor the solver need be trusted; avery simple, independent checker can type-check the elaborated
F↑C term.
To this list we can now add a completely new merit: it is dead easy
to implement deferred type errors, a feature that is desired by many
Haskell programmers.

6.

Discussion

Now that we have discussed type inference in more detail, we pause
to reflect on our design choices.
6.1

Evidence uniformity

We’ve seen that deferring type errors provides a good motivation
for treating coercions as term-level constructs. But there is anotherway in which treating coercions as values turns out to be very
convenient. In the Haskell source language, equality constraints

This accumulation of infelicities led us to the two-equality plan,and in fact we had fully implemented this design even before weever thought of deferring type errors. Now, we get the ability todefer errors regarding type unification, missing class constraints,
and implicit parameters, all in one go.
6.2

Why kind polymorphism is important

We have mentioned that both equalities (∼# ) and (∼) are kindpolymorphic, but we have not yet said why. Right from the beginning Haskell has featured kinds other than ?, such as ? → ?. During
type inference, when unifying, say, α β ∼ Maybe Int, the inferenceengine — or, more precisely, the constraint solver — must decompose the equality to give α ∼ Maybe and β ∼ Int. The former equality is at kind ? → ?, so it follows that the (∼) type constructor itself
must be either (a) magically built in or (b) poly-kinded. And similarly (∼# ).
Solution (a) is entirely possible: we could add σ ∼ τ and σ ∼# τ tothe syntax of types, and give them their own kinding rules. But there
are unpleasant knock-on effects. The optimizer would need to betaught how to optimize terms involving (∼). Worse, it turns out that
we need equalities between equalities, thus (σ1 ∼ τ1 ) ∼ (σ2 ∼ τ2 ),which in turn leads to the need for new coercion combinators todecompose such types.
Happily there are many other reasons for wanting kind polymorphism in F↑C (Yorgey et al. 2012), and once we have kind polymorphism we can readily make the equality type constructors kindpolymorphic.

6.3

let (c : Char ∼ Bool) = error "Couldn’t match..."in snd (True, (cast ’a’ c) && False)

What the Haskell programmer sees

A salient feature of Haskell’s qualified types (type classes, implicit
parameters, equality constraints) is that the type inference engine
fills in the missing evidence parameters. So if f has typeNow, simply by inlining cast and c, the optimizer can transform tosnd (True, (case error "..." of {Eq# c → ’a’ . c})&& False)

f :: (Num b, a ∼ F b) ⇒ a → b → bthen given a source-language call (f e1 e2 ), the type inference will
generate the elaborated call (f σ τ d c e1 e2 ), where σ and τ are thetypes that instantiate a and b, and d and c are evidence terms thatwitness that Num τ holds and that σ ∼ F τ, respectively.
One might wonder whether one can (in Haskell) also write
g :: (a ∼# F b) ⇒ a → b → b

After inlining (&&), and simplifying case-of-error to just a call oferror, both standard transformations in GHC’s optimizer) we get
snd (True, error "...")
Even erroneous programs are optimized by removing their deadcode! The point is this: by exposing the evaluation of coercions, weallow the existing optimizer transformations to work their magic.

and have the above evidence-generation behaviour. No, you cannot.
The whole point of the (∼) type is that it can be treated uniformly
with other evidence (bound in letrec, returned as a result of a call),whereas (∼# ) cannot. So in the source language σ ∼# τ is not a type
constraint you can write before the “⇒” in a Haskell type, and haveit participate in constraint solving. The entire constraint generationand solving process works exclusively with well-behaved, uniform,
boxed constraints. Only when constraint solving is complete does(∼# ) enter the picture, as we discuss next.

7.2

7.

That is true in System F↑C . But the Haskell programmer, who knows
only of the type σ ∼ τ, considers T1 to have this type:

Optimizing equalities

We now have a correct implementation, but it looks worryingly
expensive. After all, the constraint generation/solving process may
generate a program littered with coercion bindings and casts, allof which are invisible to the programmer, have no operationalsignificance, and merely ensure that “well typed programs don’t
go wrong”. Yet each will generate a heap-allocated Eq# box, readyto be evaluated by cast. Happily, almost all of these boxes are
eliminated by existing optimizations within GHC, as this section
describes.
7.1

Eliminating redundant boxing and unboxing

The fact that we have defined (∼) as an ordinary GADT meansthat is fully exposed to GHC’s optimizer. Consider a Haskell 98
program that turns out to be well typed. The constraint generator
will produce many constraints that are ultimately solved by reflexivity, because the two types really are equal. Here is a typical caseof an elaborated term:let (c : Char ∼ Char) = mkRefl Charin . . . (cast e c) . . .
(Recall that mkRefl and cast were defined in Section 4.2.) As it
stands, the let will heap-allocate a thunk which, when evaluated by
the cast, will turn out to be an Eq# constructor wrapping a reflexive
coercion hChari. All this is wasted work. But GHC’s optimizer caninline the definitions of mkRefl and cast from Section 4.2 to getlet (c : Char ∼ Char) = Eq# ? Char Char hChariin . . . (case c of Eq# c0 → e . c0 ) . . .
Now it can inline c at its use site, and eliminate the case expression,
giving. . . (e . hChari) . . .
Remembering that primitive casts (.) can be erased, we have eliminated the overhead. Moreover, the optimizations involved have all
been in GHC for years; there is no new special purpose magic.
What happens when a deferred type error means that a cast cannot,
and should not, be erased? Consider once more the F↑C term

Equalities and GADTs

Let us reconsider the GADT example given in Section 3.2:
data T a whereT1 :: Int → T Int
T2 :: a → T a
There we said that the constructor T1 is typed thus:
T1 : ∀a . (a ∼# Int) → Int → T a

T1 :: ∀a . (a ∼ Int) → Int → T a
It would be perfectly sound to adopt the latter type for T1 inthe elaborated program; for example, function f from Section 3.2
would be elaborated thus:
f = Λa . λ (x : T a) .
case x ofT1 (c : a ∼ Int) (n : Int)→ cast (Cons (n + 1) Nil) (mkSym [c])T2 v → Nil
Since an argument of type a ∼ Int has a lifted type with a boxed
representation, it would take up a whole word in every T1 object.
Moreover, since c is bound by the pattern match, the case expression in mkSym will not cancel with an Eq# box in the binding for c.
This is not good! What has become of our zero-overhead solution?
The solution is simple: we desugar GADTs to contain unlifted,
rather than lifted, equalities. We can do this in such a way thatthe Haskell programmer still sees only the nice well-behaved (∼)
types, as follows. First, in the elaborated program the type of T1 is:T1 : ∀a . (a ∼# Int) → Int → T a
However, the elaborator replaces every source-language call of T1
with a call of a constructor wrapper function, T1wrap, defined likethis:
T1wrap : ∀a . (a ∼ Int) → Int → T a
T1wrap = Λ(a : ?) . λ (c : a ∼ Int) . λ (n : Int) .
case c of Eq# c1 → T1 c1 n
The wrapper deconstructs the evidence and puts the payload into
T1 where, since it is erasable, it takes no space.
Dually, a source-program pattern match is elaborated into a F↑Cpattern match together with code to re-box the coercion. So ourfunction f is elaborated thus:
f = Λa . λ (x : T a) .
case x ofT1 (c1 : a ∼# Int) (n : Int)f : ∀a . F a ∼ Int → [F a] → Int
f = Λa . λ (c : F a ∼ Int) . λ (x : [F a]) .
case c of Eq# c0 → fwrk c0 x
fwrk : ∀a . F a ∼# Int → [F a] → Int
fwrk = Λa . λ (c0 : F a ∼# Int) . λ (x : [F a]) .
let c = Eq# c0 in head (cast x c) + 1→ let c = Eq# c1 -- Re-boxingin cast (Cons (n + 1) Nil) (mkSym [c])T2 v → Nil
Now the earlier optimizations will get rid of all the boxing and unboxing and we are back to nice, efficient code. The technique of unboxing strict arguments on construction, and re-boxing on patternmatching (in the expectation that the re-boxing will be optimizedaway) is precisely what GHC’s UNPACK pragma on constructor arguments does. So, once more, coercions can hitch a free ride onsome existing machinery.
7.3

How much is optimized away?

We have argued that the boxing and unboxing, introduced in theelaborated program by the type checker, will largely be eliminatedby standard optimizations. But not always! Indeed that is the point:
the main reason for going to all of this trouble is to handle smoothly
the cases (deferred type errors, recursive dictionaries) when equalities cannot, and should not, be erased. But still, one might reasonably ask, can we offer any guarantees at all?
Consider a type-correct Haskell program that contains (a) no equality superclasses, and (b) no functions that take or return a valueof type σ ∼ τ, apart from GADT constructors. This includes all
Haskell 98 programs, and all GADT programs. After typechecking
and elaboration to F↑C , suppose that we inline every use of mkRefl,
mkSym, etc, and the GADT constructor wrappers. Then
• Every use of a variable of type σ ∼ τ will be a case expressionthat scrutinises that variable, namely the unboxing case expressions in mkRefl, mkSym, etc, and GADT constructor wrappers.
• Every binding of an evidence variable of type σ ∼ τ will be alet whose right hand side returns a statically-visible Eq# box.
By inlining these let-bound evidence variables at their use sites, we
can cancel the case with the Eq# constructors, thereby eliminating
all boxing and unboxing. To illustrate, consider once more theelaboration of function f at the end of the previous subsection. If
we inline mkSym and cast we obtain:f = Λa . λ (x : T a) .
case x ofT1 (c1 : a ∼# Int) (n : Int)→ let c = Eq# c1 in -- Re-boxing
let c2 = case c of Eq# c0 → Eq# (sym [c0 ])in case c2 ofEq# c02 → Cons (n + 1) Nil . c02
T2 v → Nil
The right hand side of c2 comes from inlining mkSym, while the“case c2 . . .” comes from inlining cast. Now we can inline c in“case c . . .”, and c2 in “case c2 . . .”, after which the cancellationof boxing and unboxing is immediate.
When does this not work? Consider exception (b) above, where a
programmer writes a function that is explicitly abstracted over an
equality:f : ∀a . F a ∼ Int ⇒ [F a] → Int
f x = head x + 1
The elaborated form will look like this:f : ∀a . F a ∼ Int → [F a] → Int
f = Λa . λ (c : F a ∼ Int) . λ (x : [F a]) .
head (cast x c) + 1
Since c is lambda-bound, there is no Eq# box for the cast to cancel
with. However we can perform the same worker/wrapper split tothis user-defined function that we did for constructors, thus

Now in fwrk the boxing and unboxing cancels; and dually we arefree to inline the wrapper function f at its call sites, where theunboxing will cancel with the construction. This worker/wrapper
mechanism is precisely what GHC already implements to eliminate
boxing overheads on strict function arguments (Peyton Jones andSantos 1998), so it too comes for free. There is a small price to pay,
however: the transformation makes the function strict in its equality
evidence, and that in turn might trigger a deferred error message
slightly earlier than strictly necessary. In our view this is a trade-off
worth making. In our current implementation the worker/wrapper
transform on equalities is only applied when the function reallyis strict in the equality; we have not yet added the refinement ofmaking it strict in all equalities.
7.4

Summary

In short, although we do not give a formal theorem (which would
involve formalizing GHC’s optimizer) we have solid grounds,
backed by observation of optimized code, for stating that the uniform representation of equality evidence can be successfully optimized away in all but the cases in which it cannot and should not be
eliminated, namely for deferred type errors and functions that must
accept or return term-level equalities (such as selectors for equality
superclasses). Of course, introducing and then eliminating all theseboxes does mean a lot more work for the compiler, but this has notproved to be a problem in practice.

8.

Related work

8.1

Relation to hybrid and gradual typing

Hybrid type checking (Flanagan 2006) refers to the idea of deferring statically unproved goals as runtime checks. Achieving similar effects, but arriving from the opposite end of the spectrum softtyping tries to elimiminate statically as many runtime checks as
possible (Wright and Cartwright 1997). There are two differencescompared to our approach: First, in hybrid type checking typically
only unsolved goals will be deferred whereas insoluble ones will bereported statically. In our case, insoluble and unsolved goals will bedeferred. Second, unsolved goals will be deferred as checks in hybrid type systems, whereas they will remain errors in our system:
Our treatment of coercions does not replace static type errors byruntime checks, but rather delays triggering a static error until theoffending part of the program is evaluated, at runtime. For instance,
consider the following program, which contains a static error but iscompiled with -fdefer-type-errors:
f :: ∀a . a → a → a
f x y = x && y
There is a static error in this program because f is supposed to
be polymorphic in the type of its arguments x and y, which arenevertheless treated as having type Bool. At runtime, even if we
evaluate the application of f on arguments of type Bool, such asf True False we will get a type error “Couldn’t match type a with
Bool”, despite the fact that the arguments of f are of type Bool at
runtime. In contrast, a truly dynamic type-check would not trigger
a runtime error.

In the context of GHC, there is no straightforward way to incorporate runtime checks instead of error triggers at runtime, unlessdynamic type information is passed along with polymorphic types.
Though systems with dynamic types and coercions have been studied in the literature (Henglein 1994), we have not examined thispossibility.
There is a large body of work on interoperating statically and dynamically typed parts of a program, often referred to as gradualtyping (Ahmed et al. 2011; Siek and Taha 2006; Siek and Vachharajani 2008; Tobin-Hochstadt and Felleisen 2006). Typically, statically insoluble goals will be reported statically (Siek and Taha
2006), whereas insoluble goals which perhaps arise from the potential interoperation of dynamic and static parts of the program
will be wrapped with runtime checks. The main problem in gradual typing is to identify how to assign blame in case of a contract
violation (or a dynamic type error). We have seen in Section 5.3
that non-determinism in the dynamic placement of the type error
may well exist. Consequently it might be an interesting avenue toexplore if ideas from gradual typing could help us specify a morepredictable “blame assignment” for these deferred type errors. Note
finally that previous work on type error slicing (Haack and Wells
2004) has focused on identifying parts of a program that contributeto a type error and would be potentially useful for reducing thisnon-determinism both for static error messages and for better specifying the dynamic behaviour of an erroneous program.
8.2

Deferring type errors

DuctileJ is a plugin to the Java compiler that converts a normal Java
program to one in which type checking is deferred until runtime(Bayne et al. 2011). The authors provide an extensive discussion of
the software engineering advantages of deferring type errors, under
two main headings.
• During prototyping, programmers often comment out partly
written or temporarily out-of-date code, while prototyping
some new part. Commenting out is tiresome because one must
do it consistently: if you comment out f you must comment out
everything that calls f , and so on. Deferring type errors is a kindof lazy commenting-out process.
• During software evolution of a working system it can be burden-some to maintain global static type correctness. It may be moreproductive to explore a refactoring, or change of data representation, in part of a software system, and test that part, withoutcommitting to propagating the change globally.
We urge the reader to consult this excellent paper for a full exposition, and a good evaluation of the practical utility of deferring typeerrors both during prototyping and for software evolution.
Note however that although our motivations are similar, our implementation differs radically from that in DuctileJ. The latter works
by a “de-typing” transformation that uses Java’s runtime type information and reflection mechanisms to support runtime type checks.
This imposes a significant runtime cost – the paper reports a slowdown between 1.1 and 7.8 times. In contrast, our implementation
performs no runtime reflection and runs at full speed until the typeerror itself is encountered. The DuctileJ de-typing transformation is
also not entirely faithful to the original semantics — unsurprisingly,
the differences involve reflection — whereas ours is fully faithful,even for programs that involve Haskell’s equivalent of reflection,
the Typeable and Data classes. To be fair, many of the DuctileJcomplexities go away because Haskell is a simpler language thanJava. Further, GHC already implemented (the quite advance features of) kind polymorphism, coercions, and unboxing, which allowed us to piggyback -fdefer-type-errors onto the existing
compiler implementation with very little effort.

Deferring type errors is also a valuable tool in the context of IDE
development. In an IDE it is essential to provide feedback to theprogrammer even if the program has errors. The Visual Basic IDE
uses a hierarchy of analysis to provide gradually more functionality
depending on the type of errors present (Gertz 2005). For instance,
if there are type errors, but no parse errors, smart indentation andautomatic code pretty-printing can already be applied. However,more complicated refactorings require type information to be available. Some IDEs use error-correcting parsers to be able to provide
some functionality in the presence of parsing errors, but a type error
will require a correction by the user before the IDE can offer functionality that depends on the availability of types. Deferring typeerrors allows the compiler to complete type checking without fixing the type errors, allowing for a Haskell IDE to remain functional
even for programs that do not type-check.
8.3

Proof erasure

Coq (The Coq Team) uses a sort-based erasure process by introducing a special universe for propositions, Prop, which is analogous to
our Constraint# kind. Terms whose type lives in Prop are erased
even when they are applications of functions (lemmas) to computational terms. This is sound in Coq, since the computation language
is also strongly normalizing. Extending the computation languageof F↑C proofs or finding a way to restrict the ordinary computation
language of F↑C using kinds in order to allow it to construct primitive equalities is an interesting direction towards true dependent
types for Haskell.
Irrelevance-based erasure is another methodology proposed in thecontext of pure type systems and type theory. In the context of Epigram, Brady et al. (2003) presented an erasure technique where
term-level indices of inductive types can be erased even when they
are deconstructed inside the body of a function, since values of theindexed inductive datatype will be simultaneously deconstructedand hence the indices are irrelevant for the computation. In the
Agda language (Norell 2007) there exist plans to adopt a similar
irrelevance-based erasure strategy. Other related work (Abel 2011;
Mishra-Linger and Sheard 2008) proposes erasure in the context
of PTSs guided with lightweight programmer annotations. Therealso exist approaches that lie in between sort-based erasure andirrelevance-based erasure: for instance, in implicit calculus of constructions (Miquel 2001) explicitly marked static information (notnecessarily Prop-bound) does not affect computation and can beerased (Barras and Bernardo 2008). In F↑C the result of a computation cannot depend on the structure of an equality proof, by construction: there is no mechanism to decompose the structure of acoercion at all at the term-level. Hence a coercion value needs no
structure (since it cannot be decomposed), which allows us to perform full erasure without any form of irrelevance analysis.
This idea – of separating the “computational part” of a proof-likeobject, which always has to run before we get to a zero-cost “logical part” – is reminiscent of a similar separation that A-normal
forms introduce in refinement type systems, for instance (Bengtson et al. 2008) or the more recent work on value-dependent
types (Borgstrom et al. 2011; Swamy et al. 2011). This line of work
seems the closest in spirit to ours, with similar erasure concerns,
and there is rapidly growing evidence of the real-world potentialof these ideas – see for instance the discussion and applications
reported by Swamy et al. (2011).

9.

Future work and conclusions

Error coercion placement This paper has been about an implementation technique that uses first-class proof-like objects to al-low for deferred type errors with very low overhead. A natural next
step would be towards a declarative specification of the “elaboration” process from source to a target language which specifies theplacement of the deferred error messages on potentially erroneous
sub-terms. Recent related work on coercion placement in the context of coercive subtyping is the work of Luo (2008) and Swamy
et al. (2009); these would certainly be good starting points for investigations on a declarative specification of deferring type errors.
The canonical reference for coercion placement in a calculus with
type-dynamic is the work of Henglein (1994), but it seems somewhat disconnected from our problem as we do not have currently
any way of dynamically passing type information or executing programs that contain static errors but are safe dynamically.
In general, this problem seems very hard to tackle without exposing some of the operation of the underlying constraint solver.
In the other direction, a principled approach to deferring type errors might actually provide guidance on the order in which constraints should be solved. For instance, when solving the constraints
C1 ∪C2 ∪C3 arising from the expressions e1 , e2 , and e3 in the term
if e1 then e2 else e3 , we might want to prioritise solving the constraint C1 . In this way, if an error is caused by the interaction of theexpressions e2 or e3 with e1 , we would still be able to execute thecondition of the branch e1 before we emit a deferred type error for
e2 or e3 . Otherwise we run the danger of the term e2 or e3 forcing
some unification that makes constraint C1 insoluble, giving rise toan earlier error message (during evaluation of the condition terme1 ). However, it is not clear what should happen when C2 and C3
have a common unification variable, and there is freedom in deferring either one, for instance. Therefore this problem is certainly
worth further investigation.

The equality type Internalizing definitional equality (∼# ) as a
type (∼) is pretty standard in languages with dependent types (Licata and Harper 2005). For example, programming with first-classequality witnesses is sometimes convenient to avoid shortcomingsof implementations of dependent pattern matching.
Recent work on higher-dimensional type theory (Licata and Harper2012) goes one step further to show that the (∼) datatype can beextended with yet another constructor for term-level isomorphisms
between types. Interestingly the usual definitional equality inference rules apply for this extended equality type. Moreover theyshow that the term language can be equipped with an equational
theory that is rich enough, so that types enjoy canonical forms. Of
course the language they address is simpler in some respects (nopartiality or divergence, no polymorphism), nor is there a reduction
semantics. In a real compiler, being able to extend the (∼) datatypewith true computational isomorphisms and maintain soundness andproviding a transparent treatment of these isomorphisms with minimal programmer intervention is an interesting direction for future
research.

Conclusions In this paper we have proposed a simple and lightweight mechanism for deferring type errors, in a type-safe way that
requires no program rewriting, and preserves the semantics of the
program until execution reaches the part that contains a type error.
We have shown that this can be done in an entirely safe way in thecontext of a typed intermediate language, and in fact without requiring any modifications to System F↑C or the compiler optimizer.
This work is fully implemented in GHC, where it has in addition
greatly simplified the implementation of type inference and elaboration of Haskell to F↑C .

Acknowledgments
Particular thanks are due to Etienne Laurin, who suggested to us
the idea of deferring type errors (GHC Trac ticket 5624), although
his implementation was very different to the one described here.
We thank Stephanie Weirich and Brent Yorgey for their detailed
comments and suggestions, and the ICFP reviewers for the helpful
feedback.
This work has been partially funded by the Portuguese Foundationfor Science and Technology (FCT) via the SFRH/BD/35999/2007
grant, and by EPSRC grant number EP/J010995/1.

References
Andreas Abel. Irrelevance in type theory with a heterogeneous equality
judgement. In Foundations of Software Science and Computational
Structures, 14th International Conference, FOSSACS 2011, pages 57–
71. Springer, 2011.
Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler.
Blame for all. In Proceedings of the 38th annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL
’11, pages 201–214, New York, NY, USA, 2011. ACM. ISBN 978-14503-0490-0. doi: 10.1145/1926385.1926409.
Bruno Barras and Bruno Bernardo. The implicit calculus of constructions
as a programming language with dependent types. In Foundations ofSoftware Science and Computation Structure, pages 365–379, 2008. doi:
10.1007/978-3-540-78499-9 26.
Michael Bayne, Richard Cook, and Michael Ernst. Always-available staticand dynamic feedback. In Proceedings of 33rd International Conference
on Software Engineering (ICSE’11), pages 521–530, Hawaii, 2011.
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. Refinement types for secure implementations.
In Proceedings of the 2008 21st IEEE Computer Security Foundations
Symposium, pages 17–32, Washington, DC, USA, 2008. IEEE Computer
Society. ISBN 978-0-7695-3182-3.
Johannes Borgstrom, Juan Chen, and Nikhil Swamy. Verifying statefulprograms with substructural state and Hoare types. In Proceedings of
the 5th ACM Workshop on Programming Languages meets Program
Verification, PLPV ’11, pages 15–26, New York, NY, USA, 2011. ACM.
ISBN 978-1-4503-0487-0.
Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda — afunctional language with dependent types. In TPHOLs ’09: Proceedingsof the 22nd International Conference on Theorem Proving in Higher
Order Logics, pages 73–78, Berlin, Heidelberg, 2009. Springer-Verlag.
Edwin Brady, Conor McBride, and James McKinna. Inductive families
need not store their indices. In Stefano Berardi, Mario Coppo, andFerruccio Damiani, editors, TYPES, volume 3085 of Lecture Notes in
Computer Science, pages 115–129. Springer, 2003.
Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. Associated type synonyms. In ICFP ’05: Proceedings of the Tenth ACM
SIGPLAN International Conference on Functional Programming, pages
241–253, New York, NY, USA, 2005. ACM.
James Cheney and Ralf Hinze. First-class phantom types. CUCIS TR20031901, Cornell University, 2003.
Cormac Flanagan. Hybrid type checking. In Proceedings of the 33rd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL ’06, pages 245–256, New York, NY, USA, 2006.
ACM. doi: 10.1145/1111037.1111059.
Matthew Gertz. Scaling up: The very busy background compiler. MSDN
Magazine, 6 2005. URL http://msdn.microsoft.com/en-us/
magazine/cc163781.aspx.
Christian Haack and J. B. Wells. Type error slicing in implicitly typed
higher-order languages. Science of Computer Programming, 50:189–
224, March 2004. ISSN 0167-6423.
Fritz Henglein. Dynamic typing: syntax and proof theory. Science ofComputer Programming, 22:197–230, June 1994. ISSN 0167-6423.

Oleg Kiselyov, Simon Peyton Jones, and Chung-chieh Shan. Fun with
type functions. In A.W. Roscoe, Cliff B. Jones, and Kenneth R.
Wood, editors, Reflections on the Work of C.A.R. Hoare, History ofComputing, pages 301–331. Springer London, 2010. doi: 10.1007/
978-1-84882-912-1 14.
Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate with class:extensible generic functions. In Proceedings of the 10th ACM SIGPLAN
International Conference on Functional Programming, ICFP ’05, pages
204–215, New York, NY, USA, 2005. ACM. doi: 10.1145/1086365.
1086391.
Daniel R. Licata and Robert Harper. A formulation of dependent ML with
explicit equality proofs. Technical Report CMU-CS-05-178, Carnegie
Mellon University Department of Computer Science, 2005.
Daniel R. Licata and Robert Harper. Canonicity for 2-dimensional typetheory. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL ’12, pages
337–348, New York, NY, USA, 2012. ACM. doi: 10.1145/2103656.
2103697.
Zhaohui Luo. Coercions in a polymorphic type system. Mathematical
Structures in Computer Science, 18(4):729–751, August 2008. ISSN
0960-1295. doi: 10.1017/S0960129508006804.
Alexandre Miquel. The implicit calculus of constructions: extending puretype systems with an intersection type binder and subtyping. In Proceedings of the 5th International Conference on Typed Lambda Calculi
and Applications, TLCA’01, pages 344–359, Berlin, Heidelberg, 2001.
Springer-Verlag. ISBN 3-540-41960-8.
Nathan Mishra-Linger and Tim Sheard. Erasure and polymorphism inpure type systems. In Roberto Amadio, editor, Foundations of Software
Science and Computational Structures, volume 4962 of Lecture Notes in
Computer Science, pages 350–364. Springer Berlin / Heidelberg, 2008.
Ulf Norell. Towards a practical programming language based on dependent
type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007.
Simon Peyton Jones and John Launchbury. Unboxed values as first classcitizens in a non-strict functional programming language. In FPCA91:
Conference on Functional Programming Languages and Computer Architecture, pages 636–666, New York, NY, August 1991. ACM Press.
Simon Peyton Jones and André Santos. A transformation-based optimiser
for Haskell. Science of Computer Programming, 32(1-3):3–47, September 1998.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey
Washburn. Simple unification-based type inference for GADTs. In
Proceedings of the 11th ACM SIGPLAN International Conference on
Functional Programming, pages 50–61, New York, NY, USA, 2006.
ACM Press. ISBN 1-59593-309-3.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark
Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17(01):1–82, 2007. doi: 10.1017/
S0956796806006034.
Benjamin C. Pierce and David N. Turner. Local type inference. ACM Transactions on Programming Languages and Systems, 22(1):1–44, January

2000. ISSN 0164-0925. doi: 10.1145/345099.345100.
François Pottier and Didier Rémy. The essence of ML type inference. In
Benjamin C. Pierce, editor, Advanced Topics in Types and Programming
Languages, chapter 10, pages 389–489. MIT Press, 2005.
Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality. In Proc 4th International Workshop on Logical Frameworks andMeta-languages (LFM’04), pages 106–124, July 2004.
Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In
Scheme and Functional Programming Workshop, pages 81–92, September 2006.
Jeremy G. Siek and Manish Vachharajani. Gradual typing with unificationbased inference. In Proceedings of the 2008 symposium on Dynamic
languages, DLS ’08, pages 7:1–7:12, New York, NY, USA, 2008. ACM.
doi: 10.1145/1408681.1408688.
Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, andKevin Donnelly. System F with type equality coercions. In Proceedingsof the 2007 ACM SIGPLAN Workshop on Types in Language Design and
Implementation, pages 53–66, New York, NY, USA, 2007. ACM.
Nikhil Swamy, Michael Hicks, and Gavin M. Bierman. A theory of typed
coercions and its applications. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, ICFP ’09,
pages 329–340, New York, NY, USA, 2009. ACM. ISBN 978-1-60558332-7.
Nikhil Swamy, Juan Chen, Cedric Fournet, Pierre-Yves Strub, Karthikeyan
Bharagavan, and Jean Yang. Secure distributed programming withvalue-dependent types. In Proceedings of the 16th ACM SIGPLAN
International Conference on Functional Programming, ICFP’11, pages
266–278. ACM, September 2011. doi: 10.1145/2034773.2034811.
The Coq Team. Coq. URL http://coq.inria.fr.
Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration:from scripts to programs. In Companion to the 21st ACM SIGPLAN
Symposium on Object-Oriented Programming Systems, Languages, andApplications, OOPSLA ’06, pages 964–974, New York, NY, USA, 2006.
ACM. doi: 10.1145/1176617.1176755.
Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin
Sulzmann. OutsideIn(X): Modular Type inference with local assumptions. Journal of Functional Programming, 21, 2011.
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve
Zdancewic. Generative type abstraction and type-level computation. In
Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’11, pages 227–240, New
York, NY, USA, 2011. ACM. ISBN 978-1-4503-0490-0.
Andrew K. Wright and Robert Cartwright. A practical soft type system for
scheme. ACM Transactions on Programming Languages and Systems,
19(1):87–152, January 1997. ISSN 0164-0925. doi: 10.1145/239912.
239917.
Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones,
Dimitrios Vytiniotis, and José Pedro Magalhães. Giving Haskell apromotion. In Proceedings of the 8th ACM SIGPLAN Workshop on Types
in Language Design and Implementation, TLDI ’12, pages 53–66, New
York, NY, USA, 2012. ACM. doi: 10.1145/2103786.2103795.