TYPE INFERENCE

AS CONSTRAINT SOLVING

Simon Peyton Jones

Microsoft Research
Lambdale Sept 2019
 The task of type inference
 Reject bad programs
 Accept good programs
 The task of type inference
 Reject bad programs,
with a decent error message
 Accept Elaborate good programs
 Elaboration
sort :: a. Ord a => [a] -> [a] $fOrdInt comes from
reverse :: a. [a] -> [a] instance Ord Int where
foo :: [Int] -> [Int]
…
foo = \xs. sort (reverse xs)

$fOrdInt :: Ord Int

foo :: [Int] -> [Int]

foo = \(xs:[Int]). sort @Int $fOrdInt
(reverse @Int xs)
Elaboration
• Decorate every binder with its
type
• Add type applications
• Add dictionary applications
sort :: a. Ord a => [a] -> [a]
reverse :: a. [a] -> [a] Elaboration
foo :: a. Ord a => [a] -> [a]
foo = \xs. sort (reverse xs)

foo :: a. Ord a => [a] -> [a]

foo = /\a. \(d:Ord a). \(xs:a).
sort @a d (reverse @a xs)
Elaboration
• Decorate every binder with its type
• Add type applications
and abstractions
• Add dictionary applications
and abstractions
 Elaboration
sort :: a. Ord a => [a] -> [a]
concat :: a. [[a]] -> [a]

foo :: a. Ord a => [[a]] -> [a]

foo = \xs. concat (sort xs)

$fOrdList :: a. Ord a -> Ord [a]

Elaboration
• Decorate every binder foo :: a. Ord a => [a] -> [a]
with its type foo = /\a. \(d:Ord a). \(xs:a).
let d2:Ord [a]
• Add type applications d2 = $fOrdList @a d
and abstractions in concat @a (sort @[a] d2 xs)
• Add dictionary applications
and abstractions, $fOrdList comes from
and local bindings instance Ord a => Ord [a] where
…
 reverse :: a. [a] -> [a]
:: [Bool] -> Bool
Classic Damas-Milner and

foo = \xs. (reverse xs, and xs)

 Start with (xs:), where  is a unification variable,

standing for an as-yet-unknown type
 Typecheck (reverse xs)
Instantiate ‘reverse’ with a unification variable ,
standing for another as-yet-unknown type.
So this occurrence of reverse has type [] -> [].
Constrain expected arg type [] equal to
actual arg type , thus  ~ [].
 reverse :: a. [a] -> [a]
:: [Bool] -> Bool
Classic Damas-Milner and

foo = \xs. (reverse xs, and xs)

 Start with (xs:), where  is a unification variable,
standing for an as-yet-unknown type
 Typecheck (reverse xs)
 Instantiate ‘reverse’ with a unification variable , standing for another as-
yet-unknown type. So this occurrence of reverse has type [] -> [].
 Constrain expected arg type [] equal to actual arg type , thus  ~ [].

 Typecheck (and xs)

 Constrain expected arg type [Bool] equal to actual arg type ,
thus  ~ [Bool].
 So we need ( ~ [],  ~ [Bool])
 Solve by unification, yielding a substitution:
 := [Bool],  := Bool
 Elaboration and unification
variables
reverse :: a. [a] -> [a]
and :: [Bool] -> Bool foo = \(xs:).
(reverse @ xs, and xs)
foo = \xs. (reverse xs, and xs) Elaborate

Apply the substitution

Constraints
(zonking)
 ~ [],  ~
[Bool] foo = \(xs:[Bool]).
Solve, by unification (reverse @Bool xs, and xs)
to produce a substitution
 := [Bool],  := Main point: solving the
Bool constraints “fills in” the
elaborated program
 Unification variables
 A unification variable stands for a type; it’s a type that
we don’t yet know
 GHC sometimes calls it a “meta type variable”
 By the time type inference is finished, we should know
what every meta-tyvar stands for.
 The “global substitution” maps each meta-tyvar to the
type it stands for.
 A meta-tyvar stands only for a monotype; a type with no
