# Omnidirectional type inference for ML: principality any way

Alistair O'Brien, Didier Rémy, Gabriel Scherer

<figure><img src="image_1.png" /></figure>

## To cite this version:

Alistair O'Brien, Didier Rémy, Gabriel Scherer. Omnidirectional type inference for ML: principality any way. University of Cambridge, INRIA, IRIF, Université Paris Cité. 2025. hal-05438544

HAL Id: hal-05438544

https://inria.hal.science/hal-05438544v1

Submitted on 2 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Omnidirectional type inference for ML: principality any way

ALISTAIR O'BRIEN, University of Cambridge, United Kingdom

DIDIER RÉMY, INRIA, France

GABRIEL SCHERER, INRIA & IRIF, Université Paris Cité, France

The Damas-Hindley-Milner (ML) type system owes its success to *principality*, the property that every well-typed expression has a unique most general type. This makes inference predictable and efficient. Yet, principality is *fragile*: many extensions of ML-GADTs, higher-rank polymorphism, and static overloading-break it by introducing *fragile* constructs that resist principal inference. Existing approaches recover principality through *directional inference* algorithms, which propagate *known* type information in a fixed (or *static*) order (e.g. as in bidirectional typing) to disambiguate such constructs. However, the rigidity of a *static* inference order often causes otherwise well-typed programs to be rejected.

We propose *omnidirectional type inference*, where type information flows in a *dynamic order*. Typing constraints may be solved in any order, suspending when progress requires known type information and resuming once it becomes available, using *suspended match constraints*. This approach is straightforward for simply typed systems, but extending it to ML is challenging due to *let-generalization*. Existing ML inference algorithms type let-bindings let $x = e_1$ in $e_2$ in a fixed order-type $e_1$, generalize its type, and then type $e_2$. To overcome this, we introduce *incremental instantiation*, allowing partially solved type schemes containing suspended constraints to be instantiated, with a mechanism to incrementally update instances as the scheme is refined. Omnidirectionality provides a *general framework* for restoring principality in the presence of fragile features. We demonstrate its versatility on two fundamentally different features of OCaml: static overloading of record labels and datatype constructors and semi-explicit first-class polymorphism. In both cases, we obtain a *principal type inference algorithm* that is more expressive than OCaml's current typechecker.

## 1 Introduction

The Damas-Hindley-Milner (ML) [Damas and Milner 1982; Hindley 1969] type system has long occupied a sweet spot in the design space of strongly typed programming languages, as it enjoys the *principal types property*: every well-typed expression *e* has a most general type *σ* from which all other valid types for *e* are instances of *σ*. For example, the identity function $λx.x$ has the principal type $∀α.α → α$, generalizing types like int → int and bool → bool.

The existence of principal types in ML has important practical benefits. It makes inference predictable, compositional, and efficient: since every expression has a most general type, local typing decisions are always optimal, with no need for guessing or backtracking. Beyond inference, principality ensures that well-typedness is stable under common program transformations such as let-contraction (or inlining) and argument reordering.

Principality, however, is fragile. Many extensions of ML—such as extensible records with row-polymorphism [Garrigue 1998; Ohori 1995; Rémy 1989; Rémy and Vouillon 1997; Wand 1989] and higher-kinded types [Jones 1995b]—are *robust*: they preserve principality. Others, including GADTs [Garrigue and Rémy 2013; Schrijvers, Jones, Sulzmann and Vytiniotis 2009], higher-rank and first-class polymorphism [Garrigue and Rémy 1999; Odersky and Läufer 1996; Serrano, Hage, Jones and Vytiniotis 2020], and static overloading [Charguéraud, Bodin, Dunfield and Riboulet 2025], are *fragile*: they break principality under their *natural typing rules*.

This fragility can already be observed in OCaml through impredicative higher-rank (i.e., first-class) polymorphism, exposed by *polymorphic methods* [Garrigue and Rémy 1999] (green indicates typechecking success and red indicates failure):

Authors' Contact Information: Alistair O'Brien, University of Cambridge, Cambridge, United Kingdom, ajo41@cam.ac.uk; Didier Rémy, didier.remy@inria.fr, Paris, INRIA, France; Gabriel Scherer, gabriel.scherer@inria.fr, INRIA & IRIF, Université Paris Cité, Paris, France.
let self x = x#f x

OCaml

In OCaml, objects are defined as a collection of methods within **object ... end**, and accessed using `e#m`. Unlike Java or C++, OCaml uses *structural typing* for objects: object types are a list of method types between two chevrons e.g. `⟨f : α. α → α⟩`, where the method `f` has the polymorphic identity function type `∀α. α → α` (the `∀` being omitted in OCaml syntax). When typing `self` in the example above, one could *guess* the type of `x` to be either `⟨f : α. α → α⟩` or `⟨f : α. α → α → α⟩`—neither of which is strictly more general than the other, violating principality.

Principality can be recovered through explicit type annotations. The return type of overloaded datatype constructors may be annotated; polymorphic expressions can be annotated with a type scheme; and for GADTs, both the type of the match scrutinee and return type can be annotated with a rigid type, which is refined by type equalities introduced in each branch. In this example, the binding of `x` should be annotated with the higher-rank type `⟨f : α. α → α⟩`.

Every fragile construct has a corresponding *robust* form where the type annotation is mandatory—for instance, `(e#m : σ)` is the robust form of `e#m` for polymorphic method invocation. Robust forms preserve principality, but at the cost of being significantly more cumbersome to use. Fragile forms relieve this burden, but can only be elaborated into their robust counterpart if sufficient type information is already available from the context. Thus, typing fragile constructs ultimately amounts to identifying when type information is *known*.

Intuitively, by known information, we mean typing constraints that must hold—either from typing rules (e.g. application requires the function to have an arrow type) or programmer supplied type annotations. Yet, formulating a declarative specification for *when* type information is known is difficult: most specifications are often twisted with some direct or indirect algorithmic flavor in order to preserve principality and completeness.

The two dominant approaches thus far are *bidirectional type inference* [Pierce and Turner 1998] and *π-directional inference* [Garrigue and Rémy 1999]. Each impose some *static ordering of* inference, using it to propagate inferred types and user-provided annotations as *known* information.

While effective in many settings, the rigidity of a static ordering causes even simple examples whose type could easily be inferred to be rejected. For instance, OCaml accepts or rejects the following expression, depending on the position of the annotation:

let self₁₁ (x : ⟨f : α. α → α⟩) = if true then x#f x else x

OCaml

let self₁₂ x = if true then x#f x else (x : ⟨f : α. α → α⟩)

OCaml

We propose *omnidirectional type inference*, which relies on a *dynamic order of inference*. The solving of inference constraints may proceed in any order, suspending whenever progress requires *known* type information. Other constraints may continue to be solved; once the missing information becomes available (typically via unification), the suspended typing constraints are resumed.

We present *omnidirectionality* as a general framework for inference in the presence of fragile features. While this paper instantiates our framework for two concrete features in OCaml—static overloading and polymorphic object methods—its scope is broader: we expect it to extend to more richer features such as GADTs, polymorphic parameters [White 2023], and more generalized static overloading *à la* *Swift*.

Because our long-term goal is to integrate *omnidirectional inference* into OCaml’s *typechecker*, it must scale to ML-style polymorphism. While the idea of suspending constraints is not new (see §7), we show how suspended constraints can coexist with ML *local let-generalization*—an indispensable
feature of OCaml<fnref n="1" />—but one that makes suspended constraints uniquely difficult to implement and specify declaratively.

## Contributions

Section §2 introduces our setting: OCaml's static overloading of datatype constructors and record labels, and polymorphic methods. We review directional inference, its limitations, and motivate omnidirectional inference. To this end, we introduce our three key ideas: a new characterization of *known* type information, *suspended match constraints*, and *incremental instantiation*, and demonstrate how together they enable principal type inference for these fragile features. Before turning to technical developments, we also discuss the *limitations and trade-offs* of omnidirectionality.

The subsequent sections present our main contributions:

(§3) The OmniML calculus, an extension of ML featuring OCaml's static overloading of record labels and semi-explicit first-class polymorphism (§2.2). We give typing rules with a new declarative characterization of *known* type information.

(§4) A novel constraint language for omnidirectional inference, equipped with a semantics for suspended constraints. We describe the translation of OmniML programs to constraints representing typing problems, and establish the expected metatheoretic properties: soundness, completeness, and principality of inference.

(§5) A formal definition of our constraint solver as a series of non-deterministic rewriting rules, proved correct with respect to the constraint semantics. The rewriting rules detail our treatment for the interaction of let-generalization with suspended constraints via *incremental instantiation*, and the formal description can be directly related to an efficient implementation.

(§6) A description of an efficient implementation of our solver, including our treatment of suspended constraints and partial type schemes. Validating that omnidirectional inference for ML is practical.

Finally, §7 compares related work. Section §8 concludes with future work. Appendix §A contains a complete technical reference, collecting key definitions and figures for convenient lookup. All proofs are deferred to the appendices.

## 2 Overview

We ground our work in two fragile features of OCaml: *static overloading* of record labels and constructors, and *polymorphic object methods*. Both are useful in practice: static overloading is widely relied upon in large programs, and polymorphic methods make first-class polymorphism available within OCaml.

### 2.1 Static overloading of constructors and record labels

*Static overloading* denotes a form of overloading in which resolution is performed entirely at compile time, enabling the compiler to select a unique implementation without relying on runtime information—in contrast to *dynamic overloading*, which defers resolution to runtime via mechanisms such as dictionary-passing or dynamic dispatch. Many mainstream languages, such as C++, Rust, and Java, use static overloading; its appeal is that it provides a *zero-cost* abstraction.

OCaml supports a limited yet useful form of static overloading for record labels and datatype constructors. Ambiguity is resolved using *known type information* under its directional inference algorithm (discussed in §2.3). To illustrate static overloading in OCaml, consider two nominal record types with overlapping field names:

<footnote n="1">¹In contrast, Haskell only supports top-level implicit let-generalization.</footnote>
```
type point = { x : int; y : int }
type gray_point = { x : int; y : int; color : int }
```

With both definitions in scope, OCaml must statically disambiguate each field usage:

```
let one = { x = 42; y = 1337 }
OCaml OmniML

let ex_1 r = r.x
OCaml OmniML

let ex_2 (r : point) = r.x + r.y
OCaml OmniML

let ex_3 r = (r.x, (r : point).y)
OCaml OmniML
```

The type of expression one has the unambiguous type point, even though both point and gray_point define the fields x and y. This is because OCaml performs closed-world reasoning: the typechecker is able to unambiguously infer the type of one as point, since it is the only record type whose domain is `{ x, y }`. Similarly, `r.color` necessarily infers `gray_point` for the type of `r`.

By contrast, `r.x` is ambiguous unless the type of `r` is *known*. In `ex_1`, the type of `r` is unconstrained, so disambiguation fails.<fnref n="2" /> In `ex_2`, the annotation fixes the type of `r`, thus `r`'s type is *known* and resolves `r.x` and `r.y` unambiguously. In `ex_3`, the type of `r` can only be `point`: considering the second projection first, we learn that `r` must have the type `point`, and since it is `λ`-bound, this should make the first projection unambiguous. However, OCaml still rejects this example due to its *static order* of inference (§2.3).

*Default rules.* If local type information and closed-world reasoning are insufficient, OCaml falls back to a syntactic default: it selects the most recently defined compatible type. For example, OCaml accepts the following expression, when warnings are not turned into errors:<fnref n="2" />

```
let getx r = r.x
OCaml OmniML
```

The expression is compatible with both `point` and `gray_point`, since each defines a field `x`. But `gray_point` is chosen simply because it appears later in the source.

Such fallback behavior is inherently *non-principal*: it reflects the typechecker's decision to abandon principal inference and arbitrarily select a syntactic default when no unique type can be inferred. We therefore give no formal account of such “default rules”.

Defaulting also interacts poorly with OCaml's directional inference. Once the compiler selects a type, it commits to it—even if that choice causes errors downstream. Consider:

```
let ex_4 r = let x = r.x in x + (r : point).y
OCaml OmniML
```

Here, OCaml defaults to `gray_point` for `r` when typing `r.x`, and subsequently fails on `(r : point).y`. OmniML succeeds by suspending the resolution of `r.x` until it learns from `(r : point).y` that `r` has type `point`.

Since overloaded datatype constructors are analogous to record fields, we focus only on record fields in this work. Our prototype implementation (§6), however, supports both.

## 2.2 Polymorphic methods

Polymorphic methods [Garrigue and Rémy 1999] bring some System-F-like expressiveness to OCaml by allowing first-class polymorphism (impredicative higher-rank polymorphism) while preserving principal type inference.

<footnote n="2">²In fact, OCaml does not fail on ambiguous types, but instead applies a default resolution strategy: it emits a warning and selects the last matching type definition in scope. Here, this will amount to choosing the type `gray_point` for `r`. To check all our examples, use the options `-principal -w +41+18 -warn-error +41+18`, which enables principal type inference and escalates the associated warnings to errors.</footnote>
$e ::= [e : σ] | <e> | (e : τ) | ...$

$τ ::= [σ]^{ε} | ...$

$σ ::= τ | ∀α. σ | ∀ε. σ$

$ε ::= $

<figure><img src="image_3.png" /><figcaption>Fig. 1. Syntax and typing rules for polytypes from PolyML [Garrigue and Rémy 1999].</figcaption></figure>

*From polymorphic methods to polytypes.* Polymorphic methods can be translated into ordinary methods that carry a *polytype*: a boxed type scheme $[σ]^{ε}$ that can be explicitly unboxed at use sites. The purpose of the annotation variable $ε$ will be explained shortly. Boxed polytypes are considered to be (mono)types, enabling impredicativity. We write $[e : σ]$ to box a term $e$ with the scheme $σ$, and $<e>$ to unbox a polytype, instantiating it.

Concretely, the polymorphic method of **object method** id : $α$. $α \to α = \text{fun } x \to x \text{ end}$ is translated to **object method** id = [ fun $x \to x : α$. $α \to α$ ] end. Method invocation implicitly unboxes the polytype e.g. $x \# id$ becomes $<x \# id>$.

This reduction is useful for two reasons: (1) Inference for OCaml's object layer is largely governed by row-polymorphism, which is *robust* and does not threaten principality; it is therefore orthogonal to our concerns. In contrast, polytypes are *fragile*. (2) Polytypes underpin other features in OCaml, notably the recent addition of polymorphic function parameters [White 2013].

*Semi-explicit first-class polymorphism.* Polytypes expose the tricky interaction with principality of interest. For the remainder of this work, we therefore focus on polytypes—also called *semi-explicit first-class polymorphism* [Garrigue and Rémy 1999]—as originally formulated in the PolyML calculus, whose typing rules are collected in Figure 1.

Annotation variables record the origins of polytypes and may themselves be generalized, yielding type schemes such as $∀ε. [σ]^{ε}$. When $ε$ is generalized, the polytype is considered *known*, rather than still being inferred—this distinction is precisely the purpose of annotation variables.

The introduction form (POLYML-POLY) for polytypes is a boxing operator $[e : σ]$ with an explicit polytype annotation $σ$. The resulting expression has type $[σ_2]^{ε}$ where $ε$ is an arbitrary (typically fresh) annotation variable and $σ_2$ is a *freshened copy* of $σ_1$, i.e., a variant of $σ_1$ with only the annotation variables of $σ$ renamed (see POLYML-ANNOT below for details). Because $σ$ is supplied by the programmer, the polytype is treated as known: $[e : σ]$ also has the generalized type scheme $∀ε. [σ_2]^{ε}$. This is by design—the explicit annotation in $[e : σ]$ records that the polytype is known.

Conversely, to instantiate a polytype expression (POLYML-INST), one must use an explicit unboxing operator $<e>$, which requires no accompanying type annotation. However, the operator requires $e$ to have a *known* polytype scheme of the form $∀ε. [σ]^{ε}$ and then assigns $<e>$ the type $σ$. If, by contrast, $e$ has the type $[σ]^{ε}$ for some non-generalizable annotation variable $ε$, then $e$ is considered of a *not-yet-known* polytype, and therefore $<e>$ is ill-typed. This restriction enforces principality, preventing instantiation on *guessed* polytypes.

For example, the expression $λx. <x>$ is not typable. Indeed, the $λ$-bound variable $x$ is assigned a monotype. The only admissible type for $x$ is $x : [σ]^{ε}$ for some $σ$ and $ε$. Since $ε$ appears in the type of $x$ in the typing context at the point of typing $<x>$, it cannot be generalized prior to unboxing, rendering the term ill-typed.
POLYML-ANNOT can be used to freshen annotation variables. The auxiliary relation ($\sigma_1 : \sigma : \sigma_2$) (also used in POLYML-POLY) holds if there exists renamings $\eta_1, \eta_2$ on annotation variables (leaving ordinary type variables unchanged) and a type substitution $\theta$ such that $\sigma_1 = \theta(\eta_1(\sigma))$ and $\sigma_2 = \theta(\eta_2(\sigma))$. Intuitively, ($\sigma_1 : \sigma : \sigma_2$) first produces two fresh copies of $\sigma$, preventing unwanted sharing of annotation variables that could otherwise block generalization. It then instantiates the corresponding free type variables between these two copies using $\theta$. We usually omit annotation variables in source type annotations, since we can implicitly introduce fresh ones in their place.

For example, $\lambda x : [\sigma]. \langle x \rangle$, which is syntactic sugar for $\lambda x$. let $x = (x : [\sigma])$ in $\langle x \rangle$, is well-typed because the explicit annotation introduces a fresh variable annotation $\epsilon_1$, which can then be generalized, yielding $\forall \epsilon_1. [\sigma]^\epsilon_1$ for the type of the let-bound variable $x$.

## 2.3 Directional type inference

We now discuss the two main directional inference approaches: $\pi$-directional and bidirectional, illustrated using polytypes as a running example. We then discuss limitations of both approaches, providing us with the motivation for omnidirectional type inference.

**$\pi$-directional type inference.** Most ML type inference algorithms proceed in a fixed order when typechecking let-bindings let $x = e_1$ in $e_2$: first typecheck the definition $e_1$, generalize its type, and then typecheck the body $e_2$ under the extended environment. $\pi$-directionality, originating from PolyML (§2.2), leverages this ordering to resolve overloaded or ambiguous constructs in a *principal* way. The key point is that this ordering reveals which types are *known*, namely types that are fixed by generalization—and therefore stable enough to guide disambiguation.

A type $\tau$ (e.g. $[\sigma]^\epsilon$) is considered *known* if its annotation variables are eligible for generalization (e.g. $\forall \epsilon. [\sigma]^\epsilon$). Conversely, types with monomorphic annotation variables are considered *not-yet-known* and cannot be relied on for disambiguation.

We call this $\pi$-directional (read as “pi-directional”) type inference, to mean that *polymorphic expressions must be typed before their instances*. $\pi$-directionality is subtle, but it aligns with the implicit inference order already present in most ML-like typecheckers, making it straightforward to retrofit into existing implementations. For OCaml, the mechanism for annotation variables even comes for free, as a byproduct of the extensive optimizations in its inference algorithm.

Building on its introduction in PolyML, $\pi$-directionality was later used by Le Botlan and Rémy [2009] for empowering ML$^F$. It has since been adopted in OCaml for features such as polymorphic object methods and the overloading of record fields and variant constructors. More generally, OCaml uses $\pi$-directionality whenever the typechecker employs type-based disambiguation.

To illustrate $\pi$-directionality, consider:<fnref n="3" />

```
let pid = [ fun x -> x : α. α -> α ]
let ex₅ = let p = pid in ⟨p⟩
let ex₆ = (fun p -> ⟨p⟩) pid
```

OCaml OmniML
OCaml OmniML
OCaml OmniML

At first glance, $ex_5$ and $ex_6$ appear equivalent: both simply instantiate the polytype bound to $p$. Yet, OCaml accepts $ex_5$ and rejects $ex_6$. This is because the let-binding in $ex_5$ allows $p$ to have type scheme $\forall \epsilon. [\forall \alpha. \alpha \to \alpha]^\epsilon$, and thus its type is considered *known*—permitting unboxing (POLYML-INST). In $ex_6$, by contrast, $p$ is monomorphic at the point of instantiation as it is $\lambda$-bound, and unboxing is therefore forbidden.

<footnote n="3">³In OCaml, these examples can be typechecked by translating `[e : σ]` to **object method** $f : σ = e$ end and $\langle e \rangle$ to `e#f`. This translation is the inverse of that discussed in §2.2.</footnote>
To emphasize that this behavior is specification-driven and not an artifact of OCaml's inference algorithm, consider two equivalent versions of $ex_6$:<fnref n="4" />

let $ex_{62} = \text{app} (\text{fun } p \to \langle p \rangle) \text{ pid}$ OCaml OmniML

let $ex_{63} = \text{rev\_app} \text{ pid} (\text{fun } p \to \langle p \rangle)$ OCaml OmniML

While these terms are semantically equivalent, they highlight a potential hazard: their typability may vary under a directionally biased inference algorithm, depending on whether the function or argument is typed first. To limit such implementation-dependent behavior, OCaml infers all subexpressions in an *order-independent* manner until they are let-bound. Consequently, OCaml does not make any distinction between $ex_6$, $ex_{62}$, and $ex_{63}$.

Treating both examples uniformly is in one sense a strength of $\pi$-directionality, but it also reveals a limitation: annotability is fragile, in that well-typedness depends on the *precise* placement of annotations, often forcing the programmer to introduce annotations that would otherwise be unnecessary. For instance, the following two terms differ only in the position of the annotation, yet only the one on the left-hand side is well-typed in OCaml—while they are both well-typed in OmniML:

let $\text{self}_{21} x = \langle (x \cdot [\alpha. \alpha \to \alpha]) \rangle x$ OCaml OmniML

let $\text{self}_{22} x = \langle x \rangle (x : [\alpha. \alpha \to \alpha])$ OCaml OmniML

**Bidirectional type inference.** Bidirectional type inference is a standard alternative to unification for propagating type information. It is typically formulated by splitting typing rules into two modes: *checking mode* ($\Gamma \vdash e \Leftarrow \tau$), which typechecks a term *e* against a type *τ* in a given context, and *inference mode* which infers *e*'s type from the context alone ($\Gamma \vdash e \Rightarrow \tau$).

The type system designer assigns modes—checking or inference—to each language construct. For instance, one can decide to typecheck function applications $e_1 e_2$ by first *inferring* that $e_1$ has some function type $\tau_1 \to \tau_2$, and then *checking* $e_2$ against $\tau_1$ (*SYN-APP*); but the opposite, mode-correct choice (*CHK-APP*) is also possible:

$$ \frac{\text{SYN-APP} \quad \begin{array}{l} \Gamma \vdash e_1 \Rightarrow \tau_1 \rightarrow \tau_2 \\ \Gamma \vdash e_2 \Leftarrow \tau_1 \end{array}}{\Gamma \vdash e_1 \quad e_2 \Rightarrow \tau_2} $$

$$ \frac{\text{CHK-APP} \quad \begin{array}{l} \Gamma \vdash e_1 \Leftarrow \tau_1 \rightarrow \tau_2 \\ \Gamma \vdash e_2 \Rightarrow \tau_1 \end{array}}{\Gamma \vdash e_1 \quad e_2 \Leftarrow \tau_2} $$

Within the bidirectional framework, a type $\tau$ is *known* when it is either: (1) part of an annotation, (2) supplied as input to a checking judgment in the conclusion ($\Gamma \vdash e \Leftarrow \tau$), or (3) produced by a synthesizing premise ($\Gamma \vdash e \Rightarrow \tau$).

Using this discipline, we can recast polytypes and eliminate two artifacts needed in our $\pi$-directional presentation: explicit annotations on boxing and annotation variables. Since ($e : \tau$) already propagates known information, [*e*] requires no attached annotation; and because “knownness” now follows from inference modes rather than polymorphism, annotation variables are unnecessary. The resulting syntax and typing rules are as follows:

$e ::= [e] | \langle e \rangle | (e : \tau) | \dots$ Terms

$\tau ::= [\sigma] | \dots$ Types

$\sigma ::= \tau | \forall \alpha. \sigma$ Type schemes

$$ \frac{\text{CHK-POLY} \quad \begin{array}{l} \Gamma \vdash e \Leftarrow \sigma \\ \Gamma \vdash [e] \Leftarrow [\sigma] \end{array}}{\Gamma \vdash [e] \Leftarrow [\sigma]} $$

$$ \frac{\text{SYN-INST} \quad \begin{array}{l} \Gamma \vdash e \Rightarrow [\sigma] \\ \Gamma \vdash \langle e \rangle \Rightarrow \sigma \end{array}}{\Gamma \vdash [e] \Rightarrow [\sigma]} $$

$$ \frac{\text{SYN-ANNOT} \quad \begin{array}{l} \Gamma \vdash e \Leftarrow \tau \\ \Gamma \vdash (e : \tau) \Rightarrow \tau \end{array}}{\Gamma \vdash (e : \tau) \Rightarrow \tau} $$

However, there is usually no optimal assignment of modes: for any choice of modes, some programs will typecheck successfully, while others will fail unnecessarily. Yet, the typing rules must irrevocably commit to a fixed set of modes, after which, principal types often exist, but only

<footnote n="4">⁴app and rev\_app are the application function `fun f x → f x` and the reverse application function `fun x f → f x`, respectively.</footnote>
with respect to a specification that made non-principal choices to begin with. For instance, $ex_6$ would be ill-typed using the above rules for polytypes (with SYN-APP).

