Improved Inference for Checking Type
Annotations

arXiv:cs/0507036v1 [] 14 Jul 2005

Peter J. Stuckey1 , Martin Sulzmann2 and Jeremy Wazny1
1
NICTA Victoria Laboratories
Department of Computer Science and Software Engineering
The University of Melbourne, Vic. 3010, Australia
{pjs,jeremyrw}@cs.mu.oz.au
2
School of Computing, National University of Singapore
S16 Level 5, 3 Science Drive 2, Singapore 117543
sulzmann@comp.nus.edu.sg

Abstract. We consider type inference in the Hindley/Milner system
extended with type annotations and constraints with a particular focus
on Haskell-style type classes. We observe that standard inference algorithms are incomplete in the presence of nested type annotations. To
improve the situation we introduce a novel inference scheme for checking type annotations. Our inference scheme is also incomplete in general
but improves over existing implementations as found e.g. in the Glasgow
Haskell Compiler (GHC). For certain cases (e.g. Haskell 98) our inference
scheme is complete. Our approach has been fully implemented as part of
the Chameleon system (experimental version of Haskell).

1

Introduction

Type inference for the Hindley/Milner system [Mil78] and extensions [Rém93,Pot98,OSW99]
of it is a heavily studied area. Surprisingly, little attention has been given to the
impact of type annotations (a.k.a. user-provided type declarations) and userprovided constraints on the type inference process. For concreteness, we assume
that the constraint domain is described in terms of Haskell type classes [Jon92,HHPW94].
Type classes represent a user-programmable constraint domain which can be
used to code up almost arbitrary properties. Hence, we believe that the content
of this paper is of importance for any Hindley/Milner extension which supports
type annotations and constraints. The surprising observation is that even for
“simple” type classes type inference in the presence of type annotations becomes
a hard problem.
Example 1. The following program is a variation of an example from [JN00].
Note that we make use of nested type annotations. 1
class Foo a b where foo :: a->b->Int
instance Foo Int b
instance Foo Bool b
1

For concreteness, we annotate 1 with Int because in Haskell 1 is in general only a
number.

p y = (let f :: c -> Int
f x = foo y x
in f, y + (1::Int))
q y = (y + (1::Int), let f :: c -> Int
f x = foo y x
in f)
We introduce a two-parameter type class Foo which comes with a method foo
which has the constrained type ∀a, b.F oo a b ⇒ a → b → Bool. The two instance
declarations state that F oo Int b and F oo Bool b hold for any b. Consider
functions p and q. In each case the subexpression y+(1::Int) forces y to be of
type Int. Note that we could easily provide a more complicated subexpression
without type annotations which forces y to be of type Int. The body of function
f x = foo y x generates the constraint F oo Int tx where tx is the type of x.
Note that this constraint is equivalent to T rue due to the instance declaration.
We find that f has the inferred type ∀tx .tx → Int. We need to verify that this
type subsumes the annotated type f::c->Int which is interpreted as ∀c.c →
Int. More formally, we write Cg ⊢ σi ≤ σa to denote that the inferred type
σi subsumes the annotated type σa under some constraint Cg . Suppose σi =
(∀ā.Ci ⇒ ti ) and σa = (∀b̄.Ca ⇒ ta ) where there are no name clashes between
ā and b̄. Then, the subsumption condition is (logically) equivalent to Cg |=
∀b̄.(Ca ⊃ (∃ā.Ci ∧ ti = ta )). In this statement, we assume that |= refers to
the model-theoretic entailment relation and ⊃ refers to Boolean implication.
Outermost universal quantifiers are left implicit. Note that in our system, we
only consider type equality rather than the more general form of subtyping. For
our example, we find that the subsumption condition holds. Hence, expressions
p and q are well-typed.
Let’s see what some common Haskell implementations such as Hugs [HUG]
and GHC [GHC] say. Expression p is accepted by Hugs but rejected by GHC
whereas GHC accepts q which is rejected by Hugs! Why?
In a traditional type inference scheme [DM82], constraints are generated
while traversing the abstract syntax tree. At certain nodes (e.g. let) the constraint solver is invoked. Additionally, we need to check for correctness of type
annotations (a.k.a. subsumption check). The above examples show that different traversals of the abstract syntax tree yields different results. E.g. Hugs
seems to perform a right-first traversal. We visit f::c -> Int; f x = foo y x
first without considering the constraints arising out of the left tuple component.
Hence, we find that f has the inferred type ∀tx .F oo ty tx ⇒ tx → Int where
y has type ty . This type does not subsume the annotated type. Therefore, type
inference fails. Note that GHC seems to favor a left-first traversal of the abstract
syntax tree.
The question is whether there is an inherent problem with nested type annotations, or whether it’s simply a specific problem of the inference algorithms
implemented in Hugs and GHC.
Example 2. Here is a variation of an example mentioned in [Fax03]. We make
use of the class and instance declarations from the previous example.

2

test y = let f :: c->Int
f x = foo y x
in f y
Note that test may be given types Int → Int and Bool → Int. The constraint F oo ty tx arising out of the program text can be either satisfied by
ty = Int or ty = Bool. However, the “principal” type of test is of the form
∀ty .(∀tx .F oo ty tx ) ⇒ ty → Int. Note that the system we are considering does
not allow for constraints of the form ∀tx .F oo ty tx . Hence, the above example
has no (expressible) principal type. We note that the situation is different for
(standard) Hindley/Milner with type annotations. As shown by Odersky and
Läufer [OL96], the problem of finding a solution such that σi (the inferred type)
is an instance of σa (the annotated type) can be reduced to unification under
a mixed prefix [Mil92]. Hence, we either find a principal solution φ such that
⊢ φ(σi ) ≤ φ(σa ) or no solutions. Hence, inference for Hindley/Milner with type
annotations is complete.
We conclude that type inference for Hindley/Milner with constraints and
(nested) type annotations is incomplete. The incompleteness arises because the
subsumption check not only involves a test for correctness of annotations, but
may also need to find a solution. The above example shows that in our general
case there might not necessarily be a principal solution.
In order to resurrect completeness we could impose a syntactic restriction on
the set of programs. E.g., we could simply rule out type annotations for “nested”
let-definitions, or require that the types of all lambda-bound variables occurring
in the scope of a nested annotation must be explicitly provided (although it’s
unclear whether this is a sufficient condition). In any case, we consider these as
too severe restrictions.
In fact, the simplest solutions seems to be to enrich the language of constraints. Note that the subsumption condition itself is a solution to the subsumption problem. Effectively, we add constraints of the form ∀b̄.(Ca ⊃ (∃ā.Ci ∧ ti =
ta )) to our language of constraints. Then, ∀ty .(∀tx .F oo ty tx ) ⇒ ty → Int will
become a valid type of test in the above example. This may be a potential solution for some cases, but is definitely undesirable for Haskell where constraints
are attached to dictionaries. It is by no means obvious how to construct dictionaries [HHPW94] for “higher-order” constraints. Furthermore, we believe that
type inference easily becomes undecidable depending on the underlying primitive
constraint domain.
In this paper, we settle for a compromise between full type inference and full
type checking. We only check for the correctness of type annotations. But before
checking we infer as much as possible. Our contributions are:
– We introduce a novel formulation of improved inference for checking annotations in terms of Constraint Handling Rules (CHRs) [Frü95]. While inferring
the type of some inner expression we can reach the result of inference for
some outer expression.
– We can identify a class of programs for which inference is complete.
– Our approach is fully implemented as part of the Chameleon system [SW].
We can type a much larger class of programs compared to Hugs and GHC.
E.g., Example 1 is typable in our system. We refer to [SW] for more examples.
3

