Frozen inference constraints for type-directeddisambiguation
Olivier Martinot, Gabriel Scherer
Abstract
We present work-in-progress on type inference in presenceof type-directed name disambiguation (where an ambiguous name is resolved using type information), following theapproach of constraint-based type inference.
Our specific goal is to implement inference for OCaml
sum/variant constructor disambiguation, and our approachis to introduce “frozen constraints”, a more general constraint
mechanism. We have a prototype implementation of frozen
constraints in the Inferno library, and discuss the implementation and meta-theoretical challenges.

In constraint-based inference, typability of the user program is translated into a typing constraint whose unknowns
are type (meta)variables, and passed to a constraint solver.
Type-inference designers and implementors are encouraged
to pick a relatively generic constraint language, with a few
expressive constructs/combinators, to keep the solver simple.
The specifics of their type-system is translated away during the constraint-generation phase, in terms of these moregeneral constraints. Correspondingly, we propose a new constraint construct, frozen constraints, that is less specific thandisambiguation of variant constructors.

21Introduction

OCaml allows to use datatypes (sums/variants and records)
with overlapping variant constructor or record field names;in this case it uses type-based disambiguation to tell whichconstructor or field is meant, or warns. (This feature wasadded in OCaml 4.01 in 2013; it is also found in other languages, Agda for example.)type t = A
type u = A
let x : t = A
let y : u = A
let z = A> ^> Warning 41 [ambiguous-name]:> A belongs to several types: u t> The first one was selected.
> Please disambiguate if this is wrong.
OCaml performs this disambiguation by propagating type
annotations in subterms, a simple form of bidirectional type
inference. This is robust and predictable, but it relies on
arbitrary choices (in applications t u, do we want to propagate information from t to u or the other way around?; inlet p = e in ..., do we want to propagate informationfrom the pattern p to e or conversely?) that can frustrateusers.
In this work, we decided to look at what a unificationbased propagation of disambiguation information would look
like. We implemented a prototype of type-based constructor
disambiguation within a constraint-based type inferenceengine, Inferno [Pottier 2014a,b].

Frozen constraints

Frozen constraints represent situations where more type
information is needed to decide how we want to type-checksomething.
Let us write 𝛼 ∈ V for inference (meta)variables, 𝜏 ∈ T
for partially-inferred types containing inference variables,
and 𝐶 ∈ C for inference constraints.
A frozen constraint ⟨𝛼⟩𝑓 is built by pairing an inference
variable 𝛼, the needed variable of the constraint, and a function 𝑓 : T → C from partially-inferred types to constraints,
the callback. The intent is to wait until 𝛼 gets unified to a
non-variable type 𝜏, and have the frozen constraint then behave as the constraint 𝑓 (𝜏). (This is an informal descriptionof the expected solver behavior.)
2.1

Constructor disambiguation using frozen
constraints

Constraint generation for a term 𝑡 is typically described
as a function J𝑡K𝛼 that generates a constraint 𝐶, where theinference variable 𝛼 represents the expected type for the term𝑡 in its context. For example, the constraint for an application
can be defined asdef

J𝑡 𝑢K𝛼 = ∃𝛽𝑡 .∃𝛾𝑢 . ((𝛽𝑡 = 𝛾𝑢 → 𝛼) ∧ J𝑡K𝛽𝑡 ∧ J𝑢K𝛾𝑢 )To support constructor disambiguation, we generate for aconstructor application K 𝑡 the constraint
def

JK 𝑡K𝛼 = ∃𝛽𝑡 . (⟨𝛼⟩𝑓K,𝛽𝑡 ∧ J𝑡K𝛽𝑡 )where 𝑓K,𝛽𝑡 is a callback that is called once 𝛼 has been (partially) inferred to some non-variable type, typically a datatype
𝐷. At this point there is no ambiguity anymore: several constructors K may exist in scope, but at most one of them hastype 𝐷. 𝑓K,𝛽𝑡 will look for 𝐷 in the type declaration environment, and a unification constraint between 𝛽𝑡 and theargument type of its constructor K. Type-inference fails withOlivier Martinot, Gabriel Scherer