Recent work on contextual typing [Xue and d. S. Oliveira 2024] addresses this difficulty by deferring the commitment between SYN-APP and CHK-APP. Typing multiple arguments from right to left (CHK-APP) when sufficient contextual information is available, and thus successfully typechecks $ex_6$. Nevertheless, it still enforces a fixed order of propagation, so some well-typed programs are rejected as ill-typed (e.g. $ex_{62}$, $ex_{63}$).

In parallel, QuickLook [Serrano, Hage, Jones and Vytiniotis 2020] and Frost [Tang, Jiang, Oliveira and Lindley 2025] take a pragmatic approach to mitigating order-dependence in applications. Both target impredicative higher-rank polymorphism, using partial approximations of function and argument types to guide type inference at the point of application. This enables a limited form of argument reordering, where information from later arguments can influence the typing of earlier ones within an application spine. In practice, these mechanisms work well, but they still enforce a fixed overall direction of propagation between surrounding constructs (e.g. let-bindings).

*Limitations of directional type inference.* Bidirectional type inference is lightweight, practical, and well-suited for complex language features such as higher-rank polymorphism, dependent types, or subtyping. It supports the propagation of type information with minimal annotations. Its main downside lies in the need to fix an often arbitrary flow of type information—as in the case of function applications discussed above.

On the other hand, $\pi$-directional type inference appears better suited for ML: (1) thanks to its use of polymorphism—the essence of ML; and (2) its ability to be retrofitted easily onto existing typecheckers. But it remains surprisingly weak in some cases: it does not even allow the propagation of user-provided type annotations from a function to its argument! This weakness is sometimes counter-intuitive to the user. For example, the following would be rejected as ambiguous using $\pi$-directional type inference alone:

```
let ex_7 =
    OCaml
    OmniML
let g (f : [ α. α → α ] → int) = f pid in
    g (fun p → ⟨p⟩ 42)
```

Here, $p$ is $\lambda$-bound and therefore monomorphic. Without further propagation, the term $⟨p⟩$ would be ambiguous, as no polymorphic (and thus *known*) type can be ascribed to $p$. OCaml resolves this by supplementing $\pi$-directional inference with a form of bidirectional propagation: the expected type of $g$'s parameter $[ α. α → α ] → int$ is bidirectionally propagated to the application of $g$, assigning $p$ to have the *known* type $[ α. α → α ]$ and thereby disambiguating $⟨p⟩$.

## 2.4 Omnidirectional type inference

Omnidirectional inference infers typing constraints in any order. Constraints advance *dynamically*; those that require *known* type information suspend, and resume when other constraints supply it. This stands in contrast to the fixed *static* order of bidirectional and $\pi$-directional inference.

Consider again $ex_{62}$, $ex_{63}$ from §2.3:

```
let ex_{62} = app (fun p → ⟨p⟩) pid
    OmniML
let ex_{63} = rev_app pid (fun p → ⟨p⟩)
    OmniML
```

Under $\pi$-directionality, both terms are ill-typed; under a bidirectional approach (using SYN-APP), only $ex_{62}$ is rejected. Yet both terms have a principal type—it is merely a question of propagating type information in the right order. Omnidirectional type inference typechecks both: since it allows the typing of either side to proceed first, suspending the other until the relevant type information is *known*.
*To be or not to be known.* That is the question, indeed. To specify omnidirectionality declaratively, we must say when a type is considered *known* without relying on any fixed directional order. Our key idea is that a type is *known* when it is the *unique* type that can be inferred within some surrounding term context $\mathscr{C}$.

Take $\mathrm{ex}_{62}$ as an example, using the following term context where $\square$ denotes the hole:

let pid = [ fun x → x : α. α → α ]

let $\mathrm{ex}_{62} = \mathrm{app} (\mathrm{fun} \ p \to \square) \mathrm{pid}$

Here, $p$ has a uniquely inferrable type $[\forall \alpha. \alpha \to \alpha]$, no other type can be inferred for $p$. As a result, we can consider $p$'s type *known*.

Once the type is known, the fragile implicit term can be elaborated to a robust explicit counterpart. For example, the unboxing $\langle p \rangle$ can be elaborated into the explicitly annotated form $\langle p : \alpha. \alpha \to \alpha \rangle$. Consequently, to typecheck $\langle e \rangle$ under

the context $\mathscr{C}$, it suffices to assert that $e$ has the known polytype $[\sigma]$ and elaborate $\langle e \rangle$ into an annotated unboxing $\langle e : \sigma \rangle$, as captured by **USE-I**. The predicate $\mathscr{E}[e \triangleright [\sigma]]$—our *unicity condition*— formalizes precisely what it means for a type to be *known*. We defer its technical definition, which is rather subtle, to §3.4.

*Suspension in action.* Suspension is the mechanism that allows inference to proceed in any order, in spite of constructs that require *known* type information. In our framework, we realize this through our novel primitive: *suspended match constraints*.

A match constraint (match $\tau$ with $\overline{\rho} \Rightarrow \overline{C}$) pairs a (typically unknown) matchee type $\tau$ with a finite series of shape-pattern branches $\overline{\rho} \Rightarrow \overline{C}$. Such constraints remain *suspended* until the *shape* of $\tau$ (i.e., its top-level constructor) is known. Then, they are *discharged*: a unique branch is selected and its associated constraint has to be solved. A match constraint that is never discharged is considered unsatisfiable.

For now, it suffices to think of shapes as parts of types (e.g. the type constructor $T$ in $T \tau^5$) while shape patterns $\rho$ act as type 'destructors', binding parts of the type (e.g. the constructor name $T$) to meta-variables (e.g. the pattern variable $t$) used in $\overline{C}$. This will be made precise in §3.3.

We now illustrate the role of suspended constraints on our running *fragile* features: static overloading of records (and variants) and semi-explicit first-class polymorphism. Each feature translates the typability of the term into constraints, formalized using a constraint generation function of the form $[[e : \tau]]$, which, given a term $e$ and expected type $\tau$, produces a constraint $C$ which is satisfiable if and only if $e$ has the type $\tau$. As we will see, once we adopt the suspended constraint machinery developed in this paper, much of the complexity of these typing fragile constructs vanishes—suspended constraints do most of the heavy lifting.

For an ambiguous record projection $e.\ell$, we generate the typing constraint:

$$[[e.\ell : \tau]] \triangleq \exists \alpha. [[e : \alpha]] \wedge \text{match } \alpha \text{ with } \text{rcd } t \Rightarrow t.\ell \le (\alpha \to \tau)$$

This constraint introduces the unification variable $\alpha$, unifying it with the type of $e$ (via $[[e : \alpha]]$), and suspends resolution of the return type $\tau$ until the type $\alpha$ of $e$ becomes *known* to be some non-variable type $\tau_0$. The branch then matches $\tau_0$ against the record type pattern ($\text{rcd } t$). If $\tau_0$ is a record type ($\text{rcd } T \tau_1$) for some ground record name $T$, then the record name variable $t$ in the pattern is bound to $T$, otherwise the whole constraint fails. When $t$ is bound to $T$, the right-hand-side constraint becomes $T.\ell \le (\alpha \to \tau)$, which requires that the type of the projection of the label $\ell$ at type $T$ in the global record-declaration environment can be instantiated into $(\alpha \to \tau)$.

<footnote n="5">⁵Type constructors are prefixed, except in OCaml code, where they are postfixed.</footnote>
When typechecking the polytype unboxing operator $\langle e \rangle$, if $e$ is already known to have the type $[\sigma]$, then we can simply instantiate $\sigma$. However, if the type of $e$ is not yet known—i.e., it is a (possibly constrained) type variable $\alpha$—then we must defer until more information is available. We capture this behavior with a suspended match constraint:

$$ \llbracket \langle e \rangle : \tau \rrbracket \triangleq \exists \alpha. \llbracket e : \alpha \rrbracket \wedge \text{match } \alpha \text{ with } [s] \Rightarrow s \le \tau $$

The match remains suspended until $\alpha$ resolves to some type $\tau_0$. If, upon resolution, $\tau_0$ is $[\sigma]$, the pattern $[s]$ matches successfully, binding $\sigma$ to the polytype variable $s$ and performs the instantiation $\sigma \le \tau$. Otherwise, the pattern does not match and the constraint fails.

**Scaling to ML.** In the absence of (implicit) polymorphism, type inference is solely based on unification constraints which can be solved in any order; omnidirectional inference with suspended match constraints is then natural and easy to implement.

The difficulty originates from ML implicit let-polymorphism for which all known implementations follow the $\pi$-order: first typing the binding, generalizing it into a type scheme, and finally typing the body under the extended typing environment that binds the generalized scheme. The Hindley-Milner algorithm $\mathcal{J}$, its variants $\mathcal{W}$ or $\mathcal{M}$ [Lee and Yi 1998], or more flexible constraint-based type inference implementations [Odersky, Sulzmann and Wehr 1999; Pottier and Rémy 2005; Rémy 1990, 1992] all follow this strategy, to the best of our knowledge.

Consider the following program:

``` OCaml
type α gpoint = { x : α; y : α }
let diag (n : α) : α gpoint = { x = n; y = n }
let ex₈ gp = let getx p = p.x in getx (diag 42), (getx gp : float) OCaml OmniML
```

We introduce a new parameterized record type $\alpha$ gpoint, whose fields $x$ and $y$ are overloaded—recall that both point and gray_point already define these fields—but here they have a *polymorphic* projection type $\forall \alpha$. $\alpha$ gpoint $\rightarrow \alpha$. The function diag constructs a diagonal point, a point lying on the diagonal $x = y$, and has the type $\forall \alpha$. $\alpha \rightarrow \alpha$ gpoint.

When typechecking ex₈, we cannot infer the type of getx first, since the type of p.x is still not yet known. Instead, we must typecheck the body first, where the call getx (diag 42) reveals that p has type $\alpha$ gpoint. Failing to do so would make inference incomplete, since the program is clearly well-typed. Nor can we treat the let-binding as monomorphic, since both calls to getx use different instantiations of $\alpha$: $\alpha := \text{int in getx (diag 42)}$ and $\alpha := \text{float in (getx gp : float)}$.

We solve this by introducing *incremental instantiation*, i.e., the ability to instantiate type schemes that are not yet fully determined (so-called *partial type schemes*) and consequently revisit their instances when they are being refined, *incrementally*. This allows inferring parts of a let-body to disambiguate its definition, without duplicating constraint-solving work.

*The forest, not the trees.* Suspended match constraints offer a general framework to typing the features we have considered so far, and more. Some of those features can be handled using more specialized approaches: for example, SML employs row variables to support overloaded fields for structural records, while GHC uses qualified types to allow overloading of nominal record fields with a simple-enough type.

In contrast to these specialized mechanisms, suspended constraints are more expressive. They can handle cases where the typing rule to use on the subterms depends on the outcome of dis-ambiguation, such as overloaded polymorphic record fields or overloaded GADT constructors in patterns. Moreover, these simpler approaches typically lack a declarative semantics that justify rejecting programs with unresolved disambiguation choices.
## 2.5 Limitations

Omnidirectional inference is powerful, but not omnipotent: (1) some programs are still rejected as ambiguous, even though a unique elaboration could in principle be chosen—a deliberate “Goldilocks” compromise; (2) our current formalization cannot disambiguate based on the *return type* of overloaded projections; (3) it presently omits a formalization of *default rules* (§2.1); and (4) our framework entails a higher conceptual and implementation complexity than static directional approaches (e.g. bidirectional typechecking).

*Not too hot, not too cold.* Some expressions must be rejected even though their elaboration would be unambiguous. Consider:

``` type cie_color = { x : int; y : int; z : int } type cie_point = { x : int; y : int; color : cie_color } let ex_10 r = r.color.x OCaml OmniML
```

Neither field projections in `ex_10` can individually be disambiguated. However, if one were allowed to combine the constraints, they would jointly determine that `r` must have type `cie_point`: in `gray_point`, the field `color` has type `int`, and hence cannot itself be projected, leaving a unique consistent elaboration: `r.cie_point.color.cie_color.x`<fnref n="6" />.

Our framework nonetheless rejects `ex_10`. This is intentional: overloaded projections must be elaborated sequentially, each in isolation, rather than jointly with others. We view this restriction as a “Goldilocks” compromise: it rules out examples like the above, but avoids the intractability of full general overloading which is NP-hard, even without let-polymorphism, as shown by a reduction from 3-SAT [Charguéraud, Bodin, Dunfield and Riboulet 2025].

*No returns accepted.* At present, our system also resolves overloaded projections without taking their *return type* into account.

``` let ex_11 r = (r.x : cie_color) OCaml OmniML
```

Under the rules defined in this work, programs such as `ex_11` are rejected. This limitation is shared with existing languages such as OCaml, Haskell, and SML, none of which use the *return type* of a projection to guide disambiguation. Our framework already goes beyond these systems, but we believe that omnidirectionality provides the right foundation to incorporate *return type disambiguation*. We leave this refinement to future work.

*No defaults, by default.* We do not yet provide a formal account of *default rules* mentioned in §2.1. However, our prototype implementation, discussed in §6, does support (optionally) attaching a default strategy to each suspended constraint. In practice, defaulting proves useful and appears essential for certain features such as polymorphic parameters [White 2023]. Developing a formal treatment of defaulting within our framework is an important direction for future work.

*On complexity budgets.* Omnidirectional type inference is conceptually straightforward but technically challenging. It follows a simple key idea: solving constraints in any order, suspending when known type information is required. However, realizing this idea precisely and efficiently comes at a higher complexity cost than bidirectional or $\pi$-directional type inference.

(§3) Giving a declarative characterization of *known type information* without statically relying on directionality is hard. Our contextual rules nicely solve this problem, but their meta-theory is unsurprisingly more complex than local rules.

<footnote n="6">⁶The syntax `e.T.l` qualifies the label `l` to unambiguously belong to the type `T` in the projection.</footnote>
$\alpha, \beta, \gamma \in \mathcal{V}$

$\tau ::= \alpha | 1 | \tau_1 \rightarrow \tau_2 | \text{rcd } T \bar{\tau} | [\sigma]$

$\sigma ::= \tau | \forall \alpha. \sigma$

$T$

$\mathfrak{g} \in \mathcal{G}$

$e ::= x () | \lambda x. e | e_1 e_2 | \text{let } x = e_1 \text{ in } e_2 | (e : \exists \tilde{\alpha}. \tau)$
$\qquad | [e] | [e : \exists \tilde{\alpha}. \sigma] | \langle e \rangle | \langle e : \exists \tilde{\alpha}. \sigma \rangle$
$\qquad | \{\tilde{l} = e\} | e.\tilde{l} | T.\{\tilde{l} = e\} | e.T.\tilde{l}$

$\Gamma ::= \emptyset | \Gamma, x : \sigma$

$\Omega ::= \emptyset | \Omega, T.\ell : \forall \tilde{\alpha}. \text{rcd } T \tilde{\alpha} \rightarrow \tau$

$\zeta ::= v \tilde{y}. \tau$ ( $\zeta \in \mathcal{S}$ )

$\zeta \in \mathcal{S}_{\text{canon}}$ ($\mathcal{S}_{\text{canon}} \subset \mathcal{S}$)

$\mathsf{VAR}$
$$ \frac{x : \sigma \in \Gamma}{\Gamma \vdash x : \sigma} $$

$\mathsf{FUN}$
$$ \frac{\Gamma, x : \tau_1 \vdash e : \tau_2}{\Gamma \vdash \lambda x. e : \tau_1 \rightarrow \tau_2} $$

$\mathsf{APP}$
$$ \frac{\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2}{\Gamma \vdash e_1 e_2 : \tau_1} $$

$\mathsf{UNIT}$
$$ \frac{}{\Gamma \vdash () : 1} $$

$\mathsf{GEN}$
$$ \frac{\Gamma \vdash e : \sigma \qquad \alpha \# \text{fv}(\Gamma)}{\Gamma \vdash e : \forall \alpha. \sigma} $$

$\mathsf{INST}$
$$ \frac{\Gamma \vdash e : \forall \alpha. \sigma}{\Gamma \vdash e : \sigma[\alpha := \tau]} $$

$\mathsf{LET}$
$$ \frac{\Gamma \vdash e_1 : \sigma}{\Gamma \vdash \text{let } x = e_1 \text{ in } e_2 : \tau} $$

$\mathsf{ANNOT}$
$$ \frac{\Gamma \vdash e : \tau[\tilde{\alpha} := \tilde{\tau}]}{\Gamma \vdash (e : \exists \tilde{\alpha}. \tau) : \tau[\tilde{\alpha} := \tilde{\tau}]} $$

$\mathsf{POLY-X}$
$$ \frac{\Gamma \vdash e : \sigma[\tilde{\alpha} := \tilde{\tau}]}{\Gamma \vdash [e : \exists \tilde{\alpha}. \sigma] : [\sigma[\tilde{\alpha} := \tilde{\tau}]]} $$

$\mathsf{USE-X}$
$$ \frac{\Gamma \vdash e : [\sigma][\tilde{\alpha} := \tilde{\tau}]}{\Gamma \vdash \langle e : \exists \tilde{\alpha}. \sigma \rangle : \sigma[\tilde{\alpha} := \tilde{\tau}]} $$

$\mathsf{RCD-X}$
$$ \frac{\text{dom}(\Omega(T)) = \bar{\ell} \qquad (T.\ell_i \le \tau \rightarrow \tau_i)_{i=1}^n}{\Gamma \vdash T.\{\ell_1 = e_1; \dots; \ell_n = e_n\} : \tau} $$

$\mathsf{RCD-CLOSED}$
$$ \frac{\bar{\ell} \blacktriangleright T \qquad \Gamma \vdash T.\{\overline{\ell = e}\} : \tau}{\Gamma \vdash \{\overline{\ell = e}\} : \tau} $$

$\mathsf{RCD-PROJ-X}$
$$ \frac{T.\ell \le \tau_1 \rightarrow \tau_2}{\Gamma \vdash e : \tau_1} $$

$\mathsf{RCD-PROJ-CLOSED}$
$$ \frac{\ell \triangleright T \qquad \Gamma \vdash e.T.\ell : \tau}{\Gamma \vdash e.\ell : \tau} $$

$\mathsf{LAB-INST}$
$$ \frac{\Omega(T.\ell) = \forall \tilde{\alpha}. \text{rcd } T \tilde{\alpha} \rightarrow \tau}{T.\ell \le (\text{rcd } T \tilde{\tau} \rightarrow \tau[\tilde{\alpha} := \tilde{\tau}])} $$

<caption>Fig. 2. Syntax and explicit, robust typing rules of OmniML.</caption>

(§6) Implementing efficient incremental instantiation is non-trivial in comparison to ordinary ML instantiation, as refinements of partial type schemes must trigger re-instantiations without introducing redundant constraint solving across successive instantiations of the same scheme.

We hope to pay off some of this complexity in future work; in particular, we believe omnidirection-
ality is the missing piece to unlock modular implicits—an approach to generalized overloading and
a long-anticipated feature within the OCaml community.
## 3 The OmniML calculus

To prove correctness of type inference, we must define a language and its type system. Identifying an appropriate declarative type system to use as a specification is itself a challenging problem. In particular, natural specifications for fragile features often fail to preserve principality.

Consider records, for instance. We can ask the user to provide a type annotation by using an explicit record projection e.T.ℓ, which has a simple typing rule (RCD-PROJ-X in Figure 2). By contrast, the natural typing rule for the overloaded projections e.ℓ breaks principality (RCD-PROJ-I-NAT). For example, term λr. r.x admits two incompatible types, point → int and gray_point → int, as explained in §1.

To restore principality for overloaded projections, we require that the type of e be known—that is, determined to be a specific record type rcd T $\bar{\tau}$, rather than merely guessed. As discussed earlier (§2.4), this requirement is expressed via a unicity condition, giving rise to the contextual rule RCD-PROJ-I (Figure 3), which elaborates the fragile overloaded projection e.ℓ into its robust explicit counterpart e.T.ℓ.

$$ \begin{array}{l} \text{RCD-PROJ-I-NAT} \\ T.\ell \le \tau_1 \rightarrow \tau_2 \\ \Gamma \vdash e : \tau_1 \\ \hline \Gamma \vdash e.\ell : \tau_2 \end{array} $$

### 3.1 Syntax

OmniML (Figure 2) extends ML with two fragile constructs: polytypes and nominal records. Variants are not treated formally in OmniML, but behave analogously to records.

*Notation for collections.* We write $\overline{X}$ for a (possible empty) set of elements {$X_1, \dots, X_n$} and a (possibly empty) sequence $X_1, \dots, X_n$. The interpretation of whether $\overline{X}$ is a set or a sequence is often implicit. We write $\overline{X} \# \overline{X}'$ as a shorthand for when $\overline{X} \cap \overline{X}' = \emptyset$. We write $\overline{X}, \overline{X}'$ as the union or concatenation (depending on the interpretation) of $\overline{X}$ and $\overline{X}'$. We often write X for the singleton set (or sequence).

*Types.* Monotypes (or just types) include, as usual, type variables $\alpha$, the unit type 1, arrow types, but also nominal record types rcd T $\bar{\tau}$, and polytypes [$\sigma$]. We use a non-standard syntax rcd T $\bar{\tau}$ for record types, where T is a record name and $\bar{\tau}$ a list of type parameters.<fnref n="7" /> Type schemes $\sigma$ are of the form $\forall \bar{\alpha}. \tau$, they are equal up to the reordering of binders and removal of useless variables. Standard notions such as the set of free variables $fv(\sigma)$ and capture-avoiding substitutions $\sigma[\alpha := \tau]$ are defined in the usual way. We write $\mathcal{V}$ for the set of type variables, and use $\bar{\alpha} \# \sigma$ as a short-hand for $\bar{\alpha} \# fv(\sigma)$. Finally, $g \in \mathcal{G}$ denotes a ground type—a type with no free variables.<fnref n="8" />

*Terms.* Terms of OmniML are variables x, the unit literal (), lambda-abstractions $\lambda x. e$, applications $e_1 e_2$, annotations ($e : \exists \bar{\alpha}. \tau$), and let-bindings let $x = e_1$ in $e_2$, extended with the following expressions:

* For polytypes, we introduce implicit and explicit boxing and unboxing forms: $[e]$, $[e : \exists \bar{\alpha}. \sigma]$, and $\langle e \rangle$, $\langle e : \exists \bar{\alpha}. \sigma \rangle$ respectively.

* Overloaded record labels include record literals {$\ell_1 = e_1 ; \dots ; \ell_n = e_n$} and field projections e.ℓ. Both constructs have explicit counterparts: T.{$\ell_1 = e_1 ; \dots ; \ell_n = e_n$} and e.T.ℓ, where the explicit record annotation T._ indicates that the labels unambiguously belong to the record type T.

All annotations in OmniML are closed i.e., their quantified variables $\bar{\alpha}$ are exactly the free variables of the type $\tau$ or type scheme $\sigma$. We use $e^i$ to range over fragile, implicit terms (e.g. e.ℓ) and $e^x$ for their explicit counterparts (e.g. e.T.ℓ).

<footnote n="7">⁷Using T as an argument of (rcd T $\bar{\tau}$) rather a head constructor (T $\bar{\tau}$) will make record shape patterns easier to understand.</footnote>

<footnote n="8">⁸g can be pronounced “Fraktur g” or just “ground g”.</footnote>
Typing rules for explicit terms are mostly standard; nominal records require a more intricate (yet largely folklore) treatment of closed world reasoning. The crux of our work is the novel typing of the fragile constructs, presented in §3.4.

## 3.2 Typing rules for robust, explicit constructs

As usual, the main typing judgment $\Gamma \vdash e : \sigma$ (Figure 2) states that in context $\Gamma$, the expression $e$ has the type (scheme) $\sigma$. Rules `VAR` through `LET` are standard. Annotations $(e : \exists \tilde{\alpha}. \tau)$ (`ANNOT`) ensures that the type of $e$ is (an instance of) the type $\tau$. The type variables $\tilde{\alpha}$ are *flexibly* (or existentially) bound in $\tau$, meaning they may be instantiated to some types $\tilde{\tau}$ so that the resulting annotation matches the type of $e$. For instance, the term $(\lambda x. x + 1 : \exists \alpha. \alpha \to \alpha)$ is well-typed under `ANNOT` with the substitution $[\alpha := \text{int}]$.

**Explicit polytypes.** `POLY-X` serves as the introduction rule: given the (closed) type scheme $\sigma$, it forms a first-class polytype $[\sigma]$, requiring the expression $e$ to be at least as polymorphic as $\sigma$. `USE-X` is the corresponding elimination rule, unpacking an expression of polytype $[\sigma]$ into one of polymorphic type $\sigma$, which may be freely instantiated (via `INST`). Both rules also allow polytype annotations to be partial, i.e., $\sigma$ may have free type variables $\tilde{\alpha}$, which are existentially quantified to close the annotation, as in `ANNOT`.

**Explicit nominal records.** We assume a global label context $\Omega$ mapping labels to their projection type, i.e., type schemes of the form $\forall \tilde{\alpha}. \text{rcd } T \tilde{\alpha} \to \tau$. A label $\ell$ may belong to multiple record types, but is unique within each record type $T$. We write $\Omega(T)$ for the set of labels belonging to the record type $T: \Omega(T) \triangleq \{\ell : T.\ell : \forall \tilde{\alpha}. \text{rcd } T \tilde{\alpha} \to \tau \in \Omega\}$. We write $\Omega(T.\ell)$ for the unique scheme $\forall \tilde{\alpha}. \text{rcd } T \tilde{\alpha} \to \tau$ associated with $\ell$ in $T$ (if defined).

Label instantiations are typed by an auxiliary judgment $T.\ell \le \tau_1 \to \tau_2$ defined by `LAB-INST` and meaning that $\tau_1 \to \tau_2$ is an instance of the projection scheme $\Omega(T.\ell)$. Explicit field projections (`RCD-PROJ-X`) require that $e.T.\ell$ projects from a record $e$ of type $\tau_1$ to $\tau_2$, provided $T.\ell \le \tau_1 \to \tau_2$ holds. Explicit records (`RCD-X`) are typed similarly, checking that each field has the appropriate type. In addition, the premise asserts that the fields $\tilde{\ell}$ appearing in the record expression exactly match the labels of $T$ (i.e., dom $(\Omega(T))$).

Following OCaml, our explicit system also supports closed-world reasoning, which exploits the absence of ambiguity in the label context $\Omega$ to infer record annotations. In particular, in a record expression $\{\ell_1 = e_1 ; \dots ; \ell_n = e_n\}$, if the set of labels $\ell_1, \dots, \ell_n$ uniquely identifies a record type $T$ in the context $\Omega$, then the record has the type of $T.\{\ell_1 = e_1 ; \dots ; \ell_n = e_n\}$ (via `RCD-CLOSED`). Similarly, if the label $\ell$ is associated with exactly one record type $T$ in $\Omega$, then the projection $e.T.\ell$ has the type of $e.T.\ell$ (by `RCD-PROJ-CLOSED`).

These two forms of label uniqueness differ. A closed set of labels may uniquely identify a record type even if no individual label is unique. Conversely, a unique label implies uniqueness of every closed set containing it. For instance, recall one from §2.1:

``` OCaml
type point = { x : int; y : int }
type gray_point = { x : int; y : int; color : int }
let one = { x = 42; y = 1337 }
```

Here, the closed set $\{x, y\}$ in one uniquely identifies point, even though the individual labels $x$ and $y$ also appear in gray_point.

We formalize this closed world uniqueness using the predicates $\ell \triangleright T$ (a label uniquely identifies $T$) and $\tilde{\ell} \triangleright T$ (a closed label set uniquely identifies $T$):

$$ \ell \triangleright T \triangleq \ell \in \text{dom}(\Omega(T)) \wedge \forall T', (\ell \in \text{dom}(\Omega(T')) \implies T = T') $$