foralls in it.
 Same thing, but for type classes
sort :: a. Ord a => [a] ->
[a]
reverse :: a. [a] -> [a] foo = \(xs:[Int]).
sort @ d (reverse @ xs)
foo :: [Int] -> [Int]
foo = \xs. sort (reverse xs) Elaborate
Constraints Apply the substitution

[] ~ [], [] ~ [Int], d:Ord 

foo = \(xs:[Int]).
sort @Int $fOrdInt
Solve, by unification (reverse @Int xs)

 := Int,  := Int, Main point: solving the

d := $fOrdInt constraints “fills in” the
elaborated program
 Main point
Deferring solving
The order in
 Old school: “on the fly solving” which we
 Encounter a unification problem encounter
 Solve it constraints
 If fails, report error
 Otherwise, proceed ≠
The order in
 This will not work any more which we solve
them
[] ~ [], [] ~ [Int], d:Ord 
We have to solve  := Int,
before we can solve d:Ord 
 Deferring solving
g :: F a -> a -> Int  x::
type instance F Bool = Bool
 Instantiate g at 
f x = (g True x, ...., not x)

g True
F  ~ Bool, Order of
g True x  ~ , encounter
 ~ Bool
not x
We have to
solve this first
 Deferring solving
op :: C a x => a -> x -> Int
instance Eq a => C a Bool

f x = let g :: a Eq a => a -> a x:

g a = op a x Constraint: C a 
in g (not x)

 Cannot solve constraint (C a ) until we

“later” discover that ( ~ Bool)
 Again, need to defer constraint solving,
rather than doing it all “on the fly”
 The French approach to type inference
Haskell
Elaborated Apply Elaborated
source
program substitution source
program
with program
Constraint “holes”
Large
generation
syntax, Constraints
with many Substitution
many Small syntax, Solve
with few
constructor Residual constraint
constructors
s
Report
errors
The essence of ML type inference, Pottier & Remy,
In ATAPL, Pierce, 2005.
 The language of constraints
Haskell
source Constraints What
program
Constraint
Small syntax, exactly
Large generation
syntax, with
with few is this?
many many constructors
constructors
How does

Solve
solving work?

Residual
Report errors
constraint
 The language of constraints
W ::= Empty constraint
| W1 , W2 Conjunction
| C t1.. tn Class constraint
| t1 ~ t2 Equality constraint
| a1..an. W1W2 Implication
 The language of constraints
W ::= Empty constraint
| W1 , W2 Conjunction
| d : C t1.. tn Class constraint
| g : t1 ~ t2 Equality constraint
| a1..an. W1W2 Implication

Evidence
 [] ~ [], [] ~ [Int], d:Ord 
How solving worksDecompose
1. Take the constraints  ~ , [] ~ [Int], d:Ord 
Substitute
2. Do one rewrite
3. Repeat from 1 [] ~ [Int], d:Ord 𝛽 ≔𝛿
Decompose

 Each step takes a set of  ~ Int, d:Ord

constraints and returns a Substitute
logically-equivalent set
of constraints. d:Ord
 When you can’t do any Solve from instance declaration
more, that’s the
“residual constraint” 𝜖
 Things to notice
 Constraint solving takes place by successive rewrites
of the constraint
 Each rewrite generates a binding, for
 a type variable (fixing a unification variable)
 a dictionary (class constraints)
 a coercion (equality constraint)
as we go
 Bindings record the proof steps
 Bindings get injected back into the term
Implication constraints
 Existentials
data T where ts = [ MkT @Int $fShowInt 3
MkT :: a. Show a => a -> T , MkT @Bool $fShowBool True
]
ts :: [T]
ts = [MkT 3, MkT True]
 MkT :: a. Show a => a -> T
Existentials show :: a. Show a => a -> String

ts :: [T] ts = [ MkT @Int $fShowInt 3

ts = [MkT 3, MkT True] , MkT @Bool $fShowBool True
]

f :: T -> String f = \(t:T). case t of

f = \t. case t of MkT a (gd:Show a) (x:a)
MkT x -> show x -> show @a gd x
 MkT :: a. Show a => a -> T
