From bd62f2b9d0050cd9acd6cdadd7155a500a3db856 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 01:39:30 +0200 Subject: [PATCH] docs(design): name the fn-value resolution carve-out in 0018 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Audit follow-up (typed-MIR milestone-close drift review, clean). The boundary contract said codegen does "no callee resolution"; that is true for App callees — the only thing `Callee` totality claims over — but `resolve_top_level_fn` still resolves a dotted fn used as a *value* via `import_map` (the in-corpus-unreachable type-home residue the spec blessed at mir.2), and ctor/const resolution stay codegen-side. Tighten the prose to "no App-callee resolution" and name the value-position carve-out, so the contract is precise and a future drift review does not read the blanket claim as violated. Prose-only; no code, no test change. --- design/contracts/0018-check-codegen-boundary.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/design/contracts/0018-check-codegen-boundary.md b/design/contracts/0018-check-codegen-boundary.md index 6ee98b4..9938b99 100644 --- a/design/contracts/0018-check-codegen-boundary.md +++ b/design/contracts/0018-check-codegen-boundary.md @@ -5,7 +5,7 @@ `check` produces a single elaborated, typed artefact — a [`MirWorkspace`](../../crates/ailang-mir/src/lib.rs) — that is **total** over every fact codegen needs. Codegen consumes that artefact and -**re-derives nothing**: it performs no type synthesis, no callee +**re-derives nothing**: it performs no type synthesis, no App-callee resolution, no uniqueness inference. Every decision codegen makes reads a field MIR already carries; there is no recompute-or-guess fallback path. @@ -55,6 +55,16 @@ Cross-module name resolution in particular is resolved **once**, in (the retraction recorded in [typeclasses](0013-typeclasses.md), § "Cross-module references in synthesised bodies", invariant 2). +The totality claim is over **`App` callees**: every `App` carries a +resolved `Callee`, so codegen never walks a callee ladder to find a call +target. One value-position residue remains and is deliberately not MIR's +job — `resolve_top_level_fn` resolves a dotted fn used as a *value* (not +an `App` callee) through the module's `import_map`. That path is +unreachable for type-scoped names in the current corpus (the type-home +residue blessed in `docs/specs/0060-typed-mir.md`, mir.2 refinement); +ctor and const resolution likewise stay codegen-side. None of these is +callee resolution, so `Callee` totality is intact. + ### Failure mode this contract names A codegen arm that recomputes a fact instead of reading it off MIR is