$$ \tilde{\ell} \triangleright T \triangleq \text{dom}(\Omega(T)) = \tilde{\ell} \wedge \forall T', (\text{dom}(\Omega(T')) = \tilde{\ell} \implies T = T') $$
These predicates depend only on the global label environment $\Omega$: they ignore field types and require no contextual type information. The associated typing rules (RCD-CLOSED, RCD-PROJ-CLOSED) are therefore *robust*, since disambiguation relies solely on globally known label information rather than type-directed disambiguation.

## 3.3 Shapes

We introduce *shapes* as a generalization of type constructors. They provide a uniform treatment of both constructors and polytypes, and are useful in defining polytype unification (§6).

A shape $\zeta$ is a type with holes, written $v\bar{\gamma}. \tau$, where $\bar{\gamma}$ denotes the set of type variables representing the holes. By construction, we require $\bar{\gamma}$ to be *exactly* the free variables of $\tau$. Hence, shapes are closed and do not contain useless binders. We consider shapes equal up to $\alpha$-conversion. When $\tau$ is a ground type, we omit the binder and simply write $\tau$ for the shape. We use $\perp$ to denote the shape $v\gamma. \gamma$, which we call the *trivial shape*. Let $S$ denote the set of all shapes and $S^* \subset S$ the set of non-trivial shapes.

Shapes are equipped with the standard instantiation ordering, defined by **INST-SHAPE**. When writing $\zeta \preceq \zeta'$, we say that $\zeta$ is more general than $\zeta'$. When $\zeta$ and $\zeta'$ are more general than one another, they are actually equal. The trivial shape $\perp$ is the most general shape. If $\zeta$ is $v\bar{\gamma}.\tau$, the shape application $\zeta \bar{\tau}$ is defined as $\tau[\bar{\gamma} := \bar{\tau}]$. We say that $\zeta$ is a shape of $\tau$ when there exists $\bar{\tau}$ such that $\tau = \zeta \bar{\tau}$; in this case, we call the pair $(\zeta, \bar{\tau})$ a decomposition of $\tau$.

$$ \frac{\bar{\gamma}_2 \# v\bar{\gamma}_1. \tau}{v\bar{\gamma}_1. \tau \preceq v\bar{\gamma}_2. \tau[\bar{\gamma}_1 := \bar{\tau}_1]} $$

**Definition 3.1.** A non-trivial shape $\zeta \in S^*$ is the principal shape of the type $\tau$ iff:

(1) $\exists \bar{\tau}', \tau = \zeta \bar{\tau}'$

(2) $\forall \zeta' \in S^*, \forall \bar{\tau}', \tau = \zeta' \bar{\tau}' \implies \zeta \preceq \zeta'$

**THEOREM 3.2 (PRINCIPAL SHAPES).** Any non-variable type $\tau$ has a non-trivial principal shape $\zeta$.

A principal shape $v\bar{\gamma}.\tau$ is *canonical* if its free variables appear in the sequence $\bar{\gamma}$ in the order in which they occur in $\tau$. Canonical principal shapes are written $\zeta$, and we write $S_{\text{canon}}$ for the set of all such shapes. Each non-variable type $\tau$ has a unique canonical principal shape, written shape($\tau$). For example, shape(rcd $T \bar{\tau}$) is $v\bar{\gamma}.\text{rcd } T \bar{\gamma}$.

Shapes are particularly interesting in the context of polytypes, since polytypes can be decomposed into shapes and thus treated analogously to type constructors. For instance, the polytype $[\forall \alpha. ([\forall \beta. (\beta \rightarrow \text{int list})*\beta]) \rightarrow \alpha \rightarrow \alpha]$ has the principal shape $\zeta$ equal to $v\gamma$. $[\forall \alpha. ([\forall \beta. (\beta \rightarrow \gamma)*\beta]) \rightarrow \alpha \rightarrow \alpha]$. The original polytype can thus be represented as the shape application $\zeta$ (int list).

## 3.4 Typing rules for fragile, implicit constructs

We now turn to the typing of fragile implicit constructs (Figure 3). To prevent the kind of uncontrolled guessing permitted by *natural* typing rules (e.g. RCD-PROJ-I-NAT), we adopt *contextual* typing rules: an implicit term $e^i$ is typed *within* a surrounding one-hole term context $\mathscr{C}$ (Figure 3). The context $\mathscr{C}$ is used to ensure that the relevant type information (e.g. a shape $\zeta$) is *known*—that is, it is the unique shape $\zeta$ that can be inferred from the context, rather than an arbitrary one that could be *guessed*. Such rules are therefore inherently non-compositional.

**Unicity.** The key question for our contextual typing rules is whether the shape $\zeta$ of a term's type is *uniquely determined* by its surrounding context $\mathscr{C}$. We capture this with our *unicity conditions* $\mathscr{C}[e \triangleright \zeta | \bar{e}]$ and $\mathscr{C}[\square \triangleleft \zeta | \bar{e}]$, which state that all valid typings of the (erased) context $\mathscr{C}$ assign the same canonical shape $\zeta$ to the subterm $e$ and the context's hole $\square$, respectively.
$e ::= ... | \Box$ with $\bar{e}$
$\mathscr{E} ::= \Box | \mathscr{E} e | e \mathscr{E} | ...$

$\mathbf{HOLE}$
$\frac{(\Gamma \vdash e_i : \tau_i)^n_{i=1}}{\Gamma \vdash \Box \text{ with } \bar{e} : \tau'}$

$\mathbf{PROJ-I}$
$\mathscr{E}[e \triangleright v\bar{y}. \Pi_{i=1}^n \bar{y}]$
$\frac{\Gamma \vdash \mathscr{E}[e.j^n] : \tau}{\Gamma \vdash \mathscr{E}[e.j] : \tau}$

$\mathbf{USE-I}$
$\mathscr{E}[e \triangleright v\bar{y}. [\sigma]]$
$\frac{\Gamma \vdash \mathscr{E}[\langle e : \exists \bar{y}. \sigma \rangle] : \tau}{\Gamma \vdash \mathscr{E}[\langle e \rangle] : \tau}$

$\mathbf{POLY-I}$
$\mathscr{E}[\Box \triangleright v\bar{y}. [\sigma] | e]$
$\frac{\Gamma \vdash \mathscr{E}[[e : \exists \bar{y}. \sigma]] : \tau}{\Gamma \vdash \mathscr{E}[[e]] : \tau}$

$\mathbf{RCD-I}$
$\frac{\mathscr{E}[\Box \triangleright v\bar{y}. \text{rcd } T \bar{y} | \bar{e}]}{\Gamma \vdash \mathscr{E}[\{\overline{\ell = e}\}] : \tau}$

$\mathbf{RCD-PROJ-I}$
$\frac{\mathscr{E}[e \triangleright v\bar{y}. \text{rcd } T \bar{y}]}{\Gamma \vdash \mathscr{E}[e.T.\ell] : \tau}$

$\mathscr{E}[e \triangleright \zeta | \bar{e}] \triangleq \forall \Gamma, \tau, g, \Gamma \vdash \mathscr{E}[\Box \text{ with } \bar{e}, (e : g)] : \tau \Rightarrow \text{shape}(g) = \zeta$

$\mathscr{E}[\Box \triangleleft \zeta | \bar{e}] \triangleq \forall \Gamma, \tau, g, \Gamma \vdash \mathscr{E}[(\Box \text{ with } \bar{e}) : g)] : \tau \Rightarrow \text{shape}(g) = \zeta$

<caption>Fig. 3. Typing rules for fragile, implicitly typed extensions.</caption>

In other words, $\mathscr{E}[e \triangleright \zeta | \bar{e}]$ holds when the type of the subterm $e$ has a unique shape $\zeta$ fixed by its context $\mathscr{E}$ and sibling terms $\bar{e}$, while $\mathscr{E}[\Box \triangleleft \zeta | \bar{e}]$ holds when the expected type of the hole in $\mathscr{E}$ (with subterms $\bar{e}$) has the unique shape $\zeta$.

$\mathscr{E}[e \triangleright \zeta | \bar{e}] \triangleq \forall \Gamma, \tau, g, \Gamma \vdash \mathscr{E}[\Box \text{ with } \bar{e}, (e : g)] : \tau \Rightarrow \text{shape}(g) = \zeta$

$\mathscr{E}[\Box \triangleleft \zeta | \bar{e}] \triangleq \forall \Gamma, \tau, g, \Gamma \vdash \mathscr{E}[(\Box \text{ with } \bar{e}) : g)] : \tau \Rightarrow \text{shape}(g) = \zeta$

To make sense of these definitions, we rely on a few auxiliary notions:

(1) We write ($\Box$ with $\bar{e}$) for a *typed hole* carrying subterms $\bar{e}$. The subterms $\bar{e}$ are required to be well-typed in the current environment (*HOLE*), but their types are independent of the type of the hole: the hole itself may be assigned an arbitrary type.

(2) We introduce an *erasure* function $\lfloor e \rfloor$ that erases all not-yet-elaborated implicit constructs $e^i$ in $e$ with a typed hole around their subterms. For example, $\lfloor e.T. \rfloor$ is ($\Box$ with $\lfloor e \rfloor$). The full definition is given in Figure 4.

<figure><img src="image_4.png" /><figcaption>Fig. 4. Selected cases of the erasure of $e$. All other cases are homomorphic.</figcaption></figure>
Typed holes ensure that subterms—such as type annotations—remain present even when the implicit construct containing them is erased. This is because they may introduce constraints that can still contribute to unicity. For instance, $\lambda r. (r : \mathit{point}) \cdot x$ would be ill-typed if we erased ($r : \mathit{point}$).

The erasure of $[\mathscr{C}[\square \text{ with } (e : g), \bar{e}]]$ and $[\mathscr{C}[((\square \text{ with } \bar{e}) : g)]]$ replaces all not-yet-elaborated implicit constructs with typed holes, ensuring that the unicity of $\zeta$ is determined only by implicit terms that have been elaborated thus far. This induces a causal, or partial, order among implicit constructs: an implicit term can only be elaborated once all of its dependencies—those providing the relevant *known* type information—have themselves been elaborated. This ordering prevents self-justifying cycles in unicity and rules out “out-of-thin-air” guesses.

The attentive reader may notice that our unicity conditions contain a negative occurrences of the typing judgment. At first glance, this seems problematic for well-foundedness. However, the issue is easily resolved by noting that these occurrences arise only as typing assumptions on erased terms, which do not themselves involve any implicit rules. Formally one could make this explicit by introducing a restricted typing judgment $\Gamma \vdash_{\mathrm{robust}} e : \tau$ that excludes the implicit rules ($*-I$), and by using this strictly simpler judgment in the antecedent of unicity conditions. We omit this distinction for simplicity.

*The omnidirectional recipe.* All typing rules instantiate a common framework—the *omnidirectional recipe*—which ensures that certain omitted type annotations are uniquely determined from the context. Each construct, however, requires a specific instantiation of the framework. We first describe the framework, then present each feature separately.

*Step 1: Contextualize.* Each implicit fragile term $e^i$ is typed relative to a surrounding one-hole term context $\mathscr{C}$: its rule asserts the typability of $\Gamma \vdash \mathscr{C}[e^i] : \tau$ as the conclusion.

*Step 2: Select a unicity condition.* This is the secret ingredient! The unicity condition ensures that the shape $\zeta$ is fully determined by the surrounding context $\mathscr{C}$ and subexpressions $\bar{e}$ (e.g. the subexpressions $\bar{e}$ in $\{\ell = e\}$).

If the $e^i$ is an introduction form, we infer the shape from the context's hole $[\square \prec \zeta \mid \bar{e}]$. If $e^i$ is an elimination form, we infer the shape from the *principal term* $e$ (the term whose type contains the connective we're eliminating): $\mathscr{C}[e \triangleright \zeta \mid \bar{e}]$.

*Step 3: Elaborate.* The uniquely inferred shape $\zeta$ is used to elaborate $e^i$ into its explicit counterpart $e^x$, and the rule asserts $\Gamma \vdash \mathscr{C}[e^x] : \tau$ as a premise.

*Implicit polytypes.* Unboxing a polytype $\langle e \rangle$ is an *elimination form*. Following the omnidirectional recipe, *USE-I* is a contextual rule (*Step 1*) requiring that the principal term $e$ have the unique shape $v\bar{\gamma}$. $[\sigma]$ in the context $\mathscr{C}$ (*Step 2*). In *Step 3*, we then elaborate $\langle e \rangle$ into $\langle e : \exists\bar{\gamma}. \sigma \rangle$. Conversely, boxing with $[e]$ is an *introduction form*. In *POLY-I*, we require that the expected type of the context's hole $\mathscr{C}$ has the shape $v\bar{\gamma}$. $[\sigma]$ (*Step 2*). We then type $[e]$ as $[e : \exists\bar{\gamma}. \sigma]$ (*Step 3*).

*Implicit nominal records.* Overloaded record labels are handled analogously. Typing record projections in *RCD-PROJ-I* is an *elimination form* for the record type rcd $T \bar{\tau}$: the projection $e.\ell$ is typed as $e.T.\ell$ (*Step 3*) provided the type of expression $e$ in context $\mathscr{C}$ has record shape $v\bar{\gamma}$. rcd $T \bar{\gamma}$ (*Step 2*). For record construction, $\{\ell = e\}$ is an *introduction form*. In *RCD-I*, we type an overloaded record $\{\ell = e\}$ as $T.\{\ell = e\}$ (*Step 3*), provided the context $\mathscr{C}$ with subterms $\bar{e}$ expects a record type of shape $v\bar{\gamma}$. rcd $T \bar{\gamma}$ (*Step 2*).

We now illustrate the typing of implicit constructs with a few examples.

*Example 3.3.* Consider the term $\mathrm{ex}_3 \triangleq \lambda r. (r.x, r.point.y)$ from §2.1.<fnref n="9" /> In $\mathrm{ex}_3$, $r$ can only be of type *point*. Indeed, considering the second projection first, we should learn that $r$ is of type *point*

<footnote n="9">⁹The typing rules for tuples are standard and present in Appendix §A.</footnote>
(using RCD-PROJ-I) and since it is λ-bound, this makes the first projection unambiguous. (For record types without parameters, we use T as a shorthand for rcd T ∅.)

Formally, we derive:

$$ \frac{\mathcal{E}[r \triangleright \text{point}] \quad \emptyset \vdash \mathcal{E}[r.\text{point.x}] : \text{point} \to \text{int} * \text{int}}{\emptyset \vdash \mathcal{E}[r.\text{x}] : \text{point} \to \text{int} * \text{int}} \qquad \text{RCD-PROJ-I} $$

where the context $\mathcal{E}$ is $\lambda r$. (□, r.point.y). We have $\emptyset \vdash \mathcal{E}[r.\text{point.x}] : \text{point} \to \text{int} * \text{int}$, indeed. Therefore, it remains to show that $\mathcal{E}[r \triangleright \text{point}]$ (1). Assume $\emptyset \vdash \mathcal{E}[\square \text{ with } (r : g)] : \tau$. Since r.point.y requires r to have the type point (due to Rule RCD-PROJ-X and LAB-INST), it follows that there is no other choice but to take point for g, which proves (1).

**Example 3.4.** To illustrate a simple case of non-typability, we reconsider the example $ex_1 \triangleq \lambda r. r.x$ from §2.1. If there is a derivation of $ex_1$, then there must be one of the form:

$$ \frac{\mathcal{E}[r \triangleright v\bar{y}. \text{rcd } T \bar{y}] \quad \emptyset \vdash \mathcal{E}[r.T.x] : \tau}{\emptyset \vdash \mathcal{E}[r.x] : \tau} \qquad \text{RCD-PROJ-I} $$

where $\mathcal{E}$ is the term $\lambda r$. □, which is the largest possible context. Unfortunately, $\mathcal{E}[r \triangleright v\bar{y}. \text{rcd } T \bar{y}]$ does not hold for any $T$. Indeed, we have $\emptyset \vdash \mathcal{E}[\square \text{ with } (r : g)] : g \to \tau$. for any $g$ and $\tau$. Hence, point and gray_point are both possible shapes for the type of $r$.

**Example 3.5.** Considering the example from §2.5.

```
type gray_point = { x : int; y : int; color : int }
type cie_color = { x : int; y : int; z : int }
type cie_point = { x : int; y : int; color : cie_color }
let ex_10 r = r.color.x
```

OCaml OmniML

As explained in §2.5, $ex_{10}$ is ill-typed because our unicity conditions enforce that each implicit field projection must be resolved individually and in a sequential fashion. We view this as a “Goldilocks” solution: we deliberately trade a small loss in expressivity for the benefit of a tractable, backtracking-free inference algorithm.

To type $ex_{10}$ one must eliminate the final implicit projection in a context of the form $\mathcal{E}[e.\ell]$. It is a given that neither projection can be resolved by applying RCD-PROJ-CLOSED since the labels (color and x) are both overloaded. Thus, the implicit projections must be typed using RCD-PROJ-I. Two cases arise, neither of which are possible:

**Case $\mathcal{E}$ is $\lambda r$. □.** We should have a derivation that ends with

$$ \frac{\mathcal{E}[r.\text{color} \triangleright \text{cie\_color}] \quad \emptyset \vdash \mathcal{E}[r.\text{color.cie\_color.x}] : \tau}{\emptyset \vdash \mathcal{E}[r.\text{color.x}] : \tau} \qquad \text{RCD-PROJ-I} $$

However, $\mathcal{E}[r.\text{color} \triangleright \text{cie\_color}]$ does not hold. Indeed, the judgment $\emptyset \vdash [\mathcal{E}[(\square \text{ with } r.\text{color : g} )]] : g \to \tau$ (i.e., $\emptyset \vdash \lambda r. ((\square \text{ with } r) : g) : g \to \tau$) holds for any g. Hence, the shape of the type of $r.\text{color.x}$ is not uniquely determined and this case cannot occur.

**Case $\mathcal{E}$ is $\lambda r$. □.x.** The derivation must end with:

$$ \frac{\mathcal{E}[r \triangleright \text{cie\_point}] \quad \emptyset \vdash \mathcal{E}[r.\text{cie\_point.y}] : \tau}{\emptyset \vdash \mathcal{E}[r.\text{color}] : \tau} \qquad \text{RCD-PROJ-I} $$

However, $\mathcal{E}[r \triangleright \text{cie\_point}]$ does not hold either. Again, the judgment $\emptyset \vdash [\mathcal{E}[(\square \text{ with } r) : g]] : \tau' \to g$, (i.e., $\emptyset \vdash \lambda r. ((\square \text{ with } r) : g) : \tau' \to g$) holds for any g.
<figure><img src="image_5.png" /></figure>

## 4 Constraints

To reason about constraint-based inference, we need more than a procedure for generating and solving constraints: we require a *formal logic* of constraints, with a syntax and a declarative semantics that characterizes satisfiability. This semantics is essential: it validates the design of our constraint language and provides the foundation for proving the soundness, completeness, and principality of inference. Without it, the meta-theory of our approach cannot be stated precisely.

We now introduce the syntax and semantics of our constraint language. Building atop the constraint-based inference framework of Pottier and Rémy [2005], we adopt a constraint language (Figure 5) that includes both term and type variables. Its semantics is given by a satisfiability judgment $\phi \vdash C$ (Figure 5). The semantic environment $\phi$ assigns to each free type variable $\alpha$ a ground type $g \in \mathcal{G}$ (a type with no free variables) and to each term variable $x$ a set of ground types$^{10}$ $\mathcal{S} \subseteq \mathcal{G}$ (the instances of a type scheme bound to $x$). We write $\phi[\alpha := g]$ and $\phi[x := \mathcal{S}]$ for extensions of $\phi$, and $\phi(\tau)$ for the ground type obtained by substitution.

Constraints include basic logical forms: tautological true (`TRUE`), unsatisfiable false, and conjunctive $C_1 \wedge C_2$ (`CONJ`) constraints. The unification constraint $\tau_1 = \tau_2$ is satisfied when $\tau_1$ and $\tau_2$ are

<footnote n="10">¹⁰$\mathcal{S}$ can be pronounced "Fraktur S" or "ground S".</footnote>
equal (UNIF). An existential constraint $∃α. C$ holds if there exists a witness g for α satisfying C (EXISTS), while a universal constraint $∀α. C$ holds if C is satisfied for every binding of α (FORALL). When $σ$ is a polymorphic type scheme $∀α. τ'$, we use the notation $σ ≤ τ$ as shorthand for the instantiation constraint $∃α. τ' = τ$. OmniML-specific constraints, such as record label instantiation $t.l ≤ τ_1 → τ_2$ (§2.4), are introduced later (§4.2).

Polymorphism in the constraint language is expressed through *generalization* and *instantiation* constraints. In a generalization constraint (or *let*-constraint) let $x = λα. C_1$ in $C_2$, the definition of $x$ is a constraint abstraction $λα. C_1$, a function that, when applied to a type $τ$, returns $C_1[α := τ]$. The binding of $x$ is then available in $C_2$ and refers to this abstraction. Semantically, the abstraction $λα. C_1$ is interpreted as a set of ground types that satisfies $C_1$, and the generalization constraint requires this set to be non-empty, i.e., there is at least one instantiation of $α$ that satisfies $C_1$. Instantiations (or applications) $x τ$ eliminate abstractions by applying a type $τ$ to the abstraction bound to $x$. This holds precisely when $φ(τ) ∈ φ(x)$, i.e., $τ$ is one of the satisfiable instances of $x$. The $λ$-abstraction and application syntax follows Pottier [2014]. In other presentations, constraint abstractions $λα. ∃β. C$ are written as constrained type schemes $∀α, β. C ⇒ α$, and instantiation constraints $x τ$ are written $x ≤ τ$.

Finally, we introduce *suspended match constraints* (match $τ$ with $\bar{τ}$), which consist of:

(1) A matchee $τ$. The constraint remains suspended until the shape of $τ$ is determined, i.e., while $τ$ is a type variable.

(2) A list of branches $\bar{τ}$ of the form $ρ ⇒ C$, where $ρ$ is a shape pattern.<fnref n="11" /> The constraint $C$ is solved in the extended context produced by the matching pattern. For example, the wildcard pattern `_` matches any shape, and binds nothing. To ensure determinism, the set of patterns $\bar{ρ}$ must be *disjoint*—that is, no shape may be matched by more than one pattern in the list.

The formal semantics of suspended match constraints are somewhat involved; we return to them in the next subsection (§4.1).

Closed constraints are either satisfiable in any semantic environment (i.e., they are tautologies) or unsatisfiable. For example, the satisfiability of the constraint $∃α. α = int$ is established by the derivation on the right-hand side.

We write $C_1 ⊢ C_2$ to express that $C_1$ *entails* $C_2$, meaning every solution $φ$ to $C_1$ is also a solution to $C_2$. We write $C_1 ≡ C_2$ to indicate that $C_1$ and $C_2$ are equivalent, that is, they have exactly the same set of solutions.

Throughout this paper, we will find it convenient to work with *constraint contexts*. A constraint context $\mathcal{C}$ is simply a constraint with a *hole*, analogous to term contexts $\mathcal{E}$ introduced in §3. We write $\mathcal{C}[C]$ to denote filling the hole of the context $\mathcal{C}$ with the constraint $C$. Hole filling may capture variables, so we frequently require explicit side conditions when variable capture must be avoided. We write $bv(\mathcal{C})$ for the set of variables bound at the hole in $\mathcal{C}$.

## 4.1 Suspended constraints

A central difficulty in our work on suspended constraints was defining a satisfying semantics. The challenge lies in formalizing what it means for type information to be *known* without presupposing a *static* solving order. This is the same issue encountered in our typing rules (§3.4), and we address it in the same way: by introducing a contextual rule together with a unicity condition.