Generate constraints
show :: a. Show a => a -> String

•f:
f = \t. case t of { MkT x -> show x } •t:
Generate •x:a
• Instantiate
constraint
show with
s
From the lambda
From the case
d : Show From call of show
From (show x)
From result of foo
 MkT :: a. Show a => a -> T
Generate constraints
show :: a. Show a => a -> String

f = \t. case t of { MkT x -> show x }

Generate
constraint
s • But what is this ‘a’?
From the lambda
From the case • And how can we
d : Show From call of show
From (show x)
solve Show
From result of foo
 The Right Way: implication constraints

f = \t. case t of { MkT x -> show x }

Generate MkT :: a. Show a => a -> T

constraint show :: a. Show a => a -> String
s
From the lambda • But what is this ‘a’?
From the case
Answer: Bound by
• And how can we
{ From call of show solve d : Show
, From (show x)
Answer: from gd.
} From result of foo
 Reminder
W ::= Empty constraint
| W1 , W2 Conjunction
| d : C t1.. tn Class constraint
| g : t1 ~ t2 Equality constraint
| a1..an. W1W2 Implication
Implication
constraint Given
Wanted
 From the lambda
From the case {, }
Substitute
{ From call of show
, From (show x) {, }
} From result of foo
Solve (d:Show a), substitute d:=gd

Solving ∀ 𝒂 . ( 𝒈𝒅 : 𝑺𝒉𝒐𝒘 𝒂 ) ⇒𝛾 𝑆𝑡𝑟𝑖𝑛𝑔

Substitute

𝜖
Elaborated program with holes Elaborated program after filling holes

f = \(t:). case t of f = \(t:T). case t of

MkT a (gd:Show a) (x:a) MkT a (gd:Show a) (x:a)
-> show @ d x -> show @a gd x
 What is ‘a’?
f = \(t:T). case t of
f = \t. case t of MkT a (gd:Show a) (x:a)
MkT x -> show x -> show @a gd x

Generate • is a unification variable, standing for an as-yet-

unknown type.
constraint
• Constraint solving produces a substitution for the
s unification variables

• is a skolem constant, the type variable bound by the

MkT pattern match in the elaborated program.
{
• Each pattern match on MkT binds a fresh, distinct
, ‘a’.
}
• Every skolem in the constraints should be bound by
Level numbers and
constraint floating
 Existential escape
f2 = \t. case t of { MkT x -> x } -- Ill-typed

Generate
MkT :: a. Show a => a -> T
constraint
s
From the lambda
From the case • Can we solve by
substituting ?
{} From result of foo
 Existential escape
f2 = \t. case t of { MkT x -> x } -- Ill-typed

Generate
MkT :: a. Show a => a -> T
constraint
s
From the lambda
From the case Can we solve by
substituting ?
{} From result of foo
No! No! Noooo!
comes from an “outer
scope”
 Level numbers
f2 = \t. case t of { MkT x -> x } -- Ill-typed

Generate • Every unification variable has

constraint a level number
s • Every implication has a
From the lambda level number
From the case • We say is untouchable
under the
{} From result of foo • The untouchability rule:
you cannot solve under a , if
n<k
 Back to our earlier example
f = \t. case t of
MkT x -> show x
Now what????
Generate
constraint
s

{}

{ is untouchable!
,
}
 Floating constraints

{ }

 Float outside the

 Now is not untouchable any more
 So we can substitute
 Our ill-typed example again
f2 = \t. case t of { MkT x -> x } -- Ill-typed

Generate
constraint
s
• Cannot float outside the ,
From the lambda
From the case obviously, because it mentions
!

{} From result of foo

 Promotion
2
∀ 𝑎. ¿
 Can we float this to?
 Promotion
2  When floating an
∀ 𝑎. ¿
equality, promote
 Can we float this to? all its free
NO! unification
variables

 Instead “promote” , so we get

 Levels and floating: story so far
 Ever unification variable and F ::= d : C t1.. tn
