AILang/docs/plans/0115-mir.1b-codegen-consumes-mir.md

mir.1b — codegen consumes MIR (the atomic switch) — Implementation Plan

Parent spec: docs/specs/0060-typed-mir.md

For agentic workers: REQUIRED SUB-SKILL: use the implement skill to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Flip the entire codegen lowering walk from &Term to &MTerm, delete synth_with_extras + synth_arg_type (the type re-derivation mirror), switch their 9 call sites to read MTerm::ty(), move the public lower_workspace* entry points to take &MirWorkspace, and switch the CLI / test build paths to elaborate_workspace — so codegen re-derives no types. The three other re-derivers (type_home_module, is_static_callee, the 2nd infer_module_with_cross) STAY for mir.1b; they leave in mir.2/mir.3.

Architecture: This is the second half of spec iteration mir.1, planned against the landed mir.1a infrastructure (commit 135f4ce). It is the project's largest single mechanical change and it is atomic: there is no compiling intermediate between "codegen walks &Term" and "codegen walks &MTerm" (dual-path is spec-forbidden). The recon proved this — flipping only lower_term's signature yields 58 compiler errors cascading through lib.rs / drop.rs / match_lower.rs / escape.rs / lambda.rs. The compiler is therefore the totality checker for the mechanical arm-by-arm rename; this plan gives a correspondence rule for the mechanical flips, exact before→after for the judgement sites (the 9 synth sites, the dual-source Emitter, the escape pointer-identity, the entry-point signatures, the CLI diagnostics), and a build gate per task.

Tech Stack: ailang-mir (one field added), ailang-check (lower_module populates it), ailang-codegen (the bulk flip), crates/ail (CLI build paths + e2e callers).

---

Design decisions baked into this plan (orchestrator, resolving recon's open questions)

The recon (read-only) surfaced four design ambiguities. All four are resolved here by orchestrator judgement, within the approved spec's intent (the spec's MirModule sketch is illustrative; the spec mandates removing the re-derivers, and exact MIR shape is the planner's to fix). None is a user fork.

• OQ1 — Emitter dual-source → MirModule carries the AST module. The Emitter reads self.module.defs (AST) for Def::Type drop-fns, Def::Const, intrinsic-new markers, and the pass-1 symbol tables (module_user_fns / module_def_ail_types / module_ctor_index / module_consts), but each fn body must now come from MirDef.body (the typed MTerm). MirModule (landed mir.1a) carries only fn bodies. Resolution: add one field — MirModule.ast: Module — so codegen reads structural data from .ast and typed bodies from .defs. MirWorkspace stays the single artefact codegen consumes (it now contains the post-mono AST). This is spec-consistent: structural module reads were never a re-derivation; the spec only requires deleting the type/callee/mode/rep re-derivers. Carrying the AST also resolves the intrinsic-fn gap: lower_module skips intrinsic-bodied fns (no MirDef), so codegen iterates mir_module.ast.defs (all fns, incl. intrinsic ones handled via the intercept registry) and looks up the MirDef body by name for the non-intrinsic ones.
• OQ2 — escape pointer-identity over MTerm. escape::analyze_fn_body and lower_term key nodes by raw-pointer identity ((t as *const Term) as usize). After the flip they key *const MTerm, and the invariant is that both passes walk the same borrowed &MTerm tree — emit_fn borrows mir_def.body: &MTerm once and passes the same reference to analyze_fn_body and lower_term. A clone between the passes would silently break identity. The pointer-cast sites flip *const Term → *const MTerm; mechanical once the same-tree borrow is stated.
• OQ3 — MTerm::New stays unreachable! in codegen. Exactly as Term::New's lower_term arm is unreachable! today: every New node is desugared away before codegen (RawBuf → payload ops; monomorphic user-ADT new → dotted App, per mir.1a's commit). So elaborate_workspace's desugar pass (unchanged) eliminates New before lower_to_mir, and codegen never hits a live MTerm::New. #51 keeps building via its desugared payload path — untouched by mir.1b. (The element-type work that makes New "real" is mir.5.)
• OQ4 — CLI diagnostics: drop the separate check_workspace call. elaborate_workspace re-runs check_workspace internally and returns Err(Vec<Diagnostic>) on a type error. The build / emit-ir build paths currently print diagnostics from their own check_workspace call then process::exit(1). Resolution: those build paths drop their separate check call and let elaborate_workspace's Err drive the diagnostic print + exit(1) (one check, not two). The ail check subcommand stays on check_workspace (diagnostics-only, no build).
• emit_ir keeps &Module, calls elaborate_workspace internally, converts Err(Vec<Diagnostic>) → CodegenError. Its in-source test callers build hand-written single-module Modules using builtins (add, ==), which resolve from env.globals without a prelude, so check_workspace passes; the one ill-typed test (eq on an ADT, asserting unwrap_err) now gets its error from check (NoInstance) instead of lowering — same outcome (unwrap_err still holds). Any in-source emit_ir test that references a prelude module fn (not a builtin) and so fails the internal check is migrated to a load_workspace fixture — bounded, implement-surfaced, local.