<footnote n="11">¹¹The match constraints in this paper only use a single branch; but in a larger language there would be use-cases for having several branches; for example, record projection could be overloaded to work both on nominal records and on tuples (or objects, modules, etc.), requiring several branches in its generated constraint. So we kept the general syntax.</footnote>
To define the semantics for suspended constraints, we first introduce discharged match constraints.

*Definition 4.1 (Discharged match constraint)*. Given a suspended constraint (match $\tau$ with $\bar{\chi}$) and a canonical shape $\zeta$, we introduce the syntactic sugar (match $\tau := \zeta$ with $\bar{\chi}$) for the discharged match constraint that selects the branch in $\bar{\chi}$ that matches $\zeta$:

$$ \text{match } \tau := \zeta \text{ with } \overline{\rho \Rightarrow C} \triangleq \begin{cases} \exists \bar{\alpha}. \tau = \zeta \bar{\alpha} \wedge \theta(C_i) & \text{if } \rho_i \text{ matches } \zeta \bar{\alpha} \hookrightarrow \theta \\ \text{false} & \text{otherwise} \end{cases} $$

The first conjunct ($\tau = \zeta \bar{\alpha}$) ensures that $\zeta$ is indeed the canonical shape of $\tau$, and the second conjunct is the selected branch constraint $C_i$ under the appropriate substitution. Since the syntax of suspended match constraints requires that branch patterns are non-overlapping, the matching branch $\rho_i \Rightarrow C_i$ is uniquely determined. It may, however, be undefined if the branches are not exhaustive, in which case the discharged constraint is false.

The partial function ($\rho$ matches $\zeta \bar{\alpha}$), introduced in Figure 5, describes how a pattern $\rho$ is matched against a canonical principal shape $\zeta$. Before matching, $\zeta$ is applied with fresh shape variables $\bar{\alpha}$ (of the same arity as $\zeta$), so that the result of matching may refer to them. The match either fails or returns a substitution $\theta$ mapping pattern variables (e.g. record name variables $t$ from §2.4) to shape components (e.g. record names $T$). These components may themselves mention the freshly introduced variables $\bar{\alpha}$. In Figure 5, we only introduce the wildcard pattern and its matching rule; in §4.2 we extend both the syntax of shape patterns and the matching function itself to handle the patterns that arise in OmniML.

*A natural attempt.* As with typing rules for fragile constructs (e.g. RCD-PROJ-I-NAT), suspended match constraints have a *natural rule*:

$$ \frac{\text{MATCH-NAT} \qquad \phi \vdash \text{match } \tau := \zeta \text{ with } \bar{\chi}}{\zeta = \text{shape}(\phi(\tau)) \qquad \phi \vdash \text{match } \tau \text{ with } \bar{\chi}} $$

This rule states that a suspended constraint holds whenever the corresponding discharged constraint holds for the canonical shape of $\phi(\tau)$.

Although simple and declarative, this semantics is too permissive. It allows *guessing* the shape of $\tau$ rather than requiring it to be *known*. For example, $\exists \alpha. \text{match } \alpha$ with _ $\Rightarrow \alpha$ = int is satisfiable under the natural semantics:

$$ \frac{\text{\_ matches int } \emptyset \hookrightarrow \emptyset \qquad \frac{\text{int} = \text{int}}{\phi[\alpha := \text{int}] \vdash \alpha = \text{int}} \qquad \text{UNIF}}{\phi[\alpha := \text{int}] \vdash \text{match } \alpha \text{ with _ } \Rightarrow \alpha = \text{int}} \qquad \text{MATCH-NAT} \\ \frac{\phi \vdash \exists \alpha. \text{match } \alpha \text{ with _ } \Rightarrow \alpha = \text{int}}{\phi \vdash \exists \alpha. \text{match } \alpha \text{ with _ } \Rightarrow \alpha = \text{int}} \qquad \text{EXISTS} $$

This “out-of-thin-air” behavior does not match the intended meaning of suspended match constraints and raises several problems: (1) a reasonable solver—one that avoids backtracking—cannot be complete with respect to this semantics; and (2) it breaks the existence of principal solutions, just as the *natural* typing rules do (e.g. RCD-PROJ-I-NAT).

*Contextual semantics.* To rule out guessing, we instead adopt a *contextual* semantics: a match constraint is satisfiable only if the shape of the type is determined by the surrounding context. The corresponding rule for suspended constraints, MATCH-CTX (Figure 5), is the only non-syntax-directed
rule in our semantics.

$$ \frac{\text{MATCH-CTX} \quad \mathcal{C}[\tau!\zeta] \quad \phi \vdash \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]}{\phi \vdash \mathcal{C}[\text{match } \tau \text{ with } \bar{\chi}]} $$

In this rule, a suspended constraint (match $\tau$ with $\bar{\chi}$) in the context $\mathcal{C}$ can be discharged, provided the shape $\zeta$ is not guessed from $\phi$, but recovered from the constraint context $\mathcal{C}$. This *unicity* condition $\mathcal{C}[\tau!\zeta]$ (defined below) ensures that $\zeta$ is uniquely determined by the context $\mathcal{C}$, capturing precisely what it means for the shape of a type to be *known*.

**Definition 4.2 (Erasure).** The erasure $\lfloor C \rfloor$ of a constraint $C$ is defined as the constraint obtained by replacing suspended match constraints in $C$ with true.

**Definition 4.3 (Simple constraints).** We say that $C$ is *simple* if it contains no suspended match constraints.

**Definition 4.4 (Unicity).** We define the unicity condition $\mathcal{C}[\tau!\zeta]$, which states that $\tau$ has a unique canonical shape $\zeta$ within the context $\mathcal{C}$ as: $\forall \phi, g. \ \phi \vdash \lfloor \mathcal{C}[\tau = g] \rfloor \Rightarrow \text{shape}(g) = \zeta$.

Similarly to the unicity conditions introduced for typing rules in §3.4, unicity for constraints $\mathcal{C}[\tau!\zeta]$ relies on erasure $\lfloor \mathcal{C}[\tau = g] \rfloor$ to restrict attention to previously discharged match constraints, inducing a causal order between match constraints, enforced by MATCH-CTX.

When $\tau$ is not a variable, $\lfloor \tau!\zeta \rfloor$ holds trivially when $\zeta$ is the shape of $\tau$. Likewise, when (the erasure of) $\mathcal{C}$ is unsatisfiable, then $\mathcal{C}[\alpha!\zeta]$ holds vacuously for any $\zeta$. The interesting and nontrivial cases—the ones we illustrate next—arise when $\tau$ is a type variable and $\mathcal{C}$ is satisfiable.

**Example 4.5.** Recall the problematic example that was satisfiable under the natural semantics:

$$ \exists \alpha. \text{ match } \alpha \text{ with } \_ \Rightarrow \alpha = \text{int} $$

Under the contextual semantics, the suspended constraint appears in a context $\mathcal{C}$ with no contextual information. i.e., $\mathcal{C}$ is $\exists \alpha$. □. So for any ground type $g$, $\lfloor \mathcal{C}[\alpha = g] \rfloor$ (i.e., $\exists \alpha. \alpha = g$) is satisfiable, allowing $g$ to have an arbitrary shape (e.g. int, bool, etc.). As a result, the uniqueness condition $\mathcal{C}[\alpha!\zeta]$ never holds making MATCH-CTX inapplicable. The constraint is unsatisfiable as intended.

**Example 4.6.** Consider the satisfiable constraint:

$$ \exists \alpha. \alpha = \text{int} \land \text{match } \alpha \text{ with } \_ \Rightarrow \text{true} $$

Here, we apply the contextual rule with the context $\mathcal{C}$ equal to $\exists \alpha. \alpha = \text{int} \land \square$. Any solution $\phi$ of this context necessarily satisfies $\alpha = \text{int}$, so we have $\mathcal{C}[\alpha! \text{int}]$ and the suspended constraint can be discharged.

**Example 4.7.** Consider the more intricate example:

$$ \exists \alpha, \beta. (\text{match } \alpha \text{ with } \_ \Rightarrow \beta = \text{bool}) \land (\text{match } \beta \text{ with } \_ \Rightarrow \text{true}) \land (\alpha = \text{int}) $$

Suppose we attempt to apply MATCH-CTX to the match on $\beta$ first. We want to show $\mathcal{C}[\beta!\text{bool}]$ for the context $\mathcal{C}$ equal to $(\text{match } \alpha \text{ with } \_ \Rightarrow \beta = \text{bool}) \land \square \land \alpha = \text{int}$. Its erasure $\lfloor \mathcal{C} \rfloor$ is true $\land \square \land \alpha = \text{int}$, which imposes no constraints on $\beta$. Thus both $\lfloor \mathcal{C}[\beta = \text{int}] \rfloor$ and $\lfloor \mathcal{C}[\beta = \text{bool}] \rfloor$ are both satisfiable: unicity does not hold and MATCH-CTX cannot be applied.

By contrast, if we first discharge the match on $\alpha$, we consider the context $\mathcal{C}$ equal to $\square \land (\text{match } \beta \text{ with } \_ \Rightarrow \text{true}) \land \alpha = \text{int}$. Its erasure $\lfloor \mathcal{C} \rfloor$ equal to $\square \land \text{true} \land \alpha = \text{int}$ does constraint $\alpha$, giving $\mathcal{C}[\alpha!\text{int}]$. We may therefore discharge the match on $\alpha$, rewriting it as $(\text{match } \alpha := \text{int} \text{ with } \_ \Rightarrow \beta = \text{bool}) \text{ i.e., } \alpha = \text{int} \land \beta = \text{bool}$. Substituting back, we are left to satisfy the constraint $\mathcal{C}[\alpha = \text{int} \land \beta = \text{bool}] \text{ i.e., } \alpha = \text{int} \land \beta = \text{bool} \land (\text{match } \beta \text{ with } \_ \Rightarrow \text{true}) \land \alpha = \text{int}$. At this point,
<figure><img src="image_6.png" /><figcaption>Fig. 6. Patterns for OmniML.</figcaption></figure>

unicity for $\beta$ holds, since the context now includes $\beta = \text{bool}$. We can therefore apply MATCH-CTX to eliminate the final match constraint.

This example demonstrates that suspended constraints must be resolved in a dependency-respecting order: attempting to resolve a match constraint too early may result in unsatisfiability.

**Example 4.8.** Let us consider a constraint with a cyclic dependency between match constraints:

$$ \exists \alpha, \beta. (\text{match } \alpha \text{ with } \_ \Rightarrow \beta = \text{bool}) \land (\text{match } \beta \text{ with } \_ \Rightarrow \alpha = \text{int}) $$

Under the natural semantics this constraint is satisfiable, since one may guess the assignment $\alpha := \text{int}, \beta := \text{bool}$, making both match constraints succeed. However, our solver and contextual semantics reject it.

Without loss of generality, suppose we attempt to apply MATCH-CTX on $\alpha$ first. We must establish $\mathcal{C}[\alpha!\text{int}]$ for the context $\mathcal{C} := \square \land \text{match } \beta \text{ with } \_ \Rightarrow \alpha = \text{int}$. But the erasure $\lfloor \mathcal{C} \rfloor$ is $\square \land \text{true}$, which imposes no constraint on $\alpha$. Hence unicity fails and MATCH-CTX is inapplicable.

## 4.2 Constraint generation

We now present the formal translation from terms $e$ to constraints $C$, such that the resulting constraint is satisfiable if and only if the term is well typed. The translation is defined as a function $\llbracket e : \tau \rrbracket$, where $e$ is the term to be translated and $\tau$ is the expected type of $e$. The expected type $\tau$ is permitted to contain type variables, which can be existentially bound in order to perform type inference. The models of constraint $\llbracket e : \tau \rrbracket$ interpret the free variables of $\tau$ such that $\tau$ becomes a valid type of $e$. For example, to infer the entire type of $e$ we may pick a fresh type variable $\alpha$ for $\tau$.

*Shape patterns.* Thus far, our formal presentation of shape patterns has remained abstract, deliberately leaving the syntax and semantics of match constraints partially unspecified to accommodate a range of language features. We now concretize this by specifying the shape patterns used in OmniML (see Figure 6), and introducing the corresponding constraints for the variables they bind. Shape patterns include:

(1) Record type patterns rcd $t_-$, binding the name $T$ of a record type rcd $T \bar{\tau}$ to the record variable $t$.
<figure><img src="image_7.png" /><figcaption>Fig. 7. The constraint generation translation for OmniML.</figcaption></figure>

(2) Polytype patterns [s] matching a polytype [σ] and binding the resulting scheme to the variable s.

Each new kind of pattern introduces corresponding constraint formers: $t.\ell \le \tau_1 \to \tau_2$ asserts that $\tau_1 \to \tau_2$ is a instance of projection type associated with the explicit label $t.\ell$; dom $t = \bar{\ell}$ ensures that the domain of record type $t$ is the set of labels $\bar{\ell}$; and $s \le \tau$ checks that $\tau$ is an instance of s, while $x \le s$ asserts that every instance of x is an instance of s.

By definition, each of these constraint forms is unsatisfiable, since we do not extend the satisfiability relation to include them. Their role is purely syntactic: they only appear within the branches of a suspended match constraint. Once such a constraint is discharged (match $\tau := \zeta$ with $\bar{\rho} \Rightarrow \bar{C}$) (Definition 4.1), the substitution $\theta$ produced by the matching pattern $\rho_i$—which binds the pattern variables (e.g. $t$, $s$, etc.)—is applied to the corresponding branch $C_i$. Hence, it suffices to define the semantics of these constraint formers only for their substituted forms (e.g. $T.\ell \le \tau_1 \to \tau_2$, dom $T = \bar{\ell}$, etc.), as shown in Figure 6. We define the semantics of these substituted forms by translation into existing constraints—that is, as syntactic sugar over the existing core constraint language.

**Constraint generation.** Constraint generation $[[e : \tau]]$ is defined in Figure 7. All generated type variables are fresh with respect to the expected type $\tau$, ensuring capture-avoidance. We now review the cases of the constraint generator, beginning with the cases corresponding to traditional ML constructs.
Unsurprisingly, variables $x$ generate an instantiation constraint $x \tau$. The unit term () requires $\tau$ to be the unit type 1. A function generates a constraint that binds two fresh flexible type variables for the parameter and return types. We use a let-constraint to bind the parameter in the constraint generated for the body of the function. The let-constraint is monomorphic since $\alpha'$ is fully constrained by type variables defined outside the abstraction's scope and therefore cannot be generalized. Applications introduce two fresh flexible type variables, one for the argument type and one for the type of the function, typing each subterm with these, ensuring $\tau$ is the expected return type. Let-bindings generate a polymorphic let-constraint; $\lambda\alpha$. [[e : $\alpha$]] is a principal constraint abstraction for $e$: its intended interpretation is the set of all types that $e$ admits. Annotations bind their flexible type variables and enforce the equality of the annotated type $\tau'$ and the expected type $\tau$.

For polytypes, explicit boxing asserts that $e$ has the polymorphic type $\sigma$ (using universal quantification) and that the expected type is the polytype $[\sigma]$. Conversely, explicit unboxing requires that $\tau$ be an instance of $\sigma$. These cases introduce no suspended match constraints because the annotations can the required type information: the polytype $[\sigma]$.

By contrast, implicit unboxing suspends until the inferred type of $e$ is known to be some non-variable type $\tau_0$. At that point, the suspended match constraint attempts to match $\tau_0$ against the pattern $[s]$. If $\tau_0 = [\sigma]$, the match succeeds, binding $\sigma$ to $s$ and requiring $\tau$ to be an instance of $s$ (i.e., $\sigma \le \tau$); otherwise, the match fails and the term is ill-typed.

Implicit boxing behaves dually: we infer the principal type for $e$ using a let-constraint and suspend until the expected type of the entire term resolves to some type $\tau_0$. If $\tau_0$ matches the same pattern $[s]$ (i.e., $\tau_0 = [\sigma]$), we assert that the principal type of $e$ is at least as general as $s$, via the constraint $x \le s$ (i.e., $x \le \sigma$); otherwise, the match fails.

Record constructs are handled in a similar way, but their matching patterns concern record shapes rather than polytypes. A record projection generates a fresh variable $\alpha$ for the record type and constrain $e$ to this type, suspending until the type of $e$ ($\alpha$) resolves to some type $\tau_0$. When $\tau_0 = \text{rcd } T \bar{\tau}$, the shape pattern (rcd $t$) matches successfully, binding $T$ to the record name variable $t$; the matching branch then retrieves the projected label's type from the global label context $\Omega$ and instantiates it to match $\alpha \rightarrow \tau$. If $\tau_0$ is not a record type, the match fails and the term is ill-typed.

For record expressions, we generate a fresh variable $\alpha_i$ for each field assignment to capture the type of each $e_i$ as $\alpha_i$. The rest of the constraint is deferred until the context determines the type of the whole record type to be $\tau_0$. Once known, it is matched against the same pattern (rcd $t$). If the match succeeds (i.e., $\tau_0 = \text{rcd } T \bar{\tau}$ and $t = T$) the labels are instantiated to match the projection types $\tau \rightarrow \alpha_i$, and we additionally check that the domain of $t$ is exactly $\bar{l}$, ensuring that every label is defined. Otherwise, the constraint is unsatisfiable as intended.

Explicit records and projections, along with closed-world disambiguated terms, bypass suspension and directly instantiate the appropriate labels.

**Example 4.9.** Considering the example from §2.1:

let ex₄ r = let x = r.x in x + (r : point).y

OCaml OmniML

The typing constraint generated for ex₄ contains the following, where $\alpha$ stands for the type of r:

$$ \exists \alpha. \text{let } x = \lambda\beta. (\text{match } \alpha \text{ with } \dots) \text{ in } x \text{ int } \land \alpha = \text{point} $$

The suspended constraint can be discharged under our contextual semantics. We apply the MATCH-Ctx rule with context $\mathcal{C}$ equal to $\text{let } x = \lambda\beta. \square$ in $x \text{ int } \land \alpha = \text{point}$. Although the context includes a let-binding—which in practice involves let-generalization—we can still deduce $\mathcal{C}[\alpha!\text{point}]$, since the erased context $\mathcal{C}]$ contains the unification constraint $\alpha = \text{point}$.
This example illustrates that our formulation of suspended constraints interacts nicely with let-polymorphism. Although the two features are specified in a modular fashion, they are carefully crafted to work together, as we further show in our next example.

**Example 4.10.** A subtle yet crucial feature of our semantics is its support for *backpropagation*:

let $ex_{11} = \text{let getx } r = r.x \text{ in getx one}$

OCaml OmniML

As in the previous example, the type of $r$ cannot be disambiguated from the let-definition alone. There, the ambiguity was resolved when the type $(\alpha)$ was unified to a known type (point) in the let-body. Here, the situation is more subtle: an *instance* of getx's type scheme is taken, which only satisfies the application (getx one) if $r$ has either a variable type or the record type point. However, the projection $r.x$ would be ill-typed if $r$ had a variable type (unicity would fail), so point is the unique consistent solution. This information therefore flows back from the instances in the let-body to the let-definition, a phenomenon we call *backpropagation*.

The constraint generated when typing $ex_{11}$ is:

$\exists \alpha. \text{ let getx = } \lambda \delta. \exists \beta, \gamma. (\delta = \beta \rightarrow \gamma \land \text{ match } \beta \text{ with } \dots) \text{ in } \text{getx (point } \rightarrow \alpha)$

With the context $\mathcal{C}$ equal to let $getx = \lambda \delta. \exists \beta, \gamma. \delta = \beta \rightarrow \gamma \land \Box$ in $getx$ ($point \rightarrow \alpha$), we can show that the unicity predicate $\mathcal{C}[\beta!point]$ holds. For any $g$, the erasure $[\mathcal{C}[\beta = g]]$ is let $getx = \lambda \delta. \exists \beta, \gamma. \delta = \beta \rightarrow \gamma \land \beta = g$ in $getx$ ($point \rightarrow \alpha$). Since $getx$ is bound to the constraint abstraction $\lambda \delta. \exists \gamma. \delta = (g \rightarrow \gamma)$, the instantiation $getx$ ($point \rightarrow \alpha$) can only be satisfied when $g$ is equal to point. This proves unicity, hence the generated constraint for $ex_{11}$ is satisfiable.

## 4.3 Metatheory

Constraint generation is sound and complete with respect to the typing judgment:

**THEOREM 4.11 (CONSTRAINT GENERATION IS SOUND AND COMPLETE).** *A closed OmniML term $e$ is typable if and only if the constraint $\exists \alpha. [[e : \alpha]]$ is satisfiable.*

**THEOREM 4.12 (PRINCIPAL TYPES).** *For any well-typed closed OmniML term $e$, there exists a type $\tau$ such that: (i) $\vdash e : \tau$. (ii) For any other typing $\vdash e : \tau'$, then $\tau' = \theta(\tau)$ for some substitution $\theta$.*

# 5 Constraint solving

We now present a machine for solving constraints in our language. The solver operates as a rewriting system on constraints $C \rightarrow C'$. Once no further transitions are applicable, i.e., $C \rightarrowtail$, the constraint $C$ is either a solved form—from which we can read off a most general solution—or unsatisfiable (if the constraint $C$ is closed).

## 5.1 Unification

Our constraints ultimately reduce to equations between types, which we solve using first-order unification. Like our solver, we specify unification as a non-deterministic rewriting relation between unification problems $U_1 \rightarrowtail U_2$, that eventually reduces to a solved form $\tilde{U}$ or to false.

Unification problems $U$ (Figure 8a) are a restricted subset of constraints, extended with *multi-equations* [Pottier and Rémy 2005]—a multi-set of types considered equal. These generalize binary equalities: $\phi$ satisfies a multi-equation $\epsilon$ if all of its members are mapped to a single ground type $g$ (MULTI-UNIF). Multi-equations are considered equal modulo permutation of their members.

The unification rules are listed in Figure 8b. Rewriting proceeds under an arbitrary context $\mathcal{U}$, modulo $\alpha$-equivalence and associativity and commutativity of conjunctions. Our algorithm is largely standard [Pottier and Rémy 2005], with its main novelty being the use of *canonical principal*
$U ::= true | false | U_1 \land U_2 | \exists \alpha. U | \epsilon$

$\epsilon ::= \emptyset | \tau = \epsilon$

$C ::= ... | \epsilon$

$\mathcal{U} ::= \Box | \mathcal{U} \wedge U_2 | U_1 \wedge \mathcal{U} | \exists \alpha. \mathcal{U}$

Unification problems

Multi-equations

Constraints

Unification context

MULTI-UNIF

$$ \forall \tau \in \epsilon. \phi(\tau) = \mathfrak{g} $$

$$ \phi \vdash \epsilon $$

<figure><img src="image_8.png" /><figcaption>(b) Unification algorithm as a series of rewriting rules $U_1 \rightarrow U_2$. All shapes are principal.</figcaption></figure>

Fig. 8. Unification: syntax, semantics, and the rewriting-based solver $U_1 \rightarrow U_2$.

shapes in place of type constructors. This uniform treatment of monotypes and polytypes simplifies unification and improves on the previous treatment of polytype unification [Garrigue and Rémy 1999].

We briefly summarize the role of each rule. **U-EXISTS** lifts existential quantifiers, enabling applications of **U-MERGE** and **U-CYCLE** since all multi-equations eventually become part of a single conjunction. **U-MERGE** combines multi-equations sharing a common variable and **U-STUTTER** removes duplicate variables. **U-DECOMP** decomposes equal types with matching shapes into equalities between their subcomponents, while **U-CLASH** detects shape mismatches that result in failure. **U-NAME** introduces fresh variables for subcomponents, ensuring unification operates on *shallow terms*, making sharing of type variables explicit and avoiding copying types in rules such as **U-DECOMP**. **U-TRUE** and **U-TRIVIAL** eliminate trivial constraints, and **U-FALSE** propagates failure. Finally, **U-CYCLE** implements the *occurs check*, ensuring that a type variable does not occur in the type it is being unified with. This is a necessary condition for unification, as it would otherwise lead to infinite types. This is formalized by the relation $\alpha <_U \beta$ indicating that $\alpha$ occurs in a type equated to $\beta$ in $U$, that is, when $U = \mathcal{U}[\beta = \tau = \epsilon]$, $\alpha \in \text{fv}(\tau)$ and $\alpha, \beta \notin \text{bv}(\mathcal{U})$. A unification problem $U$ is said to be cyclic, written $\text{cyclic}(U)$, if $\alpha <_U^+ \alpha$ for some $\alpha$.

**Definition 5.1 (Solved form $\hat{U}$).** We write $\hat{U}$ for constraints in *solved form*, that is, constraints of the form $\exists \tilde{\alpha}. \bigwedge_{i=1}^n \epsilon_i$, where: (1) each $\epsilon_i$ contains at most one non-variable type; (2) each type variable may occur as a member of at most one multi-equation $\epsilon_i$; (3) the constraint is acyclic.

## 5.2 Administrative constraints