implication constraint has a level | g : t1 ~ t2
| F1 , F2
 Unification variable is
| True
untouchable under a if
 Float an equality out of an
W ::= F
implication , if does not appear
| W1 , W2
free in or .
| k a1..an. F  W
 When floating out, promote the
free unification variables of the
floated constraint
Constraint generation
and level numbers
 The “ambient” level
 When generating constraints for a term, the generator
has an “ambient” level
 Fresh unification variables are born at this level
 At a pattern match e.g. case x of { K x y -> rhs }
 Increment the ambient level
 Generate constraints for the rhs
 Wrap them in an implication constraint binding the existentials
and constraints of K
 No need for this wrapping if no existentials or constraints
e.g. case x of { Just y -> rhs; … }
 reverse :: a. [a] -> [a]
Type signatures sort :: a. Ord a => [a] -> [a]

f :: a. Ord a => [a] -> [a]

f = \xs -> reverse (sort xs)

• xs : • Type signature gives rise

• Instantiate reverse with to an implication
• Instantiate sort with constraint
• Constraints of the
{ From call of sort signature become
, Result of sort “givens” of the
} From result of foo implication
• Increment the ambient
level before generating
 Works equally well for nested
op ::
signatures
C a x => a -> x -> Int
instance Eq a => C a Bool

f x = let g :: a Eq a => a -> a x:

g a = op a x Constraint: C a 
in g (not x)

And then this

Solve this first

Constraint solving:
hither and yon
 Story so far
 Perform repeated rewrites on the
F ::= d : C t1.. tn
constraints
| g : t1 ~ t2
 Each rewrite preserves logical
| F1 , F2
meaning
| True
 Each rewrite is recorded by adding an
evidence binding, in the elaborated
program W ::= F
| W1 , W2
 The constraint language is very small
| k a1..an. F  W
 But solving is quite subtle
 Solving hither and yon

𝟏
𝑹𝒐𝒐 𝒕
𝟐 𝟏 𝟐
∀ 𝒂 𝜷 𝑩𝒐𝒐𝒍 ∀ 𝒃
𝟏 𝟏
𝑬𝒒(𝜶 ¿ ¿𝟏, 𝜷 )¿ 𝜶 𝑰𝒏𝒕
Touchable

A tree of constraints to solve

Untouchable
Solving hither and yon

𝟏
𝑹𝒐𝒐 𝒕
𝟐 𝟏 𝟐
∀ 𝒂 𝜷 𝑩𝒐𝒐𝒍 ∀ 𝒃
𝟏
𝟏
𝑬𝒒 𝜶 𝑬𝒒 𝜷 𝟏 𝜶 𝑰𝒏𝒕

Use
instance (Eq a, Eq b) => Eq
(a,b)
Solving hither and yon 𝛽 ≔ 𝐵𝑜𝑜𝑙

𝟏
𝑹𝒐𝒐 𝒕
𝟐 𝟐
∀ 𝒂 ∀ 𝒃
𝟏
𝟏
𝑬𝒒 𝜶 𝑬𝒒 𝜷 𝟏 𝜶 𝑰𝒏𝒕

Solve
Solving hither and yon 𝛽 ≔ 𝐵𝑜𝑜𝑙

𝟏
𝑹𝒐𝒐 𝒕
𝟐 𝟐
∀ 𝒂 ∀ 𝒃
𝟏
𝑬𝒒 𝜶 𝑬𝒒 𝑩𝒐𝒐𝒍
𝟏 𝜶 𝑰𝒏𝒕

Apply subst to
Solving hither and yon 𝛽 ≔ 𝐵𝑜𝑜𝑙

𝟏
𝑹𝒐𝒐 𝒕
𝟐 𝟐
∀ 𝒂 ∀ 𝒃
𝟏
𝑬𝒒 𝜶
𝟏 𝜶 𝑰𝒏𝒕

Use instance Eq Bool

Solving hither and yon 𝛽 ≔ 𝐵𝑜𝑜𝑙

