Refinement Types and the SMT Obligations Behind Them

A refinement type attaches a logical predicate to a type, so that Int becomes {v : Int | v > 0}. The predicate constrains the values that inhabit the type, which turns type checking into theorem proving: the checker must show that every value produced at a given point satisfies the predicates required of it. The mechanism that makes this practical is the reduction of each such obligation to a formula in a decidable theory and the delegation of that formula to an SMT solver. Where the formula falls outside the theory, the checker is incomplete — it rejects some correct programs — and understanding where that boundary lies is the difference between using refinement types effectively and fighting the solver.

The type, and what the predicate can mention

A refinement type is a base type paired with a predicate over a distinguished value variable: {v : B | p}, where B is a base type such as Int or Bool, or a type variable.

The predicate p is a formula in a first-order logic with the usual arithmetic and ordering operations over the base type. It can refer to v, to program variables in scope, and to other values through the same mechanism. A function type carries refinements on both sides, as in {x : {v : Int | v ≥ 0}} → {v : Int | v ≥ x}, which reads: given a non-negative integer, produce an integer at least as large.

The critical restriction is that the logic is decidable, or close enough that a solver can be relied on. Quantification over the naturals with addition and multiplication is undecidable — Hilbert’s tenth problem, resolved negatively by the MRDP theorem, which Matiyasevich completed — so refinement systems restrict themselves to fragments a solver handles: linear arithmetic, uninterpreted functions, arrays, bit-vectors, and combinations of those. A predicate that needs non-linear reasoning is either rejected or approximated. This restriction is what separates refinement types from full dependent types, where the predicate can be an arbitrary term and checking is undecidable in general.

Subtyping becomes implication

There is no separate checking rule for refinements. A value of type {v : Int | v > 0} is usable where {v : Int | v ≥ 0} is expected, and the relation between the two is subtyping: {v : B | p} <: {v : B | q} exactly when p implies q.

The implication is over all values of B, with v universally quantified. The checker discharges it by asking the solver whether p ∧ ¬q is unsatisfiable. A sat answer means the subtype relation does not hold and the program is rejected; unsat means it does. An unknown answer means the solver could not decide, and the checker must choose between rejecting (sound, incomplete) and accepting (unsound, complete). Every implementation makes this choice somewhere, though not always as a flag the programmer can reach.

A refinement type is therefore not a distinct type in the usual sense. Two refinements that a solver can prove equivalent — a strictly positive integer and one that is at least 1, for instance — are interchangeable in both directions, so they denote the same type. Type equality is mutual implication, and a checker that needs both directions must ask the solver twice.

Verification conditions from the program

Checking a function body produces one implication per obligation. Consider a division function with type div : (n : {v : Int | v ≥ 0}) → (d : {v : Int | v > 0}) → {v : Int | v ≥ 0}, defined as div n d = n / d.

The obligation is: for all n, d, if n ≥ 0 and d > 0, then the result of n / d is ≥ 0. The checker does not know the semantics of division unless the language gives it a refinement — typically an uninterpreted function with axioms, or a built-in theory of integer division. In either case the formula is n ≥ 0 ∧ d > 0 ⟹ n / d ≥ 0, which is valid over the integers with a floor or truncating division, since a non-negative dividend and a positive divisor yield a non-negative quotient. The checker emits the negation, the solver answers unsat, and the function is accepted.

The emitted query, in the solver’s input language, uses div for integer division:

(declare-const n Int)
(declare-const d Int)
(assert (>= n 0))
(assert (> d 0))
(assert (not (>= (div n d) 0)))
(check-sat)          ; unsat, so the obligation holds

The (div n d) term is where the theory matters: div is SMT-LIB’s operator for integer division rounded toward negative infinity, and a solver that implements the Ints theory reasons about it rather than treating it as opaque, so the negation is unsatisfiable. If division were instead an uninterpreted function, the solver would return sat — the negation is satisfiable because nothing constrains the function — and the checker would reject the function for lack of a proof.

The general shape of the emitted formula is a conjunction of the path condition, the refinements of the arguments, and the assumptions from pattern matches, implying the refinement required of the result. For a function with several branches, each branch produces its own formula, and the path condition differs per branch because the pattern match contributes equalities and disequalities.

This is where the scaling problem appears. A function with k branches and m intermediate bindings produces on the order of k·m formulas, each containing the path condition up to that point. The formulas grow with the length of the straight-line path, because every binding’s refinement is conjoined. A checker that emits each obligation independently therefore pays a cost that is quadratic in the size of the function body, and the practical fix is to slice the path condition to the variables each obligation mentions. Slicing is a syntactic pass over the formula and reduces the solver’s work substantially, at the cost of sometimes losing a fact the solver would have needed.

