AILang/docs/specs/0060-typed-mir.md

Typed MIR — the check→codegen elaboration boundary — Design Spec

Date: 2026-05-31 Status: Approved Authors: orchestrator + Claude

Goal

Introduce a typed mid-level IR (MIR) as the single artefact that crosses the check → codegen boundary, carrying every fact check proves — node types, statically-resolved callees, parameter modes / consume counts, and value representation (heap vs. static Str) — so that codegen re-derives nothing.

Today there is no such artefact. crates/ail/src/main.rs:2293 calls ailang_check::check_workspace(&ws), discards its result, and at :2348 hands ailang_codegen::lower_workspace(&ws) the raw Workspace. CheckedModule (crates/ailang-check/src/lib.rs:1283) carries only top-level (Type, hash) — zero interior annotation. Codegen therefore runs four independent re-derivations of information check already computed:

1. Type synthesis at every node — synth_with_extras (crates/ailang-codegen/src/lib.rs:3242, ~270 lines) + synth_arg_type (:3238), a second inference engine mirroring the checker's lookup ladder.
2. Callee resolution — type_home_module (:2809), "mirrors the checker's TypeDef-first ladder", replicated at three sites, plus is_static_callee (:2830).
3. Uniqueness / mode — infer_module_with_cross (:1002), the identical pass ailang-check::linearity already ran; codegen re-runs it to recover consume_count for drop placement (:2326 comment: "the typechecker has already pinned uniqueness").
4. Str representation — the !is_str gate on the Term::Recur superseded-value dec (~:2131), a conservatism codegen cannot resolve because it lacks the heap/static distinction.