𝟏
𝑹𝒐𝒐 𝒕
𝟐 𝟐
∀ 𝒂 ∀ 𝒃
𝟏
𝟏 𝜶 𝑰𝒏𝒕
𝑬𝒒 𝜶

Float out of
Solving hither and yon 𝛽 ≔ 𝐵𝑜𝑜𝑙

𝟏
𝑹𝒐𝒐 𝒕
𝟐
∀ 𝒂
𝟏
𝟏 𝜶 𝑰𝒏𝒕
𝑬𝒒 𝜶
Discard empty
 Solving hither and yon
2 1
∀ 𝑎 . 𝜖 ⇒ {𝐸𝑞 𝛼 }

𝟏
𝑹𝒐𝒐 𝒕
𝟐
∀ 𝒂
𝟏
𝑬𝒒 𝜶
Solve
 Solving hither and yon
2
∀ 𝑎 . 𝜖 ⇒ {𝐸𝑞 𝐼𝑛𝑡 }

𝟏
𝑹𝒐𝒐 𝒕
𝟐
∀ 𝒂
𝑬𝒒 𝑰𝒏𝒕
Apply subst to
Solving hither and yon
2
∀ 𝑎. 𝜖 ⇒ 𝜖

𝟏
𝑹𝒐𝒐 𝒕
𝟐
∀ 𝒂

Use instance Eq Int

Solving hither and yon
𝜖
Main message 𝟏
 Constraint solving may
𝑹𝒐𝒐 𝒕
involve going to and fro
over the tree
 No problem!
Discard empty
Back to the big picture
 The French approach to type inference
Haskell
Elaborated Apply Elaborated
source
program substitution source
program
with program
Constraint “holes”
Large
generation
syntax, Constraints
with many Substitution
many Small syntax, Solve
with few
constructor Residual constraint
constructors
s
Report
errors
The essence of ML type inference, Pottier & Remy,
In ATAPL, Pierce, 2005.
 The advantages of being French
 Constraint generation has a lot of cases (Haskell has a
big syntax) but is rather easy.
 Constraint solving is tricky! But it only has to deal
with a very small constraint language.
 Generating an elaborated program is easy: constraint
solving “fills the holes” of the elaborated program
 Robustness
 Constraint solver can work in whatever order it likes
(incl iteratively), unaffected by of the order in which
you traverse the source program.
 A much more common approach: solve typechecking
problems in the order you encounter them
 Result: small (even syntactic) changes to the program
can affect whether it is accepted 
TL;DR: generate-then-solve is much more robust
 Error messages
 All type error messages are generated from the final,
residual unsolved constraint.
 Hence type errors incorporate results of all solved
constraints. Eg “Can’t match [Int] with Bool”, rather
than “Can’t match [a] with Bool”
 Much more modular: error message generation is in one
place (TcErrors) instead of scattered all over the type
checker.
 Constraints carry “provenance” information to say
whence they came
 Practical benefits
 Highly modular
 constraint generation (7 modules, 3000 loc)
 constraint solving (5 modules, 3000 loc)
 error message generation (1 module, 800 loc)
 Efficient: constraint generator does a bit of “on the fly”
unification to solve simple cases, but generates a
constraint whenever anything looks tricky
 Provides a great “sanity check” for the type system: is it
easy to generate constraints, or do we need a new form of
constraint?
Things I have sadly not talked about
 Coercions: the evidence for equality
 Type families, and “flattening”
 Functional dependencies, injectivity, and “Derived” constraints
 Deferred type errors and typed holes
 Unboxed vs boxed equalities
 Nominal vs representational equality (Coercible etc)
 Kind polymorphism, levity polymorphism, matchabilty
polymorphism
 … and quite a bit more
Things I have sadly not talked about
 Coercions: the evidencew s equality
for
e n
o o d g s
 g “flattening”
Type families,eand in
Th y t h y
z s il
 Functional dependencies, c ra )injectivity,
