The type checker gets a second context

I think I made the last few type-system sketches too eager to give every good idea its own mechanism. Relationship types got links. Rel got a fact graph. Facet split generic types into observable surfaces. Each move helped, but the pile started to look like exactly the kind of language design I was trying to avoid: four elegant features standing beside each other, politely refusing to admit they were the same problem.

So I started again with a narrower question. What is the smallest type checker I can imagine that still gets most of the practical value from refinement types, dependent types, cross-value relationships, and serious generic abstraction? I want soundness to have a boring proof outline, and I want type resolution to have an algorithm I can explain without gesturing toward a theorem prover in another process.

The answer I keep arriving at has two contexts. Call the language Fibre for now. The ordinary type system lives in Γ. A separate logical context, Φ, records facts about the current values. The important restriction is that Φ never participates in ordinary type equality or unification.

Γ ; Φ ⊢ e ⇒ τΓ ; Φ ⊢ e ⇐ τΓ  ordinary types   x : Int   xs : Vec A   f : A -> BΦ  facts about current value identities   i >= 0   i < len(xs)   len(out) = len(xs)   Sized(packet)

The shape stays principal#

The base layer should be aggressively conventional. I would start with the same family of ideas behind Lionel Parreaux's Simple-sub: infer compact principal structural types with subtyping, then simplify them into something a person can read. The newer 2026 work on Boolean-algebraic subtyping shows how much further that base can go with unions, intersections, negation, tagged records, and recursive types while keeping a principled structural story.

Fibre does not require the fanciest version. That is part of the point. Γ can evolve from a small Hindley-Milner-ish core toward richer algebraic subtyping without changing what a length proof means, because a length proof never became a subtype edge in the first place.

Refinement information enters through a second syntax. A refined value is an ordinary shape plus a proposition that must hold in Φ.

type Positive = { x: Int | x > 0 }type Fin(n: Nat) =  { i: Nat | i < n }rel Sized(p: Packet) :=  p.len = len(p.body)fn get[A](xs: Vec A, i: Fin(len(xs))) -> Afn send(p: Packet)  needs Sized(p)

Positive and Fin(n) look like ordinary refinement types. Sized is a relationship over two fields. get looks dependently typed because the second parameter mentions the first. The checker does not need three different internal representations for those lines. They all become facts in the fibre over the current environment.

A relationship is a refinement with more than one endpoint#

The packet example from the earlier essays survives almost unchanged. Its fields stay boring, while the useful agreement between them gets a name.

type Packet = {  len: U16  body: Bytes}rel Sized(p: Packet) :=  p.len = len(p.body)fn decode(input: &mut Cursor) -> p: Packet  gives Sized(p){  let n = input.readU16()  let body = input.readExact(n)  return Packet { len: n, body }}

A successful call to readExact(n) contributes a fact saying the returned buffer has length n. The constructor copies n into the header. Congruence is enough to connect those equalities and establish Sized(p). Nothing about the runtime packet carries a proof object unless the program explicitly asks for one.

Untrusted input still needs a boundary. Fibre has a boring operation for that too: a dynamic check promotes a proposition into Φ on the successful path.

fn sendChecked(p: Packet) -> Result Unit BadLength {  check Sized(p) else {    return Err(BadLength)  }  send(p)  return Ok(())}

This split matters to me more than making invalid states universally unrepresentable. Logging a malformed packet is useful. Rejecting it before transmission is useful. The type system should let the operation that needs the relationship ask for it instead of forcing every intermediate value into a different nominal type.

Dependent typing becomes substitution#

Full dependent type theory lets arbitrary terms appear in types, which immediately raises the question of when two type-level programs are equal. Fibre refuses that problem. Term dependency appears only inside refinements and contracts, where function application substitutes actual values into logical formulas.

fn split[A](xs: Vec A, at: Nat)  -> (left: Vec A, right: Vec A)  gives {    len(left) + len(right) = len(xs)    len(left) <= at  }let (a, b) = split(items, 8)// Φ now contains:// len(a) + len(b) = len(items)// len(a) <= 8

At the call site, xs becomes items and at becomes 8. The two postconditions are reindexed into the caller's Φ. Category theorists have been using fibrations to talk about exactly this sort of indexing and substitution for decades; Bart Jacobs' work on comprehension categories is one standard route into that semantics.

More recent work gives this refinement story directly. Satoshi Kura's categorical construction of dependent refinement type systems starts with an underlying type system and a fibration of predicates, then lifts dependent products, dependent sums, effects, and recursion under suitable conditions. That is close enough to the mathematical picture here that I would use it as the semantic blueprint rather than inventing a bespoke model.

A dependent pair is equally ordinary. The second component can refer to the first in its refinement while both runtime values remain plain data.