Files this plan creates or modifies:

• Modify: crates/ailang-mir/src/lib.rs — add ast: Module to MirModule.
• Modify: crates/ailang-check/src/lower_to_mir.rs — populate ast.
• Modify: crates/ailang-codegen/Cargo.toml — add ailang-mir dep.
• Modify: crates/ailang-codegen/src/lib.rs — the bulk flip + deletes
  • entry-point signatures + emit_ir.
• Modify: crates/ailang-codegen/src/drop.rs — &Term→&MTerm, 4 synth sites.
• Modify: crates/ailang-codegen/src/match_lower.rs — &Term/&[Term]/&[Arm]→MIR, 3 synth sites.
• Modify: crates/ailang-codegen/src/escape.rs — analysis walkers &Term→&MTerm.
• Modify: crates/ailang-codegen/src/lambda.rs — &Term→&MTerm.
• Modify: crates/ailang-codegen/tests/{embed_record_layout_pin,embed_staticlib_lowering,eq_primitives_pin}.rs — callers build MIR.
• Modify: crates/ail/src/main.rs — build / emit-ir / staticlib paths → elaborate_workspace.
• Modify: crates/ail/tests/e2e.rs — 6 lower_workspace_with_alloc callers.

---

The Term → MTerm correspondence rule (used throughout Task 2)

Every codegen match on a Term re-matches the MTerm counterpart. The mapping is structural and 1:1 except for the four noted shifts. The build gate is the totality checker — the compiler flags every unconverted arm. Apply this rule at every match site the recon enumerated; the judgement sites (synth reads, callee unwrap, escape pointer, dual-source) get exact code in the steps below.

Term arm	MTerm arm	Shift
Lit { lit }	Lit { lit, ty } for non-Str; Literal::Str → new Str { lit, rep } arm	Str split (rep unused at mir.1b)
Var { name }	Var { name, ty }	—
App { callee, args, tail }	App { callee, args, tail, ty }	callee: Callee (unwrap Indirect), args: Vec<MArg>
Let { name, value, body }	Let { name, mode, init, body, ty }	value→init; mode ignored (mir.3)
If { cond, then, else_ }	If { cond, then, else_, ty }	children Box<MTerm>
Do { op, args, tail }	Do { op, args, tail, ty }	args: Vec<MArg>
Ctor { type_name, ctor, args }	Ctor { type_name, ctor, args, ty }	args: Vec<MArg>
Match { scrutinee, arms }	Match { scrutinee, arms, ty }	arms: Vec<MArm> (MArm.pat reuses ast::Pattern)
Lam { … }	Lam { …, ty }	ret_ty: Type (not Box), body Box<MTerm>
Seq { lhs, rhs }	Seq { lhs, rhs, ty }	—
Clone { value }	Clone { value, ty }	—
ReuseAs { source, body }	ReuseAs { source, body, ty }	inner MTerm::Ctor destructure
Loop { binders, body }	Loop { binders, body, ty }	binders: Vec<MLoopBinder> (.init is MTerm, not Box)
Recur { args }	Recur { args, ty }	args: Vec<MArg>
New { … }	New { … }	arm stays unreachable! (OQ3)
Intrinsic	Intrinsic { ty }	unit → struct variant