Section §4 introduced the constraint language used for constraint generation (§4.2). In this section we extend the language with a small set of administrative constraints: auxiliary constructs that
<table><tr><td><i>i</i></td><td>Instantiation variables</td></tr><tr><td><i>C</i> ::= ... | let <i>x</i> α [α&#x0304;] = <i>C</i><sub>1</sub> in <i>C</i><sub>2</sub> | ∃<i>i</i><sup><i>x</i></sup>. <i>C</i> | <i>i</i>(α) ↣ τ</td><td>Constraints</td></tr><tr><td><b>r</b> ::= (<b>g</b>, <i>φ</i>) (r ∈ <b>R</b>)</td><td>Ground regions</td></tr><tr><td><b>R</b> ⊆ <b>R</b></td><td>Sets of ground regions</td></tr><tr><td><i>φ</i> ::= ... | <i>φ</i>[<i>x</i> := <b>R</b>] | <i>φ</i>[<i>i</i> := <i>φ</i>']</td><td>Semantic environments</td></tr></table>

$$ \phi(\lambda\alpha[\bar{\alpha}].C) \triangleq \{(\bar{g}, \phi[\alpha := \bar{g}, \bar{\alpha} := \bar{\bar{g}}]) \in \mathcal{R} : \phi[\alpha := \bar{g}, \bar{\alpha} := \bar{\bar{g}}] \cup C\} $$

<table><caption>Fig. 9. Syntax and semantics of region-based let and incremental instantiation constraints.</caption><tr><td style="vertical-align: top;"><b>LET<sub>R</sub></b><br/><b>R</b> = <i>φ</i>(λα[α&#x0304;].<i>C</i><sub>1</sub>) &nbsp;&nbsp; <b>R</b> ≠ ∅<br/><i>φ</i>[<i>x</i> := <b>R</b>] ∪ <i>C</i><sub>2</sub><br/><i>φ</i> ⊢ let <i>x</i> α [α&#x0304;] = <i>C</i><sub>1</sub> in <i>C</i><sub>2</sub></td><td style="vertical-align: top;"><b>APP<sub>R</sub></b><br/>(<i>φ</i>(τ), <sub>?</sub>) ∈ <i>φ</i>(<i>x</i>)<br/><i>φ</i> ⊢ <i>x</i> τ</td><td style="vertical-align: top;"><b>EXISTS-INST</b><br/>(<sub>?</sub>, <i>φ</i>') ∈ <i>φ</i>(<i>x</i>)<br/><i>φ</i>[<i>i</i> := <i>φ</i>'] ⊢ <i>C</i><br/><i>φ</i> ⊢ ∃<i>i</i><sup><i>x</i></sup>. <i>C</i></td><td style="vertical-align: top;"><b>INCR-INST</b><br/>(<i>φ</i>(<i>i</i>)(α) = <i>φ</i>(τ)<br/><i>φ</i> ⊢ <i>i</i>(α) ↣ τ)</td></tr></table>

never appear in generated constraints, but are introduced internally by the solver to manage generalization and incremental instantiation.

These administrative constraints enable the solver to represent and refine *partial type schemes* as solving progresses, capturing intermediate generalization states and tracking how instantiations evolve as suspended constraints are discharged.

**Regional let-constraints.** As is standard in constraint-based formulations of ML type inference [Pottier and Rémy 2005], generalization-related rules operate on constraints of the form let $x = \lambda\alpha$. $\exists\bar{\alpha}$. $C_1$ in $C_2$. The outermost existentially quantified variables $\bar{\alpha}$ correspond to the potentially generalizable variables. We refer to this existential prefix $\exists\bar{\alpha}$ as a *region*. Intuitively, a region delimits the scope of variables that may be generalized once the abstraction has been fully solved.

To make regions explicit, we introduce regional let-constraints let $x$ $\alpha$ [$\bar{\alpha}$] = $C_1$ in $C_2$ (Figure 9), where $\alpha$ is the *root* of the region and $\bar{\alpha}$ are auxiliary existential variables. The order of $\bar{\alpha}$ is immaterial; regions are considered equal up to permutation of these variables.

Satisfiability of regional let-constraints is defined in Figure 9. The semantics of an abstraction with a region, written $\phi(\lambda\alpha[\bar{\alpha}].C)$, is a set $\mathcal{R}$ of ground regions that satisfy $C$. A ground region $r$ is a pair $(\bar{g}, \phi)$; it satisfies the constraint abstraction $\lambda\alpha[\bar{\alpha}].C$ if $\phi$ satisfies $C$, and $\bar{g}$ is $\phi(\alpha)$. Intuitively, the region environment $\phi$ carries a ground type for each inference variable $\beta$ occurring in $C$; in particular, a ground instance for $\alpha$ and $\bar{\alpha}$.

The rules `LET<sub>R</sub>` and `APP<sub>R</sub>` are the *regional counterparts* of the `LET` and `APP` rules introduced in §4. They are semantically equivalent to their non-regional forms, except that each operates over sets of ground regions (`R`), rather than sets of ground types (`S`). The additional environment $\phi$ carried by these ground regions (`g`, `φ`) is semantically inert for `LET<sub>R</sub>` and `APP<sub>R</sub>` themselves, but will become important later, in the semantics of *incremental instantiation* constraints (§5.2).

Regional let-constraints strictly generalize ordinary let-constraints, as captured by the equivalence:

$$ \text{let } x = \lambda\alpha. \exists\bar{\alpha}. C_1 \text{ in } C_2 \equiv \text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } C_2 $$

*The trouble with lets.* Solving let-constraints is deceptively difficult. Naively, let-constraints (or generalization constraints) could be solved by copying constraints:

$$ \frac{\text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } \mathcal{C}[x \tau] \quad \alpha, \bar{\alpha} \# \tau \quad x \# \text{bv}(\mathcal{C})}{\text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } \mathcal{C}[\exists \alpha, \bar{\alpha}. \alpha = \tau \land C_1]} \xrightarrow{\text{S-LET-APP-BETA}} $$
This rule, due to Pottier and Rémy [2005], resembles $\beta$-reduction in some presentations of explicit substitutions. While this rule is sound when $C_1$ is a simple constraint, it becomes unsound for abstractions containing suspended constraints.

To see why, consider again the example $ex_8$ from §2.4:

```
type α gpoint = { x : α; y : α }
let diag (n : α) : α gpoint = { x = n; y = n }
let ex_8 gp = let getx p = p.x in getx (diag 42), (getx gp : float) OCaml OmniML
```

As explained earlier, this program is clearly well-typed: the type of p is unambiguously determined as $\beta$ gpoint through backpropagation from the first application of getx (getx (diag 42)). The (simplified) generated constraint for $ex_8$ contains:

$$ \exists \alpha_{gp}, \delta. \quad \begin{array}{l} \text{let getx} = \lambda \alpha_{getx}. \exists \alpha_p, \gamma. \wedge \\ \qquad \left( \begin{array}{@{}l@{}} \alpha_{getx} = \alpha_p \rightarrow \gamma \\ \text{match } \alpha_p \text{ with } (\text{rcd } t \_) \Rightarrow t.x \le \alpha_p \rightarrow \gamma \end{array} \right) \\ \text{in getx (rcd gpoint int } \rightarrow \delta) \wedge \text{getx } (\alpha_{gp} \rightarrow \text{float}) \end{array} $$

If we now apply S-LET-APP-BETA to both applications of getx (removing the let-constraint for concision), we obtain:

$$ \exists \alpha_{gp}, \delta. \quad \exists \alpha_{p_1}, \gamma_1. \wedge \left( \begin{array}{@{}l@{}} \text{rcd gpoint int } \rightarrow \delta = \alpha_{p_1} \rightarrow \gamma_1 \\ \text{match } \alpha_{p_1} \text{ with } (\text{rcd } t \_) \Rightarrow t.x \le \alpha_{p_1} \rightarrow \gamma_1 \end{array} \right) \\ \wedge \quad \exists \alpha_{p_2}, \gamma_2. \wedge \left( \begin{array}{@{}l@{}} \alpha_{gp} \rightarrow \text{float} = \alpha_{p_2} \rightarrow \gamma_2 \\ \text{match } \alpha_{p_2} \text{ with } (\text{rcd } t \_) \Rightarrow t.x \le \alpha_{p_2} \rightarrow \gamma_2 \end{array} \right) $$

The first conjunct is satisfiable, since $\alpha_{p_1}$ is unified with rcd gpoint int, thereby discharging the match constraint on $\alpha_{p_1}$. The second, however, is not: $\alpha_{p_2}$ remains underdetermined, leaving its match constraint unsatisfiable. Thus, although the original constraint was satisfiable, the application of S-LET-APP-BETA makes it unsatisfiable. By copying the abstraction, we lose the essential sharing between both instantiations—namely, that both copies of $\alpha_p$ ($\alpha_{p_1}$ and $\alpha_{p_2}$) must have the same shape $\gamma$. rcd gpoint $\gamma$. This loss of sharing is precisely why S-LET-APP-BETA is unsound in the presence of suspended constraints.

A tempting alternative, used in Vytiniotis, Jones, Schrijvers and Sulzmann [2011] and Beneš and Brachthäuser [2025], is to treat the let-bindings monomorphically, sharing $\alpha_p$ directly between both applications. However, this is incomplete: in $ex_8$, the two calls to getx require different instantiations of $\alpha_p$-int gpoint and float gpoint, respectively.

Even setting soundness aside, S-LET-APP-BETA is inefficient. Each application duplicates constraint solving work for the same abstraction. A more efficient approach is to solve once and reuse: first solve the abstraction once—e.g. reducing it to $\lambda\alpha[\bar{\alpha}]$. $\bar{\epsilon}$, where $\bar{\alpha}$ are generalizable variables—and then reuse the result at each instantiation site by only copying the solved constraint $\epsilon$. This mirrors the generalization and instantiation steps of ML inference algorithms such as $W: \lambda\alpha[\bar{\alpha}]$. $\bar{\epsilon}$ corresponds to the type scheme $\forall \bar{\alpha}. \vartheta(\alpha)$, where $\vartheta$ is the most general unifier of $\bar{\epsilon}$. Pottier and Rémy [2005] formalize this connection, and the optimized treatment is naturally expressed as a strategy on top of their S-LET-APP-BETA rule.

We therefore face two related challenges: (1) handle instantiation soundly in the presence of suspended constraints, and (2) to avoid redundant work by reusing *partial* results across instantiations.

To address both, we introduce *partial type schemes*, our second novel mechanism for omnidirectional inference. Partial type schemes are type schemes that delay commitment to certain quantifications (e.g. $\alpha_p$ and $\gamma$). Such *partially generalized variables* are treated as generalized, but can be incrementally refined in future as suspended constraints are discharged.
Returning to our running example, we begin with the partial type scheme $\forall \alpha_p, \gamma. \alpha_p \rightarrow \gamma$ for `getx`, since the suspended match constraint in its abstraction cannot yet be solved. We continue solving the body of the let-constraint, tracking every instances of this partial scheme. As type information flows back—e.g. when the shape of $\alpha_p$ becomes known via backpropagation from the first application of `getx`—the scheme is refined to $\forall \beta$. `rcd gpoint $\beta \rightarrow \beta$`. The second application of `getx` then updates its instantiation accordingly, unifying $\alpha_{p2}$ with `rcd gpoint $\beta_2$` and $\gamma_2$ with $\beta_2$.

**Incremental instantiation.** To support partial type schemes, we also extend the constraint language with *incremental instantiation constraints* (Figure 9). We introduce two new constraint formers:

(1) $\exists i^x.C$, which binds a fresh instantiation $i$ of $x$'s region within $C$, and

(2) $i(\alpha) \rightarrow \tau$, which asserts that the copy of $\alpha$ in $i$ equals $\tau$.

The instantiation variable $i$ is required to ensure all incremental instantiations $i(\alpha) \rightarrow \tau$ are solved uniformly.

Within the solver, we view incremental instantiations as markers indicating which parts of the abstraction still need to be copied, and abstractions themselves are treated as partial type schemes.

This mechanism enables efficient handling of constraint instantiations: solved parts are reused immediately, while suspended constraints can be solved later, further refining the abstraction and propagating new equations to all instantiation sites.

We now turn to the semantics of incremental instantiations (Figure 9). The existential constraint $\exists i^x.C$ is satisfiable (*exists-inst*) if $C$ is satisfiable with $i$ bound to one of the region environments $\phi'$ in the interpretation of $x$. An incremental instantiation $i(\alpha) \rightarrow \tau$ is satisfiable (*incr-inst*) exactly when $i$'s instance of $\alpha$ (i.e., $\phi(i)(\alpha)$) is equal to $\tau$.

When a regional abstraction let $x \alpha [\bar{\alpha}] = C_1$ in $C_2$ contains an incremental instantiation constraint $i(\beta) \rightarrow \tau$, and $i$ is an instantiation of $x$, the variable $\beta$ may range over any free variable of $C_1$—including $\alpha$ and the regional variables $\bar{\alpha}$. In other words, the regional let-constraint let $x \alpha [\bar{\alpha}] = C_1$ in $C_2$ provides a non-obvious scoping rule: the variables $\alpha$ and $\bar{\alpha}$ are also bound in $C_2$, but may occur there only within incremental instantiations of $x$. This subtlety justifies introducing an explicit syntax for regional let-constraints, rather than encoding them as let $x = \lambda\alpha. \exists \bar{\alpha}. C_1$ in $C_2$.

## 5.3 Solving rules

We now gradually introduce the rules of the constraint solver itself (Figures 10 to 12; for a complete view with all rules placed together, see Appendix §A). These rules define a non-deterministic rewriting system, operating modulo $\alpha$-equivalence, and the associativity and commutativity of conjunction. Rewriting takes place under an arbitrary one-hole constraint context $\mathscr{C}$. A constraint $C$ is satisfiable if it rewrites to a solved form $\tilde{U}$ (Definition 5.1); otherwise it gets stuck—in particular, false is considered a stuck constraint.

**Basic rules.** Figure 10 contains a selected set of basic solving rules, drawn from the standard repertoire of small-step constraint solvers for ML type inference. `S-UNIF` invokes the unification algorithm on the current unification problem. The unification algorithm itself is treated as a black box by the solver, so the system could be extended with any equational theory of types implemented by the unification algorithm. `S-LET` rewrites let-constraints into regional form. `S-EXISTS-CONJ` lifts existentials across conjunctions; `S-LET-EXISTSLEFT` and `S-LET-EXISTSRIGHT` lift existentials across let-binders; `S-LET-CONJLEFT`, `S-LET-CONJRIGHT` hoist constraints out of let-binders when they are independent of the local variables. Collectively, these lifting rules normalize the structure of each region into a block of existentially bound variables, whose body consists of a conjunction of
<figure><img src="image_9.png" /></figure>

solved multi-equations followed by a residual constraint—typically an instantiation, let-binding, or suspended constraint.

OmniML-specific constraints, such as the label and polytype instantiation constraints ($t.l \le \tau_1 \to \tau_2, s \le \tau, \text{etc.}$), require no special treatment in our solver. Once their pattern variables are substituted—after solving a match constraint—they are desugared into constraints already handled by the solver.

*Incremental instantiations.* Figure 11 describes the solving rules in charge of incremental instan-
tiation. Incremental instantiation constraints are reduced using the following rules:

(1) **S-INST-COPY** copies the shape of a type to the instantiation site, introducing fresh variables for each subcomponents and marking them with corresponding instantiation constraints. We write $i^x(\beta) \rightsquigarrow \tau$ as a shorthand for $i(\beta) \rightsquigarrow \tau$ when $i$ is bound with $\exists i^x$ in the context. To ensure termination, the abstraction must contain acyclic types.

(2) **S-INST-UNIFY** unifies two instantiations if they both refer to the same source variable $\beta$ at the same instantiation site $i$.

There are three cases in which an instantiation constraint is eliminated:

(1) A nullary shape is copied and no further instantiations are needed (S-INST-COPY).

(2) The copied variable $\beta$ is polymorphic, and thus the instantiation constraint imposes no restriction (S-INST-POLY), provided no other instantiations of $\beta$ remain at the same instantiation side (if not, then apply S-INST-UNIFY).

(3) The copy is monomorphic and in scope, so we unify it directly (S-INST-MONO).

**S-LET-APPR** rewrites an instantiation constraint $x \tau$ introducing an incremental instantiation constraint $i(\alpha) \to \gamma$. Here, $i$ is a fresh instantiation of $x$, $\alpha$ is the *root* of $x$'s region, and $\gamma$ is a fresh alias for $\tau$. We introduce $\gamma$ explicitly, since our rewriting rules for incremental instantiations generally assume that the copied type is a variable rather than an arbitrary type.

*Let-constraints.* Figure 11 also presents the rules governing generalization. **S-LET-SOLVE** removes a let-constraint when the bound term variable is unused and the abstraction is satisfiable. **S-COMPRESS** determines that a regional variable $\beta$ is an alias for $\gamma$. We replace every free occurrence of $\beta$ with $\gamma$—including the domains of any incremental instantiation constraints, written as the substitution $[x(\beta) := \gamma]$.

Conceptually, **S-COMPRESS** acts a variable-level analogue of **S-INST-COPY**: both rules copy solved constraints $\epsilon$ from an abstraction to its instantiation constraints. While **S-INST-COPY** propagates
<figure><img src="image_10.png" /><figcaption>Fig. 11. Solving rules for let-constraints and instantiations.</figcaption></figure>

the head shape of a multi-equation, S-COMPRESS propagates equalities between variables within a multi-equation, thereby enabling subsequent applications of S-INST-UNIFY.

S-EXISTS-LOWER implements the non-trivial case of lowering existentials across let-binders. It identifies a subset of variables in the region of a let-constraint that are unified with variables from outside the region. Such variables are considered monomorphic and thus cannot be generalized; they can instead be safely lowered to the outer scope.

This is the case when the types of $\bar{\beta}$ are determined in a unique way. In short, C determines $\bar{\beta}$ if and only if the solutions for $\bar{\beta}$ are uniquely fixed by the solutions to other variables in C.

*Definition 5.2.* C determines $\bar{\beta}$ if and only if every ground assignments $\phi$ and $\phi'$ that satisfy (the erasure of) C and coincide outside of $\bar{\beta}$ coincide on $\bar{\beta}$ as well.

$$C \text{ determines } \beta \triangleq \forall \phi, \phi'. \phi \vdash [C] \wedge \phi' \vdash [C] \wedge \phi =_{\bar{\beta}} \phi' \implies \phi = \phi'$$

Conceptually, this corresponds to the negation of the generalization condition in ML: a type variable *cannot* be generalized if it appears in the typing context. In the constraint setting, it *cannot* be generalized if it depends on variables from outside the region. For instance, $\exists \beta. \alpha = \beta \rightarrow \gamma$ determines $\gamma$, as $\alpha$ is free and therefore constrains the solution of $\gamma$.

To decide when C determines $\bar{\alpha}$, we introduce the judgment $\vdash C$ determines $\bar{\alpha}$, which syntactically proves that $\bar{\alpha}$ are determined in C. If C is of the form $\exists \bar{\beta}. C'$ where $\bar{\beta} \# \bar{\alpha}$, then we search for a multi-equation $\epsilon$ in C' of the form: (DET-DOM) $\gamma = \epsilon'$ where $\gamma \# \bar{\alpha}, \bar{\beta}$ and $\bar{\alpha} \subseteq \text{fv}(\epsilon')$, or
<figure><img src="image_11.png" /><figcaption>Fig. 12. Rewriting rules for suspended match constraints.</figcaption></figure>

(DET-ESC) $\tilde{\alpha} = \tau = \epsilon'$ where $fv(\tau) \# \tilde{\alpha}, \tilde{\beta}$. This syntactic relation coincides with the semantic definition of determinacy whenever C is in solved form. Otherwise, it is a sound approximation of the semantic definition.

Lowering such variables improves solver efficiency. It avoids unnecessary duplication of work that would otherwise occur via S-INST-COPY. Because these variables are determined by monomorphic ones, lowering allows the solver to apply S-INST-MONO directly at instantiation sites, rather than duplicating equivalent constraints that ultimately express the same semantic fact—that the variable is monomorphic and shared across instances.

**Suspended match constraints.** Figure 12 describes the rules for discharging suspended constraints. S-MATCH-CTX solves suspended match constraints. It would not be effective to allow rewriting whenever the unicity condition $\mathscr{C}[\tau!\zeta]$ holds, because it is not a-priori feasible to check or decide this semantic condition which quantifies over all solutions. Instead we introduce a restricted, decidable approximation via three syntactic “unicity rules” that form the judgment $\vdash \mathscr{C}[\tau!\zeta]$.

The unicity rule UNI-TYPE applies when $\tau$ is a non-variable type $\tau$, in which case the shape is simply shape($\tau$). UNI-VAR applies when the scrutinee is a variable $\alpha$ and the context establishes that $\alpha$ is equal to some non-variable type $\tau$ by exhibiting an equality $\alpha = \tau = \epsilon$ and $\tau$ is a non-variable type. In this case, the shape of $\alpha$ is shape($\tau$).

Finally, UNI-BACKPROP expresses backpropagation, previously illustrated in Example 4.10. In particular, the shape of a regional variable can sometimes be determined from its instantiations. If an abstraction contains a regional variable $\alpha'$, and the constraint context includes an incremental instantiation $i^x(\alpha') \to \gamma$ such that the instance $\gamma$ of $\alpha'$ has the unique shape $\zeta$, then $\alpha'$ must also have shape $\zeta$, as any other shape would render the instantiation unsatisfiable. This rule is well-founded because the regional depth of the hole strictly decreases in the premise.

For a solved context $\tilde{\mathscr{C}}$, this syntactic is moreover sound and complete with respect to the semantic definition of unicity: $\mathscr{C}[\tau!\zeta]$ holds if and only if $\vdash \mathscr{C}[\tau!\zeta]$ is derivable (Appendix Lemma C.11).

## 5.4 Metatheory

We establish the correctness of our solver. Correctness follows from three standard metatheoretic properties: *progress*, *preservation*, and *termination*. Together, they ensure that every satisfiable (term-variable-closed) constraint eventually reduces to an equivalent solved form.

**Definition 5.3.** A constraint $C$ is term-variable-closed if all its term variables $x$ are bound i.e., $fv(C) \subseteq \mathcal{V}$.

**LEMMA 5.4 (SCOPE PRESERVATION).** If $C_1 \rightarrow C_2$, then $fv(C_1) \supseteq fv(C_2)$.

**THEOREM 5.5 (CLOSED PROGRESS).** If a term-variable-closed constraint $C$ cannot take a step $C \rightarrow C'$, then either:
(1) C is solved.

(2) C is false.

(3) for every match constraint $\hat{C}$ [match $\alpha$ with $\bar{\chi}$] in C, $\hat{C}$ [$\alpha!\zeta$] does not hold for any $\zeta$.

**THEOREM 5.6 (TERMINATION).** *The constraint solver terminates on all inputs.*

**THEOREM 5.7 (PRESERVATION).** *If $C_1 \rightarrow C_2$, then $C_1 \equiv C_2$.*

**COROLLARY 5.8 (CORRECTNESS).** *For the term-variable-closed constraint C, C is satisfiable if and only if $C \rightarrow^* \hat{U}$ and $\hat{U}$ is a solved form equivalent to C.*

# 6 Implementation

We have two working prototypes implementing the OmniML language with suspended match constraints and partial type schemes, in which we have reproduced the various type-system features and examples presented in this work. One closely follows the constraint-based presentation described here.<fnref n="12" /> It is public and open-source, available at https://github.com/johnyob/omniml. Its implementation is inspired by previous work such as Inferno [Pottier 2014, 2018]. It uses state-of-the-art ML type inference implementation techniques for efficiency, such as a Tarjan’s union-find data structure for unification [Tarjan 1975] and ranks (or levels) for efficient generalization [Rémy 1992]. Let us discuss a few salient points.

*Unification and scheduling.* Each unsolved unification variable maintains a *wait list* of suspended constraints that are blocked until the variable is unified with a concrete type. When such a unification occurs, the wait list is flushed: the suspended constraints are scheduled on the global constraint scheduler, which is responsible for eventually solving them.

*From a stack to a tree.* Some efficient implementations of ML type inference, starting with Rémy [1992], represent the solver state as a linear *stack* of inference regions, from the outermost variable scope to the current region. Each let-binding and, more generally, each generalization location, introduces a new scope, hence a new region. Since the solver visits the source terms, hence introduces local regions in a depth-first manner, these variable scopes may be represented by an integer *rank* or *level*<fnref n="13" /> attached to each inference variable or type node. Unification maintains these levels to their minimum value when merging types, which amounts to compute the least common ancestor of the region types should belong to. The use of integer levels to represent regions, which is quite efficient and simple to implement, does not suffice for partial generalization. If generalization at some region contain a variable appearing in a suspended match constraint, the region must be kept alive while we continue inference in other regions. Hence, later parts of the constraint may introduce a new let-region at the same level that is unrelated to the suspended one—neither its ancestor nor its descendant—breaking the linear assumption that allowed the representation of variable scopes by integer levels.

We must instead use a *tree* of nested let-regions to represent scopes. Under this scheme, levels no longer uniquely determine a variable’s region. Instead, we interpret a level relative to a path in the region tree from the root. When two variables are unified, they must always lie on some shared path—by scoping invariants—so computing their minimum level (along this path) still suffices to determine the least common ancestor: we keep the efficient integer comparisons.

*Partial generalization.* Generalization is the process of determining which type variables are polymorphic and which are monomorphic (i.e., implementing `S-EXISTS-LOWER`). *Partial generalization*

<footnote n="12">¹²The other prototype is a direct implementation of type inference based on semi-unification which we discuss in §7.</footnote>

<footnote n="13">¹³Ranks or levels in fact correspond to De Bruijn levels.</footnote>
arises when a region cannot be fully generalized due to suspended constraints that may still update its variables. To manage this, we classify type variables into four categories:

(I) Variables are yet to be generalized.

*Introduced by instantiations or source types in constraints*

(G) Variables that are generalized.

*Not accessible from any instance type. Definitely polymorphically.*

(PG) Variables that are partially generalizable.

*Generalizable variables mentioned by suspended match constraint or partial instantiations.*

*Maybe polymorphic, maybe monomorphic.*

(PI) Variables that were previously partially generalized but have since been updated.

*Awaiting re-generalization. Introduced by the unification of partial generics.*

