Wado

WEP: Elaborator Architecture — TypeSystem, Signatures, Annotate, Reify

Context

The elaborate phase is the largest and most entangled part of the compiler. Everything under wado-compiler/src/elaborator/ extends one Elaborator<'a, H> struct, which was the single home for type interning, trait resolution, method dispatch, name resolution, use→def recording, and AST → TIR construction. Adding a fact, cache, or registry had no principled place to land; the default was "another field on Elaborator."

Four problems compounded as the language grew.

The elaborator was a God Object, in data and in operations

Every concern the phase touches was bolted onto the same struct, and every module reached into it via impl<'a, H> Elaborator<'a, H>. The conceptually independent layers — the type system, the per-module annotation facts, the AST → TIR walk — had no type-level boundary. Borrow-checker pressure pushed shared state into Rc<RefCell<…>> even where shared mutability was not conceptually required, masking the real ownership question of where a fact lives. The per-module construction site, which rebuilt the whole struct for each loaded module, was the canonical demonstration: no field could be added without editing it, and none removed without touching every module reading from self.

The operations were the second half of the same problem. Walker code (the resolve_* recursion that writes sem and emits diagnostics) and query code (method lookup, trait queries, callee-signature lookups) share one &mut self. Nothing but review discipline stopped a query from mutating walk state, or a walker arm from open-coding a query.

annotate did not annotate

The elaborator ran in two calls, annotate_modules then build_tir_from_state. The intent was that annotate produces a snapshot the LSP can query and build_tir is the batch-only extension that emits TIR. The implementation did not honour it: annotate_modules covered only declaration-level information, and all body-level work — inference, name resolution, dispatch, coercion choice, the desugar rewrites — happened inside build_tir_from_state as a side effect of TIR emission. There was no point at which the facts were complete, so what the LSP read was a by-product of a batch-only artefact rather than a phase output with a contract.

Queries re-resolved foreign declaration ASTs on demand

Roughly 40 loaded_modules reads outside reify each fetched a declaration's AST to re-resolve its signature at the use site: free-function signatures, impl headers and impl-method signatures, trait-declaration methods, effect ops and resource statics, globals, data sections, associated-type bounds. No site outside reify ever read a method body except trait default-method synthesis. Signatures were the whole coupling.

That re-resolution was the root of everything else. resolve_type is a four-way seam — it interns through tysys, records use→def edges into sem.bindings, reads the scope, and logs — so any query calling it needs all of Elaborator, &mut. A suppression flag existed so a query re-resolution would not record non-authoritative edges over the owning module's. A perspective swap replaced ten fields so resolve_type could run under a foreign module's import context.

Reachability had no home

elaborate must produce reachability information: the LSP renders unused locals, imports and items (see wep-2026-05-16-unused-diagnostics.md), and reify emits only the items reachable from world exports, so what reaches monomorphize / lower / optimize is what the program can run. Neither was possible while the elaborator exposed no "annotation complete" checkpoint.

Decision

elaborate is four components and an explicit phase order. The boundary between the components is enforced by types, not review:

TypeSystem (+ Signatures)  — pipeline-wide queries; no AST, no sem writes, no logging
ModuleSemantics            — per-module facts
Elaborator                 — the per-module walker: AST in, facts out
Reify                      — facts in, TIR out

Phase order

parse → bind → load → analyze
   ↓
annotate_decls   — types → TraitEnv + Signatures → per-module decl facts
   ↓
annotate_bodies  — ×N, the walker; sole output is a populated ModuleSemantics
   ↓
liveness         — reachability over every module's recorded edges
   ↓
reify            — ×N, AST + ModuleSemantics → TirModule
   ↓
monomorphize → lower → optimize → codegen

The LSP path stops after liveness and consumes Semantics; it builds no TIR. The batch path runs through reify into the downstream pipeline.

TypeSystem — the pipeline-wide type knowledge

Holds the TypeTable arena, the TraitEnv, the builtin / WASI / world registries, the included-files map, Signatures, the program's data declarations (DataDecls), and the read-only caches built once during annotate_decls. A walk's local declarations extend DataDecls in a second table set of the same shape. It exposes the operations the rest of the compiler asks of "the type system": interning, coercion, inference, type checking, trait queries, method lookup. It does not know about Module or ModuleSource-keyed per-module state.