Arg access: wherever an arm reads &args[i] (a &Term), it now reads &args[i].term (the MTerm inside the MArg). Wherever it read self.synth_arg_type(&args[i]), it reads args[i].term.ty(). Callee access: App's callee is Callee::Indirect(Box<MTerm>) at mir.1b; unwrap it to reach the inner MTerm (see Task 2 Step 4). Imports: each flipped file adds use ailang_mir::{MTerm, MArg, MArm, MLoopBinder, Callee, …} and keeps use ailang_core::ast::{…, Pattern, Type, Literal} (patterns/literals/types are unchanged).

---

Task 1: MirModule.ast + codegen's ailang-mir dep (additive, green)

This task is additive — it extends a landed type and wires a dep; nothing consumes the new field yet, so the whole suite stays green.

Files:

• Modify: crates/ailang-mir/src/lib.rs

• Modify: crates/ailang-check/src/lower_to_mir.rs

• Modify: crates/ailang-codegen/Cargo.toml

• Step 1: Add ast: Module to MirModule

In crates/ailang-mir/src/lib.rs, extend the import and the struct:

use ailang_core::ast::{Literal, Module, Pattern, Type};

#[derive(Debug, Clone)]
pub struct MirModule {
    pub name: String,
    /// The post-mono AST module. codegen reads structural data
    /// (Def::Type / Def::Const / ctor layouts / intrinsic-fn markers /
    /// imports) from here; the typed fn bodies come from `defs`. This
    /// keeps `MirWorkspace` the single artefact codegen consumes —
    /// structural reads were never a re-derivation, so carrying the AST
    /// alongside the typed bodies does not reintroduce one.
    pub ast: Module,
    pub defs: Vec<MirDef>,
}

• Step 2: Populate ast in lower_module

In crates/ailang-check/src/lower_to_mir.rs, the lower_module return already builds MirModule { name, defs } — add the ast field with the post-mono module clone:

    Ok(MirModule { name: module.name.clone(), ast: module.clone(), defs })
}

• Step 3: Add the ailang-mir dependency to codegen

In crates/ailang-codegen/Cargo.toml, under [dependencies] (after ailang-core.workspace = true), add:

ailang-mir.workspace = true

(No cycle: codegen → check → mir → core; ailang-mir is a leaf. This edge lets codegen name MTerm / MArg / Callee / MirWorkspace directly rather than only transitively.)

• Step 4: Build gate — additive, nothing breaks

Run: cargo test --workspace Expected: PASS — whole suite green (the ast field is additive; lower_module populates it; the mir.1a lower_to_mir_ty pins still pass; codegen does not yet read ast). This confirms the foundation before the atomic flip.

---

Task 2: the atomic codegen flip (lib + all codegen tests)

The whole of codegen's lowering walk flips &Term → &MTerm in one task — there is no compiling intermediate. Apply the correspondence rule (above) at every Term::* match the recon enumerated; the steps below give exact code for the judgement sites. The task's build gate (cargo test -p ailang-codegen --no-run) is the totality checker: it does not go green until every arm, signature, and caller inside the codegen crate (lib + in-source tests + tests/) is converted.

Files:

• Modify: crates/ailang-codegen/src/lib.rs

• Modify: crates/ailang-codegen/src/drop.rs

• Modify: crates/ailang-codegen/src/match_lower.rs

• Modify: crates/ailang-codegen/src/escape.rs

• Modify: crates/ailang-codegen/src/lambda.rs