At generalization time, we conservatively approximate whether a variable may be updated in the future using *guards*. A guard is a mark on a variable that indicates the variable is captured by some suspended constraint that has not yet been solved. Guarded variables are generalized as partial generics (*PG*); unguarded ones are fully generalized (*G*).

When an instance is taken from a partial generic, we retain a forward reference from the partial generic (*PG*) to the instance. This enables the generic to notify the instance that it has been updated, propagating the updated type structure to all instances. This mirrors, in reverse, the way our formalized solver uses incremental instantiation constraints to track copies. In addition, the instance remains guarded by the partial generic until the latter is either lowered or fully generalized.

Once a suspended match constraint is solved, it removes the guards it introduced. This may enable previously partial generics to become fully generalizable. Conversely, if a partially generalized variable is lowered (e.g. by S-EXISTS-LOWER), it must be unified with all its instances.

*Lazy generalization.* Repeatedly generalizing a region after every update is expensive. Instead we generalize on demand. We mark regions as “stale” when they may require re-generalization. When an instance is taken, we re-generalize the stale descendants of the region in the region tree.

Although this technique prevents premature re-generalization before instantiation, it only optimizes for a common case. In some situations, re-generalization before instantiation can still be more costly than instantiating first, since the instantiation may discharge suspended constraints that further refine the region's partial type scheme.

# 7 Related work

*Overloading*. Qualified types [Jones 1995a], best known for their use in Haskell's type-classes, are related to our suspended match constraints: both represent constraints on types or type variables that are delayed. At generalization time, constraints on generalizable variables are retained in the type scheme, yielding a constrained type scheme $\forall \bar{a}. C \Rightarrow \tau$. This is much simpler to implement than our partial type schemes, but it provides a different behavior: each instance may resolve C differently (as the constraint is copied on instantiation). Qualified types are excellent choice when this is the desired behavior, typically for *dynamic overloading* [Wadler and Blott 1989]. But they are insufficient when we require a unique resolution of the constraint across all instances—as in *static overloading*. Static overloading can be emulated using qualified types by applying implementation-defined tweaks to specific built-in type-classes, enforcing that resolution is global and failing when it is under-determined. However, such mechanisms lack a clear declarative semantics: to our knowledge, capturing failure due to missing information requires our unicity conditions.

Leijen and Ye [2025] recently proposed a bidirectional account of generalized static overloading within ML. However, their approach is limited by its reliance on fixed directionality (§2.3). Variational typechecking [Chen, Erwig and Walkingshaw 2014] was originally developed for reasoning
about well-typed CPP #ifdef-style macros, introducing *choices* $a\langle e_1, e_2 \rangle$, where *a* is a *dimension* with *alternatives* $e_1$ and $e_2$. Once dimensions are fixed, we are able to project a well-typed non-variational program. Beneš and Brachthäuser [2025] apply this machinery to recast static overloading as variational typing, with a resolution algorithm that uniquely selects the dimensions. However, their system removes *local let-generalization* and requires an exponential-time resolution procedure—an unavoidable consequence of the NP-hardness of *general* static overloading [Charguéraud, Bodin, Dunfield and Riboulet 2025].

Partial type schemes provide an alternative that preserves ML's local let-generalization while suspended constraints offer a tractable account of static overloading. By enforcing resolution using *known* type information (captured by our novel unicity condition) rather than *guessed* information, our approach remains tractable. Our experience suggests that this is a "goldilocks" solution: expressive enough for most applications, yet tractable, and (crucially) compatible with ML's *local let-generalization*. However, we have not yet extended our approach to capture *generalized static overloading*; developing a full omnidirectional account of that setting is left to future work.

***Suspended constraints.*** Suspending constraints that cannot be solved yet is not a novel idea: it is a standard approach to implement unification dependently-typed systems. This goes back to Huet's algorithm for higher-order unification [Huet 1975] and pattern unification [Miller 1991] where flexible-flexible pairs are delayed until at least one side becomes rigid. Our contribution lies in combining constraint suspension with ML-style implicit polymorphism— largely absent from dependently typed systems—and in formulating a declarative constraint semantics.

Conditional constraints [Pottier 2000] also delay resolution, waiting until the top-level constructor of a type is known. They provide an **if-then-else**-like primitive, but differ crucially from our suspended constraints: in Pottier's system, an unresolved conditional constraint is considered satisfiable, whereas in ours, an unresolved suspended constraint is not. This difference forces our semantics to track what is *known* in a context. Consequently, unresolved conditional constraints may enter a generalized type scheme as a form of qualified types, while our suspended constraints cannot. These semantic differences lead the two approaches to address very different user-facing type system features.

Outsideln [Schrijvers, Jones, Sulzmann and Vytiniotis 2009] is a type system for GADTs that introduces *delayed implications* of the form $[\bar{\alpha}](\forall\beta.C_1 \Rightarrow C_2)$. Constraint solving for delayed implications proceeds in two steps; solving simple constraints first and then solving delayed implications. The deferral ensures that inference for GADT match branches occurs when more is known about the scrutinee and expected return type from the context. To ensure principality, Outsideln enforces an algorithmic restriction: the variables $\bar{\alpha}$ must already be instantiated to concrete type constructors before they may be unified by the implication's conclusion $C_2$. This ensures information only flows from the outside into the implication's conclusion. Notably, they do give a declarative specification for this restriction, using an elegant but mysterious quantification on all possible ways to type the context outside the GADT clauses. Using our new perspective on *known* type information, we can say that their semantics enforces that only *known* information from outside GADT clauses can be used inside. Later work on Outsideln argues [Vytiniotis, Jones, Schrijvers and Sulzmann 2011] that delayed implication constraints make local let-generalization all but unmanageable, both in theory and implementation. Their proposed fix is to abandon local let-generalization altogether. By contrast, our work shows that the difficult interactions between let-generalization and suspended constraints can be resolved. Furthermore, Outsideln forgoes a declarative specification complete with respect to its inference algorithm, on the grounds that such a specification would be "as complicated and hard to understand as the [inference] algorithm". We
believe that our *omnidirectional recipe* could provide a declarative specification: one capable of
being principal and complete for GADTs, and we would be interested in studying this application.

*Higher-rank polymorphism.* Polytypes are not *higher-rank* in the usual sense; our interest in them stems from their role in OCaml's inference of polymorphic methods. Many systems for higher-rank polymorphism exist; here we highlight a few in the context of ML.

MLF is an extension of ML that supports first-class polymorphism that goes beyond the power of System F, while retaining type inference. It is a generalization of Garrigue and Rémy [1999]'s polytypes, relying on π-directionality, but it remains unclear how to effectively scale MLF to the rest of OCaml's features. FreezeML is an impredicative type inference system in which polymorphic variables can be *frozen*, written [x], and only allowing instantiation on ordinary (unfrozen) variables x. Unlike polytypes, FreezeML permits higher-rank types directly in the syntax of types, though these can be encoded back into polytypes. The essential difference is that generalization of higher-rank types is implicit, inferring the most-general type (if one exists).

QuickLook [Serrano, Hage, Jones and Vytiniotis 2020], Haskell's latest approach at impredicative higher-rank polymorphism, uses bidirectional propagation to take a "quick look" at the spine of an application to guide instantiation of higher-rank functions. This permits *argument reordering*, by allowing later arguments to influence the type of earlier ones within the same application spine. It mitigates the order-dependence of fixed directionality (§2.3) but still enforces a global direction of type propagation between surrounding constructs (e.g. let-bindings). In this sense, QuickLook is *locally omnidirectional* but *globally directional*: they reduce order sensitivity within applications, but do not provide a declarative account of type flow between arbitrary constructs, as required for omnidirectionality. More recently, Frost [Tang, Jiang, Oliveira and Lindley 2025] follows a similar line but extends it to handle η-expansion and introduces a freezing operator, akin to that of FreezeML, that helps propagate type information when the default order of inference is insufficient.

*Type-based disambiguation in SML.* In SML, tuples are treated as structural records with numeric labels, and projections such as #1 or #2 are type-directed. This relies on row typing: if *e* has the type {j = τ<sub>j</sub>; ϱ}, where ϱ is a row describing the remaining tuple fields, then *e*.j has type τ<sub>j</sub>. The same mechanism also underlies record projections.

However, SML does not support row-polymorphic definitions: restricting to monomorphic rows allows a simple yet efficient compilation strategy for records and tuples. To enforce this, SML adds a prose side-condition to the typing rules requiring that each row variable be fully determined by the “program context” [Milner, Harper, MacQueen and Tofte 1997, Section 4.11]. Our unicity conditions provides a precise, declarative specification for this informal restriction, filling a gap in the original specification.

Rossberg [2008, page 36] remarks that this restriction interacts poorly with let-polymorphism
and therefore not supported in practice:

Under item 1 the Definition states that “the program context” must determine the
exact type of flexible records, but it does not specify any bounds on the size of
this context. Unlimited context is clearly infeasible since it is incompatible with
let polymorphism: at the point of generalization the structure of a type must be
determined precisely enough to know what we have to quantify over. We thus
restrict the context for resolving flexible records to the innermost surrounding
value declaration, as most other SML systems seem to do as well. This is in par
with our treatment of overloading (see 5.8).
We have solved this difficult interaction between disambiguation and let-polymorphism. In particular, we implemented tuples in our prototype and formalize their meta-theory in Appendix §A; the system behaves as expected.

We also remark that Poly/ML [Matthews 2005] goes further than other SML implementations on this front, supporting examples that even rely on backpropagation

let fun fst r = #1 r in (fst (1, 2), fst (true, false)) end; Poly/ML OmniML

*Record field overloading in GHC.* Haskell 98 derives selector functions for each record field, an approach that precludes declaring two record types with the same field names within a single module. GHC 6.8.1 (2007) introduced the `DisambiguateRecordField` extension for type-directed disambiguation of record labels,<fnref n="14" /> and GHC 8.0.1 (2016) added `DuplicateRecordFields`, allowing distinct record types with overlapping field names in the same module.

However, the GHC developers found that type-based disambiguation using bidirectional type inference is not sufficiently predictable in practice for users [Gundry 2017], and that the reliance on projection functions, rather than a dedicated projection syntax, further complicated the implementation by making all function calls potentially ambiguous. As a result, GHC is gradually moving away from type-based disambiguation towards an approach based on qualified types constraints of the form `HasField "x" a b` (OverloadedRecordDot, 2017).<fnref n="15" />

For instance, the projection `ex₁` from §2.1 would be written as:

ex₁ :: HasField "x" a b => a → b
ex₁ r = getField @"x" r

GHC OmniML

It is worth emphasizing that OmniML rejects this program. Since OmniML implements *static* overloading, it requires a unique resolution for each overloaded occurrence; as a result, programs such as `ex₁`, whose projection is ambiguous, are ill-typed. In constrast, a type-class-based solution—*i.e.*, one using qualified types—implments *dynamic* rather than *static* overloading, allowing each instantiation to resolve the field independently. This distinction has practical consequences: dynamic overloading is able to naturally support field-polymorphic programs such as `ex₁`, but it does not guarantee efficient code generation (though GHC is often able to optimize type-class programs effectively).

Beyond efficiency, the `HasField` approach is also limited in expressiveness. It works well for records with 'simple' field types (*i.e.*, field types with *uniform* typing rules for projections), but it does not scale to field types where the typing rule itself depends on type-directed disambiguation—such as fields containing polymorphic types or GADT existentials. In contrast, suspended match constraints naturally accommodate such non-uniformity in typing rules.

*Semi-unification.* Semi-unification [Henglein 1989, 1993], introduced in the late 1980's, is a generalization of unification that solves a collection $\bigwedge_{i \in I} \tau_i \le \tau'_i$ of *instantiation inequalities*, meaning that there exist a unifier $\theta$ and a collection of substitutions $\bar{\rho}$ such that $\rho_i(\theta(\tau_i)) = \theta(\tau'_i)$. Unfortunately, semi-unification was soon proved undecidable [Kfoury, Tiuryn and Urzyczyn 1993] and almost abandoned for type inference purposes—even though Henglein observed that his semi-algorithm appeared to terminate on most ML type inference problems involving polymorphic

<footnote n="14">¹⁴https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/disambiguate_record_fields.html</footnote>

<footnote n="15">¹⁵https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/hasfield.html</footnote>
recursion.<fnref n="16" /> Moreover, in the absence of polymorphic recursion, semi-unification constraints arising from ML type inference are acyclic and therefore guaranteed to terminate.

Semi-unification constraints can be solved *incrementally*, in any order, making them a natural foundation for scaling omnidirectional type inference to ML-style polymorphism. Although it offered little advantage for traditional ML inference, Henglein’s algorithm was *omnidirectionally-ready*, merely waiting for fragile constructs to give it new life!

Motivated by this observation, we explored a second prototype that implements let-generalization via semi-unification. To enable a more direct encoding of type inference problems and improve solving efficiency, we enriched semi-unification constraints with a notion of *scope*, forming the same tree-like structure as regions in our *generalization tree* (§6). This extends the formalization of semi-unification with *unknowns* proposed by Lushman and Cormack [2008], and allows for more efficient handling of *monomorphization*—that is, instantiations that collapse into unification constraints (akin to *S-INST-MONO* in our constraint solver).

Although this prototype began from a different perspective, the implementation problems and their solutions turned out to be strikingly similar to those in our first prototype (described in §6). This close correspondence naturally raises the question of whether partial type schemes could be enriched to cope with polymorphic recursion.

## 8 Conclusions

We presented a constraint-based framework for omnidirectional type inference, scaled to ML with *local let-generalization*. Central to our approach is a new declarative account of when a type is *known* from the context, rather than *guessed*. Our constraint solver is omnidirectional: constraints may be solved in *any way*, enabled by partial type schemes. Through two instantiations of our *omnidirectional recipe*, we obtained a sound, complete, and *principal* type inference algorithm—in short, principality held *anyway*, precisely because of omnidirectionality.

*Future work.* We aim to extend our framework to support more advanced features. One direction is generalized *static overloading*; another is *higher-rank polymorphism*. We also plan to investigate *default rules*—a mechanism where ambiguity is resolved by falling back on a default, non-principal choice *e.g.* OCaml selects the most recent matching record type in scope for ambiguous field names.

## Acknowledgments

This work builds on a work-in-progress presentation of suspended constraints by Martinot and Scherer [2021]. We thank the anonymous reviewers for their thoughtful feedback and questions, and Simon Peyton-Jones, whose insightful remarks, we hope, helped us make this work more approachable. We are also grateful to Adam Gundry for clarifying aspects of record-field disambiguation in GHC, and to Jeremy Yallop for his sage guidance throughout this project. Finally, we thank Brendan Coll, Daniel Gooding, Micheal Lee, and François Pottier for their helpful comments on earlier drafts.

## References

* Jiří Beneš and Jonathan Immanuel Brachthäuser. 2025. The Simple Essence of Overloading. (2025).

* Arthur Charguéraud, Martin Bodin, Jana Dunfield, and Louis Riboulet. 2025. Typechecking of Overloading. In *Journées Francophones des Langages Applicatifs*.

* Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2014. Extending Type Inference to Variational Programs. *ACM Transactions on Programming Languages and Systems* 36, 1 (March 2014), 1–54. https://doi.org/10.1145/2518190

<footnote n="16">¹⁶Although the undecidability of semi-unification already implied the existence of such examples, the specific class of examples of non-terminating cases was only characterized later [Figueiredo and Camarao 2004]. These patterns are extremely complex, suggesting that they are unlikely to appear in practice, unless crafted deliberately.</footnote>
Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In *Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages* (Albuquerque, New Mexico) (POPL '82). Association for Computing Machinery, New York, NY, USA, 207-212. https://doi.org/10.1145/582153.582176

Lucilia Figueiredo and Carlos Camarao. 2004. Semi-unification and Periodicity of Turing Machines. (2004). https://www.researchgate.net/profile/Carlos-Camarao/publication/268426611_Semi-unification_and_Periodicity_of_Turing_Machines

Jacques Garrigue. 1998. Programming with polymorphic variants. In *ML workshop*, Vol. 13. Baltimore.

Jacques Garrigue and Didier Rémy. 1999. Extending ML with Semi-Explicit Higher-Order Polymorphism. *Information and Computation* 155, 1/2 (1999), 134-169. http://www.springerlink.com/content/m303472288241339/ A preliminary version appeared in TACS'97.

Jacques Garrigue and Didier Rémy. 2013. Ambivalent Types for Principal Type Inference with GADTs. In *Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings* (Lecture Notes in Computer Science, Vol. 8301), Chung-chieh Shan (Ed.). Springer, 257-272. https://doi.org/10.1007/978-3-319-03542-0_19

Adam Gundry. 2017. Overloaded Record Fields. https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0023-overloaded-record-fields.rst GHC proposal/RFC.

Fritz Henglein. 1989. *Polymorphic Type Inference and Semi-Unification*. PhD. New York University.

Fritz Henglein. 1993. Type inference with polymorphic recursion. *ACM Trans. Program. Lang. Syst.* 15, 2 (April 1993), 253-289. https://doi.org/10.1145/169701.169692

Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. *Transactions of the american mathematical society* 146 (1969), 29-60.

Gérard Huet. 1975. A unification algorithm for typed λ-calculus. *Theoretical Computer Science* 1, 1 (1975).

Mark P. Jones. 1995a. *Qualified types: theory and practice*. Cambridge University Press.

Mark P. Jones. 1995b. A System of Constructor Classes: Overloading and Implicit Higher-Order Polymorphism. *J. Funct. Program.* 5, 1 (1995), 1-35. https://doi.org/10.1017/S0956796800001210

A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. 1993. The Undecidability of the Semi-unification Problem. *Information and Computation* 102, 1 (1993), 83-101. https://doi.org/10.1006/inco.1993.1003

Didier Le Botlan and Didier Rémy. 2009. Recasting MLF. *Information and Computation* 207, 6 (2009), 726-785. https://doi.org/10.1016/j.ic.2008.12.006

Oukseh Lee and Kwangkeun Yi. 1998. Proofs about a folklore let-polymorphic type inference algorithm. *ACM Transactions on Programming Languages and Systems* 20, 4 (July 1998), 707-723. https://doi.org/10.1145/291891.291892

Daan Leijen and Wenjia Ye. 2025. Principal Type Inference under a Prefix. In *PLDI'25. ACM*, 1-24. https://www.microsoft.com/en-us/research/publication/principal-type-inference-under-a-prefix/ Backup Publisher: ACM SIGPLAN.

Brad Lushman and Gordon V Cormack. 2008. *Constraint-Based Typing for ML via Semiunification*. Technical Report CS-2008-10. University of Waterloo, Ontario, Canada. 49 pages.

Olivier Martinot and Gabriel Scherer. 2021. Frozen inference constraints for type-directed disambiguation. In *ML Family Workshop*. online, South Korea. https://inria.hal.science/hal-03510890

David Matthews. 2005. Poly/ML. https://github.com/polymol/polymol version 4.1.

Dale Miller. 1991. Unification of Simply Typed Lamda-Terms as Logic Programming. In *Logic Programming, Proceedings of the Eighth International Conference, Paris, France, June 24-28, 1991*, Koichi Furukawa (Ed.). MIT Press, 255-269.

Robin Milner, Robert Harper, David MacQueen, and Mads Tofte. 1997. *The Definition of Standard ML*. The MIT Press. https://doi.org/10.7551/mitpress/2319.001.0001

Martin Odersky and Konstantin Läufer. 1996. Putting Type Annotations to Work. In *Conference Record of POPL '96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, January 21-24, 1996*, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 54-67. https://doi.org/10.1145/237721.237729

Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type inference with constrained types. *Theory and Practice of Object Systems* 5, 1 (1999), 35-55. https://doi.org/10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4

Atsushi Ohori. 1995. A Polymorphic Record Calculus and Its Compilation. *ACM Trans. Program. Lang. Syst.* 17, 6 (1995), 844-895. https://doi.org/10.1145/218570.218572

Benjamin C. Pierce and David N. Turner. 1998. Local Type Inference. In *POPL '98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998*, David B. MacQueen and Luca Cardelli (Eds.). ACM, 252-265. https://doi.org/10.1145/268946.268967

François Pottier. 2000. A Versatile Constraint-Based Type Inference System. *Nord. J. Comput.* 7, 4 (2000), 312-347.

François Pottier. 2014. Hindley-Milner elaboration in applicative style. In *ICFP*. http://cambium.inria.fr/~fpottier/publis/fpottier-elaboration.pdf
François Pottier. 2018. Inferno. A library for constraint-based Hindley-Milner type inference. https://gitlab.inria.fr/fpottier/inferno Available on opam https://opam.ocaml.org/.

François Pottier and Didier Rémy. 2005. The Essence of ML Type Inference. In *Advanced Topics in Types and Programming Languages*, Benjamin C. Pierce (Ed.). MIT Press, Chapter 10, 389–489. https://pauillac.inria.fr/~remy/attapl/

Didier Rémy. 1989. Type checking records and variants in a natural extension of ML. In *Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages* (Austin, Texas, USA) (POPL '89). Association for Computing Machinery, New York, NY, USA, 77–88. https://doi.org/10.1145/75277.75284

Didier Rémy. 1990. *Algèbres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels*. Thèse de doctorat. Université de Paris 7.

Didier Rémy. 1992. *Extending ML Type System with a Sorted Equational Theory*. Research Report 1766. Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France.

Didier Rémy and Jerome Vouillon. 1997. *Objective ML: A Simple Object-Oriented Extension of ML*. In *Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997*, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM Press, 40–53. https://doi.org/10.1145/263699.263707

Andreas Rossberg. 2008. HaMLet: To Be Or Not To Be Standard ML. https://people.mpi-sws.org/~rossberg/hamlet/hamlet-1.3.1.pdf hamlet manual, version 1.3.1.

Tom Schrijvers, Simon L. Peyton Jones, Martin Sulzmann, and Dimitrios Vytiniotis. 2009. Complete and decidable type inference for GADTs. In *Proceeding of the 14th ACM SIGPLAN international conference on Functional programming*, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, Graham Hutton and Andrew P. Tolmach (Eds.). ACM, 341–352. https://doi.org/10.1145/1596550.1596599

Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis. 2020. A quick look at impredicativity. *Proc. ACM Program. Lang.* 4, ICFP (2020), 89:1–89:29. https://doi.org/10.1145/3408971

Wenhao Tang, Shengyi Jiang, Bruno C. d. S. Oliveira, and Sam Lindley. 2025. Freezing Bidirectional Typing. presented at the ML Family Workshop.

Robert Endre Tarjan. 1975. Efficiency of a Good But Not Linear Set Union Algorithm. *J. ACM* 22, 2 (1975), 215–225. https://doi.org/10.1145/321879.321884

Dimitrios Vytiniotis, Simon L. Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X) Modular type inference with local assumptions. *J. Funct. Program.* 21, 4-5 (2011), 333–412. https://doi.org/10.1017/S0956796811000098

Philip Wadler and Stephen Blott. 1989. How to Make ad-hoc Polymorphism Less ad-hoc. In *Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989*. ACM Press, 60–76. https://doi.org/10.1145/75277.75283

Mitchell Wand. 1989. Type Inference for Record Concatenation and Multiple Inheritance. In *Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89)*, Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 92–97. https://doi.org/10.1109/LICS.1989.39162

Leo White. 2013. Semi-explicit polymorphic parameters. presented at the ML Family Workshop.

Leo White. 2023. Semi-explicit polymorphic parameters. (sep 2023). Presentation at the Higher-order, Typed, Inferred, Strict: ML Family workshops.

Xu Xue and Bruno C. d. S. Oliveira. 2024. Contextual Typing. *Proc. ACM Program. Lang.* 8, ICFP (2024), 880–908. https://doi.org/10.1145/3674655
# Organization of appendices

*Reference appendix.* §A gives a full reference for all definitions, grammars and figures in the paper, including all cases (even those omitted from the main paper for reasons of space).

*Proof appendices.* These appendices contain proofs for the formal claims in the article. They are typically written tersely.

* §B proves properties of the constraint language and its semantics. The main result is canonicalization, which morally establishes that uses of the contextual rule MATCH-CTX can be “permuted down” in the proof until they are all at the bottom of the derivation, followed by a proof on a simple constraint.

* §C proves the correctness of the constraint solver with respect to the semantics.

* §D proves the properties about the OmniML type system, in particular the correctness of constraint generation.
## A Full technical reference

This section repeats all the technical definitions mentioned in the paper, including the cases, rules, and definitions that were omitted from the main paper to save space. It can serve as a useful cheatsheet to understand a definition in full, or when studying the meta-theory of the system.

$$ \alpha, \beta, \gamma \in \mathcal{V} $$

$$ \tau ::= \alpha \mid 1 \mid \tau_1 \rightarrow \tau_2 \mid \Pi_{i=1}^n \tau_i \mid \text{rcd } T \ \bar{\tau} \mid [\sigma] $$

$$ \sigma ::= \tau \mid \forall \alpha. \sigma $$

### g

$$ \mathbf{r} ::= (g, \phi) $$

$$ \mathfrak{G} \subseteq \mathfrak{G} $$

$$ \mathfrak{R} \subseteq \mathfrak{R} $$

$$ \begin{array}{l} C ::= \text{true} \mid \text{false} \mid C_1 \wedge C_2 \mid \exists \alpha. C \mid \forall \alpha. C \mid \tau_1 = \tau_2 \\ \qquad \mid \text{let } x = \lambda \alpha. C_1 \text{ in } C_2 \mid x \ \tau \\ \qquad \mid \text{match } \tau \text{ with } \bar{\chi} \\ \qquad \mid \epsilon \mid \text{let } x \ \alpha [\bar{\alpha}] = C_1 \text{ in } C_2 \mid \exists i^x. C \mid i(\alpha) \rightsquigarrow \tau \\ \qquad \mid t. \ell \le \tau_1 \rightarrow \tau_2 \mid \text{dom } t = \bar{\ell} \mid s \le \tau \mid x \le s \end{array} $$

$$ \chi ::= \rho \Rightarrow C $$

$$ \rho ::= \_ | \Pi \alpha_j \mid \text{rcd } t \ _ | [s] $$

$$ \phi ::= \emptyset | \phi[\alpha := g] | \phi[x := \mathfrak{G}] | \phi[x := \mathfrak{R}] | \phi[i := \phi'] $$

$$ U ::= \text{true} \mid \text{false} \mid U_1 \wedge U_2 \mid \exists \alpha. U \mid \epsilon $$

$$ \epsilon ::= \emptyset \mid \tau = \epsilon $$

$$ \begin{array}{l} \mathcal{C} ::= \Box | \mathcal{C} \wedge C \mid C \wedge \mathcal{C} \mid \exists \alpha. \mathcal{C} \mid \forall \alpha. \mathcal{C} \\ \qquad \mid \text{let } x = \lambda \alpha. \mathcal{C} \text{ in } C \mid \text{let } x = \lambda \alpha. C \text{ in } \mathcal{C} \\ \qquad \mid \text{let } x \ \alpha [\bar{\alpha}] = \mathcal{C} \text{ in } C \mid \text{let } x \ \alpha [\bar{\alpha}] = C \text{ in } \mathcal{C} \mid \exists i^x. \mathcal{C} \end{array} $$

$$ \zeta ::= v \bar{\gamma}. \tau $$

### s

$$ \begin{array}{l} e ::= x \mid () \mid \lambda x. e \mid e_1 \ e_2 \mid \text{let } x = e_1 \text{ in } e_2 \mid (e : \exists \bar{\alpha}. \tau) \\ \qquad \mid \{\ell = e\} \mid e. \ell \mid T. \{\ell = e\} \mid e.T. \ell \\ \qquad \mid (e_1, \dots, e_n) \mid e. j \mid e.n.j \\ \qquad \mid [e] \mid [e : \exists \bar{\alpha}. \sigma] \mid \langle e \rangle \mid \langle e : \exists \bar{\alpha}. \sigma \rangle \\ \qquad \mid \Box \text{ with } \bar{e} \end{array} $$

$$ \begin{array}{l} \mathcal{E} ::= \Box | \mathcal{E} \ e | e \mathcal{E} \mid \text{let } x = \mathcal{E} \text{ in } e \mid \text{let } x = e \text{ in } \mathcal{E} \mid (\mathcal{E} : \exists \bar{\alpha}. \tau) \\ \qquad \mid \{\ell_1 = e_1 \ \dots \ \ell_i = \mathcal{E} \ \dots \ \ell_n = e_n\} \mid \mathcal{E}. \ell \\ \qquad \mid T. \{\ell_1 = e_1 \ \dots \ \ell_i = \mathcal{E} \ \dots \ \ell_n = e_n\} \mid \mathcal{E}. T. \ell \\ \qquad \mid (e_1, \dots, \mathcal{E}, \dots, e_n) \mid \mathcal{E}. j \mid \mathcal{E}. j^n \\ \qquad \mid [\mathcal{E}] \mid [\mathcal{E} : \exists \bar{\alpha}. \sigma] \mid \langle \mathcal{E} \rangle \mid \langle \mathcal{E} : \exists \bar{\alpha}. \sigma \rangle \\ \qquad \mid \Box \text{ with } e_1, \dots, \mathcal{E}, \dots, e_n \end{array} $$

$$ \Gamma ::= \emptyset | \Gamma, x : \sigma $$

$$ \Omega ::= \emptyset | \Omega, \ell : \forall \bar{\alpha}. \text{rcd } T \ \bar{\alpha} \rightarrow \tau $$

Type variables

Types

Type schemes

Ground types

Ground region

Sets of ground types

Sets of ground regions

Constraints

Branches

Shape patterns

Semantic environment

Unification problems

Multi-equations

Constraint contexts

Shapes

Canonical principal shapes

Terms

Term contexts

$\phi \vdash C$ Under the environment $\phi$, the constraint $C$ is satisfiable.
$$ \frac{\text{TRUE}}{\phi \vdash \text{true}} $$

$$ \frac{\text{CONJ}}{\phi \vdash C_1 \quad \phi \vdash C_2} \qquad \frac{\text{EXISTS}}{\phi \vdash \exists \alpha. C} $$

$$ \frac{\text{FORALL}}{\phi \vdash \exists \alpha. C} $$

$$ \frac{\text{UNIF}}{\phi \vdash \tau_1 = \tau_2} $$

$$ \frac{\text{UNIF}}{\phi \vdash \tau_1 = \tau_2} $$

$$ \text{LET} \qquad \frac{\mathfrak{S} = \phi(\lambda\alpha. C_1) \qquad \mathfrak{S} \neq \emptyset}{\phi[x := \mathfrak{S}] \vdash C_2} $$

$$ \frac{\text{APP}}{\phi \vdash x \tau} \qquad \frac{\phi(\tau) \in \phi(x)}{\phi \vdash x \tau} $$

$$ \frac{\text{MATCH-CTX}}{\mathscr{C}[\tau!\zeta] \qquad \phi \vdash \mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}]} \qquad \phi \vdash \mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}] $$