an error if 𝛼 has been unified with a type that is not a sum/variant type, or if it has no constructor K.
This use of frozen constraints does not try to disambiguate
constructors in all possible cases. For example, if may be that
there are two constructors K declared in the environment,
but the type of 𝑡 is only compatible with one of them; ourapproach makes no attempt to enumerate the declarations of
K and try them with backtracking. This differs from previous
proposals for disambiguation using disjunctive constraints– generating a disjunction of constraints, one for each constructor K in the environment. We don’t guess, we wait forthe context to propagate disambiguation information on thetype of K. This is much closer in spirit and behavior to thebidirectional propagation of type annotations, but it uses
general unification rather than bidirectional propagation, so
it would apply in more situations.
For example, the following uses of the constant constructor 𝐾 at type 𝐷 would be disambiguated, illustrating theabsence of an arbitrary direction of progagation to typeapplications: (𝜆(𝑥 : 𝐷). 𝑡) 𝐾, and (𝑥 : 𝐷 → 𝜏) 𝐾, and(𝜆𝑥 . match 𝑥 with K → 𝑢) (𝑡 : 𝐷).
Remark. One may think of this approach to typed-directeddisambiguation as a limited form of qualified types (say, typeclass inference). Inference for qualified types collects usage
constraints from terms (as our frozen constraints); at generalization time, unsolved usage constraints are turned into qualified constraint abstractions, to be instantiated separately byeach caller. We use frozen constraints for a language feature
for which the qualified-type approach is not desirable: we
do not want ad-hoc polymorphism on constructor names,
their meaning should be exactly the same for all callers of
the surrounding definition. We discuss in the next section
the issues that arise at generalization-time.
Another interesting distinction is that frozen constraints
may in general produce arbitrary constraints once unfrozen,
whereas a qualified type constraint or type-class typically
can express only simpler constraints on its qualified names.
It is not obvious, for example, how one could allow for disambiguation of GADT constructors using qualified types– how to express the still-unknown existential types andequality constraints in the qualified constraint, and how to
type-check its application under this constraint.

3

Implementation challenges

When encountering a frozen constraint ⟨𝛼⟩𝐶, our solver
waits for 𝛼 to be unified with some non-variable type structure. At the very end of the solving process, if some constraints remain frozen, we don’t make any guess but failwith a type error – the user needs to adds annotations todisambiguate the program.
The difficulty is the interaction between frozen constraints
and let-generalization. Suppose a definition let 𝑥 = 𝑡 in the
middle of the program, where we want let to be typed using

Hindley-Milner generalization. If a frozen constraint ⟨𝛼⟩𝑓is generated within the constraint for 𝑡, and remains frozen
once the solver finishes working on 𝑡, what should we do?
Should we fail now, or delay the frozen constraint, and how
does this interact with generalization?
We reason on whether 𝛼 itself is generalizable. If 𝛼 isgeneralizable, then this means that no type in the rest of theprogram mentions 𝛼. No inference work in the rest of theprogram will ever deduce a non-variable structure for 𝛼, sowe can as well fail now with an error.
If 𝛼 is not generalizable, it is tempting to postpone theresolution of ⟨𝛼⟩𝑓 and go on with generalization. But thisis unsound: the constraints generated by 𝑓 once 𝛼 will beknown may mention other inference variables currently inscope, some of which may be in generalizable position. If wegeneralize without looking at 𝑓 , they will be out of scope by
the time ⟨𝛼⟩𝑓 gets unfrozen.
Our solution is to reason on 𝑓 as a closure: we reason on theset of inference variables that are “captured” by 𝑓 , mentioned
in any possible expansion of 𝑓 – in our implementation we
ask the programmer of the constraint generator to list thesecaptured variables.
If none of the captured variables of the callback are generalizable, then the frozen constraint can safely be delayed tolater – failing now would be incomplete. If some of the captured variables, say 𝛽, are generalizable, we have a problem
again: it is unsound in general to generalize now without
unfreezing ⟨𝛼⟩𝑓 , but is is incomplete to fail now, because unfreezing 𝛼 would result in a constraint 𝑓 (𝛼) that may unify
𝛽 with a non-generalizable type.
Consider for example the following program:fun old ->let g x = 1 + old (K x) in(g 0, (old : D -> int))
When inferring let g x = ... before generalization, K x
produces a frozen constraint whose needed variable is its
return type 𝛼, and the use of the old function makes this𝛼 non-generalizable, The callback of the frozen constraint
mentions the inference variable of x, which is generalizable. Generalizing now would give the polymorphic type'a -> int, which is unsound. But failing is incomplete, as
the program contains an annotation (old : D -> int) thatwould unfreeze the frozen constraint, whose solving wouldin turn correctly infer x depending on the declaration of K.
The more complete approach in this case (which we hopeis actually complete) is to suspend disbelief : if generalization encounters a young variable 𝛽 that is needed by a yetunsolved callback function frozen on the non-generalizable
𝛼, we stop mid-way through generalization, producing apartially-frozen scheme ∀𝛼 1 ..𝛼𝑛 . . . . ⟨𝛼⟩𝛽 . . .. 𝛽 remains in an
uncertain state until 𝛼 is unfrozen, and we continue inferring the rest of the program, hoping to be able to un-freeze
𝛼. When our solver encounters an instantiation constraint