What the solver cannot do, and how systems cope

Three limits recur.

Non-linear arithmetic. x * y > 0 with both variables free is outside the decidable fragment. Solvers handle some cases by interval reasoning or by case splits on signs, but a formula that genuinely needs multiplication of two unknowns will return unknown. Systems cope by requiring the programmer to supply a lemma or by treating the multiplication as uninterpreted and losing the ability to prove anything about it.

Quantifiers. A refinement that must hold for all elements of a collection needs a quantifier, and quantified formulas over infinite domains are where SMT solvers are least reliable. A system that supports quantified refinements — “every element of this list is positive” — typically restricts the quantifier’s body to a fragment and relies on triggers to instantiate it. Triggers are patterns the solver uses to decide when to instantiate a quantified axiom, and a missing or unsuitable trigger is a common cause of a proof that fails for no apparent reason.

Heap reasoning. A refinement over a mutable field must mention the heap, and the heap changes. Systems that support this add an explicit heap parameter to every formula and use framing conditions to say which parts of the heap an operation may modify. The formulas grow with the number of live references, and the solver’s work grows faster. This is why refinement types are most often applied to pure or immutable code, and why the mutable fragment of such a language usually has a coarser type system.

Inference: the liquid-types approach

Requiring the programmer to write every refinement makes the system unusable. Liquid types infer them by restricting the shape of predicates to a finite set of candidates drawn from the program’s own terms.

The restriction is that a refinement is a conjunction of predicates of the form v ⋈ e, where ⋈ is a comparison and e is an expression from a fixed set: program variables, literals, and applications of uninterpreted functions to those. The set of candidate predicates for a given type is therefore finite — at most one predicate per comparison operator per expression in scope — and inference becomes a search for a consistent assignment of subsets of that set to each type variable: a fixed point over the lattice of candidate sets.

The fixed point is computed by constraint propagation rather than by search. Each binding’s obligation is a Horn-style constraint, and the solver initialises every unknown refinement to the smallest set (or the largest, depending on the direction of the rule) and repeatedly weakens or strengthens the sets of the variables that occur in a violated constraint until no constraint is violated. Every step strictly moves one set along the finite lattice, so the iteration terminates, and the result is the most precise refinement expressible in the candidate language that satisfies all the obligations. That is the sense in which the types are liquid: they flow along the constraints to a fixpoint within the fragment.

The cost is that a property not expressible as a conjunction of comparisons cannot be inferred. A predicate like “the list is sorted” needs a quantified invariant and must be written by hand. The benefit is that the common cases — non-negativity, bounds, non-nullness, length equalities — are inferred without annotation, and the annotation burden is confined to the properties that need quantification.

Where refinement types meet the rest of the system

Termination. A refined type proves properties of results, not that results exist. A function whose refinement is {v : Int | false} — the empty type — is a specification of a function that cannot return normally. Checking its body proves only that no path reaches a return with a value that satisfies false, which is vacuous; whether the function diverges on some input, diverges everywhere, or raises is not something the refinement logic sees. Proving termination is a separate obligation, and systems that require it add a termination checker that works on the same kind of ranking function the refinement logic can express.

Effects. A function that writes to a mutable cell has a type that mentions the heap before and after. Refinement systems that support this encode the state as an extra parameter, which is the same idea as the effect rows in algebraic effects and effect rows, specialized to a single mutable store. The two mechanisms compose: a row can carry a refined description of the state it touches, and a handler’s clause can be verified against the refinement of the state it produces.

Gradual adoption. Because a refinement type is a base type plus a predicate, the unrefined type is the refinement with the predicate true. A program can therefore be checked with no refinements at all and refined incrementally, one signature at a time. This is the property that makes refinement types practical in an existing codebase: a function with no annotated refinement at its use site has nothing to prove beyond the base types, so the checker asks the solver only about the signatures that have been annotated. The same idea of letting an expected type drive the checking of a term, rather than requiring every term to infer one, is what bidirectional type checking formalizes; refinement checking is that structure with a solver at each comparison.

Error attribution. A failed obligation names the formula, which is a conjunction of assumptions and a conclusion, and the programmer must find which assumption is wrong. Systems mitigate this by tracking the provenance of each conjunct — the source location of the binding that produced it — and by asking the solver for an unsat core of the validated obligation, the subset of the assumptions that already suffices to imply the conclusion. If a binding the programmer expected to matter is absent from the core, it played no part in the failure. An unsat core is usually far smaller than the original formula, and the reduction is the main diagnostic tool a refinement checker offers.