Every member of the raw-buf bug family (#43 / #46 / #47 / #49 / #51 / #53 — all "check-clean, build-divergent") is a point where codegen's re-derivation disagreed with what check knew, patched one leg at a time. This milestone removes the re-derivation architecture itself.

Framing — these are regression guards, not RED→GREEN bugs

As of 2026-05-31 (HEAD) the acute crashes are already patched leg by leg:

Program	Status at HEAD	Held green by
#51 (new RawBuf (con Int) 3) used via size only	builds	ee4107c (check-side — honours the written type-arg)
#53 (new Counter 42) over a user ADT	builds	420703d (codegen-side mirror — "symmetric to check")
#49 heap-Str loop binder across recur	builds, leaks live=3	unfixed — the one open leg, #[ignore]'d (02775b5)

So the milestone is not "make three crashing programs compile." It is "remove the codegen re-derivation whose leg-by-leg patches keep these programs green today — without breaking their correctness — and close the one genuinely-open leg (#49) structurally instead of with a fourth patch." The check-side corrections (ee4107c, #46/744ad41) are healthy — they correctly populate what MIR will carry, and they stay. The codegen-side mirrors (420703d, the synth_with_extras loop-binder replay in db710b1, the recur dec legs) are the disease, and they are deleted as their information moves into MIR.

The empirical acceptance evidence is therefore: #51 and #53 keep building while synth_with_extras / the type_home mirrors that hold them green are deleted (correctness survives removal of the re-derivation), plus #49 goes live=3 → live=0 (the one RED→GREEN).

Architecture

A new leaf crate ailang-mir defines the IR types. It is a neutral bridge: ailang-check depends on it to produce MIR, ailang-codegen depends on it to consume MIR. The edge codegen → check already exists (crates/ailang-codegen/Cargo.toml), so no cycle is created; ailang-mir itself has no AILang-crate dependencies except ailang-core (for Type).

.ail.json ─ parse ─ resolve ─ desugar ─ typecheck ─ lift ─ monomorphise ─┐
                                                                          │  lower_to_mir  (NEW, in ailang-check)
                          monomorphised AST ───────────────────────────  ┴──▶  MirModule  ──▶  emit LLVM IR
                                                  (typed, mode/callee/rep-annotated)   (codegen: reads, derives nothing)

• The authoring AST (Form A, content-addressed, hashable) is unchanged. MIR is a compiler-internal derived form — never authored, never hashed, never round-tripped. This preserves the authoring contract: an author writes no type the checker already infers (the feature-acceptance redundancy bar).
• lower_to_mir runs after monomorphisation, on the post-mono workspace — the same artefact codegen lowers today. It is not a phase of check_workspace (which stops at typecheck, pre-mono): if MIR were built pre-mono it would not carry the monomorphic specialisations monomorphise_workspace appends and codegen emits, reintroducing the very check↔codegen gap this milestone closes. The build path is wrapped by one front-end entry point, elaborate_workspace, that runs check → lift → mono → lower_to_mir and yields a MirWorkspace on success or the existing Vec<Diagnostic> on a type error.
• One type engine, not two. lower_to_mir walks the post-mono AST with check's own canonical synth to fill ty on every node. This is still a type walk — synth is a pure &Term → Type function and the AST carries no node-ids, so MIR cannot be a side-table read; it is built inline by walking. What the milestone removes is not the walk but the second engine: codegen's synth_with_extras is a hand-copied mirror of synth that drifts from it (every raw-buf bug is a drift point). Replacing the mirror with a single post-mono call to the canonical synth, materialised as MIR, deletes the drift class structurally — there is no longer a second implementation to disagree.
• lower_workspace* in codegen take &MirWorkspace instead of &Workspace. The Emitter fields and methods that re-derive (locals' carried Type, synth_with_extras, type_home_module, the second infer_module_with_cross run) are deleted; their consumers read the MIR annotation directly.

This also resolves a standing model drift: design/models/0003-pipeline.md already advertises "lower to MIR (SSA-like, named SSA values)" — an artefact that never existed. This milestone makes the model true.

Concrete code shapes

User-facing programs (the boundary's witnesses — parse-gated)

These three .ail programs are the milestone's empirical anchor. All three are ail check-clean today (the disagreement is downstream of check), so they exercise exactly the boundary this milestone owns.

#51 — element type carried only by the author's annotation (a RawBuf read only for its size; nothing else observes the element type). Regression guard: must keep building as the codegen element-type re-derivation is removed.

(module new_rawbuf_size_only
  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (let b (new RawBuf (con Int) 3)
        (app print (app RawBuf.size b))))))

#53 — monomorphic (new T …) over a user ADT, the dotted callee Counter.new that codegen resolves today only via a hand-copied mirror of the checker's ladder. Regression guard: must keep building once the mirror is deleted and the callee arrives pre-resolved in MIR.

(module new_counter_user_adt
  (data Counter (ctor MkCounter (con Int)))
  (fn new (type (fn-type (params (con Int)) (ret (con Counter)))) (params n)
    (body (term-ctor Counter MkCounter n)))
  (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params)
    (body (let c (new Counter 42) (do io/print_str "ok\n")))))

#49 — heap-Str loop binder replaced across recur (the seed is a static literal, each recur rebinds to a fresh str_concat heap slab). The one RED→GREEN: leaks live=3 today (one slab per recur iteration superseded without a drop); must reach live=0.

(module loop_recur_str_binder
  (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params)
    (body
      (let s
        (loop (acc (con Str) "x") (i (con Int) 0)
          (if (app ge i 3)
              acc
              (recur (app str_concat acc "y") (app + i 1))))
        (app print s)))))

Implementation shape (secondary — before → after)

MIR node — the bridge type (new, ailang-mir). Each node carries the facts codegen used to re-derive:

// ailang-mir/src/lib.rs  (NEW)
pub struct MirModule { pub name: String, pub defs: Vec<MirDef> }
pub struct MirDef { pub name: String, pub sig: Type, pub body: MTerm }