e a and “Derived”
e s e b l y e
constraints f th n a t h
l o s o t h i n e
l a
e dand
A type(rerrors i
w typed l v
o holes
 Deferred e e d -s
r
a a nd l - n
a rk
h a t e o
 Unboxed vs boxed n e requalities
e w
g e ra m
 f
Nominal vs representational equality (Coercible etc)
 … and quite a bit more
 Conclusion
 Generate constraints then solve, is THE way to do type
inference.
Vive la France
 Background reading
 OutsideIn(X): modular type inference with local assumptions
(JFP 2011). Covers implication constraints but not floating or
level numbers.
 Practical type inference for arbitrary-rank types (JFP 2007). Full
executable code; but does not use the Glorious French Approach
 EXTRA SLIDES
There is lots more to say.
Far too much to fit in a 1-hr talk.
Some of these extra topics are in the following
slides.
Evidence of equality
Equality constraints generate evidence too!

data T a where K1 :: a. (a~Bool) =>

K1 :: Bool -> T Bool Bool -> T a
K2 :: T a

f :: T a -> Maybe a
f x = case x of
K1 z -> Just z
K2 -> Nothing
Equality constraints generate evidence too!

f :: T a -> Maybe a K1 :: a. (a~Bool) =>

f = (a:*) (x:T a). Bool -> T a
case x of
K1 (c:a~Bool) (z:Bool)
-> Just z  c2
K2 -> False Plus
constraint
to solve

∀ . ( c : a Bool ) ⇒(𝑐 2 : 𝑀𝑎𝑦𝑏𝑒 𝐵𝑜𝑜𝑙 𝑀𝑎𝑦𝑏𝑒𝑎)

 Equality constraints
generate evidence too!
2
∀ . ( 𝑐 :𝑎 𝐵𝑜𝑜𝑙 ) ⇒(𝑐 2: 𝑀𝑎𝑦𝑏𝑒 𝐵𝑜𝑜𝑙 𝑀𝑎𝑦𝑏𝑒 𝑎)
Decompose c2 := Maybe
c3
2
∀ . ( 𝑐 : 𝑎 𝐵𝑜𝑜𝑙 ) ⇒ (𝑐 3 : 𝐵𝑜𝑜𝑙 𝑎)
c3 := c4 ; Sym
Use given to substitute
c
for
2 a
∀ . ( 𝑐 : 𝑎 𝐵𝑜𝑜𝑙 ) ⇒ (𝑐 3 : 𝐵𝑜𝑜𝑙 𝐵𝑜𝑜𝑙)
Proving Bool~Bool is c4 := Refl Bool
easy
2
∀ . (𝑐 :𝑎 𝐵𝑜𝑜𝑙 ) ⇒ 𝜖
 Plug the evidence back into the term

f :: T a -> Maybe a
f = (a:*) (x:T a)
case x of
K1 (c:a~Bool) (z:Bool)
-> Just z  (Maybe (Refl Bool ; Sym c))
K2 -> False
 Floating with GADTs

data T a where What type should we infer for f?

K :: Bool -> T Bool  f :: b. T b -> b

f x = case x of  f :: b. T b -> Bool

K z -> True
Neither is more general than
(a substitution instance of)
the other!
data T a where
T1 :: Bool -> T Bool
Floating with GADTs

f x = case x of
• Float, and solve?
T1 z -> True

Get f :: b. T b -> Bool

f:
x:
• Rewrite to using the
given ; then float and
solve
Get b. T b -> b
data T a where
T1 :: Bool -> T Bool
Floating with GADTs

f x = case x of Solution
T1 z -> True
Do not float anything
f: out of an implication
x: that has “given”
equalities

Result (in this case):

“cannot unify
untouchable with Bool”
data
K1
T a where
:: Bool -> T Bool
Floating with GADTs
K2 :: T a
f2 x = case x of
Another branch,
K1 z -> True
with no given
K2 -> False
equalities, may
f: resolve the
x: ambiguity

From the K2 branch,

no implication
needed
Deferred type errors
andtyped holes
 Type errors considered harmful
 The rise of dynamic languages
 “The type errors are getting in my way”
 Feedback to programmer
 Static: type system
 Dynamic: run tests
“Programmer is denied dynamic feedback in the periods when the
program is not globally type correct” [DuctileJ, ICSE’11]
 Type errors considered harmful
 Underlying problem: forces programmer to fix all type
errors before running any code.

Goal: Damn the

torpedos
Compile even type-incorrect
programs to executable code,
without losing type
soundness
 How it looks
bash$ ghci –fdefer-type-errors
ghci> let foo = (True, ‘a’ && False)
Warning: can’t match Char with Bool
gici> fst foo
True
ghci> snd foo
Error: can’t match Char with Bool

 Not just the command line: can load modules

with type errors --- and run them
 Type errors occur at run-time if (and only if) they
are actually encountered
Type holes: incomplete programs
{-# LANGUAGE TypeHoles #-}
module Holes where
f x = (reverse . _) x
 Quick, what type does the “_” have?
[Link]:18:
Found hole ‘_’ with type: a -> [a1]
Relevant bindings include
f :: a -> [a1] (bound at [Link]:1)
x :: a (bound at [Link]:3)
In the second argument of (.), namely ‘_’
In the expression: reverse . _
In the expression: (reverse . _) x

 Agda does this, via Emacs IDE

 Multiple, named holes
f x = [_a, x::[Char], _b:_c ]
Holes:2:12:
Found hole `_a' with type: [Char]
In the expression: _a
In the expression: [_a, x :: [Char], _b : _c]
In an equation for `f': f x = [_a, x :: [Char], _b : _c]

Holes:2:27:
Found hole `_b' with type: Char
In the first argument of `(:)', namely `_b'
In the expression: _b : _c
In the expression: [_a, x :: [Char], _b : _c]

Holes:2:30:
Found hole `_c' with type: [Char]
In the second argument of `(:)', namely `_c'
In the expression: _b : _c
In the expression: [_a, x :: [Char], _b : _c]
 Combining the two
 -XTypeHoles and –fdefer-type-errors work together
 With both,
 you get warnings for holes,
 but you can still run the program

 If you evaluate a hole you get a runtime error.

 Just a hack?
 Presumably, we generate a program with suitable run-
time checks.
 How can we be sure that the run-time checks are in the
right place, and stay in the right places after
optimisation?
 Answer: not a hack at all, but a thing of beauty!
 Zero runtime cost
 When equality is insoluble...

Haskell term (True, ‘a’ && False)

el og
ai e

ab ra
tr at
s

pr
nt

or m
ns er
c o en

at
ed
G

c7 : Int ~ Bool (True, (‘a’  c7) &&

False)
Constraints Elaborated program
(mentioning constraint variables)
 Step 2: solve constraints
 Use lazily evaluated “error” evidence
 Cast evaluates its evidence
 Error triggered when (and only when) ‘a’
must have type Bool
let c7: Int~Bool
Solve = error “Can’t match ...”

c7 : Int ~ Bool (True, (‘a’  c7) &&

False)
Constraints Elaborated program
(mentioning constraint variables)
 Step 2: solve
Uhconstraints
oh! What
 Use lazily evaluated became of
“error” evidence
coercion
 Cast evaluates its evidence erasure?
 Error triggered when (and only when) ‘a’
must have type Bool
let c7: Int~Bool
Solve = error “Can’t match ...”

c7 : Int ~ Bool (True, (‘a’  c7) &&

False)
Constraints Elaborated program
(mentioning constraint variables)
 Hole constraints
(a new form of constraint)
Haskell term True && _

el og
ai e

ab ra
tr at
s

pr
nt

or m
ns er
c o en

at
ed
G

h7 : Hole  (True && h7)

 ~ Bool
Elaborated program
Constraints (mentioning constraint variables)
 Hole constraints...
 Again use lazily evaluated “error”
evidence
 Error triggered when (and only when) the
hole is evaluated
let h7: Bool
= error “Evaluated
Solve hole”

h7 : Hole Bool (True && h7)

Elaborated program
Constraints (mentioning constraint variables)
Generalisation
Generalisation (Hindley-Milner)
f :: Int -> Float -> (Int,Float)
f x y = let g v = v+v
in (g x, g y)
 We need to infer the most general type for
g :: a. Num a => a -> a
so that it can be called at Int and Float
 Generate constraints for g’s RHS, simplify
them, quantify over variables not free in the
environment
 BUT: what happened to “generate then
solve”?
 A more extreme example

data T a where
C :: T Bool
D :: a -> T a Should this
typecheck?
f :: T a -> a -> Bool
f v x = case v of
C -> let y = not x
In the C in y
alternative, we D x -> True
know a~Bool
 A more extreme example

data T a where
C :: T Bool
D :: a -> T a What
about this?
f :: T a -> a -> Bool
f v x = let y = not x
in case v of Constraint
a~Bool arises
C -> y from match on C
D x -> True
A more extreme example

data T a where
C :: T Bool
D :: a -> T a Or this?

f :: T a -> a -> Bool

f v x = let y () = not x
in case v of
C -> y ()
D x -> True
 A more extreme example
data T a where Here we
abstract over But this
C :: T Bool the a~Bool surely
D :: a -> T a constraint should!
f :: T a -> a -> Bool
f v x = let y :: (a~Bool) => () -> Bool
y () = not x
in case v of
C -> y ()
D x -> True
 A possible path [Pottier et al]
Abstract over all unsolved constraints from RHS
 Big types, unexpected to programmer
 Errors postponed to usage sites
 (Serious) Sharing loss for thunks
 (Killer) Can’t abstract over implications
f :: (forall a. (a~[b]) => b~Int) => blah
 A much easier path
Do not generalise local let-bindings at all!
 Simple, straightforward, efficient
 Polymorphism is almost never used in local bindings (see
“Modular type inference with local constraints”, JFP)
 GHC actually generalises local bindings that could have
been top-level, so there is no penalty for localising a
definition.
EFFICIENT EQUALITIES
 Questions you might like to ask
 Is this all this coercion faff efficient?
 ML typechecking has zero runtime cost; so anything
involving these casts and coercions looks inefficient,
doesn’t it?
 Making it efficient
let c7: Bool~Bool = refl Bool
in (x  c7) && False)

 Remember deferred type errors: cast

must evaluate its coercion argument.
 What became of erasure?
Take a clue from unboxed values
x `plusInt` x

data Int = I# Int# = case x of I# a -

>
plusInt :: Int -> Int -> Int case x of I# b -
plusInt x y >
= case x of I# a -> I# (a +# b)
case y of I# b ->
I# (a +# b) = case x of I# a -
>
Library code I# (a++#
Inline a)
optimise
 Expose evaluation to optimiser