The name is the membership rule: "would a new field belong in the type system itself?" gates admission and prevents drift back into God-Object behaviour.

Query shape is fn query(&self, ctx: &Scope, scope: &TypeLookup, …) -> …, and three rules define the boundary: TypeSystem never walks a body, never mutates ModuleSemantics, and never logs. It reads the declaration ASTs that Signatures and TraitEnv hold, and answers a site's AstId through Resolutions. Queries return data — including reason chains (wep-2026-06-02-diagnostic-reason-chains.md) — and the walker turns them into diagnostics.

ModuleSemantics — per-module facts

One instance per loaded module, owned by Semantics in an IndexMap<ModuleSource, ModuleSemantics>, decomposed into four sub-structs with explicit membership rules:

Each sub-struct admits a field only when "does this fit the sub-struct's responsibility?" has a clear yes/no answer. A field that cannot be placed is a design question, not a default into the catch-all.

Every fact map keys by bare AstId, which is globally unique ((AstIdSpace, local)). That is what lets a fact recorded while walking foreign AST name its node exactly, whichever module's map it lands in.

A fact has one home, the map the walk wrote it into, and every phase reads it there. Semantics, keyed by bare AstId too, holds no second copy: it routes a fact to the module whose walk recorded it. Routing is per fact kind, because a node two walks reach splits its kinds across them — a callee's parameter default is typed at each call site, while its own module records the edges around it.

A body fact belongs to a walk, not to a module

One module's walk is not one walk. A tuple for-of body is a single source sub-tree resolved once per element, so one AstId inside it carries one fact per element: a different receiver type, a different method, a different From impl. sem.types therefore holds one BodyFacts per walk — the module's own, plus the overlay each tuple for-of peeled off it — and a reader names the walk it wants rather than the module.

The maps a walk records are named once, in with_body_facts! (sem/types.rs). The BodyFacts struct, the lens split_off truncates back to, the fact count, and reify's ann_* accessors are generated from that list, so a map added to it is peeled per element and read through the overlays with no second list to keep in step. That is the load-bearing part: the copies are what fell out of step, silently and per fact kind, and each omission was a miscompile of the shape "every element gets the last element's answer".

Membership: a map whose value can differ between the elements a tuple for-of unrolls belongs to BodyFacts. assign_places does not — an identifier's place is the same whichever element binds it — and neither do the declaration-level maps (impl_facts, function_effects, fn_param_types, …), since a declaration is walked once.

Reading is total over the walks at every layer. Reify consults the active overlay stack innermost-first and then the module's own (Reify::ann); TypeAnnotations::all answers every walk's value for one node; Fact::all lifts that through Semantics' routing, so a check that must hold for a call site inside an unrolled body sees each element's dispatch (Semantics::method_dispatches_at) rather than one of them. Semantics::fact_at keeps the singular shape and answers the first walk's.

Signatures — every declaration signature is a decl-pass fact

Rule: after annotate_decls, no phase re-resolves a declaration signature from AST. Each signature is resolved exactly once, by the decl pass, in its own declaration frame, and stored as TypeId-level facts:

The canonical frame: a signature is resolved under its declaring module's import scope, with Self bound to the impl target, impl and method type params as TypeParam slots, and associated types as the impl's own bindings. Use sites substitute into that frame and never re-resolve. A signature whose meaning would depend on the use site cannot exist under this rule; if one is found, that is a design bug to surface fail-loud, not a licence to re-resolve.

