Files

T

Brummel bd62f2b9d0 docs(design): name the fn-value resolution carve-out in 0018

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.

2026-06-01 01:39:30 +02:00

3.8 KiB

Raw Permalink Blame History

Check→codegen boundary

check produces a single elaborated, typed artefact — a MirWorkspace — that is total over every fact codegen needs. Codegen consumes that artefact and 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.

The producer is ailang-check::lower_to_mir, driven by elaborate_workspace; the consumer is ailang-codegen::lower_workspace, whose public entry points take &MirWorkspace. The build path is

Workspace → elaborate_workspace → MirWorkspace → lower_workspace → LLVM IR

lower_to_mir re-enters check's own canonical synth on the post-mono AST, so the MIR each node carries is the same judgement check proved, not a parallel re-derivation. This is the source of the totality guarantee: a fact in MIR is a fact check ratified.

What MIR carries (the totality)

MIR is structurally complete over all 17 Term variants (ailang-core/src/ast.rs), and each node carries the annotation classes codegen formerly re-derived:

ty on every node — the synthesised type. Codegen reads layout, drop shape, and mangling off it.
Callee on every App — Static { module, fn_name, sig } / Builtin { name, sig } / Indirect. The static target is resolved in lower_to_mir; codegen reads the identity, it does not walk a callee ladder.
Mode + consume — per-arg modes on MArg and the per-binder consume_count on MirDef.consume. Drop placement reads these; the modes/linearity contract is memory-model.
StrRep on every Str literal — Static (constexpr GEP into rodata) / Heap (promoted via str_clone). The producer decides the representation; codegen emits what the rep says (see str-abi).

What codegen no longer holds

The re-derivers that made codegen a second, weaker type pass are gone and stay grep-clean: synth_with_extras, synth_arg_type, type_home_module, and codegen's own infer_module_with_cross run. Cross-module name resolution in particular is resolved once, in lower_to_mir, into Callee::Static — codegen does not re-resolve it (the retraction recorded in typeclasses, § "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 drift, even when it computes the right answer — it reintroduces the weaker parallel pass this boundary exists to delete, and the next post-mono inconsistency it silently tolerates is a latent miscompile. The architect agent walks codegen for type synthesis, callee-ladder walks, and uniqueness inference during drift review; any reappearance is a regression against this contract, not a local style choice.

The pipeline view of where this stage sits is pipeline.

3.8 KiB Raw Permalink Blame History

Check→codegen boundary