fn readFrame(input: &mut Cursor)  -> (n: Nat, bytes: Bytes where len(bytes) = n){  let n = input.readU16().toNat()  let bytes = input.readExact(n)  return (n, bytes)}

This deliberately gives up some things Agda, Idris, Lean, and F* can express. You cannot normalize an arbitrary recursive function inside type equality because Fibre has no such equality. The reward is that the ordinary type solver never becomes a theorem prover by accident.

Generic code can quantify over the fibre#

Refinements get much more interesting when a generic function can abstract over the predicate itself. The useful precedent is Abstract Refinement Types, which showed that refinement parameters can be encoded as uninterpreted propositions while preserving SMT-based decidability.

fn preserve[A, P: Pred A](  x: A,  f: fn(A) -> A,) -> y: A  needs P(x)  gives P(y){  let y = f(x)  prove P(y)  return y}

P is opaque inside the generic. The function may assume it, require it, pass it along, and return evidence for it, but it cannot inspect the definition. That is exactly the abstraction boundary I want. A generic relationship behaves more like a type parameter than like a macro that pastes arbitrary logic into the solver.

Type constructors fit the same picture. Facet's idea that a higher-kinded parameter can be an ordinary compile-time function still works, while laws about values produced by that constructor live in Φ.

facet Seq(F: Type -> Type) {  fn len[A](xs: F A) -> Nat  fn map[A, B](xs: F A, f: fn(A) -> B) -> ys: F B    gives len(ys) = len(xs)}fn mapTwice[F, A, B, C](  xs: F A,  ab: fn(A) -> B,  bc: fn(B) -> C,) -> ys: F C  where Seq(F)  gives Seq(F).len(ys) = Seq(F).len(xs){  let bs = Seq(F).map(xs, ab)  return Seq(F).map(bs, bc)}

F belongs to the type-level part of Γ. The length-preservation law belongs to the fibre. The generic body is checked once under both abstractions. We do not need a special mechanism called associated refinement, another one called typeclass law, and a third one called dependent postcondition.

The automatic logic should be almost disappointingly small#

Liquid Types earned their usefulness by trading logical expressiveness for automation. Their original PLDI paper combines Hindley-Milner inference with predicate abstraction to infer dependent refinements with very little annotation. Fibre keeps that bargain and makes the automatic fragment even more explicit. The Liquid Types paper is still the obvious ancestor here.

term t ::=    x  | c  | measure(t)  | t + kfact φ ::=    t = t  | t <= t + k  | tag(x) = K  | R(t1, ..., tn)  | φ and φR is an opaque relation symbol unless a library summaryor an explicit proof opens it.

Ground equality with uninterpreted measures such as len is a congruence-closure problem. Nelson and Oppen's classic work gives decision procedures for quantifier-free equality by computing that closure. Bounds and offsets use difference constraints, the same graph-shaped family that underlies zones and the more expressive octagon abstract domain. Antoine Miné's octagon paper gives the familiar quadratic-space, cubic-closure engineering point for that richer domain.

known:  body = readExact(cursor, n)  len(readExact(cursor, n)) = n  packet.len = n  packet.body = bodycongruence:  len(body) = n  packet.len = n  len(packet.body) = len(body)therefore:  packet.len = len(packet.body)  Sized(packet)

I would begin even smaller than octagons: equalities plus difference constraints shaped like x - y <= k, finite constructor tags, and opaque relation symbols. Multiplication, quantifiers, induction, arbitrary recursive unfolding, and user-defined solver theories stay out of the default loop. They can cross an explicit proof boundary instead.

This is stricter than modern SMT-backed refinement systems. It is also easier to profile, cache, and explain. The new 2026 Ranger work on practical range refinements is a useful reminder that there is still active research in getting useful imperative refinements from a deliberately narrow domain plus bidirectional and flow-sensitive inference, rather than solving every theorem the language can state.

Mutation changes identities, not the logic#

Refinements over mutable data are where clean whiteboard systems usually start lying. If two aliases can mutate the same field, a fact about that field can become false behind the checker's back. I would borrow the strong part of Rust's bargain here: refined mutation requires a unique path.