AST survives inside an entry only where the value is irreducibly AST and the consumer is the walker or reify, never a query: param-default exprs (resolved per call site under the callee's scope, per wep-2026-04-11-default-arguments.md), associated-const value exprs, trait default-method bodies.

Placement: one struct in elaborator/sig.rs, next to the DeclSig / MethodSig / ImplSig shapes it stores, held on TypeSystem behind an Rc and assembled once from the per-module ModuleDecls digests between the decl and body passes. Keyed by the declaring node's AstId, with name-keyed indices layered on top.

Membership rule: one entry per source declaration, holding what that declaration says — its signature, or the declaration-level datum it is. Nothing computed from a use site, and nothing a later phase recomputes.

Signatures deliberately does not extend TraitEnv. The two are built in different phases over different alphabets: TraitEnv::build runs before any decl pass and indexes names ("which impls exist, on what receiver, for what trait"), then freezes behind Arc; signatures are TypeId-level and can only exist after the decl pass has interned types. Hanging signatures off ImplHeader would make TraitEnv a two-phase build-then-backfill structure and cost it the immutability its consumers rely on. Two maps under the same (ModuleSource, AstId) key compose just as well at the use site.

One canonical frame implies one way to leave it

A signature's canonical frame is only enforceable if there is exactly one operation that instantiates it. The TypeId-level primitive is canonical (TypeTable::substitute_type_params, keyed by slot index), but nothing paired a signature with the slots it is abstract over, so each consumer open-coded "clone the param types, substitute each, substitute the return".

So a signature is a DeclSig: the slots plus the parameter and return types resolved against them. DeclSig::instantiate fills the slots positionally and is how a use site reads one; inference, which solves for the arguments, is the one consumer that reads the canonical types directly. MethodInfo is not independently computed — it is exactly instantiate(impl_method_sig, receiver_args).

An impl block's own declaration facts are its ImplSig: its resolved target, that target's type arguments, its trait reference's arguments, its type X = … bindings, its target's fq name, and which trait declaration it implements. All resolved in the block's frame, all read back through one instantiation.

A frame is abstract over its projections too, and only a use site can fill them

Slots are not the whole of what a declaration frame leaves open. A signature written against Self::Item is abstract over what Self::Item means, and that cannot be a declaration fact: I: IntoIterator<Item = u8> is written at the caller. Filling the slots without it yields a projection the use site cannot resolve — which is exactly why the trait-bound path re-resolved its callee's AST under a doctored scope instead of instantiating.

So the substitution carries both: SlotProjections maps a slot to what the projections rooted at it stand for, and TypeTable::substitute_type_params_with is the one implementation, with the slot-only substitute_type_params as its empty case.

The use site answers for every associated type the trait declares, not only the ones its bound names. Rebuilding the recorded projection over the substituted base recovers its owning trait and bounds but not its bindings, and those bindings are use-site data — I::Iter knowing Item = u8 comes from the caller. Leaving the rest to the rebuild produces a projection that differs from the one the same name resolves to when written in source, and two spellings of one type that do not intern together are a type error at the use site.

A projection's own assoc_type_bindings are types resolved in the same frame, so they carry its slots and are substituted with everything else — the rule every other arm follows.

What a bound's right-hand side denotes is deliberately not resolved to fill a gap. Self there names the bounded type, so answering would mean rebinding Self for the duration — but a frame's assoc_type_bindings shadow it, so an unrelated impl's type Item = … answers for a type parameter's, and recursion through the right-hand side has no fixpoint. An unanswered name stays abstract.

AST-shaped facts belong to TraitEnv, TypeId-level facts to Signatures

Both are declaration facts, and the phase that asks decides which structure can answer. TraitEnv::build runs before any decl pass; Signatures is assembled after all of them. So a fact the decl pass needs about itself — which trait declares Self::X, asked while resolving that trait's own method signatures — can only live on TraitEnv, alongside TraitDeclHeader. Filing it in the digest type-checks and silently answers None.

One place per question

The digest only holds if each question it answers has a single implementation. Every convergence below was forced by a defect where two of them disagreed:

Scope — transient walk state with RAII-only mutation

One Scope struct (elaborator/scope.rs) holds the walk's transient state. That is the trait-resolution context, the module a travelled expression resolves in, and the stacks that stop a question from asking itself again: an associated-type binding, a binder's bound closure, type_implements_trait and the member edges it has taken. It also holds the flag that stops a speculative walk from recording use→def edges.

Effect parameters live in TraitContext itself. They are declared in a signature's type_params list, so they are generic-scope state, and the TypeParamScope guard restores them with the rest of the context.

Guards make every change: TypeParamScope (with with_type_param_args and with_type_params_bound), with_self_binding, unless_on_walk for the two recursion sets, the type_implements_trait frame guard, and util::replaced behind with_resolving_home and with_reference_recording_suppressed. Enforceable by inspection: no mem::replace or manual clone-restore of Scope's own fields outside a guard.

The rule is about transient walk state, not about this struct. Any value saved for a sub-walk and restored after it needs a guard. Without one, an early return or a panic leaves it swapped. The guards are:

The perspective guards and with_overlay rest on one replace-and-restore helper, util::replaced. with_caller_bindings_hidden nests FunctionContext::replacing frames, which hand back a guard rather than taking a closure.

Elaborator — the walker

pub struct Elaborator<'a, H: CompilerHost> {
    tysys: TypeSystem,          // shared handle (+ Signatures)
    sem: ModuleSemantics,       // owned; driver swaps per module
    symbols: &'a SymbolTable,
    logger: &'a Logger<'a, H>,
    current_module_source: ModuleSource,  // set at entry
    entry_module_source: ModuleSource,
    annotate_ctx: Scope,        // guard-managed transient state
    invocations: Rc<InvocationIndex>,
    interner: Rc<RefCell<ModuleSourceInterner>>,
    infer_holes: InferHoleTable,
    checked_type_param_defaults: IndexMap<DefId, bool>,
}