• Modify: crates/ailang-codegen/tests/{embed_record_layout_pin,embed_staticlib_lowering,eq_primitives_pin}.rs

• Step 1: Flip the entry-point signatures + lower_workspace_inner pairing

In crates/ailang-codegen/src/lib.rs, change the five entry points to take &MirWorkspace:

pub fn lower_workspace_with_alloc(mir: &MirWorkspace, alloc: AllocStrategy) -> Result<String> {
    lower_workspace_inner(mir, alloc, Target::Executable)
}
pub fn lower_workspace_staticlib_with_alloc(mir: &MirWorkspace, alloc: AllocStrategy) -> Result<String> {
    lower_workspace_inner(mir, alloc, Target::StaticLib)
}
pub fn lower_workspace(mir: &MirWorkspace) -> Result<String> {
    lower_workspace_inner(mir, AllocStrategy::Rc, Target::Executable)
}
pub fn lower_workspace_staticlib(mir: &MirWorkspace) -> Result<String> {
    lower_workspace_inner(mir, AllocStrategy::Rc, Target::StaticLib)
}
fn lower_workspace_inner(mir: &MirWorkspace, alloc: AllocStrategy, target: Target) -> Result<String> {
    // …
}

In lower_workspace_inner: the desugar block (lib.rs:295-313) is deleted — elaborate_workspace already desugared + lifted + mono'd before producing the MIR. The pass-1 symbol tables (lib.rs:333-396) now iterate mir.modules and read each mir_module.ast.defs (AST structure) instead of ws.modules's m.defs. The pass-2 per-module Emitter construction (lib.rs:400-455) hands the Emitter both &mir_module.ast (for structural reads) and &mir_module.defs (for bodies) — see Step 2. The entry-main check (lib.rs:460-472) reads mir.modules[&mir.entry].ast for the main signature.

Implementer note. Read lower_workspace_inner's current body (lib.rs:294-472) and re-point every ws/m.defs read at mir/mir_module.ast.defs. The structure of the two passes is unchanged — only the source of each module's defs moves from the raw Workspace to mir_module.ast, and a second source (mir_module.defs) is added for bodies.

• Step 2: Emitter holds AST module + MIR bodies; emit_module / emit_fn pairing

The Emitter (lib.rs:730) currently holds module: &Module. Keep that (it now points at mir_module.ast) and add a body source — a map or slice of the module's MirDefs. Minimal shape: store mir_bodies: &'a [MirDef] (from mir_module.defs) on the Emitter, and have emit_module look up each fn's body by name.

emit_module (lib.rs:1054) iterates self.module.defs (AST) as today for Def::Type / Def::Const / intrinsic markers. For each Def::Fn(f):

• If f is intrinsic-bodied (matches!(f.body, Term::Intrinsic) — reads the AST FnDef, unchanged): handle via the intercept registry as today; no MIR body.
• Else: look up the MirDef whose name == f.name in self.mir_bodies, and call emit_fn(f, &mir_def.body) — f (AST FnDef) supplies sig / params / export / the intrinsic marker; &mir_def.body (&MTerm) supplies the typed body.

emit_fn (lib.rs:1265) signature gains the body: fn emit_fn(&mut self, f: &FnDef, body: &MTerm). Inside:

• The param-bind loop (lib.rs:1344) that pushed the AST param Type into locals' 4th slot stays — param types come from f.ty via crate::fn_param_types-equivalent (the AST signature), unchanged.
• escape::analyze_fn_body(body) (was &f.body) and self.lower_term(body) (was &f.body) both take the same borrowed &MTerm body (OQ2 — one borrow, shared, no clone).
• The intrinsic early-return (matches!(f.body, Term::Intrinsic), lib.rs:1394/1126) still reads the AST f.body — it is a signature-only marker; unchanged.