pub enum MTerm {
    Lit  { lit: Literal, ty: Type },
    Var  { name: String, ty: Type },
    Call { callee: Callee, args: Vec<MArg>, ty: Type, tail: bool },  // (2) callee pre-resolved
    Let  { name: String, mode: Mode, init: Box<MTerm>, body: Box<MTerm>, ty: Type },  // (3) mode
    New  { type_name: String, elem: Option<Type>, args: Vec<MTerm>, ty: Type },        // (1) elem carried
    Recur{ args: Vec<MArg>, ty: Type },
    Str  { lit: String, rep: StrRep },   // (4) Heap | Static — set by lower_to_mir
    // … one variant per Term node, each with `ty`
}
pub struct MArg  { pub term: MTerm, pub mode: Mode, pub consume_count: u32 }  // (3)
pub enum Callee  { Static { module: String, fn_name: String }, Indirect(Box<MTerm>) }  // (2)
pub enum StrRep  { Heap, Static }  // (4)
pub enum Mode    { Owned, Borrow }

check boundary (ailang-check):

// before — crates/ailang-check/src/lib.rs:1283
pub struct CheckedModule { pub symbols: IndexMap<String, (Type, String)> }   // signatures only

// after — one front-end entry wraps check → lift → mono → lower_to_mir
pub fn elaborate_workspace(ws: &Workspace) -> Result<MirWorkspace, Vec<Diagnostic>>;
// runs the full front end and lowers the POST-mono workspace to MIR.
// (check_workspace stays for the diagnostics-only callers — `ail check`,
//  which stops at typecheck; elaborate_workspace is the build path.)

codegen boundary (ailang-codegen):

// before — crates/ailang-codegen/src/lib.rs:278 + the Emitter re-derivers
pub fn lower_workspace(ws: &Workspace) -> Result<String>;
fn synth_with_extras(&self, t: &Term, …) -> Result<Type>;   // ~270 lines — DELETED
fn type_home_module(&self, …) -> Option<String>;            // ×3 mirrors — DELETED
let uniqueness = infer_module_with_cross(module, …);        // 2nd pass — DELETED

// after — codegen consumes MIR, reads annotations
pub fn lower_workspace(mir: &MirWorkspace) -> Result<String>;
// e.g. a Call's target is `callee` (no is_static_callee lookup);
//      a node's type is `mterm.ty()` (no synth);
//      drop placement reads `MArg.consume_count` (no re-inference).

Components

• ailang-mir (new crate): MirModule / MirDef / MTerm / Callee / Mode / StrRep / MirWorkspace. Leaf; depends only on ailang-core.
• ailang-check::lower_to_mir (new module): walks the monomorphised AST with check's canonical synth and emits MTerm, filling ty on every node. Later iterations fill callee (mir.2), mode / consume_count (mir.3), rep (mir.4).
• ailang-check::elaborate_workspace (new entry): the single front-end function — runs check_workspace (diagnostics gate), lift_letrecs, monomorphise_workspace, then lower_to_mir on the post-mono workspace. Returns MirWorkspace or the diagnostics. This moves the mono orchestration out of the CLI and behind one boundary.
• ailang-codegen (rewired): entry points take &MirWorkspace; the four re-derivers are removed iteration by iteration as their annotation lands in MIR.
• CLI (crates/ail/src/main.rs): the build path calls elaborate_workspace (which now subsumes the explicit lift + mono steps the CLI orchestrated) and threads MirWorkspace into lower_workspace*. check / diagnostics paths stay on check_workspace; the emit-ir path builds MIR via the same front-end entry.

Data flow

Workspace (AST) → typecheck (unchanged) → lift (unchanged) → monomorphise (unchanged) → lower_to_mir (post-mono AST + canonical synth → MirWorkspace) → lower_workspace (MirWorkspace → LLVM IR text) → clang. The single type-inference engine is check's synth: lower_to_mir calls it once over the post-mono bodies to materialise MIR, and codegen reads the result rather than running its own synth_with_extras mirror. The remaining synth walk inside typecheck (pre-mono, for diagnostics) and the lower_to_mir walk (post-mono, for MIR) are not redundant — they run on different workspaces for different purposes, and both are the same canonical engine, never a divergent copy.

Error handling