fn truncate(p: &unique Packet, n: Nat) {  // p0 : Packet  // Φ contains Sized(p0)  p.body = take(p.body, n)  // p1 : Packet  // facts mentioning the old body are gone  // Sized(p1) is no longer known  p.len = len(p.body)  // p2 : Packet  // the assignment gives p2.len = len(p2.body)  // Sized(p2) is known again}

Internally, each write gives the place a fresh SSA-like identity. Facts mentioning the old projection do not automatically transfer to the new one. Nico Lehmann and collaborators' Flux is the closest practical evidence I know for this combination: it uses Rust's ownership discipline to make refined mutable locations and strong updates tractable, and formalizes the safety dependency on the aliasing model.

Fibre would be less ambitious than Flux's full refinement language. The lesson I want is narrower: aliasing control gives a fact context a trustworthy notion of "the value after this write." Without that, every relational invariant around mutation turns into a miniature separation-logic problem.

Bidirectionality draws the line around clever inference#

A principal base type does not imply that every rich signature should be inferred. Higher-rank polymorphism, indexed types, and existentials are exactly where bidirectional typing earns its keep: synthesize ordinary information, check expressive information against a known boundary.

Jana Dunfield and Neel Krishnaswami's bidirectional typing survey lays out that design discipline, while their work on indexed types and existentials shows a sound and complete bidirectional account with refinement-style equality information and significant inference. Fibre would use the same social contract with the programmer: ordinary expressions synthesize; dependent views and higher-rank boundaries are places where a signature may be required.

That keeps the hard feature from infecting every local variable. Most code sees principal shapes and facts learned from control flow. The fancy type appears where a human chose to make it part of an API.

Soundness should reduce to an erasure theorem#

I do not want the soundness argument to depend on trusting the source syntax. The clean route is to elaborate Fibre into a proof-explicit core, then erase the proofs before execution.

source  { x: T | φ(x) }proof-explicit core  (x: T, ghost: Proof φ(x))source  fn f(x: T) -> y: U    needs P(x)    gives Q(x, y)proof-explicit core  fn f(    x: T,    ghost in: Proof P(x),  ) -> (    y: U,    ghost out: Proof Q(x, y),  )erase(ghost) = nothing at runtime

Explicit Refinement Types takes a related route: proofs are present in the formal calculus, refinements erase to a simply typed program, and the authors formalize soundness in Lean. Their system intentionally gives up SMT automation to support a much richer logic. Fibre would use the same proof-erasure shape while allowing the small automatic solver to synthesize many of those ghost proofs. The lambda-ert paper is useful here precisely because it separates the semantic question from solver convenience.

proof targetIf:  Γ ; Φ ⊢ e ⇐ T  and every fact in Φ is true of the current runtime valuesthen:  erase(e) cannot reach an operation whose needs-clause is false,  and if erase(e) returns v, v has the ordinary runtime shape T.

The actual mechanized proof would still be work. The architecture at least keeps the obligations legible: prove the base calculus sound, prove every automatic decision procedure sound, prove elaboration preserves the source judgments, then prove erasure preserves runtime behavior. A stronger solver can make the checker accept more programs without changing the theorem.

Compilation closes the fibre early#

The performance story gets better if Φ is local by construction. A function, recursive SCC, or explicit checking scope gets a fresh fact graph. When the scope closes, the compiler exports a summary and throws the working proof state away.

FunctionSummary split {  shape:    forall A.    (Vec A, Nat) -> (Vec A, Vec A)  needs:    true  gives:    len(left) + len(right) = len(input)    len(left) <= at  effects:    none  local Γ graph: discarded  local Φ graph: discarded}

This is the same direction as Make the type checker forget, now with a cleaner theoretical boundary. Callers depend on a principal type plus a small set of named contracts, not on the callee's internal equality graph, branch refinements, or solver variables.

The fixed solver fragment gives the compiler an unusually concrete cost model. Classic congruence closure has near-linear or n log n-family algorithms for the ground equality problem. Difference-bound closure has a cubic worst case in the number of variables in one pack, which is why the pack should be one local function-sized neighbourhood instead of the whole program. The type graph and fact graph can be cached and invalidated independently.

The research pieces already exist; the cut is the experiment#

I do not think the mathematical ingredients here are new. Fibrations already organize predicates over contexts. Liquid typing already makes dependent refinements automatic. Abstract refinements quantify over predicates. Flux connects refinements to ownership. Bidirectional systems handle indexed and existential boundaries. Algebraic-subtyping work keeps pushing principal structural inference further.

The part I have not found packaged this way is the strict algorithmic separation: principal structural inference never sees logical predicates; the logical fibre is a fixed product of small decidable theories; cross-value relationships are ordinary named contracts; dependent types elaborate to substitution in that fibre; abstract predicates are generic parameters; and every function closes both contexts into a small summary. Structural Refinement Types gets surprisingly close on the algebraic side, and Kura's categorical construction gets close on the semantic side, which is why I would be cautious about calling the combination novel before a serious literature pass.

Still, it is specific enough to build. The first prototype does not need induction, a universe hierarchy, a general SMT bridge, dependent pattern matching, or a kind checker. It needs two graphs, a bidirectional boundary, a tiny proof language, and enough syntax to make the distinction visible without turning every function signature into a paper.

The Jacquard cards in the photograph are separate strips connected into one program for the loom. Fibre's split feels similar in a useful, unromantic way. Γ says what shape of thing can pass through the machine. Φ carries the holes that constrain this particular run. Keeping the two strips separate is what lets the checker stay small while the program says more.