$$ \frac{\text{MULTI-UNIF}}{\forall \tau \in \epsilon, \phi(\tau) = \mathfrak{g}} $$

$$ \frac{\text{LETR}}{\phi \vdash \text{ let } x \ \alpha \ [\bar{\alpha}] = C_1 \text{ in } C_2} \qquad \frac{\text{APPR}}{\phi \vdash x \tau} $$

$$ \frac{\text{APP'R}}{\phi(\tau), \_ \in \phi(x)} \qquad \frac{\phi \vdash x \tau}{\phi \vdash x \tau} $$

$$ \frac{\text{EXISTS-INST}}{\phi[\_ := \phi'] \vdash C} \qquad \frac{\text{INCR-INST}}{\phi \vdash i^x. C} $$

$$ \frac{\phi(i)(\alpha) = \phi(\tau)}{\phi \vdash i(\alpha) \rightsquigarrow \tau} $$

$$ T.\ell \le \tau_1 \rightarrow \tau_2 \quad \triangleq \quad \left\{ \begin{array}{ll} \exists \bar{\alpha}. \tau_1 = \text{rcd } T \bar{\alpha} \wedge \tau_2 = \tau & \text{if } \Omega(T.\ell) = \forall \bar{\alpha}. \text{rcd } T \bar{\alpha} \rightarrow \tau \\ \text{false} & \text{otherwise} \end{array} \right. \\ \text{dom } T = \bar{\ell} \quad \triangleq \quad \left\{ \begin{array}{ll} \text{true} & \text{if } \text{dom } (\Omega(T)) = \bar{\ell} \\ \text{false} & \text{otherwise} \end{array} \right. \\ (\forall \bar{\alpha}. \tau') \le \tau \quad \triangleq \quad \exists \bar{\alpha}. \tau' = \tau \\ x \le (\forall \bar{\alpha}. \tau) \quad \triangleq \quad \forall \bar{\alpha}. x \tau $$

$$ \text{match } \tau := \zeta \text{ with } \rho \Rightarrow \bar{C} \quad \triangleq \quad \left\{ \begin{array}{ll} \exists \bar{\alpha}. \tau = \zeta \bar{\alpha} \wedge \theta(C_i) & \text{if } \rho_i \text{ matches } \zeta \bar{\alpha} \hookrightarrow \theta \\ \text{false} & \text{otherwise} \end{array} \right. $$

$$ \phi(\lambda\alpha.C) \triangleq \{\mathfrak{g} \in \mathcal{G} : \phi[\alpha := \mathfrak{g}] \vdash C\} $$

$$ \phi(\lambda\alpha[\bar{\alpha}].C) \triangleq \{(\mathfrak{g}, \phi[\alpha := \mathfrak{g}, \bar{\alpha} := \bar{\mathfrak{g}}]) \in \mathcal{R} : \phi[\alpha := \mathfrak{g}, \bar{\alpha} := \bar{\mathfrak{g}}] \vdash C\} $$

$$ \mathscr{C}[\tau!\zeta] \triangleq \forall \phi, \mathfrak{g}, \phi \vdash [\mathscr{C}[\tau = \mathfrak{g}]] \implies \text{shape}(\mathfrak{g}) = \zeta $$

<figure><img src="image_12.png" /></figure>

The shape $\zeta'$ is an instance of $\zeta$. Alternatively, $\zeta'$ is more general than $\zeta$.

$$ \frac{\text{INST-SHAPE}}{v\bar{\gamma}_1. \tau \preceq v\bar{\gamma}_2. \tau [\bar{\gamma}_1 := \bar{\tau}_1]} $$

We write $\perp$ for the trivial shape $v\gamma$. $\gamma$. $S$ denotes the set of shapes and $S^*$ is the set of non-trivial shapes.

**Definition A.1.** A non-trivial shape $\zeta \in S^*$ is the principal shape of the type $\tau$ iff:

(1) $\exists \bar{\tau}', \tau = \zeta \bar{\tau}'$

(2) $\forall \zeta' \in S^*, \forall \bar{\tau}', \tau = \zeta' \bar{\tau}' \Rightarrow \zeta' \preceq \zeta'$

A principal shape $v\bar{\gamma}$. $\tau$ is *canonical* if the sequence of its free variables $\bar{\gamma}$ appear in the order in which the variables occur in $\tau$. shape($\tau$) is the canonical principal shape of $\tau$.
$$ \rho \text{ matches } \zeta \bar{\gamma} \leftrightarrow \theta $$

The pattern $\rho$ matches the shape $\zeta$ with fresh components $\bar{\gamma}$ binding pattern variables in $\theta$.

$$ \Pi \alpha_j \text{ matches } (v\bar{\gamma}. \Pi_{i=1}^n \bar{\gamma}) \bar{\gamma}' \triangleq [\alpha := \gamma_j'] \quad \text{if } n \ge j $$

$$ \text{rcd } t \text{ _ matches } (v\bar{\gamma}. \text{rcd } T \bar{\gamma}) \bar{\gamma}' \triangleq [t := T] $$

$$ [s] \text{ matches } (v\bar{\gamma}. [\sigma]) \bar{\gamma}' \triangleq [s := \sigma[\bar{\gamma} := \bar{\gamma}']$$

### C simple

The constraint C is simple.

SIMPLE-TRUE
true simple

SIMPLE-FALSE
false simple

SIMPLE-CONJ

$C_1 \text{ simple} \quad C_2 \text{ simple}$

$C_1 \wedge C_2 \text{ simple}$

SIMPLE-EXISTS

$C \text{ simple}$

$\exists \alpha. C \text{ simple}$

SIMPLE-FORALL

$C \text{ simple}$

$\forall \alpha. C \text{ simple}$

SIMPLE-UNIF

$\tau_1 = \tau_2 \text{ simple}$

SIMPLE-LET

$C_1 \text{ simple} \quad C_2 \text{ simple}$

$\text{let } x = \lambda \alpha. C_1 \text{ in } C_2 \text{ simple}$

SIMPLE-APP

$x \tau \text{ simple}$

SIMPLE-MULTI-UNIF

$\epsilon \text{ simple}$

SIMPLE-LETR

$C_1 \text{ simple}$

$C_2 \text{ simple}$

$\text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } C_2 \text{ simple}$

SIMPLE-EXISTS-INST

$C \text{ simple}$

$\exists i^x. C \text{ simple}$

SIMPLE-INCR-INST

$i(\alpha) \rightsquigarrow \tau \text{ simple}$

We write $\phi \vdash_{\text{simple}} C$ for the satisfiability of a simple constraint C.

### C simple

The constraint context $\mathcal{C}$ is simple.

SIMPLE-CTX-HOLE

$\Box \text{ simple}$

SIMPLE-CTX-CONJ-LEFT

$\mathcal{C} \text{ simple}$

$C \text{ simple}$

$\mathcal{C} \wedge C \text{ simple}$

SIMPLE-CTX-CONJ-RIGHT

$\mathcal{C} \text{ simple}$

$C \text{ simple}$

$C \wedge \mathcal{C} \text{ simple}$

SIMPLE-CTX-EXISTS

$\mathcal{C} \text{ simple}$

$\exists \alpha. \mathcal{C} \text{ simple}$

SIMPLE-CTX-FORALL

$\mathcal{C} \text{ simple}$

$\forall \alpha. \mathcal{C} \text{ simple}$

SIMPLE-CTX-LET-ABS

$\mathcal{C} \text{ simple}$

$C \text{ simple}$

$\text{let } x = \lambda \alpha. \mathcal{C} \text{ in } C \text{ simple}$

SIMPLE-CTX-LET-IN

$C \text{ simple}$

$\mathcal{C} \text{ simple}$

$\text{let } x = \lambda \alpha. C \text{ in } \mathcal{C} \text{ simple}$

SIMPLE-CTX-EXISTS-INST

$\mathcal{C} \text{ simple}$

$\exists i^x. \mathcal{C} \text{ simple}$

### [C]

The erasure of C.
<figure><img src="image_13.png" /></figure>

### $\phi \Vdash C$ Under the semantic environment $\phi$, the constraint $C$ is canonically satisfiable.

$$ \frac{\text{CAN-SIMPLE} \quad \phi \vdash_{\text{simple}} C}{\phi \Vdash C} $$

$$ \frac{\text{CAN-MATCH-CTX} \quad \mathcal{C}[\tau!\zeta] \qquad \phi \Vdash \mathcal{C}[\text{match } \tau := \zeta \text{ with } \bar{\alpha}]}{\phi \Vdash \mathcal{C}[\text{match } \tau \text{ with } \bar{\alpha}]} $$

### $T.\ell \le \tau_1 \to \tau_2$ The label $\ell$ of the record $T$ has the field type $\tau_2$ and record type $\tau_1$.

$$ \frac{\text{LAB-INST} \qquad \Omega(T.\ell) = \forall \bar{\alpha}. \text{rcd } T \bar{\alpha} \to \tau}{T.\ell \le \text{rcd } T \bar{\tau} \to \tau[\bar{\alpha} := \bar{\tau}]} $$

### $\ell \triangleright T$ The label $\ell$ infers the unique record name $T$.

### $\bar{\ell} \triangleright T$ The closed set of labels $\bar{\ell}$ infer the unique record name $T$.

$$ \frac{\text{LAB-UNI} \qquad \ell \in \text{dom}(\Omega(T)) \qquad \forall T', \ell \in \text{dom}(\Omega(T')) \implies T = T'}{\ell \triangleright T} $$

$$ \frac{\text{LABS-UNI} \qquad \text{dom}(\Omega(T)) = \bar{\ell} \qquad \forall T', \text{dom}(\Omega(T')) = \bar{\ell} \implies T = T'}{\bar{\ell} \triangleright T} $$

### $\Gamma \vdash e : \sigma$ Under the typing context $\Gamma$, the term $e$ is assigned the type $\sigma$
$\mathbf{VAR}$
$x : \sigma \in \Gamma$
$\Gamma \vdash x : \sigma$

$\mathbf{FUN}$
$\Gamma, x : \tau_1 \vdash e : \tau_2$
$\Gamma \vdash \lambda x. e : \tau_1 \rightarrow \tau_2$

$\mathbf{APP}$
$\Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2$
$\Gamma \vdash e_2 : \tau_1$
$\Gamma \vdash e_1 e_2 : \tau_2$

$\mathbf{UNIT}$
$\Gamma \vdash () : 1$

$\mathbf{annot}$
$\Gamma \vdash e : \tau[\tilde{\alpha} := \tilde{\tau}]$
$\Gamma \vdash (e : \exists \tilde{\alpha}. \tau) : \tau[\tilde{\alpha} := \tilde{\tau}]$

$\mathbf{Gen}$
$\Gamma \vdash e : \sigma$ $\alpha \# \Gamma$
$\Gamma \vdash e : \forall \alpha. \sigma$

$\mathbf{Inst}$
$\Gamma \vdash e : \forall \alpha. \sigma$
$\Gamma \vdash e : \sigma[\alpha := \tau]$

$\mathbf{Let}$
$\Gamma \vdash e_1 : \sigma$ $\Gamma, x : \sigma \vdash e_2 : \tau$
$\Gamma \vdash \text{let } x = e_1 \text{ in } e_2 : \tau$

$\mathbf{Tuple}$
$(\Gamma \vdash e_i : \tau_i)^{n}_{i=1}$
$\Gamma \vdash (e_1, \dots, e_n) : \Pi^{n}_{i=1} \tau_i$

$\mathbf{Proj-X}$
$\Gamma \vdash e : \Pi^{n}_{i=1} \tau_i$ $1 \le j \le n$
$\Gamma \vdash e.j^n : \tau_j$

$\mathbf{Proj-I}$
$\mathscr{E}[e \triangleright v \tilde{\gamma}. \Pi^{n}_{i=1} \tilde{\gamma}]$ $\Gamma \vdash \mathscr{E}[e.j^n] : \tau$
$\Gamma \vdash \mathscr{E}[e.j] : \tau$

$\mathbf{Poly-X}$
$\Gamma \vdash e : \sigma[\tilde{\alpha} := \tilde{\tau}]$
$\Gamma \vdash [e : \exists \tilde{\alpha}. \sigma] : [\sigma[\tilde{\alpha} := \tilde{\tau}]]$

$\mathbf{Poly-I}$
$\mathscr{E}[\Box \triangleleft v \tilde{\gamma}. [\sigma] | e]$ $\Gamma \vdash \mathscr{E}[[e : \exists \tilde{\gamma}. \sigma]] : \tau$
$\Gamma \vdash \mathscr{E}[[e]] : \tau$

$\mathbf{Use-X}$
$\Gamma \vdash e : [\sigma][\tilde{\alpha} := \tilde{\tau}]$
$\Gamma \vdash \langle e : \exists \tilde{\alpha}. \sigma \rangle : \sigma[\tilde{\alpha} := \tilde{\tau}]$

$\mathbf{Use-I}$
$\mathscr{E}[e \triangleright v \tilde{\gamma}. [\sigma]]$ $\Gamma \vdash \mathscr{E}[\langle e : \exists \tilde{\gamma}. \sigma \rangle] : \tau$
$\Gamma \vdash \mathscr{E}[\langle e \rangle] : \tau$

$\mathbf{RCD-X}$
$\mathrm{dom}(\Omega(T)) = \tilde{\ell}$ $(T.\ell_i \le \tau \rightarrow \tau_i)^{n}_{i=1}$ $(\Gamma \vdash e_i : \tau_i)^{n}_{i=1}$
$\Gamma \vdash T.\{\ell_1 = e_1; \dots; \ell_n = e_n\} : \tau$

$\mathbf{RCD-CLOSED}$
$\tilde{\ell} \triangleright T$ $\Gamma \vdash T.\{\overline{\ell = e}\} : \tau$
$\Gamma \vdash \{\overline{\ell = e}\} : \tau$

$\mathbf{RCD-I}$
$\mathscr{E}[\Box \triangleleft v \tilde{\gamma}. \mathrm{rcd} T \tilde{\gamma} | \tilde{e}]$ $\Gamma \vdash \mathscr{E}[T.\{\overline{\ell = e}\}] : \tau$
$\Gamma \vdash \mathscr{E}[\{\overline{\ell = e}\}] : \tau$

$\mathbf{RCD-PROJ-X}$
$T.\ell \le \tau_1 \rightarrow \tau_2$ $\Gamma \vdash e : \tau_1$
$\Gamma \vdash e.T.\ell : \tau_2$

$\mathbf{RCD-PROJ-CLOSED}$
$\ell \triangleright T$ $\Gamma \vdash e.T.\ell : \tau$
$\Gamma \vdash e.\ell : \tau$

$\mathbf{RCD-PROJ-I}$
$\mathscr{E}[e \triangleright v \tilde{\gamma}. \mathrm{rcd} T \tilde{\gamma}]$ $\Gamma \vdash \mathscr{E}[e.T.\ell] : \tau$
$\Gamma \vdash \mathscr{E}[e.\ell] : \tau$

$\mathbf{Hole}$
$(\Gamma \vdash e_i : \tau_i)^{n}_{i=1}$
$\Gamma \vdash \Box \text{ with } \tilde{e} : \tau'$

$\mathscr{E}[e \triangleright \zeta] \triangleq \forall \Gamma, \tau, g, \Gamma \vdash \mathscr{E}[\Box \text{ with } (e : g)] : \tau \implies \mathrm{shape}(g) = \zeta$
$\mathscr{E}[\Box \triangleleft \zeta | \tilde{e}] \triangleq \forall \Gamma, \tau, g, \Gamma \vdash \mathscr{E}[((\Box \text{ with } \tilde{e}) : g)] : \tau \implies \mathrm{shape}(g) = \zeta$
Γ ⊢ e : τ ] [ Γ ⊢ e : τ ] is satisfiable iff e has the expected known type τ under known context Γ.

[[e : σ]] [[e : σ]] is satisfiable iff e has the expected known type σ.

[[e : τ]] [[e : τ]] is satisfiable iff e has the expected known type τ.

$$
[[x : \tau]] \quad \triangleq \quad x \tau
$$

$$
[[() : \tau]] \quad \triangleq \quad \tau = 1
$$

$$
[[\lambda x. e : \tau]] \quad \triangleq \quad \exists \alpha, \beta. \text{let } x = \lambda \alpha'. \alpha' = \alpha \text{ in } [[e : \beta]] \wedge \tau = \alpha \to \beta
$$

$$
[[e_1 e_2 : \tau]] \quad \triangleq \quad \exists \alpha, \beta. [[e_1 : \beta]] \wedge [[e_2 : \alpha]] \wedge \beta = \alpha \to \tau
$$

$$
[[\text{let } x = e_1 \text{ in } e_2 : \tau]] \quad \triangleq \quad \text{let } x = \lambda \alpha. [[e_1 : \alpha]] \text{ in } [[e_2 : \tau]]
$$

$$
[[ (e : \exists \tilde{\alpha}. \tau') : \tau ]] \triangleq \exists \tilde{\alpha}. [[e : \tau'] ] \wedge \tau = \tau'
$$

$$
[[ (e_1, \dots, e_n) : \tau ]] \triangleq \exists \bar{\alpha}. \tau = \Pi_{i=1}^n \bar{\alpha} \wedge \bigwedge_{i=1}^n [e_i : \alpha_i]
$$

$$
[[e.j^n : \tau]] \quad \triangleq \quad \exists \alpha, \bar{\alpha}. [[e : \alpha]] \wedge \alpha = \Pi_{i=1}^n \bar{\alpha} \wedge \tau = \alpha_j
$$

$$
[[e.j : \tau]] \quad \triangleq \quad \exists \alpha. [[e : \alpha]] \wedge \text{match } \alpha \text{ with } \Pi \beta_j \Rightarrow \tau = \beta
$$

$$
[[e : \exists \bar{\alpha}. \sigma] : \tau] \quad \triangleq \quad \exists \bar{\alpha}. [[e : \sigma]] \wedge \tau = [\sigma]
$$

$$
[[\langle e : \exists \bar{\alpha}. \sigma \rangle : \tau]] \triangleq \exists \bar{\alpha}, \beta. [[e : \beta]] \wedge \beta = [\sigma] \wedge \sigma \le \tau
$$

$$
[[\langle e \rangle : \tau]] \quad \triangleq \quad \exists \alpha. [[e : \alpha]] \wedge \text{match } \alpha \text{ with } [s] \Rightarrow s \le \tau
$$

$$
[[e] : \tau] \quad \triangleq \quad \text{let } x = \lambda \alpha. [[e : \alpha]] \text{ in match } \tau \text{ with } [s] \Rightarrow x \le s
$$

$$
[e.\ell : \tau] \quad \triangleq \quad \begin{cases} [e.T.\ell : \tau] & \text{if } \ell \triangleright T \\ \exists \alpha. [e : \alpha] \wedge \text{match } \alpha \text{ with rcd } t_- \Rightarrow t.\ell \le \alpha \to \tau & \text{otherwise} \end{cases}
$$

$$
[[e.T.\ell : \tau]] \quad \triangleq \quad \exists \alpha. [[e : \alpha]] \wedge T.\ell \le \alpha \to \tau
$$

$$
\overline{[\{\overline{\ell} = e\} : \tau]} \triangleq \left\{
\begin{array}{@{}l@{}}
  \overline{[T.\{\overline{\ell} = e\} : \tau]} \\
  \quad \exists \bar{\alpha}. \bigwedge_{i=1}^n [e_i : \alpha_i] \\
  \quad \wedge \text{ match } \tau \text{ with rcd } t_- \Rightarrow (\text{dom } t = \bar{\ell} \wedge \bigwedge_{i=1}^n t.\ell_i \le \tau \to \alpha_i)
\end{array}
\right.
\quad \text{if } \bar{\ell} \triangleright T \\
\text{otherwise}
$$

$$
[[T.\overline{\{\ell = e\}} : \tau]] \triangleq \exists \bar{\alpha}. \bigwedge_{i=1}^{n} [e_i : \alpha_i] \wedge \text{dom } T = \bar{\ell} \wedge \bigwedge_{i=1}^{n} T.\ell_i \le \tau \to \alpha_i
$$

$$
\Box \text{ with } \bar{e} : \tau] \quad \triangleq \quad \exists \bar{\alpha} . \bigwedge_{i=1}^{n} [e_i : \alpha_i]
$$

$$
[[e : \forall \bar{\alpha}. \tau]] \quad \triangleq \quad \forall \bar{\alpha}. [[e : \tau]]
$$

$$
[[\emptyset \vdash e : \tau]] \quad \triangleq \quad [[e : \tau]]
$$

$$
[[x : \sigma, \Gamma \vdash e : \tau]] \quad \triangleq \quad \text{let } x = \lambda \alpha. \sigma \le \alpha \text{ in } [[\Gamma \vdash e : \tau]]
$$

Note: When τ is α it is considered an unknown expected type.

**e simple** The term *e* is simple.
$$ \frac{\text{SIMPLE-VAR}}{x \text{ simple}} \qquad \frac{\text{SIMPLE-FUN}}{\lambda x. e \text{ simple}} \qquad \frac{\text{SIMPLE-APP}}{e_1 \text{ simple} \quad e_2 \text{ simple}} \qquad \frac{\text{SIMPLE-UNIT}}{() \text{ simple}} $$

$$ \frac{\text{SIMPLE-LET}}{\text{let } x = e_1 \text{ in } e_2 \text{ simple}} \qquad \frac{\text{SIMPLE-ANNOT}}{(e : \exists \bar{\alpha}. \tau) \text{ simple}} \qquad \frac{\text{SIMPLE-TUPLE}}{(e_i \text{ simple})_{i=1}^n}{(e_1, \dots, e_n) \text{ simple}} \qquad \frac{\text{SIMPLE-PROJ-X}}{e \text{ simple}} \frac{e \cdot j^n \text{ simple}}{e \cdot j^n \text{ simple}} $$

$$ \frac{\text{SIMPLE-POLY-X}}{[e : \exists \bar{\alpha}. \sigma] \text{ simple}} \qquad \frac{\text{SIMPLE-USE-X}}{\langle e : \exists \bar{\alpha}. \sigma \rangle \text{ simple}} \qquad \frac{\text{SIMPLE-RCD-X}}{T.\{\ell_1 = e_1 \dots \ell_n = e_n\}} \qquad \frac{\text{SIMPLE-RCD-CLOSED}}{\{\ell_1 = e_1 \dots \ell_n = e_n\}} \frac{\bar{\ell} \triangleright T}{\ell_1 \triangleright T} $$

$$ \frac{\text{SIMPLE-RCD-PROJ-X}}{e \text{ simple}} \qquad \frac{\text{SIMPLE-RCD-PROJ-CLOSED}}{e.T.\ell \text{ simple}} \qquad \frac{\text{SIMPLE-HOLE}}{e.\ell \text{ simple}} \frac{(e_i \text{ simple})_{i=1}^n}{(\square \text{ with } \bar{e}) \text{ simple}} $$

<figure><img src="image_14.png" /></figure>

$[e]$ The erasure of $e$.

$$ \begin{array}{l@{\quad}l@{\quad}l} \lfloor x \rfloor & \triangleq & x \\ \lfloor \lambda x. e \rfloor & \triangleq & \lambda x. \lfloor e \rfloor \\ \lfloor e_1 \ e_2 \rfloor & \triangleq & \lfloor e_1 \rfloor \lfloor e_2 \rfloor \\ \lfloor \, \rfloor & \triangleq & () \\ \lfloor \text{let } x = e_1 \text{ in } e_2 \rfloor & \triangleq & \text{let } x = \lfloor e_1 \rfloor \text{ in } \lfloor e_2 \rfloor \\ \lfloor (e : \exists \bar{\alpha}. \tau) \rfloor & \triangleq & (\lfloor e \rfloor : \exists \bar{\alpha}. \tau) \\ \lfloor (e_1, \dots, e_n) \rfloor & \triangleq & (\lfloor e_1 \rfloor, \dots, \lfloor e_n \rfloor) \\ \lfloor e.j \rfloor & \triangleq & \square \text{ with } \lfloor e \rfloor \\ \lfloor e.j^n \rfloor & \triangleq & \lfloor e \rfloor \cdot j^n \\ \lfloor (e : \exists \bar{\alpha}. \sigma) \rfloor & \triangleq & (\lfloor e \rfloor : \exists \bar{\alpha}. \sigma) \\ \lfloor \, \rfloor & \triangleq & \square \text{ with } \lfloor e \rfloor \\ \lfloor \langle e \rangle \rfloor & \triangleq & \square \text{ with } \lfloor e \rfloor \\ \lfloor (e : \exists \bar{\alpha}. \sigma) \rfloor & \triangleq & \langle \lfloor e \rfloor : \exists \bar{\alpha}. \sigma \rangle \\ \lfloor \{\ell_1 = e_1; \dots; \ell_n = e_n\} \rfloor & \triangleq & \begin{cases} \{\ell_1 = \lfloor e_1 \rfloor; \dots; t_n = \lfloor e_n \rfloor\} & \text{if } \bar{\ell} \triangleright T \\ \square \text{ with } \lfloor e_1 \rfloor, \dots, \lfloor e_n \rfloor & \text{otherwise} \end{cases} \\ \lfloor T.\{\ell_1 = e_1; \dots; \ell_n = e_n\} \rfloor & \triangleq & T.\{\ell_1 = \lfloor e_1 \rfloor; \dots; \ell_n = \lfloor e_n \rfloor\} \\ \lfloor e.T.\ell \rfloor & \triangleq & \begin{cases} \lfloor e \rfloor.\ell & \text{if } \ell \triangleright T \\ \square \text{ with } \lfloor e \rfloor & \text{otherwise} \end{cases} \\ \lfloor \, \rfloor & \triangleq & \lfloor e \rfloor \cdot T.\ell \\ \lfloor \square \text{ with } \bar{e} \rfloor & \triangleq & \square \text{ with } (\lfloor e_i \rfloor)_{i=1}^n \\ \end{array} $$

<figure><img src="image_15.png" /></figure>

Under the typing context $\Gamma$, the simple term $e$ has the type $\tau$.
$$
\begin{array}{l}
\text{VAR-SD} \\
x : \forall \bar{\alpha}. \tau \in \Gamma \\
\Gamma \vdash_{\text{simple}}^{\text{sd}} x : \tau[\bar{\alpha} := \bar{\tau}]
\end{array}
$$

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\text{LET-SD} & \Gamma \vdash_{\text{simple}}^{\text{sd}} e_1 : \tau_1 & \bar{\alpha} \# \text{fv}(\Gamma) & \Gamma, x : \forall \bar{\alpha}. \tau_1 \vdash_{\text{simple}}^{\text{sd}} e_2 : \tau_2 \\
& \multicolumn{3}{c}{\Gamma \vdash_{\text{simple}}^{\text{sd}} \text{let } x = e_1 \text{ in } e_2 : \tau_2}
\end{array}
$$

$$
\begin{array}{c}
\text{POLY-X} \\
\Gamma \vdash_{\text{simple}}^{\text{sd}} e : \tau[\bar{\alpha} := \bar{\tau}] \qquad \bar{\beta} \# \Gamma \\
\hline
\Gamma \vdash_{\text{simple}}^{\text{sd}} [e : \exists \bar{\alpha}. \forall \bar{\beta}. \tau] : [\sigma[\bar{\alpha} := \bar{\tau}]]
\end{array}
$$

$$
\begin{array}{c}
\text{USE-X} \\
\Gamma \vdash e : [\forall \bar{\beta}. \tau][\bar{\alpha} := \bar{\tau}] \\
\hline
\Gamma \vdash \langle e : \exists \bar{\alpha}. \forall \bar{\beta}. \tau \rangle : \tau[\bar{\alpha} := \bar{\tau}, \bar{\beta} := \bar{\tau}']
\end{array}
$$

### $\Vdash e : \tau$

The term *e* canonically has the type *τ*.

$$
\begin{array}{c}
\text{CAN-BASE} \\
\emptyset \vdash_{\text{simple}}^{\text{sd}} e : \tau \\
\hline
\Vdash e : \tau
\end{array}
$$

$$
\begin{array}{c@{\qquad}c}
\text{CAN-PROJ-I} & \\
\mathscr{C}[e \triangleright v\bar{\gamma}. \Pi_{i=1}^n \bar{\gamma}] & \Vdash \mathscr{C}[e.j^n] : \tau \\
\hline
\Vdash \mathscr{C}[e.j] : \tau
\end{array}
$$

$$
\begin{array}{c}
\text{CAN-POLY-I} \\
\mathscr{C}[\Box \lhd v\bar{\gamma}. [\sigma] | e] \qquad \Vdash \mathscr{C}[[e : \exists \bar{\gamma}. \sigma]] : \tau \\
\hline
\Vdash \mathscr{C}[[e]] : \tau
\end{array}
$$

$$
\begin{array}{c@{\qquad}c}
\text{CAN-USE-I} & \\
\mathscr{C}[e \triangleright v\bar{\gamma}. [\sigma]] & \Vdash \mathscr{C}[\langle e : \exists \bar{\gamma}. \sigma \rangle] : \tau \\
\hline
\Vdash \mathscr{C}[\langle e \rangle] : \tau
\end{array}
$$

$$
\begin{array}{c}
\text{CAN-RCD-I} \\
\mathscr{C}[\Box \lhd v\bar{\gamma}. \text{rcd } T \bar{\gamma} | \bar{e}] \qquad \Vdash \mathscr{C}[T.\{\ell_1 = e_1 ; \dots ; \ell_n = e_n\}] : \tau \\
\hline
\Vdash \mathscr{C}[\{\ell_1 = e_1 ; \dots ; \ell_n = e_n\}] : \tau
\end{array}
$$

$$
\begin{array}{c@{\qquad}c}
\text{CAN-RCD-PROJ-I} & \\
\mathscr{C}[\Box \lhd v\bar{\gamma}. \text{rcd } T \bar{\gamma} | e] & \Vdash \mathscr{C}[e.T.\ell] : \tau \\
\hline
\Vdash \mathscr{C}[e.\ell] : \tau
\end{array}
$$

$U \rightarrow U'$

The unifier rewrites *U* to *U'*.

$$
\begin{array}{c}
\text{U-EXISTS} \\
(\exists \alpha. U_1) \wedge U_2 \qquad \alpha \# U_2 \\
\hline
\exists \alpha. U_1 \wedge U_2
\end{array}
$$

$$
\begin{array}{c}
\text{U-CYCLE} \\
U \qquad \text{cyclic}(U) \\
\hline
\text{false}
\end{array}
$$

$$
\begin{array}{c}
\text{U-TRUE} \\
U \wedge \text{true} \\
\hline
U
\end{array}
$$

$$
\begin{array}{c@{\qquad}c}
\text{U-FALSE} & \\
\mathcal{U}[\text{false}] \qquad \mathcal{U} \neq \Box & \\
\hline
\text{false}
\end{array}
$$

$$
\begin{array}{c}
\text{U-MERGE} \\
\alpha = \epsilon_1 \wedge \alpha = \epsilon_2 \\
\hline
\alpha = \epsilon_1 = \epsilon_2
\end{array}
$$

$$
\begin{array}{c}
\text{U-STUTTER} \\
\alpha = \alpha = \epsilon \\
\hline
\alpha = \epsilon
\end{array}
$$

$$
\begin{array}{c@{\qquad}c}
\text{U-NAME} & \\
\zeta (\bar{\tau}, \tau_i, \bar{\tau}') = \epsilon \qquad \alpha \# \bar{\tau}, \bar{\tau}', \epsilon \qquad \tau_i \notin \mathcal{V} & \\
\hline
\exists \alpha. \alpha = \tau_i \wedge \zeta (\bar{\tau}, \alpha, \bar{\tau}') = \epsilon
\end{array}
$$

$$
\begin{array}{c@{\qquad}c}
\text{U-DECOMP} & \\
\zeta \bar{\alpha} = \zeta \bar{\beta} = \epsilon & \\
\hline
\zeta \bar{\alpha} = \epsilon \wedge \bar{\alpha} = \bar{\beta}
\end{array}
$$

$$
\begin{array}{c}
\text{U-CLASH} \\
\xrightarrow{\zeta \bar{\alpha} = \zeta' \bar{\beta} = \epsilon} \quad \xrightarrow{\zeta \neq \zeta'} \\
\hline
\text{false}
\end{array}
$$

$$
\begin{array}{c}
\text{U-TRIVIAL} \\
\epsilon \quad |\epsilon| \le 1 \\
\hline
\text{true}
\end{array}
$$

$C \rightarrow C'$

The constraint solver rewrites *C* to *C'*.
$$ \text{S-UNIF} 
\begin{array}{rcl}
U_1 & \longrightarrow & U_2 \\
\hline
U_2 & &
\end{array}
$$

$$ \text{S-TRUE} 
\begin{array}{rcl}
C & \wedge & \text{true} \\
\hline
C & &
\end{array}
$$

$$ \text{S-FALSE} 
\begin{array}{rcl}
\mathscr{C}[\text{false}] & & \mathscr{C} \neq \square \\
\hline
\text{false} & &
\end{array}
$$

$$ \text{S-LET} 
\begin{array}{rcl}
\text{let } x = \lambda\alpha. C_1 \text{ in } C_2 & & \\
\hline
\text{let } x \alpha [\emptyset] = C_1 \text{ in } C_2 & &
\end{array}
$$

$$ \text{S-EXISTS-CONJ} 
\begin{array}{rcl}
(\exists\alpha. C_1) \wedge C_2 & \alpha \# C_2 & \\
\hline
\exists\alpha. C_1 \wedge C_2 & &
\end{array}
$$

$$ \text{S-LET-EXISTSLEFT} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = \exists\beta. C_1 \text{ in } C_2 & \beta \# \alpha, \bar{\alpha}, C_2 & \\
\hline
\text{let } x \alpha [\bar{\alpha}, \beta] = C_1 \text{ in } C_2 & &
\end{array}
$$

$$ \text{S-LET-EXISTSRIGHT} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } \exists\beta. C_2 & \beta \# \alpha, \bar{\alpha}, C_1 & \\
\hline
\exists\beta. \text{let } x = \lambda\bar{\alpha}. C_1 \text{ in } C_2 & &
\end{array}
$$

$$ \text{S-LET-CONJLEFT} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = C_1 \wedge C_2 \text{ in } C_3 & C_1 \# \alpha, \bar{\alpha} & \\
\hline
C_1 \wedge \text{let } x \alpha [\bar{\alpha}] = C_2 \text{ in } C_3 & &
\end{array}
$$

$$ \text{S-LET-CONJRIGHT} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } (C_2 \wedge C_3) & x \# C_3 & \\
\hline
C_3 \wedge \text{let } x \alpha = C_1 \text{ in } C_2 & &
\end{array}
$$

$$ \text{S-MATCH-CTX} 
\begin{array}{rcl}
\mathscr{C}[\text{match } \tau \text{ with } \bar{\chi}] & \vdash & \mathscr{C}[\tau!\zeta] \\
\hline
\mathscr{C}[\text{match } \tau := \zeta \text{ with } \bar{\chi}] & &
\end{array}
$$

$$ \text{S-INST-NAME} 
\begin{array}{rcl}
i(\alpha) \rightsquigarrow \tau & \tau \notin \mathcal{V} & \\
\hline
\exists\gamma. \gamma = \tau \wedge i(\alpha) \rightsquigarrow \gamma & &
\end{array}
$$

$$ \text{S-LET-APPR} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[x \tau] & \gamma \# \tau & x \# \text{bv}(\mathscr{C}) \\
\hline
\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[\exists\gamma, i^x. i(\alpha) \rightsquigarrow \gamma \wedge \gamma = \tau] & &
\end{array}
$$

$$ \text{S-INST-COPY} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[i^x(\alpha') \rightsquigarrow \gamma] & C = C' \wedge \alpha' = \zeta \bar{\beta} = \epsilon & \alpha' \in \alpha, \bar{\alpha} \\
\hline
\neg\text{cyclic}(C) & \bar{\beta}' \# \alpha', \gamma, \bar{\beta} & x \# \text{bv}(\mathscr{C}) \\
\hline
\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[\exists\bar{\beta}'. \gamma = \zeta \bar{\beta}' \wedge i^x(\bar{\beta}) \rightsquigarrow \bar{\beta}'] & &
\end{array}
$$

$$ \text{S-INST-UNIFY} 
\begin{array}{rcl}
i(\alpha) \rightsquigarrow \gamma_1 \wedge i(\alpha) \rightsquigarrow \gamma_2 & & \\
\hline
i(\alpha) \rightsquigarrow \gamma_1 \wedge \gamma_1 = \gamma_2 & &
\end{array}
$$

$$ \text{S-INST-POLY} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = \bar{\epsilon} \wedge C \text{ in } \mathscr{C}[i^x(\alpha') \rightsquigarrow \gamma] & \forall \alpha'. \exists \alpha. \bar{\epsilon} \equiv \text{true} & \\
\hline
\alpha' \in \alpha, \bar{\alpha} & \alpha' \# C & i(\alpha') \# \text{insts}(\mathscr{C}) \\
\hline
\text{let } x \alpha [\bar{\alpha}] = \bar{\epsilon} \wedge C \text{ in } \mathscr{C}[\text{true}] & &
\end{array}
$$

$$ \text{S-INST-MONO} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[i^x(\beta) \rightsquigarrow \gamma] & \beta \notin \alpha, \bar{\alpha} & x, \beta \# \text{bv}(\mathscr{C}) \\
\hline
\text{let } x \alpha [\bar{\alpha}] = C \text{ in } \mathscr{C}[\beta = \gamma] & &
\end{array}
$$

$$ \text{S-COMPRESS} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}, \beta] = C_1 \wedge \beta = \gamma = \epsilon \text{ in } C_2 & \beta \neq \gamma & \\
\hline
\text{let } x \alpha [\bar{\alpha}] = C_1[\beta := \gamma] \wedge \gamma = \epsilon[\beta := \gamma] \text{ in } C_2[x(\beta) := \gamma] & &
\end{array}
$$

$$ \text{S-Gc} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}, \beta] = C_1 \wedge \beta = \epsilon \text{ in } C_2 & \beta \# C_1, \epsilon, C_2 & \\
\hline
\text{let } x \alpha [\bar{\alpha}] = C_1 \wedge \epsilon \text{ in } C_2 & &
\end{array}
$$

$$ \text{S-EXISTS-LOWER} 
\begin{array}{rcl}
\text{let } x \alpha [\bar{\alpha}, \beta] = C_1 \text{ in } C_2 & \vdash & \exists\alpha, \bar{\alpha}. C_1 \text{ determines } \bar{\beta} \\
\hline
\exists\bar{\beta}. \text{let } x \alpha [\bar{\alpha}] = C_1 \text{ in } C_2 & &
\end{array}
$$

$$ \text{S-EXISTS-EXISTS-INST} 
\begin{array}{rcl}
\exists i^x. \exists \alpha. C & & \\
\hline
\exists \alpha. \exists i^x. C & &
\end{array}
$$
<figure><img src="image_16.png" /></figure>

### C. Under $\mathcal{C}$, the type $\tau$ has the provably unique canonical shape $\zeta$.

<figure><img src="image_17.png" /></figure>

**Definition A.2.** C determines $\bar{\beta}$ if and only if every ground assignments $\phi$ and $\phi'$ that satisfy (the erasure of) C and coincide outside of $\beta$ coincide on $\bar{\beta}$ as well.

$$ C \text{ determines } \beta \triangleq \forall \phi, \phi'. \phi \vdash [C] \wedge \phi' \vdash [C] \wedge \phi =_{\setminus \bar{\beta}} \phi' \implies \phi = \phi' $$

### C. C determines $\bar{\alpha}$ provably determines $\bar{\alpha}$.

$$ \begin{array}{c} \text{S-DET-DOM} \\ \vdash \exists \bar{\beta}, \bar{\alpha} \qquad \bar{\alpha} \subseteq \text{fv}(\epsilon) \\ \vdash \exists \bar{\beta}. C \wedge \gamma = \epsilon \text{ determines } \bar{\alpha} \end{array} \qquad \begin{array}{c} \text{S-DET-ESC} \\ \vdash \text{fv}(\tau) \# \bar{\alpha}, \bar{\beta} \\ \vdash \exists \bar{\beta}. C \wedge \bar{\alpha} = \tau = \epsilon \text{ determines } \bar{\alpha} \end{array} $$

### C. The set of instantiations in C.
$$
\begin{align*}
\text{insts}(\text{true}) &\triangleq \emptyset \\
\text{insts}(\text{false}) &\triangleq \emptyset \\
\text{insts}(C_1 \land C_2) &\triangleq \text{insts}(C_1) \cup \text{insts}(C_2) \\
\text{insts}(\exists\alpha. C) &\triangleq \text{insts}(C) \\
\text{insts}(\forall\alpha. C) &\triangleq \text{insts}(C) \\
\text{insts}(\tau = \tau') &\triangleq \emptyset \\
\text{insts}(\text{let } x = \lambda\alpha. C_1 \text{ in } C_2) &\triangleq \text{insts}(C_1) \cup \text{insts}(C_2) \\
\text{insts}(x \tau) &\triangleq \emptyset \\
\text{insts}(\epsilon) &\triangleq \emptyset \\
\text{insts}(\text{let } x \alpha [\tilde{\alpha}] = C_1 \text{ in } C_2) &\triangleq \text{insts}(C_1) \cup \text{insts}(C_2) \\
\text{insts}(\exists i^x. C) &\triangleq \text{insts}(C) \\
\text{insts}(i(\alpha) \to \tau) &\triangleq \{i(\alpha)\}
\end{align*}
$$

Definition A.3 (Measure). For the relation $\phi \vdash C$, the following measure enables a useful induction principle:

$$ \|C\| \triangleq \langle \#\text{match } C, |C| \rangle $$

where $\langle \dots \rangle$ denotes a pair with lexicographic ordering, and:

(1) $\#\text{match } C$ is the number of match $\tau$ with $\bar{\chi}$ constraints in $C$.

(2) the last component $|C|$ is a structural measure of constraints i.e., a conjunction $C_1 \land C_2$ is larger than the two conjuncts $C_1, C_2$.

``$\llbracket \mathscr{E}[\Box : \tau'] : \tau \rrbracket$`` is a satisfiable context iff the context $\mathscr{E}$ has the expected type $\tau$ given the hole has the type $\tau'$.

$$
\begin{align*}
\llbracket \Box[\Box : \tau] : \tau \rrbracket &\triangleq \Box \\
\llbracket (\mathscr{E} \ e)[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \alpha, \beta. \alpha = \beta \to \tau \land \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \land \llbracket e : \beta \rrbracket \\
\llbracket (e. \mathscr{E})[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \alpha, \beta. \alpha = \beta \to \tau \land \llbracket e : \alpha \rrbracket \land \llbracket \mathscr{E}[\Box : \tau'] : \beta \rrbracket \\
\llbracket (\text{let } x = \mathscr{E} \text{ in } e)[\Box : \tau'] : \tau \rrbracket &\triangleq \text{let } x = \lambda \alpha. \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \text{ in } \llbracket e : \tau \rrbracket \\
\llbracket (\text{let } x = e \text{ in } \mathscr{E})[\Box : \tau'] : \tau \rrbracket &\triangleq \text{let } x = \lambda \alpha. \llbracket e : \alpha \rrbracket \text{ in } \llbracket \mathscr{E}[\Box : \tau'] : \tau \rrbracket \\
\llbracket (\mathscr{E} : \exists \tilde{\alpha}. \tau'')[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \tilde{\alpha}. \tau = \tau'' \land \llbracket \mathscr{E}[\Box : \tau'] : \tau \rrbracket \\
\llbracket (e_1, \dots, \mathscr{E}_j, \dots, e_n)[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \tilde{\alpha}. \tau = \Pi_{i=1}^n \alpha_i \land \bigwedge_{i \neq j} \llbracket e_i : \alpha_i \rrbracket \land \llbracket \mathscr{E}_j[\Box : \tau'] : \alpha_j \rrbracket \\
\llbracket (\mathscr{E}.j^n)[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \alpha, \tilde{\alpha}. \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \land \alpha = \Pi_{i=1}^n \alpha_i \land \tau = \alpha_j \\
\llbracket (\mathscr{E}.j)[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \alpha. \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \land \text{match } \alpha \text{ with } \Pi \gamma_j \Rightarrow \tau = \gamma \\
\llbracket (\mathscr{E} : \exists \tilde{\alpha}. \sigma)[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \tilde{\alpha}. \llbracket \mathscr{E}[\Box : \tau'] : \sigma \rrbracket \land \tau = \sigma \\
\llbracket (\mathscr{E} : \exists \tilde{\alpha}. \sigma)[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \tilde{\alpha}, \beta. \llbracket \mathscr{E}[\Box : \tau'] : \beta \rrbracket \land \beta = \sigma \land \sigma \le \tau \\
\llbracket \mathscr{E}[\Box : \tau'] : \tau \rrbracket &\triangleq \text{let } x = \lambda \alpha. \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \text{ in } \\
&\phantom{\triangleq \text{let } x = \lambda \alpha.} \text{match } \tau \text{ with } [s] \Rightarrow x \le s \\
\llbracket (\mathscr{E})[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \alpha. \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \land \text{match } \alpha \text{ with } [s] \Rightarrow s \le \tau \\
\llbracket (\mathscr{E}.t)[\Box : \tau'] : \tau \rrbracket &\triangleq \begin{cases}
\llbracket (\mathscr{E}.T.t)[\Box : \tau'] : \tau \rrbracket & \text{if } t \triangleright T \\
\exists \alpha. \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \\
\land \text{ match } \alpha \text{ with } \text{rcd } t \Rightarrow t.t \le \alpha \to \tau & \text{otherwise}
\end{cases} \\
\llbracket (\mathscr{E}.T.t)[\Box : \tau'] : \tau \rrbracket &\triangleq \exists \alpha. \llbracket \mathscr{E}[\Box : \tau'] : \alpha \rrbracket \land T.t \le \alpha \to \tau
\end{align*}
$$