lower_to_mir runs only on a typechecked module, so it encounters no type errors. A failure to lower (e.g. an unresolved callee that the checker accepted — exactly today's check↔codegen disagreement) is an internal compiler error, surfaced as a distinct MirLoweringError, not a user diagnostic: by construction, if check passed, lowering must succeed. This is the structural property the milestone buys — the class "check-clean but codegen-divergent" becomes a single guarded invariant (elaborate_workspace returns Ok ⇒ MIR is complete ⇒ codegen cannot fall through to an UnknownVar).

Testing strategy

• Regression guards (green → must stay green): the #51 and #53 programs above, plus the full existing workspace suite, run after each re-deriver removal. The property: deleting the codegen re-derivation does not change observable output.
• #49 RED→GREEN: crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs — the #[ignore] is lifted in mir.4; live=0 under AILANG_RC_STATS.
• Re-derivation-is-gone pins: each iteration adds a guard that the removed function is absent (e.g. a codegen unit test that the resolved callee comes from MIR, not a ladder walk) so the re-derivation cannot silently return.
• elaborate ⇒ codegen-total invariant: a test that a curated set of check-clean programs all lower to MIR and emit IR — the structural replacement for the bug family.

Iteration decomposition

Strategy: MIR is structurally complete over all 17 Term variants (crates/ailang-core/src/ast.rs:436) from mir.1 (codegen consumes it fully — no AST/MIR dual path). Each iteration adds one annotation class and deletes the matching codegen re-derivation.

Iter	Adds to MIR	Deletes from codegen	Acceptance
mir.1	structural MIR + ty on every node	synth_with_extras + synth_arg_type	whole suite green (regression); synth_with_extras gone
mir.2	Callee::Static pre-resolved	type_home_module ×3 + is_static_callee; lockstep pair lower_app ↔ is_static_callee struck from CLAUDE.md	#53 guard green via MIR
mir.3	Mode + consume_count	second infer_module_with_cross run (:1002)	#43/#47 guards green; drop placement reads MIR
mir.4	StrRep (loop-carried Str ⇒ Heap via str_clone at loop entry)	the !is_str recur dec gate	#49 live=0; #[ignore] lifted
mir.5	element-type / Term::New fully on MIR + ledger	last re-derivation residue	#51 guard green via MIR; ledger consistent

mir.5 carries the ledger work as part of the milestone (per CLAUDE.md: contract changes ship with the iteration that needs them):

• New contract design/contracts/NNNN-check-codegen-boundary.md: the invariant "codegen re-derives nothing; MIR is total over what check proved; elaborate_workspace ⇒ codegen cannot fall through."
• Revise design/contracts/0013-typeclasses.md:106-120: the passage that blesses codegen-side cross-module re-resolution as correct-by-design is retracted — resolution now lives in MIR.
• Correct design/models/0003-pipeline.md: the "lower to MIR" line becomes true (point at the real stage).
• INDEX design/INDEX.md: add the boundary contract row; the qualified-xref / codegen rows re-point at MIR consumption.
• Issue hygiene: close #51 / #53 (now structurally held, not patch-held); milestone #7 (raw-buf) is reset to not met and subsumed — #49/#51/#53 become MIR-iteration acceptance, not a separate patch track.

Acceptance criteria

1. ailang-codegen contains no type synthesis, no callee-ladder walk, and no uniqueness inference: synth_with_extras, synth_arg_type, type_home_module, and the infer_module_with_cross call are removed; grep-clean.
2. The build path is Workspace → elaborate_workspace → MirWorkspace → lower_workspace; codegen's public entry points take &MirWorkspace.
3. The #51 and #53 programs build and run unchanged across every iteration (correctness survives re-deriver removal).
4. The #49 program reaches live=0; its test's #[ignore] is lifted.
5. The lower_app ↔ is_static_callee lockstep pair is gone from CLAUDE.md (structurally unnecessary), and 0013's blessed re-resolution passage is retracted.
6. design/models/0003-pipeline.md's MIR line names the real stage; the new boundary contract is in INDEX.
7. The full workspace test suite is green at each iteration close.