Take a clue from unboxed values
data a ~ b = Eq# (a ~# b)
let c7 = refl Bool
() :: (a~b) -> a -> b in (x  c7) && False
x  c = case c of
Eq# d -> x # d ...inline refl, 
= (x # (refl# Bool))
refl :: t~t && False
refl = /\t. Eq# (refl# t)
Inline + optimise
Library code
 So (~#) is the primitive type constructor

 (#) is the primitive language construct

 And (#) is erasable

 Implementing ~#
data T where
T1 :: a. (a~#Bool) -> Double# -> Bool -> T a

A T1 value allocated in the heap looks like

this
64 32
bits bits
T1 ??? 3.8

Question: what is the True

representation for (a~#Bool)?
 Implementing ~#
data T where
T1 :: a. (a~#Bool) -> Double# -> Bool -> T a

A T1 value allocated in the heap looks like this

0 bits 64 32
bits bits
T1 3.8

Question: what is the

representation for (a~#Bool)? True
Answer: a 0-bit value
Boxed and primitive equality
data a ~ b = Eq# (a ~# b)

 User API and type inference deal exclusively in

boxed equality (a~b)
 Hence all evidence (equalities, type classes, implicit
parameters...) is uniformly boxed
 Ordinary, already-implemented optimisation unwrap
almost all boxed equalities.
 Unboxed equality (a~#b) is represented by 0-bit
values. Casts are erased.
 Possibility of residual computations to check
termination