(Var-∀E)

(x : ∀ā.D ⇒ t) ∈ Γ
Pp |= C ⊃ [t̄/ā]D
C, Γ ⊢ x : [t̄/ā]t

(Abs)

C, Γ ⊢ e1 : t1 → t2
C, Γ ⊢ e2 : t1
C, Γ ⊢ e1 e2 : t2
ā = fv(C1 , t1 )
C2 ∧ C1 , Γ.(g : ∀ā.C1 ⇒ t1 ) ⊢ e1 : t1
C2 , Γ.(g : ∀ā.C1 ⇒ t1 ) ⊢ e2 : t2
g :: C1 ⇒ t1
C2 , Γ ⊢ let
in e2 : t2
g = e1

C, Γ.x : t1 ⊢ e : t2
C, Γ ⊢ λx.e : t1 → t2

C1 , Γ ⊢ e 1 : t1
ā = fv(C1 , t1 ) − fv(Γ )
(Let)
C2 , Γ.(g : ∀ā.C1 ⇒ t1 ) ⊢ e2 : t2
C2 , Γ ⊢ let g = e1 in e2 : t2

(LetA)

(App)

Fig. 1. Hindley/Milner with Type Annotations

We continue in Section 2 where we formally introduce an extension of the
Hindley/Milner system with constraints and type annotations. Section 3 is the
heart of the paper. We first motivate our approach by example before mapping
the entire type inference problem to CHRs. Type inference then becomes CHR
solving. In Section 4 we discuss related work and conclude.

2

Types and Constraints

We present an extension of the Hindley/Milner system with constraints and type
annotations.
f :: C ⇒ t
in e
Expressions e ::= x | λx.e | e e | let f = e in e | let
f =e
Types
t ::= a | t → t | T t̄
Type Schemes σ ::= t | ∀ā.C ⇒ t
Constraints C ::= t = t | U t̄ | C ∧ C
CHRs
R ::= U t̄ ⇐⇒ C | U1 t1 , ..., Un tn =⇒ C
We write ō to denote a sequence of objects o1 , ..., on and o : t to denote o1 :
t1 , ..., on : tn . W.l.o.g., we assume that lambda-bound and let-bound variables
have been a-renamed to avoid name clashes. We record these variables in some
environment Γ . Note that we consider Γ as an (ordered) list of elements, though
we commonly use set notation. We denote by {x1 : σ1 , . . . , xn : σn }.x : σ the
environment {x1 : σ1 , . . . , xn : σn , x : σ}.
Our type language consists of variables a, type constructors T and type
application, e.g. T a. We use common notation for writing function and list
types. We also make use of pairs, integers, booleans etc. in examples.
We find two kinds of constraints. Equations t1 = t2 among types t1 and t2
and user-defined constraints U t̄. We assume that U refers to type classes such
as F oo. For our purposes, we restrict ourselves to single-headed simplification
CHRs U t̄ ⇐⇒ C and multi-headed propagation CHRs U1 t1 , ..., Un tn =⇒ C.
We note that CHRs describe logic formula. E.g. U t̄ ⇐⇒ C can be interpreted
as ∀ā.U t̄ ↔ (∃b̄.C) where ā = fv(t̄) and b̄ = fv(C) − ā, and U1 t1 , ..., Un tn =⇒ C
can be interpreted as ∀ā.(U1 t1 ∧ ... ∧ Un tn ) ⊃ (∃b̄.C) where ā = fv(t1 , ..., tn )
and b̄ = fv(C) − ā. Via CHRs we can model most known type class extensions.
We refer the interested reader to [SS04] for a detailed account of translating
4

classes and instances to CHRs. We claim that using CHRs we can cover a sufficiently large range of Hindley/Milner type systems with constraints such as
functional dependencies, records etc. Note that CHRs additionally offer multiheaded simplification CHRs which in our experience so far do not seem to be
necessary in the type classes context. Due to space limitations, we only give one
simple example showing how to express Haskell 98 type class relations in terms
of CHRs.
We assume that the meaning of user-defined constraints (introduced by class
and instance declarations) has already been encoded in terms of some set Pp of
CHRs. User-defined functions are recorded in some initial environment Γinit .
Example 3. Consider
class Eq a where (==) :: a->a->Bool
instance Eq a => Eq [a]
class Eq q => Ord a where (<) :: a->a->Bool
class Foo a b where foo :: a->b->Int
instance Foo Int b
instance Foo Bool b
Note that the declaration class Eq a => Ord a introduces a new type class
Ord and imposes the additional condition that Ord a implies Eq a (which is
sensible assuming that an ordering relation assumes the existence of an equality
relation). We can model such a condition via a propagation rule. Hence, Pp
consists of
(Super) Ord a =⇒ Eq a (F1) F oo Int b ⇐⇒ T rue
(Eq1) Eq a ⇐⇒ Eq [a] (F2) F oo Bool b ⇐⇒ T rue
and Γinit = {(==) : ∀a.Eq a ⇒ a → a → Bool, (<) : ∀a.Ord a ⇒ a → a →
Bool, f oo : ∀a, b.F oo a b ⇒ a → b → Int}.
We introduce judgments of the form C, Γ ⊢ e : t where C is a constraint,
Γ refers to the set of lambda-bound variables, predefined and user-defined functions, e is an expression and t is a type. We leave the type class theory Pp implicit. We say a judgment is valid iff there is a derivation w.r.t. the rules found
in Figure 1. Commonly, we require that constraints appearing in judgments are
satisfiable. We say that a valid judgment is satisfiable iff all constraints appearing in the derivation are satisfiable. A constraint is satisfiable w.r.t. a type class
theory iff we find some model satisfying the theory and constraint. We say a
theory Pp is satisfiable iff we find some model for Pp .
In rule (Var-∀E), we assume that x either refers to a lambda- or let-bound
variable. Note that only let-bound variables and primitives can be polymorphic.
For convenience, we combine variable introduction with quantifier elimination.
We can build an instance of a type scheme if the instantiated constraint is
entailed by the given constraint w.r.t. type class theory Pp .
In rule (Let) we couple the quantifier introduction rule with the introduction
of user-defined functions. In our formulation, C2 does not necessarily guarantee
that C1 is satisfiable. However, our rule (Let) is sound for a lazy semantics which
applies to Haskell.
5

Rule (LetA) introduces a type annotation. Note that we assume that type
annotations are closed, i.e. all variables appearing in C1 ⇒ t1 are assumed to
be universally quantified. This is the assumption made for Haskell 98 [Has].
Note that the environment for typing the function body includes the binding
g : ∀ā.C1 ⇒ t1 . Hence, we allow for polymorphic recursive functions.
The other rules are standard. Note that we left out the rule for monomorphic
recursive functions for simplicity.

3

Type Inference via CHRs