Reify — mechanical

reify_module(&Module, &TypeSystem, &ModuleSemantics) → TirModule. The walker mirrors the AST shape; each visit method looks up the corresponding annotation on ModuleSemantics.types and emits a TIR node. No inference, no name resolution, no dispatch decisions. Monomorphic instances created during reify intern through TypeSystem.

Completeness rule — the contract that makes reify mechanical: every fact reify needs to emit a node is recorded by annotate, keyed by AstId. Reify re-derives only what is uniquely determined by the AST alone — literal kinds, the syntactic shape of a node (Index vs Field) — never anything scope-, inference-, dispatch-, or mangling-sensitive.

Three boundary invariants keep it that way:

Liveness

liveness computes source-level reachability between annotate_bodies and reify. Its policy surface — roots, stdlib exclusion, suppression, severity — is owned by wep-2026-05-16-unused-diagnostics.md. This WEP owns the mechanism: the data it produces, the graph it walks, and the contract reify holds against it.

Liveness is a non-optional field on Semantics, computed immediately after every ModuleSemantics is populated and before reify. It carries the items reachable from production roots ∪ tests (reify's gate), the candidates reachable from neither, and the candidates reachable from tests but not production. The diagnostic emitter and reify read the same reachability result; CompilerOptions::unused_diagnostics gates only whether the dead set is emitted as warnings, never the reify gate.

Nodes are the top-level code items of every loaded module — free functions, impl methods, trait methods including default bodies, and globals — each keyed by its defining AstId. Stdlib items are nodes too, since user code reaches them, but only user-authored nodes are eligible for the dead set. liveness::compute builds a private AstId → enclosing-item map per module in one structural walk, so a use inside a closure maps to its enclosing top-level item.

Each recorded use-site becomes an edge enclosing-item(use) → target, from two sources: bindings.references, whose def-side is a node (free-function calls, global reads, variant-case construction, and the method a spelled call dispatched to), and the dispatch facts in types for the sites that spell no name at all — an overloaded operator, a subscript read or write, a From conversion, a for-of iterator, a literal coercing through From<Array<…>>, and a handler binding, whose target is the whole impl block the dispatch wrapper may route any of the effect's operations to. Each such fact carries the DefId dispatch selected, recorded at the same moment as the decision, so the edge names a declaration rather than re-deriving one from a mangled name. Reachability is a single BFS from the root set; the node set and edges are static, so no fixed point is needed.

Fail-loud, not fail-safe: a dispatch fact that cannot be resolved to a defining AstId is a graph bug, not an over-approximation site. If the graph drops a live item, the missing symbol surfaces as an ICE downstream — never as silently miscompiled output — and the fix is the missing edge kind. The dual failure, an item that is unused but not reported, is what this design optimises against.

A declared method carrying a default body is a node like any other, not a root. The call that lands on it records a dispatch fact, so the body rides that edge. A program reaching neither the method nor an impl of its trait therefore needs none of what the body calls. That is what keeps core:prelude's parse and format closures out of a program that parses and formats nothing. Two kinds of declared method have no fact to ride, and each is a root:

Three paths are undecidable at the source level, and each gets a stated rule rather than a blanket over every trait impl.

A trait method reached through a generic type parameter (fn show<T: Display>(x: T) { x.fmt() }, C::from_iter(self), or a projection like S::MapSerializer): annotate records the edge to the trait method, and the concrete impl is selected during monomorphization, which the source graph does not run. So reaching a trait method reaches the corresponding method on every impl of that trait. Broader than "every reachable impl" only because impl-block reachability is not itself a question this graph answers. It is also what carries the faces a derive expands into: the synthesised body is TIR this graph never sees, but the impls it calls are reached through the bound like any other, from a T: Serialize entry point down through Serializer::begin_seq.

A generic impl block standing beside one written for a single instantiation of the same head (impl<T> Tag for Box_<T> and impl Tag for Box_<i32>): coherence Rule 1 gives the specific block, and monomorphization settles it by mangled-name collision. The source spells only the call through the template, so the template's method gets an edge to the specific block's same-named method — an edge, not a root: a program that never reaches the template needs neither block.

A trait whose calls a synthesis pass mints after this one runs: the format traits behind ${x:spec}, whose callee is read from a specifier annotate does not interpret, and the reflection faces reflect_bridge mints per monomorphized type. No fact names either, so the methods of a block implementing one are roots. Membership is CompilerItem::dispatched_by_synthesis, so the registry states the rule once and a trait added later cannot be forgotten.

Gating reify is sound only because every semantic diagnostic that can fire on dead code (effect, stores, purity, world-export conformance) is produced from Semantics rather than the emitted TIR. Those checks ran on TirModules historically, so dropping a dead function silently suppressed its error. optimize/dce.rs stays in place for the post-monomorphization population — monomorph clones, synthesised CM bindings, effect-dispatch helpers — that never passes through Semantics; it retires only from diagnostic emission.

The prune before lower

liveness answers source-level reachability. prelower_reach asks the same question again over the monomorphized TIR, which holds a different population. It walks from the roots and drops every function no root reaches, so lower never translates it and optimize never walks it. Compiling the Gale generator at -O1, that is 11825 of 23267 functions: lower falls from 3.76s to 2.89s and optimize from 19.75s to 18.27s.

A root is a CM export, a .wasm asset's export, a compiler item, a per-type bridge, a global initializer, or an impl of Eq, Ord or ReflectVariant. Those three traits are the ones lower dispatches to from a node that names no callee: a match pattern, a wide-int literal comparison, a builtin::variant_tag marker. Every other call lower writes is spelled through a CompilerItem, which is a root already.

An impl is matched by the trait's declaration identity, not by its spelling, because an impl writes the trait with its own type arguments — StrSlice implements Eq<String>, which no spelling of Eq matches.

The root set has to be this narrow to be worth anything. Rooting every impl of every compiler-item trait leaves 693 functions pruned instead of 11825, because Inspect alone is derived for every type and reaches 8837 of them.

Enumerating the minters is not a fix for the class, since the next one added breaks it again. The net goes in Interner::resolve, where every minted call lands: a debug build asserts there that it never stubs a name the prune dropped, and the panic names the callee and what is_root owes it. A new minter then fails in CI on the first fixture that exercises it, rather than surfacing as an unresolved call at WIR build. WADO_NO_PRELOWER_PRUNE holds the prune back, so a missing root is a flag to flip rather than a compiler to rebuild.

The two checks answer different questions and both are needed. WADO_TRACE=prelower_reach reports per compile how much of the TIR the walk reached, which is how to size a root set. Comparing the output bytes of every fixture compiled both ways is the correctness check: 1996 are byte-identical, none differ, and none fail in one arm alone. Around 840 fail to compile under --world test either way, so compare the arms rather than count failures. A larger program can still differ in the serial of a $Closure_N name. lower hands those out in translation order, so a smaller population renumbers them; the code around them is the same.

Naming

elaborate survives as the umbrella term and physical directory name; wado-compiler/src/elaborator/ hosts the layers as submodules. The phase names exposed in pipeline diagrams and entry points are annotate and reify. This matches the established use of "elaboration" in PL theory (Coq, Lean, Idris) for the same kind of work.

Rejected alternative

Passing a narrow "resolution context" — type table, reference sink, logger, scope — into the query layer, keeping on-demand foreign-signature resolution. Rejected: it re-creates the God Object as a parameter bundle. The suppression gate, the perspective swaps, and the per-use-site re-resolution all stay — it treats the symptom, and the query layer still cannot be tested without a walker. The digest removes the cause.

Implementation

Module layout

wado-compiler/src/elaborator.rs    # umbrella
wado-compiler/src/elaborator/
├── tysys.rs       # TypeSystem and its operations
├── sig.rs         # Signatures, DeclSig / MethodSig / ImplSig
├── scope.rs       # Scope and its RAII guards
├── sem.rs         # ModuleSemantics (re-exports its sub-structs)
├── sem/{bindings,imports,types,decls}.rs
├── liveness.rs    # cross-module reachability
└── reify.rs       # AST + ModuleSemantics → TirModule

The four sub-structs of ModuleSemantics each get their own file because their membership rule is file-scoped. The crate uses the no-mod.rs convention.

sem/types.rs opens with with_body_facts!, the list every per-walk map is declared in. It is exported, and reify invokes it with its own accessor macro, so the two files cannot hold different lists: a map is added in one place and the accessor appears.

Reading the digest

A consumer reads it via .expect(…) — a missing entry is a loud panic, never a fallback to AST re-resolution. That needs no separate completeness test: the body walk visits every impl block in every module and .expects the entry, so the suite fails deterministically at the declaration rather than at whichever use site reaches it first.

How the trait-bound path reads the digest

A method reached through a generic bound instantiates the recorded MethodSig, in three parts:

The query writes no walk state: no scope to enter, no self_type to set, no assoc_type_bindings to seed and restore.

What the dispatch path reads instead of an impl block's AST

Every question lookup_method_info asked of the AST is the declaring block's own ImplSig entry, instantiated through the slot map the candidate's shape implies (instantiate_slots, since a blanket, &-target or variadic-tuple block binds its slots from the receiver in a way the target arguments alone do not say):

Nothing about the answer is call-site-shaped except the slot map, so the query neither swaps a perspective nor suppresses a recording.

Invariants, enforceable by inspection

Each is a grep:

Rule Target Now
Hand-kept copies of the body-fact list 0 0
Body-fact reads in reify outside ann_* 0 1
AST-map reads outside reify / decl pass 0 0
Whole-module AST scans outside the decl pass 0 0
Reify resolve_type call sites 1 1
Reify loaded_modules / symbols reads 0 9
Reify type_lookup() call sites 0 14
TypeLookup { … } literals 1 3
TirTypeParam { … } literals 1 3
is_real_type_param re-spelled inline 0 2
Name-keyed AST predicates 0 1
AST-level type-param substitution helpers 0 0
Walk state swapped and restored outside a guard 0 0
Scope, label or overlay frames popped by hand 0 0
with_module_perspective_for call sites 1 1
with_reference_recording_suppressed call sites 1 1
Walker signatures taking or returning a TIR node 0 0

The perspective and suppression rows are floors, not zeroes, and each is a walker frame rather than a query: the perspective swap is the retry a travelled expression gets when it spells a generic type only its own module imports (wep-2026-04-11-default-arguments.md), and the surviving suppression is the argument-classification probe. Every row whose count exceeds its target is on the roadmap.

Roadmap

Each item below is a measurement over the tree, and each says what finishing it means. An item that waits on another says so. Three rules are what they are measured against.

A data declaration admits an effect parameter it then ignores

struct Holder<effect E, T> and variant Maybe<effect E, T> parse and compile. The dense type-argument space holds no position for E (RealTypeParams), so the parameter names nothing a use site can fill and nothing a body can read. A declaration whose parameter means nothing is a declaration the language should not admit. Derivation sees the same shape and stops short of it: at -O0, Maybe::Just(3) on the power-assert operand path reports Maybe<i32> does not implement ReflectVariant from core:prelude, which names neither the effect parameter nor the declaration that wrote it.

An impl head admits one on the same terms, where it named a slot no argument filled until register_impl_block_params stopped counting it.

Finishing it takes a decision on the language rule: reject the parameter at its own span when a struct, variant, newtype or impl declares one, and both the silent drop and that diagnostic go away. Until then, the slot is filtered rather than refused, which is what tests/fixtures/data_decl_non_real_type_param_slot.wado and tests/fixtures/impl_assoc_type_non_real_param_slot.wado pin.

A trait's default body answers to no package boundary

Two rules meet here. A pub free function is a root, being the package's external surface. An impl method rides on the call that reaches it, whatever its visibility. A declared method with a default body follows the second, so a private helper that only a pub trait's unreached default body calls is reported dead. That is right for a program and a false positive for a library, whose consumer would reach the method. No package in the tree hits it: wado check over the lib entry of package-gale, package-jade, package-marl and package-cm-catalog reports no such warning.

Finishing it means a decision on which rule a declared method follows. The question behind it is whether liveness roots a package's external surface at all once the compile has an entry program, whose world exports are the only roots the emitted component keeps. Item::Impl leaves the same question open, rooting no method however visible.

What the compiler names after liveness is not in one list

pub seeds both closures, so a pub stdlib function is emitted whether or not this program reaches it. Only the production closure needs it: pub is the package's external surface, which decides whether an item is reported dead, and optimize/dce.rs already drops a pub item the entry does not reach. Seeding the reify gate as well is what hides every entity the compiler reaches for by name after this pass, because the blanket keeps them all emitted.

Demoting pub to seed_export shows what the blanket covers. Compiling export fn run() {} then panics on core:rt::unreachable, called by a body that synthesis mints. Rooting that reaches the allocator, whose block the compiler picks by #[allocator] at Phase 7. Past that, core:builtin's bodyless declarations are gone from the package, and every call to one mints an extern stub instead. CompilerItem records some of these and nothing records the rest.

Finishing it means that list, one entry per entity named after liveness runs, with the pass that names it stating its trigger. "The prune before lower" above answers the same question on the lower side, and says what a list alone does not settle.

Two things bound the work. The rest of the closure is held by real edges from the format and parse impls that CompilerItem::dispatched_by_synthesis roots, so the list pays only once those roots narrow. And Interner::resolve's shadowing assertion compares bare names across modules, calling core:builtin's unreachable a shadow of core:rt's. It reports the audit's own progress as a defect until it compares identities.

export fn run() {} carries 1973 functions, 1213 of them bodied, and reaches 23 from its exports and global initializers. Count them with grep '^fn ' over wado dump and it reads 196 instead, because the dump writes pub fn for most of them.

A call to an operation with nothing to reach panics at WIR

A resource operation has no body, so the #[cm("...")] import is the only thing a call to it can reach. Declaring one that names no import is accepted — 11 fixtures and 46 integration cases declare such an operation to give a resource a method shape, and never call it — and calling one reaches wir_build naming a function no module holds, where it panics rather than being reported at its span:

internal resource Widget {
    fn poke(&self, n: i32);
}
export fn run() with Widget {
    Widget::poke(&(1 as Widget), 3);
}

Finishing it means a check over the dispatch a call records, which is the only place total over both spellings: Widget::poke(&w, 3) records a StaticMethodDispatch and w.poke(3) a MethodDispatch, and each carries the method_def whose parent says the operation is a resource's. wir_build cannot answer it — it holds names, not declarations — and rejecting the declaration instead is the wrong altitude: the corpus writes those declarations on purpose.

An argument check is a lookup away from being skipped

Every call path checks its arguments, but each reaches its own lookup to learn what the callee declares. The count and the parameter list have to come from the same lookup, or a call is checked against a signature that is not its callee's. Two shapes made that concrete. One lookup returned an empty list both for "declares no parameters" and for "not answered here", so a nullary callee's arguments were dropped along with their side effects. Another site took the count from a first-match lookup and the parameter list from a unique-match one, so an overloaded from was checked against whichever impl the index held first.

Both are closed where they were found. The three static spellings (Type::method, Type::<T>::method, ns::Type::method) share one check_static_call_args, and one lookup answers what a static declares. The shape survives elsewhere: 15 sites across 4 files emit ArgumentCountMismatch, and only one of them is that shared check. The rest assemble the callee's parameter list themselves, and nothing in a signature says which of the two questions — "what does this name declare" and "which declaration does this call select" — a given lookup answers.

Finishing it: one check_args(sig, args, spans) every call path calls, fed by one lookup that returns a selected signature or says it selected none. The selection stays with the overload path, which is the only place that holds the arguments.

Reify still resolves names

The completeness rule holds for the facts that exist; what is left is the facts that do not. Reify carries symbols and loaded_modules for 9 reads and runs type_lookup() at 14 sites, in a phase whose contract is that it resolves no names. Its one surviving resolution, resolve_global_type, reads a global's declared type in that global's own module scope.

The reads that remain are also fail-safe where the contract is fail-loud: 66 unwrap_or* defaults against 43 .expects. Most are legitimately optional ("this node has no coercion"), but the ones that are not silently change emitted TIR — an unknown field name writes field 0, a malformed literal emits 0 — and unescape_checked is the model for that group: the body walk already rejected the input, so the reify-side read is an .expect.

Finishing it means one recorded fact per question reify re-asks: the callee's shape on a CallExpr, the field's index and type on a FieldAccessExpr, and the owner and case index on every case identifier and pattern. The two borrowed AST inputs and resolve_global_type then have no caller left.

The same shape is written several times

Each row is a duplicate block of eleven lines or more, found by normalising whitespace and comments away and comparing windows across the phase. They disagree in the ways copies do.

Shape Copies Where
A let pattern bound into the function context 2 stmt.rs
A struct pattern's missing-field check 2 stmt.rs
An operator call's arguments wrapped by arg_ref_wraps 2 reify.rs
An impl's associated types resolved and registered 2 trait_query.rs
A Reflect* static call's receiver checks 2 reflect.rs
An indexed base's nominal head, for [] dispatch 2 expr.rs
A trait impl sought on a newtype, then on its base 2 trait_query.rs
A canonical identifier rebuilt for a qualified case 2 expr.rs and reify.rs

call.rs re-spells is_real_type_param inline twice, each with a no-default filter beside it. Everywhere else the projection rule has one source.

Finishing it: each row is a mechanical merge, and none changes what the language accepts — the e2e corpus is the verification.

The decl pass answers by scan

A module's item list is walked 25 times and the module list iterated 16 times between the start of annotate_modules and the end of build_tir_from_state. A module's use declarations alone are walked by several of those, once per collector that needs namespace imports and again per iteration of the newtype fixpoint. So a new declaration fact defaults to a new scan rather than a place in an existing walk.

Finishing it: one walk the collectors hang off, and one TypeLookup constructor that the decl pass and TypeSystem::type_lookup both call.

The walker still carries the compilation unit

A walker method that reads nothing but TypeSystem answers on TypeSystem, which has 204 methods to the walker's 747. The walker's 186 &self methods read the module's facts or the scope, or emit a diagnostic, so none of them moves without a carrier for that state.

AnnotateState still exists, reaching effect_check.rs and semantics.rs as a carrier, and the borrowed compilation-unit inputs (symbols, logger, interner, invocations, entry module) are still five separate fields threaded identically through module_elaborator and Reify::new rather than one ElabEnv.

Finishing it: dissolve AnnotateState, with tysys, module_semantics, liveness and world_registry landing on Semantics and the rest becoming driver locals or ElabEnv fields.

The hole sweep is still a hand list

infer_hole.rs::sweep_body_facts enumerates the BodyFacts maps that can hold a TypeId by hand — 16 of the 20 — so a map added to with_body_facts! sweeps only if someone remembers. The four it omits carry none today; nothing in the type system says so.

Finishing it: a substitution implementation per fact value type and a loop generated from the same list, so an omission is a missing impl rather than a silent leak of an unsolved variable into reify.

Per-element checks read one walk

BodyFacts makes every walk's answer reachable, and reify, liveness and the effect / stores / purity checks read them all. The type-driven half of those checks does not: Semantics::expression_type and local_type answer the first walk, so a check reasoning about a value's type inside a tuple for-of body sees the first element's. A body binding a resource in one element and a plain value in another is checked against one of them.

Finishing it: either a cursor that scopes a Semantics query to one instantiation's walk — which is what reify's overlay stack already is — or moving the per-element part of those checks into the annotate walk, where the element is the frame being walked. Which of the two is a design question, not a mechanical one.

Consequences

Benefits

Trade-offs

Risks and mitigations

See Also