Implementer note. The exact Emitter field plumbing (lifetime on mir_bodies, how emit_module threads it) is yours to wire against the landed Emitter struct; the contract is: structural reads off self.module (= mir_module.ast), body off the matched MirDef.body, one &MTerm borrow shared between escape + lowering.

• Step 3: Flip lower_term (lib.rs:1604) per the correspondence rule

fn lower_term(&mut self, t: &MTerm) -> Result<(String, String)>. Re-match every arm per the correspondence table. Children that were &Box<Term> are now &Box<MTerm> (same self.lower_term(child) call); arg lists that were &[Term] are &[MArg] (self.lower_term(&arg.term)). Two arms need explicit handling:

• Lit split. Replace the single Lit arm with two:

  MTerm::Lit { lit, .. } => { /* the existing non-Str literal lowering, unchanged */ }
  MTerm::Str { lit, .. } => { /* the existing Literal::Str lowering body, lifted out of the old Lit arm */ }
  

  (The old Term::Lit arm's Literal::Str branch becomes the Str arm's body; the rep field is ignored at mir.1b.)

• Let synth read (the binder type). At lib.rs:1725, replace:

  let val_ail = self.synth_arg_type(value)?;
  

  with:

  let val_ail = value.ty();
  

  (value is the &Box<MTerm> init; MTerm::ty() returns the carried Type directly — no ?.) The 4th locals slot (lib.rs:1727) is now sourced from this. The inherited-mode Term::Var read (lib.rs:1742) becomes MTerm::Var.

• Step 4: Flip lower_app (lib.rs:2340) — callee unwrap + the 2 arith synth reads

lower_app's args: &[Term] → &[MArg]; every self.lower_term(&args[i]) → self.lower_term(&args[i].term). The callee/name resolution (is_static_callee, type_home_module) takes a &str name and is unchanged (stays for mir.2). The App arm's static-dispatch test (lib.rs:1918-1927) that currently reads if let Term::Var { name } = callee.as_ref() now unwraps the Callee:

// callee is Callee::Indirect(Box<MTerm>) at mir.1b; the static name,
// if any, is the inner MTerm::Var. (mir.2 replaces this with
// Callee::Static and deletes is_static_callee.)
let callee_mterm: &MTerm = match callee {
    Callee::Indirect(inner) => inner.as_ref(),
    Callee::Static { .. } => unreachable!("callee is Indirect until mir.2"),
};
if let MTerm::Var { name, .. } = callee_mterm {
    // … existing static-dispatch path on `name`, unchanged …
}

The two arithmetic/neg arg-type reads — lib.rs:2359 and lib.rs:2394:

let arg_ty = self.synth_arg_type(&args[0])?;

both become:

let arg_ty = args[0].term.ty();

(then the existing builtin_binop_typed(name, &arg_ty) / Int-vs-Float match on arg_ty is unchanged).

Implementer note. lower_app may be reached both from the MTerm::App arm of lower_term (callee + args already split) and as a helper. Confirm how the App arm calls lower_app (it currently destructures Term::App { callee, args, tail } then dispatches on the callee name); thread the Callee unwrap so lower_app still gets a &str name and &[MArg] args. emit_call (lib.rs:2625), emit_indirect_call (lib.rs:2724), lower_effect_op (lib.rs:2972) all take args: &[Term] → &[MArg]; their args.iter() / .zip(...) read .term.

• Step 5: Delete synth_with_extras + synth_arg_type

Delete synth_arg_type (lib.rs:3238-3240) and synth_with_extras (lib.rs:3242-3519) entirely (~280 lines). Their internal calls to type_home_module / collect_owner_local_types vanish with them (those helpers stay — used elsewhere). The module_def_ail_types reads inside synth_with_extras (lib.rs:3292/3301/3321) vanish; the field itself stays (read at lib.rs:2687 for mir.3 mode work) and so do its other readers.