We introduce our improved inference scheme first by example. Then, we show
how to map the typing problem to a set of CHRs. We give a description of the
semantics of CHRs adapted to our setting. Finally, we show how to perform type
inference in terms of CHR solving.
3.1 Motivating Examples
The following examples give an overview of the process by which we abstract
the typing problem in terms of constraints and CHRs.
Example 4. Consider the following program.
g y = let f x = x in (f True, f y)
We introduce new predicates, (special-purpose) user constraints, g(t) and
f (t) to constrain t to the types of functions g and f respectively. It is necessary
for us to provide a meaning for these constraints, which we will do in terms of
CHR rules. The body of each rule will contain all constraints arising from the
definition of the corresponding function, which represent that function’s type.
For the program above we may generate rules similar to the following.
g(t) ⇐⇒ t = ty → (t1 , t2 ), f (tf 1 ), tf 1 = Bool → t1 , f (tf 2 ), tf 2 = ty → f2
f (t) ⇐⇒ t = tx → tx
The arrow separating the rule head from the rule body can be read as logical
equivalence. Variables mentioned only in a rule’s body are implicitly existentially
quantified.
In the g rule we see that g’s type is of the form ty → (t1 , t2 ), where t1 and t2
are the results of applying function f to a Bool and a ty . We represent f’s type,
at both call sites in the program, by the f user constraint.
The f rule is much more straightforward. It simply states that t is f ’s type
if t is the function type tx → tx , for some tx , which is clear from the definition
of f.
We can infer g’s type by performing a CHR derivation, solving the constraint
g(t) by applying CHRs (removing the constraint matching the lhs with the rhs).
Note that we avoid renaming variables where unnecessary.
g(t) ֌g t = ty → (t1 , t2 ), f (tf 1 ), tf 1 = Bool → t1 , f (tf 2 ), tf 2 = ty → f2
֌f t = ty → (t1 , t2 ), tf 1 = tx → tx , tf 1 = Bool → t1 , f (tf 2 ), tf 2 = ty → f2
֌f t = ty → (t1 , t2 ), tf 1 = tx → tx , tf 1 = Bool → t1 , tf 2 = t′x → t′x , tf 2 = ty → f2
If we solve the resulting constraints for t, we see that g’s type is ∀ty .ty →
(Bool, ty ).
6