Frozen inference constraints for type-directed disambiguation𝑥 ⩽ 𝜏, for a use of a let-bound variable 𝑥 whose generalization is suspended on the needed variable 𝛼, it must generatea fresh variable 𝛾 for the suspended part ⟨𝛼⟩𝛽. Once 𝛼 gets
unfrozen, the solver must be able to come back and unify
this 𝛾 with the correct generalization of 𝛽.
To summarize, when encountering a still-frozen constraint⟨𝛼⟩𝑓 at generalization time:
1. If 𝛼 is generalizable, fail.
2. If 𝛼 and all the variables mentioned/captured by 𝑓 arenon-generalizable, proceed with generalization andkeep the frozen constraint for later.
3. If 𝛼 is non-generalizable, but some variables captured
in 𝑓 are generalizable, suspend generalization of thosevariables and try type-checking the rest of the program.
3.1

Generalization tree

The standard approach to efficiently implement generalization is to track the rank of each inference variable, where therank measures the number of nested let-bindings between
the place where the inference variable is currently scoped
and the root of the term. As inference progresses, unifications widen the scope of variables, so they become bound in
earlier let-binding, their rank decreases. The generalizablevariables are exactly those whose rank remained exactly therank of the let-binding we are about to exit.
In particular, Inferno implements its inference state as adynamic array of of regions1 (sets of variables bound in thesame let-binding), indexed by their rank. Unfortunately, this
implementation is not flexible enough to implement “generalization suspension”: if the generalization of the most recent
region gets partially suspended due to frozen constraints, theregion must be kept alive to store the suspended variables.
Inference continue in the rest of the program, but we maythen enter a new let-binding that creates a new region, thatis neither a child nor an ancestor of the suspended region.
We need to move from a linear array/stack of regions to atree of generalization regions.
With a tree of generalization regions, the notion of “rank”
does not uniquely identify a variable region anymore. When
unifying two variables, it is not enough to compute theirminimum rank and assign it to both. They move to the nearest common ancestor in the tree, which may be older than
the region of both variables.
However, rank optimizations are still partially applicable. For example, when we generalize a leaf region, all thevariables we traverse/inspect were created in this, and somewere moved to one of its ancestors. All regions of interest lie
in a path from the current region to the root of the region
tree, so they may be uniquely indexed by their rank.
1 For more intuition on the connection to region-based memory allocation,see Kiselyov.

4

Theoretical challenges

We can give a simple semantics to frozen constraints, in theusual style of a judgment 𝜙 ⊩ 𝐶 stating that 𝜙 is a solution tothe constraint 𝐶, where 𝜙 is a mapping from inference variables to fully-inferred types, which do not mention inference(meta)variables anymore.
𝜙 ⊩ 𝑓 (𝜙 (𝛼))𝜙 ⊩ ⟨𝛼⟩𝑓However, our solver is not complete with respect to thissemantics. Consider for example the complete constraint
def(on a free existential variable 𝛼) 𝐶 = ⟨𝛼⟩(𝜆_. 𝛼 = int): thisconstraint contains no information on how to guess 𝛼 outside
the callback, but once we unfreeze it it tells us that 𝛼 must
be int. Our solver will not unfreeze the constraint and failwith a typing error, but the assignment 𝛼 ↦→ int is a solution:[𝛼 ↦→ int] ⊩ ⟨𝛼⟩(𝜆_. 𝛼 = int) holds.
We believe that the solver is right and the semantics iswrong, or rather, that the semantics fails to match our intuition of the semantics should be. Our intent is that the valueof a needed variable 𝛼 should not be guessed, but deduced –without knowing the constraint. A semantics that encourages guessing types out of thin air is simpler, but it does
not capture our intuition and we believe that it would becomplex and costly to implement in practice.
We are still looking for a stricter semantics that forbids thiskind of “out of thin air” solution, by imposing that the valueof 𝛼 is determined outside the frozen constraint. (This may
be similar to some works in type inference that some part oftheir derivations to be principal, to forbid over-specializedsolutions.) The question is how to do this while preserving
a declarative specification, as simple as possible.

Acknowledgments
We are very grateful to François Pottier and Didier Rémy forfruitful discussions on this work.

References
Oleg Kiselyov. How OCaml type checker works – or what polymorphismand garbage collection have in common. URL http://okmij.org/ftp/ML/generalization.html.
François Pottier. Hindley-Milner elaboration in applicative style. In ICFP,
September 2014a. URL http://gallium.inria.fr/~fpottier/publis/fpottierelaboration.pdf.
François Pottier. the Inferno library: https://gitlab.inria.fr/fpottier/inferno,2014b.