Verify the field module_def_ail_types (lib.rs:759) has no remaining reader that was only synth_with_extras — the :2687 read (in emit_call's borrow-drop) stays. (If, after the delete, the field has zero readers, leave it — mir.3 needs it; a #[allow(dead_code)] is acceptable rather than removing and re-adding it. Confirm the :2687 reader survives.)

• Step 6: Flip drop.rs (4 synth sites + signatures)

Apply the correspondence rule to drop.rs's walkers and rewrite the 4 synth reads:

• is_rc_heap_allocated (:457, value: &Term → &MTerm); arms :462/466/478 re-match MTerm; the Loop arm at :487:

  match self.synth_arg_type(value) {
      Ok(t) => { /* is_ptr && !is_str on t */ }
      Err(_) => false,
  }
  

  becomes (no Result):

  let t = value.ty();
  let is_ptr = matches!(crate::synth::llvm_type(&t).as_deref(), Ok("ptr"));
  let is_str = matches!(&t, Type::Con { name, .. } if name == "Str");
  is_ptr && !is_str
  

• synth_callee_ret_mode (:513, callee: &Term → &MTerm): :514 let cty = self.synth_arg_type(callee).ok()?; → let cty = callee.ty(); (and the match cty { Type::Fn { ret_mode, .. } => Some(ret_mode), _ => None } stays).

• drop_symbol_for_binder (:533, value: &Term → &MTerm); arms :535/546/560 re-match MTerm; :561 if let Ok(Type::Con { name, .. }) = self.synth_arg_type(value) → if let Type::Con { name, .. } = value.ty().

• emit_inlined_partial_drop (:844, value: &Term → &MTerm); arm :851 re-match; :862 self.synth_arg_type(value).ok().and_then(|ty| …) → self.partial_drop_symbol_for_type(&value.ty()) (wrap to match the surrounding if let (Some(sym), Some(mask)) shape — value.ty() is infallible, so the .ok() disappears).

• :463 term_ptr identity cast *const Term → *const MTerm.

• Step 7: Flip match_lower.rs (3 synth sites + signatures)

• lower_ctor (:42, args: &[Term] → &[MArg]): :82 .map(|a| self.synth_arg_type(a)).collect::<Result<_>>()? → .map(|a| a.term.ty()).collect::<Vec<_>>() (no Result); :98/99 lower a.term.

• lower_reuse_as_rc (:179, source: &Term → &MTerm, body_args: &[Term] → &[MArg]): :201 Term::Var → MTerm::Var; :263 same .map(|a| a.term.ty()); :288 lower a.term.

• lower_match (:440, scrutinee: &Term → &MTerm, arms: &[Arm] → &[MArm]): :445 let s_ail = self.synth_arg_type(scrutinee)?; → let s_ail = scrutinee.ty();; :459/460 Term::Var → MTerm::Var; :476/477 the Vec<(CtorRef, &Arm, …)> → &MArm; :480 arm.pat and :481/484/488 Pattern::* are unchanged (MArm.pat reuses ast::Pattern); arm.body is now MTerm.

• Step 8: Flip escape.rs + lambda.rs (pure walkers)

escape.rs: analyze_fn_body (:97), walk (:110), escapes (:227), collect_free_vars (:446) flip &Term → &MTerm; all Term::* arms re-match MTerm::* (the Str literal becomes its own arm); pattern_bound_names (:430, &Pattern) is unchanged. Import (:83): add use ailang_mir::MTerm; (keep Pattern/NewArg from ast). The #[cfg(test)] ctor(...) -> Term helper (:574): if the escape unit tests build Term directly, either flip the helper to build MTerm or keep the tests AST-only by testing a thin MTerm wrapper — implementer judgement; the gate is that escape's tests compile and pass.

lambda.rs: lower_lambda (:39, lam_body: &Term → &MTerm; :222 calls lower_term), and the thunk-body walker / collect_captures (:373, t: &Term → &MTerm); pattern_bound_names (:509, &Pattern) unchanged.

• Step 9: Flip emit_ir (lib.rs:213) — build MIR internally

emit_ir keeps &Module. Replace its body's terminal lower_workspace(&ws) (lib.rs:230) with an elaborate_workspace call, converting the diagnostics error to a CodegenError:

pub fn emit_ir(m: &Module) -> Result<String> {
    let mut modules = BTreeMap::new();
    modules.insert(m.name.clone(), m.clone());
    let ws = Workspace {
        entry: m.name.clone(),
        modules,
        root_dir: std::path::PathBuf::from("."),
        registry: ailang_core::workspace::Registry::default(),
    };
    let mir = ailang_check::elaborate_workspace(&ws)
        .map_err(|diags| CodegenError::Internal(format!(
            "elaborate failed: {}",
            diags.iter().map(|d| d.message.clone()).collect::<Vec<_>>().join("; ")
        )))?;
    lower_workspace(&mir)
}

Implementer note. Confirm CodegenError::Internal(String) is the right variant (grep the enum); confirm Diagnostic exposes .message (else use its Display). ailang_check is a direct dep of codegen. The two in-source #[cfg(test)] lower_workspace_with_alloc callers (lib.rs:3709/3728) build a ws via test helpers — flip them to ailang_check::elaborate_workspace(&ws) then pass &mir. The ill-typed emit_ir test (eq on ADT, unwrap_err) now errors from check inside elaborate — unwrap_err still holds.

• Step 10: Flip codegen's tests/ integration callers

• eq_primitives_pin.rs:30 lower_workspace(&ws) — it already runs check_workspace + monomorphise_workspace (:23-29); collapse that block to let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates"); lower_workspace(&mir).

• embed_record_layout_pin.rs:28 lower_workspace_with_alloc(&ws, Rc) and embed_staticlib_lowering.rs:23/58/78 (lower_workspace_staticlib_with_alloc ×2, lower_workspace_with_alloc) — these do not yet import ailang_check; add use ailang_check::elaborate_workspace;, build let mir = elaborate_workspace(&ws).expect("elaborates"); from the load_workspace ws, and pass &mir to the lowering call. (ailang-check is reachable from codegen's own integration tests — confirmed by eq_primitives_pin.rs:9's existing use ailang_check::….)

• Step 11: Build gate — codegen crate fully converted

Run: cargo test -p ailang-codegen 2>&1 | tail -20 Expected: PASS — codegen lib + in-source tests + tests/ integration all compile and pass. The synth_with_extras / synth_arg_type deletion is grep-clean within codegen:

Run: git grep -nE 'synth_with_extras|synth_arg_type' crates/ailang-codegen/src/ Expected: no matches (only possibly a doc-comment mention to reword — if any remain in prose, reword them; the recon found module/fn doc-comments naming synth_arg_type at match_lower.rs:18, subst.rs:75, synth.rs:60/204, drop.rs:856 — reword these to describe the MTerm::ty() read).

---

Task 3: external callers (CLI build paths + e2e)

The entry-point signature change to &MirWorkspace breaks the callers in crates/ail. Thread them all here; the gate is the full workspace.

Files:

• Modify: crates/ail/src/main.rs

• Modify: crates/ail/tests/e2e.rs

• Step 1: CLI build path → elaborate_workspace (+ OQ4 diagnostics)

In crates/ail/src/main.rs, the build_to fn (:2286+): replace the block that runs check_workspace (:2293) + per-module desugar/lift (:2320-2330) + monomorphise_workspace (:2346) + lower_workspace_with_alloc(&ws, alloc) (:2348) with:

let mir = match ailang_check::elaborate_workspace(&ws) {
    Ok(mir) => mir,
    Err(diags) => {
        for d in &diags {
            eprintln!("{}: [{}] {}", /* severity */ d.severity_str(), d.code, d.message);
        }
        std::process::exit(1);
    }
};
let ir = ailang_codegen::lower_workspace_with_alloc(&mir, alloc)?;

Implementer note. Match the existing diagnostic-print format used by the ail check human path (main.rs ~:611-620) — reuse the same eprintln! shape (severity / code / message / span) so build-time and check-time diagnostics read identically. Drop build_to's own separate check_workspace call (OQ4: elaborate_workspace runs it internally). The has_export gate and any read of ws.modules…f.export stays on the pre-elaborate AST ws (it is structural, not in MIR at the CLI level) — confirm it reads ws, not mir.

• Step 2: CLI staticlib build path → elaborate_workspace

build_staticlib (:2456+): same shape — replace its check_workspace (:2464) + lift (:2482-2488) + monomorphise_workspace (:2495) + lower_workspace_staticlib_with_alloc(&ws, alloc) (:2512) with an elaborate_workspace call + lower_workspace_staticlib_with_alloc(&mir, alloc). The has_export check (:2499-2505) stays on the AST ws.

• Step 3: CLI emit-ir path → elaborate_workspace

Cmd::EmitIr arm (:647+): it currently prints diagnostics from its own check_workspace (:651) then lifts/monos (:682-695) then calls lower_workspace / lower_workspace_staticlib (:705/707). Replace with elaborate_workspace, driving diagnostics from its Err (OQ4):

let mir = match ailang_check::elaborate_workspace(&ws) {
    Ok(mir) => mir,
    Err(diags) => { /* print diags as above */ std::process::exit(1); }
};
let ir = if emit == "staticlib" {
    ailang_codegen::lower_workspace_staticlib(&mir)?
} else {
    ailang_codegen::lower_workspace(&mir)?
};

The has_export gate (:697-704) stays on the AST ws.

• Step 4: e2e.rs — 6 lower_workspace_with_alloc callers

In crates/ail/tests/e2e.rs, each of the 6 callers (:1537/1708/1782/1871/1994/2084) is preceded by its own load + lift + mono block. For each: replace the lift/mono block with let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates"); and pass &mir to lower_workspace_with_alloc(&mir, AllocStrategy::Rc).

Implementer note. Read each caller's preceding block (e.g. :1517-1536 for the first) and collapse its explicit desugar/lift/mono into the single elaborate_workspace call. The ws source (a load_workspace or hand-built workspace) stays; only the lift→mono→lower bridge changes.

• Step 5: Full workspace gate

Run: cargo test --workspace 2>&1 | grep -E 'test result:|error\[|FAILED' | grep -v 'ok\.' | sort | uniq -c Expected: no error[ / no FAILED lines.

Run: cargo test --workspace 2>&1 | grep -c 'test result: ok' Expected: the same count as before mir.1b (102) — every existing test still green, the #49 pin still the single ignored (lifts at mir.4).

• Step 6: Acceptance — #51/#53 still build + run; synth grep-clean

Run (the two regression witnesses build and run unchanged): cargo run -q -p ail -- run examples/new_counter_user_adt.ail Expected: prints ok (exit 0). Run: cargo run -q -p ail -- run examples/new_rawbuf_size_only.ail Expected: builds and runs (prints the size; exit 0).

Run (no type re-derivation left in codegen): git grep -nE 'synth_with_extras|synth_arg_type' crates/ailang-codegen/src/ Expected: no matches.

---

Notes for the orchestrator (commit + handoff)

• Commit shape: one cohesive commit — the atomic switch is one logical change. Subject e.g. feat(codegen): mir.1b — codegen consumes MIR; delete the synth_with_extras type-derivation mirror. Body: the boundary now reads ty off MIR (one engine, not two); the three other re-derivers stay (mir.2/mir.3); MirModule carries the AST for structural reads (single artefact preserved); refs #49 (closure at mir.4).
• Spec mir.1 row is now complete across mir.1a + mir.1b: structural MIR + ty landed; synth_with_extras + synth_arg_type gone.
• Next (mir.2): Callee::Static pre-resolved; delete type_home_module ×3 + is_static_callee; strike the lower_app ↔ is_static_callee lockstep pair from CLAUDE.md.