Example 5. The program below is a slightly modified version of the program
presented in Example 4.
g y = let f x = (y,x) in (f True, f y)
The key difference is that f now contains a free variable y. Since y is monomorphic within the scope of g we must ensure that all uses of y, in all definitions,
are consistent, i.e. each CHR rule which makes mention of ty , y’s type, must
be referring to the same variable. This is important since the scope of variables
used in a CHR rule is limited to that rule alone.
In order to enforce this, we perform a transformation akin to lambda-lifting,
but at the type level. Instead of user constraints of form f (t) we now use binary
constraints f (t, l) where the l parameter represents f’s environment.
We would generate rules like the following from this program.
g(t, l) ⇐⇒ t = ty → (t1 , t2 ), f (tf 1 ), tf 1 = Bool → t1 , f (tf 2 , htxi), tf 2 = ty → f2 , l = ls
f (t, l) ⇐⇒ t = tx → (ty , tx ), l = (hty |tsi)
We write ht1 , ..., tn i to indicate a type-level list containing n types. A list with
an n-element prefix but an unbounded tail is denoted by ht1 , ..., tn |ti. When unifying such a type against another list, t will be bound to some sublist containing
all elements after the nth.
As mentioned above, we now use binary predicates to represent the type of a
function. The first argument, which we commonly refer to as the t component,
will still be bound to the function’s type. The second component, which we call l,
represents a list of unbound variables in scope of that function. We have ensured
that whenever the f constraint is invoked from the g rule that ty , the type of y,
is made available to it. So, in essence, the ty that we use in the f rule will have
the same type as the ty in g, rather than simply being a fresh variable known
only in g.
Example 6. We now return to the program first introduced in Example 1, and
generate the CHR rules corresponding to the function p, which is repeated below.
For simplicity we will assume that (+) is defined only on Ints, i.e. (+) : Int →
Int → Int.
p y = (let f :: c -> Int
f x = foo y x
in f, y + (1::Int))
We generate the following CHRs from this fragment of the program. We also
include the rule which represents foo’s type, and the rule which corresponds to
the instance F oo Int b.
p(t, l) ⇐⇒ t = ty → (t1 , t2 ), f (t1 , (hty i, hty , tx i), t2 = tr ,
tplus = Int → Int → Int, tplus = ty → Int → tr , l = (ls, hty , tx i)
fa (t, l) ⇐⇒ p(t′ , l), t = c → Int, l = (hty |lsi, hty , tx i)
f (t, l) ⇐⇒ t = tx → tr , f oo(tf oo , ls′ ), tf oo = ty → tx → tr , fa (t, l),
l = (hty |lsi, hty , tx i)
f oo(t, l) ⇐⇒ t = a → b → Int, F oo a b
F oo Int b ⇐⇒ T rue
7

Here we have extended the scheme which we used to generate the constraints
in the previous example. We stick to binary predicates, but have expanded the
l component to include two lists. The first list, which we refer to as the local l
component contains, as before, a type-level list of all unbound lambda variables
in scope of the function. The second list, which we will often denote LT simply
contains all of the lambda-bound variables from the top-level definition down,
in a fixed order.
We introduce a symbol fa and generate a new rule to represent f’s annotated
type. Note also that we add a call to the f rule to unify f’s inferred type with
the declared type.
As demonstrated earlier, in order to check f it is necessary to consider all
of the type information available in f’s context. In particular, for this program,
it is critical that we know y has type Int, in order to reduce the F oo Int b
constraint which arises from the use of foo, but is absent from the annotation.
The way we introduce f’s context into f is by adding a call from the fa rule
to the immediate parent definition, which in this case is represented by p. In this
instance we are not interested in p’s type, only the effect it has on lambda-bound
variables, and any type class constraints which may arise. Note that if p were
itself embedded within a function definition, then it too would have such a call
(to its own parent), and so f would indirectly inherit p’s context.
We perform the following simplified derivation to demonstrate that the CHR
formulation above captures the necessary context information within f.
f (t, l) ֌f f oo(tf oo , ls′ ), tf oo = ty → tx → tr , fa (t, l),
l = (hty i, hty , tx i), ...
֌f oo tf oo = a → b → Int, F oo a b, tf oo = ty → tx → tr , fa (t, l),
l = (hty i, hty , tx i), ...
we can simplify this to:
F oo ty tx , fa (t, l), l = (hty i, hty , tx i), ...
֌fa F oo ty tx , p(t′ , l), l = (hty i, hty , tx i), ...
֌p F oo ty tx , tplus = Int → Int → Int, tplus = ty → Int → tr ,
l = (ls, hty , tx i), l = (hty i, hty , tx i), ...
֌F oo tplus = Int → Int → Int, tplus = ty → Int → tr ,
l = (ls, hty , tx i), l = (hty i, hty , tx i), ...
Through the call to p from fa we introduce sufficient context information to
determine that ty is an Int, and to consequently reduce away the F oo constraint
using the instance rule. Note that the LT component is necessary here because
p is not aware of its own lambda-bound variables. Without the LT component,
p would not be able to “export” the required information about ty to f .
3.2 Constraint and CHR Generation
In detail, we show how to map expressions to constraints and CHRs. Lambdaabstractions such as λx.e are preprocessed and turned into λx :: tx .e where tx
is a fresh type variable. We assume that LT contains all such type variables tx
attached to lambda-abstractions.
For each function definition f=e we generate a CHR of the form f (t, l) ⇐⇒ C
where l refers to a pair (ll , lg ). The constraint C is generated out of the program
text of e. We maintain that ll denotes the set of types of lambda-bound variables
in the environment and lg refers to LT the types of all lambda-bound variables.
8

Constraint Generation:
t, l, lg fresh (f ∈ E or
fa ∈ E f non-recursive)
(Var-f)
C = {f (t, l), l = (htx i, lg )}
{x : tx }, E, f ⊢C (C t)

(x : t1 ) ∈ Γ t2 fresh
(Var-x)
Γ, E, x ⊢C (t2 = t1 t2 )

(VarA-f)

fa ∈ E f recursive t, l, lg fresh C = {fa (t, l), l = (htx , lg i)}
{x : tx }, E, f ⊢C (C t)

Γ.x : t1 , E, e ⊢C (C t2 )
(Abs) C ′ = {C, t3 = t1 → t2 } t3 fresh
Γ, E, λx :: t1 .e ⊢C (C ′ t3 )
(Let)

Γ, E ∪ {g}, e2 ⊢C (C t)
Γ, E, let g = e1 in e2 ⊢C (C t)

(App)

Γ, E, e1 ⊢C (C1 t1 )
Γ, E, e2 ⊢C (C2 t2 ) t3 fresh
Γ, E, e1 e2 ⊢C (C1 , C2 , t1 = t2 → t3 t3 )

(LetA)

Γ, E ∪ {ga }, e2 ⊢C (C t)
g :: C1 ⇒ t1
Γ, E, let
in e2 ⊢C (C t)
g = e1

CHR Generation:

(Var) h, Γ, E, v ⊢R ∅

(App)

h, Γ, E, e1 ⊢R P1
h, Γ, E, e2 ⊢R P2
h, Γ, E, e1 e2 ⊢R P1 ∪ P2

(Abs)

h, Γ.x : t, E, e ⊢R P
h, Γ, E, λx :: t.e ⊢R P

Γ = {x1 : t1 , . . . , xn : tn } t, t′2 , l, lr, lg fresh
g, Γ, E, e1 ⊢R P1 h, Γ, E ∪ {g}, e2 ⊢R P2 Γ, E, e1 ⊢C (C1′ t′1 )
(Let)
P = P1 ∪ P2 ∪ {g(t, l) ⇐⇒ C1′ , t′1 = t, l = (ht1 , . . . , tn |lri, LT ), h(t′2 , l)⊖ }
h, Γ, E, let g = e1 in e2 ⊢R P

(LetA)

Γ = {x1 : t1 , . . . , xn : tn } t, t′2 , l, lr fresh
g, Γ, E ∪ {ga }, e1 ⊢R P1 h, Γ, E ∪ {ga }, e2 ⊢R P2 Γ, E ∪ {ga }, e1 ⊢C (C1′ t′1 )
P = P1 ∪ P2 ∪
(
)
′′
ga (t, l) ⇐⇒ t = t1 , C1′′ , l = (ht1 , ..., tn |lri, LT ), h(t′2 , l)⊖
g(t, l) ⇐⇒ l = (ht1 , . . . .tn |lri, LT ), ga (t, l), C1′ , t = t′1
h, Γ, E, let

g :: C1′′ ⇒ t′′1
in e2 ⊢R P
g = e1

Fig. 2. Constraint and CHR Generation

We make use of list notation (on the level of types) to refer to the types
of λ-bound variables. In order to avoid confusion with lists of values, we write
hl1 , . . . , ln i to denote the list of types l1 , . . . , ln . We write hl|ri to denote the list
of types with head l and tail r.
For constraint generation, we employ judgments Γ, E, e ⊢C (C t) where
environment Γ , set of predicate symbols E and expression e are input values and
constraint C and type t are output parameters. Note that Γ consists of lambdabound variables only whereas E holds the set of predicate symbols referring to
primitive and let-defined functions. Initially, we assume that Einit holds all the
9

symbols defined in Pinit which is the CHR representation of all functions in Γinit .
The rules can be found in Figure 2.
Consider rule (Var-f). If the function does not carry an annotation or the
function is not recursive 2 we make use of the definition CHR. However, strictly
making use of the definition CHR might introduce cycles among CHRs, e.g. consider polymorphic recursive functions. In such cases we make use of the annotation CHR, see rule (VarA-f). In both rules we set l to the sequence of types of
all lambda-variables in scope. Note that we might pass in more types of lambdabound variables than expected by that function. This is safe because we leave
the first component of l “open” at definition sites. That is, we expect at least
the types of lambda-bound variables in scope at the definition site and possibly
some more. The second component which refers to the sequence of all types of
lambda-bound variables appearing in the entire program is left unconstrained.
This component will be only constrained at definition sites (see CHR generation
rules (Let) and (LetA)). Note that in rule (Abs) the order of lambda-bound
variables added to type environment matters. Hence, we silently treat Γ as a list
rather than a set. In rules (Let) and (LetA) the constraints arising out of e1 might
not appear in C unless we use function g in e2 . Note that we do not generate a
constraint for the subsumption condition which will be checked separately.
For rule generation, we employ judgments of the form h, Γ, E, e ⊢R P where
CHR h, environment Γ , set of predicate symbols E and expression e are input
values and the set P of CHRs is the output value. As an invariant we maintain
that h refers to the surrounding definition of expression e. Initially, we assume
that h refers to some trivial CHR h(t, l) ⇐⇒ T rue and E refers to the set of
primitive functions. We refer to Figure 2 for details. There are two interesting
rules.
Rule (Let) deals with unannotated functions. Note that we do not add g to E
when generating constraints and rules from e1 . Hence, we assume for simplicity
that unannotated functions are not allowed to be recursive. Of course, our system [SW] handles unannotated, recursive functions. Their treatment is described
in a forthcoming report The novel idea of our inference scheme is that we reach
surrounding constraints within the definition of g via the constraint h(t2 , l)⊖ .
The ⊖ marker (left out in Example 6 for simplicity) serves two purposes: (1) We
potentially create cycles among CHRs because we might reintroduce renamed
copies of surrounding constraints. Markers will allow us to detect such cycles to
avoid non-termination of CHRs. (2) Variables occurring in marked constraints
are potentially part of the environment. Hence, we should not quantify over those
variables. Examples will follow shortly to highlight these points.
Rule (LetA) is similar to rule (Let). Here, the annotation CHR includes the
surrounding definition h. The actual inference result is reported in the definition
CHR.
3.3

CHR Solving

We introduce the marked CHR semantics. We assume that each constraint is
attached with either a ⊖ marker or a ǫ (pronounced empty) marker. The empty
marker is commonly left implicit. We refer to constraints carrying a ⊖ marker
as marked constraints. A constraint carrying the empty marker is unmarked. In
2

We can easily check whether a function is recursive or not by a simple dependency
analysis.

10

case of CHR rule application on a marked constraint, we mark all constraints in
the body before adding them to the constraint store.
Definition 1 (Marked CHR Application). Let d = (U t̄)a (or d = f (t̄)a )
be a primitive constraint where a ∈ {⊖ ,ǫ }. We define mark(d) = a. We write
d⊖ to denote (U t̄)⊖ (or f (t̄)⊖ ).
Let (R) c1 , ..., cn =⇒ d1 , ..., dm ∈ P and C be a constraint. Let φ be the
m.g.u. of all equations in C. Let c′1 , ..., c′n ∈ C such that there exists a substitution
θ on variables in rule (R) such that θ(ci ) = φ(c′i ) for i = 1...n. Then, C ֌R
C, d′1 , ..., d′m where

di
if mark(c′j ) 6= ⊖ for j = 1...n
d′i =
(di )⊖ otherwise
Let (R) c ⇐⇒ d1 , ..., dm ∈ P and C be a constraint. Let φ be the m.g.u. of
all equations in C. Let c′ ∈ C such that there exists a substitution θ on variables
in rule (R) such that θ(c) = φ(c′ ), that is user-defined constraint c′ matches the
left-hand side of rule (R). Then, C ֌R C − c′ , d′1 , ..., d′m where d′i are as above.
A derivation step from global set of constraints C to C ′ using an instance of
rule r is denoted C ֌r C ′ . A derivation, denoted C ֌∗P C ′ is a sequence of
derivation steps using either rules in P such that no further derivation step is
applicable to C ′ . The operational semantics of CHRs exhaustively apply rules to
the global set of constraints, being careful not to apply propagation rules twice
on the same constraints (to avoid infinite propagation). We say a set of CHRs
is terminating if for each C there exists C ′ such that C ֌∗P C ′ .
Example 7. Consider
class Erk a where erk :: a
class Foo a where foo :: a
f = (erk, let g :: Foo a => a; g = foo in g)
Here is a sketch of the translation to CHRs.
ga (t) ⇐⇒ f (t′ )⊖ , F oo t
g(t) ⇐⇒ ga (t), F oo t

f (t) ⇐⇒ t = (a, b), Erk a, g(b)

Consider the derivation
g(t1 ) ֌g ga (t1 ), F oo t1 ֌ga f (t′ )⊖ , F oo t1
֌f t′ = (a, b), (Erk a)⊖ , g(b)⊖ , F oo t1
֌g t′ = (a, b), (Erk a)⊖ , ga (b)⊖ , (F oo b)⊖ , F oo t1
In step ֌f we propagate ⊖ to all new constraints. Note that we encounter
a cycle among CHRs (see underlined constraints). Indeed, CHRs may be “nonterminating” because we introduce repeated duplicates of surrounding constraints.
To avoid non-termination we introduce an additional CHR Cycle Removal step
...
֌g
t′ = (a, b), (Erk a)⊖ , ga (b)⊖ , (F oo b)⊖ , F oo t1
֌CCR t′ = (a, b), (Erk a)⊖ , (F oo b)⊖ , F oo t1
which is defined as follows.
11

Definition 2 (CHR Cycle Removal). Let f (t, l) ∈ C and f (t′ , l′ )⊖ ∈ C ′
and a derivation ... ֌ C ֌ ... ֌ C ′ . Then, ... ֌ C ֌ ... ֌ C ′ ֌CCR
C ′ − f (t′ , l′ )⊖ .
We assume that ֌CCR is applied aggressively.
We argue that this derivation step is sound because any further rule application on ga (b)⊖ will only add renamed copies of constraints already present in
the store.
Lemma 1 (CCR Soundness). Let P be a set of CHRs and C and C ′ two
¯fv(C) C ′ .
constraints such that C ֌∗P C ′ . Then P |= C ↔ ∃
We can also argue that we break any potential cycle among predicate symbols referring to function symbols. Note that we do not consider breaking cycles
among two unmarked constraints. Such cases will only occur in case of unannotated, recursive functions which are left out for simplicity. A detailed description
of such cases will appear in a forthcoming report. Also note that we never remove cycles in case of user-defined constraints. In such a case, the type class
theory might be non-terminating. Hence, we state the the CCR derivation steps
preserves termination assuming the type class theory is terminating.
Lemma 2 (CCR Termination). Let Pp be a terminating type class theory,
h(t, l) ⇐⇒ T rue a CHR, Einit a set of primitive predicate symbols, Pinit a set of
CHRs and (Γ, e) a typing problem such that h, Γ, Einit , e ⊢R Pe and (Γinit , Pinit )
models Einit for some Γinit . Then, Pp ∪ Pe ∪ Pinit is terminating.
3.4

Type Inference via CHR Solving

Consider type inference for an expression e w.r.t. an environment Γ of lambdabound variables and an environment Γinit of primitive functions and type class
theory Pp . We assume (Pint , Eint ) model Γinit such that for each f : ∀ā.C ⇒ t′ we
find f (t, l) ⇐⇒ C, t = t′ ∈ Pinit and f ∈ Einit . Then, we generate Γ, e ⊢C (C t)
and h, Γ, Einit , e ⊢R Pe . We generally assume that P denotes Pp ∪ Pe ∪ Pinit .
For typability we need to check that (1) constraint C is satisfiable, and (2)
all type annotations in e are correct. We are now in the position to describe
CHR-based satisfiability and subsumption check procedures.
Definition 3 (Satisfiability Check).
Let P be a set of CHRs and C a constraint such that C ֌∗P C ′ for some
constraint C ′ . We say that C is satisfiable iff the unifier of all equations in C ′
exists.
Soundness of the above definition follows from results stated in [SS02] in combination with Lemma 1. Of course, decidability of the satisfiability check depends
on whether CHRs are terminating.
To check for correctness of type annotations we first need to calculate the
set of all subsumption problems. Let Esub(e) be the set of all predicate symbols
ga where each ga refers to some subexpression (let g :: C1 ⇒ t1 ; g = e1 in e2 )
in e. Let Fsub(e) be a formula such that ∀t, l.(ga (t, l) ↔ g(t, l)) ∈ Fsub(e) for all
ga ∈ Esub(e) . It remains to verify that the type annotation is correct under the
abstraction of type inference in terms of P . Formally, we need to verify that
12

P |= Fsub(e) where P refers to first-order logic interpretation of the set of CHRs
P . In [SS02], we introduced a CNF (Canonical Normal Form) procedure to test
for equivalence among constraints ∀t, l.(ga (t, l) ↔ g(t, l)) w.r.t. some set of CHR
by executing ga (t, l) and g(t, l) and verify that the resulting final stores are
equivalent modulo variables in the initial store (here {t, l}). Thus, we can phrase
¯t,l .C to denote ∃fv(C) − {t, l}.C.
the subsumption check as follows. We write ∃
Definition 4 (Subsumption Check). Let ga ∈ Esub(e) and P be a set of
CHRs. We say that g’s annotation is correct iff (1) we execute ga (t, l) ֌∗P C1
¯t,l .C1 ) ↔ (∃
¯t,l .C2 ).
and g(t, l) ֌∗P C2 , (2) we have that |= (∃
Soundness of the above definition follows from results stated in [SS02] in combination with Lemma 1.
Example 8. Recall Example 7 and the derivation g(t1 ) ֌∗ t′ = (a, b), (Erk a)⊖ , F oo t1 .
A similar calculation shows that ga (t1 ) ֌∗ s′ = (c, d), (Erk c)⊖ , F oo t1 . Note
that the resulting constraints are logically equivalent modulo variable renamings.
Hence, g’s annotation is correct.
Note that in our formulation of type inference, the type of an expression is
described by a set of constraints w.r.t. a set of CHRs. The following procedure describes how to build the associated type scheme. Markers attached to constraints
provide important information which variables arise from the surrounding scope.
Of course, we need to be careful not to quantify over those variables.
Definition 5 (Building of Type Schemes). Let P be a set of CHRs, g a
function symbol. We say function g has type ∀ā.C ′ ⇒ t′ w.r.t. P iff (1) We
have that g(t, l) ֌∗ C, l = (ll , lg ) for some constraint C, (2) φ, the m.g.u. of
C, l = (ll , lg ) exists, (3) let D ⊆ φ(C) such that D is maximal and D consists
of unmarked user-defined constraints only, (4) let ā = fv(D, φt) − fv(φll ), (5) let
C ′ = φ(C) and t′ = φ(t).
Example 9. According to Example 8 we find that g has type ∀t1 .(Erk a, F oo t1 ) ⇒
t1 . Note that Erk a arises from f’s program text.
We are able to state soundness of our approach.
Theorem 1 (Soundness). Let Pe , Pp and Pinit be three sets of CHRs, h a
CHR in Pinit , Γ an environment of simply-typed bindings, Γinit an environment
of primitive functions, e an expression, Einit a set of predicate symbols, C a
constraint and t a type such that (Pinit , Einit ) models Γinit and Γ, Einit , e ⊢C
(C t) and h, Γ, Einit , e ⊢R Pe and type checking of all annotations in e is
successful. Let C ֌∗Pp ∪Pinit ∪Pe C ′ for some constraint C ′ . Let φ be the m.g.u. of
C ′ where we treat all variables in Γ as Skolem constants. Then, φ(C ′ ), φ(Γ ) ∪
Γinit ⊢ e : φ(t).
The challenge is to identify some sufficient criteria under which our type
inference method is complete. Because we only check for subsumption we need
to guarantee that each subsumption condition will be either true or false. E.g. in
Example 2 the subsumption condition boils down to the constraint ∀tx .F oo ty tx .
Note that we can satisfy this constraint by setting ty to either Int or Bool. Hence,
13

our task is to prevent such situations from happening. In fact, such situations can
never happen for single-parameter type classes. But what about multi-parameter
type classes? The important point is to ensure that fixing one parameter will
immediately fix all the others. That is, in case of ∀tx .F oo ty tx we know that
tx is uniquely determined by ty . We can enforce such conditions in terms of
functional dependencies [Jon00].
Definition 6. We say a type class T C is fully functional iff we find a class
declaration class TC a1 ... an | fd1 ,..., fdn where fdi = ai -> a1 ...
ai−1 ai+1 ... an .
We argue that for fully functional dependencies solutions (if they exist) must
be unique. In fact, this is not sufficient because there are still cases where we
need guess.
Example 10. Consider the following simplified representation of the Show class.
class Show a where
show :: a->String
read :: String->a
f :: Show a => String->String
f x = show (read x)
The subsumption check boils down to the formula ∀a.Show a ⊃ ∃a′ .Show a′
which is obviously a true statement (take a′ = a). However, in our translation
to CHRs we effectively check for Show a ↔ Show a′ which obviously does not
hold.
There are further sources where we need to take a guess.
Example 11. Consider
class Foo
instance Show Int
instance Foo a => Show a
where Pp = {(S1) Show Int ⇐⇒ T rue (S2) Show a ⇐⇒ F oo a}. We have that
Pp |= Show Int. However, Show Int ֌S2 F oo Int where |= F oo Int 6↔ T rue
which suggests that Pp |= Show Int might not hold. Clearly, by guessing the
right path in the derivation we find that Show Int ֌S1 T rue.
To ensure that our subsumption check (Definition 4) is complete we need to
rule out ambiguous types and require that the type class theory is complete. A
type is ambiguous iff we can not determine the variables appearing in constraints
by looking at the types alone. The annotation f::Show a=>String->String in
Example 10 is ambiguous. A type class theory Pp is complete iff Pp is confluent,
terminating and range-restricted (i.e. grounding the lhs of CHRs grounds the
rhs) and all simplification rules are single-headed. The type class theory Pp in
Example 11 is non-confluent. In [SS02] we have identified these conditions as
sufficient to ensure completeness of the Canonical Normal Form procedure to
test for equivalence among constraints.
Theorem 2. Let Pp a complete and fully functional type class theory. Then
our CHR-based inference scheme infers principal types if the types arising are
unambiguous.
14

4

Related Work and Conclusion

Simonet and Pottier [SP04] introduce HMG(X) a refined version of HM(X) [OSW99,Sul00]
which includes among others type annotations. Their type inference approach is
based on the “allow for more solutions” philosophy. Hence, they achieve complete type inference immediately. However, they only consider tractable type
inference for the specific case of equations as the only primitive constraints.
An approach in the same spirit is considered by Hinze and Peyton-Jones [HJ00].
They sketch an extension of Haskell to allow for “higher-order” instances which
logically correspond to nested equivalence relations. As pointed out by Faxén [Fax03],
in such an extended Haskell version it would be possible to type the program in
Example 2. We believe this is an interesting avenue to pursue. We are not aware
of any formal results nor a concrete implementation of their proposal.
Pierce and Turner [PT00] develop a local type inference scheme where userprovided type information is propagated inwards to nodes which are below
the annotation in the abstract syntax tree. Their motivation is to remove redundant annotations. Note that Peyton-Jones and Shields [PJS04] describe a
particular instance of local type inference based on the work by Odersky and
Läufer’s[OL96]. In our approach we are able to freely distribute type information
across the entire abstract syntax tree. Currently, we only distribute information
about the types of lambda-bound variables and type class constraints. We believe that our approach can be extended to a system with rank-k types. We plan
to pursue this topic in future work.
In this paper, we have presented a novel inference scheme where the entire
type inference problem is mapped to a set of CHRs. Due to the constraint-based
nature of our approach, we are able to make available the results of inference for
outer expressions while inferring the type of inner expressions. We have fully implemented the improved CHR-based inference system as part of the Chameleon
system [SW] Our system improves over previous implementations such as Hugs
and GHC. For some cases, e.g. unambiguous Haskell 98 programs, we can even
state completeness. We note that our improved inference scheme can host the
type debugging techniques described in [SSW03,SSW04].
In future work, we plan to follow the path of Odersky and Läufer [OL96]
and compute (non-principal in general) solutions to subsumption problems. We
strongly believe that our improved CHR-based inference will be of high value
for such an attempt. Another alternative inference approach not mentioned so
far is to only generate all necessary subsumption problems σi ≤ σa and wait
for the “proper” moment to solve or check them. Of course, we still need to
process them in a certain order and might fail for the same reason we failed
in Example 1. Clearly, our constraint-based approach allows us to “exchange”
intermediate results among two subsumption problems which may be crucial for
successful inference.

References
DM82.
Fax03.

L. Damas and R. Milner. Principal type-schemes for functional programs.
In Proc. of POPL’82, pages 207–212. ACM Press, January 1982.
K. F. Faxén. Haskell and principal types. In Proc. of Haskell Workshop’03,
pages 88–97. ACM Press, 2003.

15

Frü95.

T. Frühwirth. Constraint handling rules. In Constraint Programming: Basics and Trends, LNCS. Springer-Verlag, 1995.
GHC.
Glasgow haskell compiler home page. http://www.haskell.org/ghc/.
Has.
Haskell 98 language report. http://research.microsoft.com/Users/simonpj/haskell98-revised/haskell98-report
html/.
HHPW94. C. V. Hall, K. Hammond, S. Peyton Jones, and P. Wadler. Type classes in
Haskell. In ESOP’94, volume 788 of LNCS, pages 241–256. Springer-Verlag,
April 1994.
HJ00.
Ralf Hinze and Simon Peyton Jones. Derivable type classes. In Proc. of
the Fourth Haskell Workshop, September 2000.
HUG.
Hugs home page. haskell.cs.yale.edu/hugs/.
JN00.
M.
P.
Jones
and
J.
Nordlander,
2000.
http://haskell.org/pipermail/haskell-cafe/2000-December/001379.html.
Jon92.
M. P. Jones. Qualified Types: Theory and Practice. D.phil. thesis, Oxford
University, September 1992.
Jon99.
M. Jones. Typing haskell in haskell. In Haskell Workshop, September 1999.
Jon00.
M. P. Jones. Type classes with functional dependencies. In Proc. of
ESOP’00, volume 1782 of LNCS. Springer-Verlag, 2000.
Mil78.
R. Milner. A theory of type polymorphism in programming. Journal of
Computer and System Sciences, 17:348–375, Dec 1978.
Mil92.
D. Miller. Unification under a mixed prefix. J. Symb. Comput., 14(4):321–
358, 1992.
OL96.
M. Odersky and K. Läufer. Putting type annotations to work. In Proc. of
POPL’96, pages 54–67. ACM Press, 1996.
OSW99. M. Odersky, M. Sulzmann, and M Wehr. Type inference with constrained
types. Theory and Practice of Object Systems, 5(1):35–55, 1999.
PJS04.
S. Peyton-Jones and M. Shields. Practical type inference for arbitrary-rank
types. Submitted for publication, 2004.
Pot98.
F. Pottier. A framework for type inference with subtyping. In Proc. of
ICFP’98, pages 228–238. ACM Press, 1998.
PT00.
B.C. Pierce and D.N. Turner. Local type inference. ACM Transactions on
Programming Languages and Systems, 22(1):1–44, 2000.
Rém93.
D. Rémy. Type inference for records in a natural extension of ML. In
Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of
Object-Oriented Programming. Types, Semantics and Language Design.
MIT Press, 1993.
SP04.
V. Simonet and F. Pottier. Constraint-based type inference with guarded
algebraic data types. Submitted to ACM Transactions on Programming
Languages and Systems, June 2004.
SS02.
P. J. Stuckey and M. Sulzmann. A theory of overloading. In Proc. of
ICFP’02, pages 167–178. ACM Press, 2002.
SS04.
P.J. Stuckey and M. Sulzmann. A theory of overloading. ACM Transactions
on Programming Languages and Systems, 2004. To appear.
SSW03.
P.J. Stuckey, M. Sulzmann, and J. Wazny. Interactive type debugging in
Haskell. In Proc. of Haskell Workshop’03, pages 72–83. ACM Press, 2003.
SSW04.
P. J. Stuckey, M. Sulzmann, and J. Wazny. Improving type error diagnosis.
In Proc. of Haskell’04, pages 80–91. ACM Press, 2004.
Sul00.
M. Sulzmann. A General Framework for Hindley/Milner Type Systems
with Constraints. PhD thesis, Yale University, Department of Computer
Science, May 2000.
SW.
M.
Sulzmann
and
J.
Wazny.
Chameleon.
http://www.comp.nus.edu.sg/˜ sulzmann/chameleon.

16

A

Variations

Our exisiting translation to CHRs is slightly lazier than most inference algorithms in the sense that we do not infer the types of let-bound variables which
are never called.
Example 12. Consider:
f x = let g = x x
in x
We generate CHR rules that look like the following:
f (t) ⇐⇒ t = tx → tx
g(t) ⇐⇒ tx = tx → t
Since the f rule never calls g, the unsatisfiable constraint is not introduced,
and this program is considered well-typed.
This “laziness” can be problematic whenever we need to compare the inferred
type of some function with its declared type. Consider an annotated function g,
nested within the definition of function f , from which we generate an inference
rule, g(t, l) ⇐⇒ ga (t, l), Ci , and an annotation rule, ga (t, l) ⇐⇒ f (t′ , l′ )⊖ , Ca .
It’s possible that the types of some global variables are affected in g, but not in
ga . In order for g(t, l) and ga (t, l) to be equivalent, we depend on g’s context, as
called in the ga rule, to in turn call g and introduce those missing constraints.
Example 13. Consider the following program.
f y = let g :: Bool
g = y
in ’a’
We generate the following (simplified) CHR rules:
f (t, l) ⇐⇒ t = Char, l = (hi, hty i)
g(t, l) ⇐⇒ t = ty , l = (hty i, hty i), ga (t, l)
ga (t, l) ⇐⇒ t = Bool, l = (hty i, hty i), f (t′ , l)
Even though g’s type annotation is acceptable, out subsumption check would
fail, because g(t, l) and ga (t, l) are not equivalent wrt the l component. Clearly,
the g rule implies ty = Bool, but the ga rule does not.
We can remedy this situation by ensuring that all nested functions are called
by their parent function. In this way, when we consider a function annotation,
the definition of the function becomes part of its context.
Example 14. We modify the program of Example 13, forcing f to call g, but
disregard its value.
f y = let g :: Bool
g = y
in const ’a’ g
17

The CHR rule associated with f would now look something like:
f (t, l) ⇐⇒ tconst = a → b → a, a = Char, t = ty → a,
l = (hi, hty i), g(b, l′ )
This solves our immediate problem, in that the constraints arising from g(t, l)
and ga (t, l) are now equialent wrt t and l.
Unfortunately this does not work in the case where the function we call is
recursive. Consider:
f y = let g :: Bool
g = const y g
in ’a’
Here, if f were to call g, the constraint generated to represent g’s type would
be ga (t′ , l′ ). We then face the same problem, that from within ga we have no
association between ty and Bool.
Clearly, a syntactic transformation of the source program to introduce calls
to otherwise uncalled functions is not sufficient. We must modify the CHR generation process to directly insert calls to the inference constraints of functions
which are not already called.
Example 15. We return to the rules generated in Example 13. The following
CHR rule is a modified version of the f rule above which now contains a call to
g, further constraining the lambda-bound type variables.
f (t, l) ⇐⇒ t = Char, l = (hi, hty i), g(t′ , l)⊖
Using this modified rule, we see now that g(t, l) and ga (t, l), are equivalent,
since ty = Bool in both. The ⊖ mark on the g constraint is not significant
here, though it does accomodates the simpler form of cycle breaking (by simply removing the repeated constraint) than the equivalent unmarked constraint
would.

B

Monomorphic Recursive Functions

In case of monomorphic recursive functions (i.e. recursive functions with no type
annotation) we need to update our strategy for breaking cycles among CHRs
(Definition 2). We denote by NRF the set of all non-recursive functions, by
MRF the set of all recursive functions which carry no type annotations and by
ARF the set of all annotated recursive functions.
Definition 7 (CHR Cycle Removal). Let f (t, l)⊖ ∈ C and f (t′ , l′ )⊖ ∈ C ′
where f ∈ NRF ∪ ARF and a derivation ... ֌ C ֌ ... ֌ C ′ . Then, ... ֌ C ֌
... ֌ C ′ ֌CCR C ′ − f (t′ , l′ )⊖ .
Let f (t, l) ∈ C and f (t′ , l′ )⊖ ∈ C ′ where f ∈ MRF and a derivation ... ֌
C ֌ ... ֌ C ′ . Then, ... ֌ C ֌ ... ֌ C ′ ֌CCR C ′ − f (t′ , l′ )⊖ , t′ = t.
Let f (t, l) ∈ C and f (t′ , l′ ) ∈ C ′ where f ∈ MRF and f (t′ , l′ ) is known
to arise from the exact same program source location as f (t, l), and given a
derivation ... ֌ C ֌ ... ֌ C ′ . Then, ... ֌ C ֌ ... ֌ C ′ ֌Mono C ′ −
f (t′ , l′ ), t′ = t.
We assume that ֌CCR and ֌Mono are applied aggressively.
18

Note that according to the definition of a ֌Mono step, we should only ever
break cycles amongst constraints representing unannotated, recursive function
types when they arise from the same program location. Unifying the types of
different calls to the same function is overly restrictive, as the following example
illustrates.
Example 16. Consider the following program.
e = let f = f
in (f::Int, f::Bool)

The two fs in the body of e are calls to the same recursive, unannotated
function. i.e. f ∈ M RF . It would be unnecessarily restrictive, however, to aggressively apply ֌Mono here and unify the types of the two fs, resulting in a
type error. Indeed, these two fs are not even part of the same cycle.
We note that breaking cycles among constraints arising from the exact same
program source location is sufficient.
Example 17. Consider
f = ... f1 ... f2
where we added numbers 1 and 2 to different uses sites of f. Here is a sketch of
type inference where we annotate ֌ to refer to the number of CHR steps applied
so far. f ֌n f1 , f2 ֌f f1,1 , f1,2 , f2 . In the last step we reduce a call to f at
location 1. Note that we make use of a refined marking scheme. We keep track
of the original source location and add the location of the constraint introduced
to the store to the existing locations. We refer to [SSW03] for the details of such
a “location-history” aware refinement of the CHR semantics. Hence, applying
rule (Mono) twice will remove f1,1 and f1,2 (and equate the types of f1,1 and
f1,2 with f ). Similarly, we remove the cycles created by f2 .
We note that for ֌CCR there is no need to equate the l component in case
of f ∈ MRF . The l component is always set at the use site of functions (see
constraint generation rules (Var-f)). Equating the l component would yield a
strictly weaker system.
Example 18. Consider f x = ( f1 ..., let g y = ... f2 ...in g) where
we added numbers 1 and 2 to different (monomorphic) uses sites of f. Here
is a sketch of type inference f ֌n ...f1 , ..., g ֌n+m ...f1 , ..., f2 where natural
numbers n and m refer to the number of CHR steps applied so far. Assume we
fully equate f1 and f2 . Note that their local ll components differ (because this
component is always exact!) Hence, type inference fails.
Note that (as before in case of ARF and NRF ) we only break cycles among
constraints which carry the same marker. This yields a more precise method.
Example 19. Assume we have situation where
... ֌ f (Int), ... ֌ ... ֌ f (t)⊖ , ...
Removing f (t)⊖ and adding t = Int might be too restrictive.
19

Note that by construction ֌Mono never applies to ARF and NRF . Any
potential cycle will be eventually broken. We can re-establish Lemmas 2 and
and state a slightly stronger Lemma 1 which guarantee soundness of our CHRbased inference approach.
Lemma 3 (CCR-Mono Soundness). Let P be a set of CHRs and C and C ′
¯fv(C) C ′ ⊃ C.
two constraints such that C ֌∗P C ′ . Then P |= ∃
¯fv(C) C ′ does not hold anymore. We may reject typable
Note that P |= C ⊃ ∃
programs because we stricly enforce the (Mono) rule.
Example 20. Consider
h x = (h1 ’a’) && (h2 True)
Here is a sketch of type inference.
֌
֌
֌Mono
֌Mono
↔

h(t)
t = tx → Bool, h1 (Char → Bool), h2 (Bool → Bool)
t = tx → Bool, Char → Bool = tx′ → Bool, h1,1 (Char → Bool),
h1,2 (Bool → Bool), h2 (Bool → Bool)
t = tx → Bool, Char → Bool = tx′ → Bool, Char → Bool = Char → Bool,
h1,2 (Bool → Bool), h2 (Bool → Bool)
t = tx → Bool, Char → Bool = tx′ → Bool, Char → Bool = Char → Bool,
Char → Bool = Bool → Bool, h2 (Bool → Bool)
F alse

It is interesting to note is that our type inference scheme for recursive function is more relaxed compared to the one found in some other established type
checkers.
Example 21. Consider the following program.
e
e
f
f
g

:: Bool
= g
:: Bool -> a
= g
= f e

In the case of GHC, the following error reported is:
mono-rec.hs:5:
Couldn’t match ‘Bool -> a’ against ‘Bool’
Expected type: Bool -> a
Inferred type: Bool
In the definition of ‘f’: f = g
The problem reported here stems from the fact that within the mutually
recursive binding group consisting of e, f and g, f is assigned two ununifiable
types, Bool and Bool → a: the first because it must have the same type as g,
which according to e must be Bool; and the second because of its type declaration.
20

Our translation scheme is more liberal than this, in that g’s type within e
and f may be different. Essentially, we only require that the type of a variable
be identical at all locations within the mutually recursive subgroup if a type
declaration has been provided for that variable.
(Simplified) Translation of the above program to CHRs yields.
ea (t) ⇐⇒ t = Bool
e(t) ⇐⇒ g(t)
fa (t) ⇐⇒ t = Bool → a
f (t) ⇐⇒ g(t)
g(t) ⇐⇒ ea (te ), fa (tf ), tf = te → Bool
It is clear from the above that there are no cycles present amongst these rules.
We can use them to successfully infer a type for any of the variables in the
program.
In fact, our handling of binding groups is similar to [Jon99] where type inference of binding groups proceeds as follows:
1. Extend the type environment with the type signatures. In this case f::forall
a. Bool -> a and e::Bool.
2. Do type inference on the bindings without type signatures, in this case g = f
e. Do generalisation too, and extend the environment, giving g :: forall
a. a.
3. Now, and only now, do type inference on the bindings with signatures.

21

