plan: mir.1b — codegen consumes MIR (the atomic switch)

Second half of spec iteration mir.1, planned against the landed mir.1a infrastructure (135f4ce). This is the project's largest single mechanical change and it is atomic: codegen's entire lowering walk flips from &Term to &MTerm with no compiling intermediate (dual-path is spec-forbidden). plan-recon proved the blast radius with a compile stub (flipping only lower_term's signature → 58 cascading errors across lib.rs/drop.rs/match_lower.rs/escape.rs/lambda.rs, baseline restored green). The plan gives a Term→MTerm correspondence rule for the mechanical arm renames (the build gate is the totality checker), exact before→after for the judgement sites (the 9 synth_arg_type reads → ty(), the dual-source Emitter, escape pointer-identity, entry-point signatures, CLI diagnostics), and a satisfiable gate per task. Four recon open-questions resolved by orchestrator judgement (within the approved spec's intent; the spec's MirModule sketch is illustrative and exact shape is the planner's): - OQ1: MirModule gains `ast: Module` — codegen reads structural data (Type/Const/ctor/intrinsic markers/symbol tables) from .ast, typed fn bodies from .defs. MirWorkspace stays the single artefact (it now contains the post-mono AST); structural reads were never a re-derivation, so this does not reintroduce one. Also resolves the intrinsic-fn gap (lower_module skips intrinsic bodies; codegen iterates ast.defs and looks up MirDef bodies by name). - OQ2: emit_fn borrows mir_def.body:&MTerm once and shares it between escape::analyze_fn_body and lower_term (pointer identity is only stable within one borrowed tree); casts flip to *const MTerm. - OQ3: MTerm::New's codegen arm stays unreachable! — New is desugared away before codegen (RawBuf→payload, monomorphic user-ADT new→dotted App), exactly as Term::New is today; #51 builds unchanged. - OQ4: the CLI build/emit-ir paths drop their separate check_workspace call and let elaborate_workspace's Err drive diagnostics (one check, not two); `ail check` stays on check_workspace. - emit_ir keeps &Module, calls elaborate_workspace internally, converts Err(diags)→CodegenError; its builtin-only in-source tests check clean without a prelude. Task structure: Task 1 (additive) extends MirModule + populates ast + adds codegen's ailang-mir dep, gate cargo test --workspace. Task 2 (the atomic flip) converts the whole codegen crate including its tests, gate cargo test -p ailang-codegen (deliberately excludes crates/ail so the not-yet-threaded external callers don't fail this gate). Task 3 threads the crates/ail callers (CLI build/emit-ir/staticlib + 6 e2e callers), gate cargo test --workspace == 102 ok (the mir.1a baseline), #51/#53 build+run, synth_with_extras/synth_arg_type grep-clean. refs #49
2026-05-31 14:23:26 +02:00
parent 135f4ceed7
commit 1a1a68df8b
1 changed files with 655 additions and 0 deletions
@@ -0,0 +1,655 @@
+# 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 `Module`s 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:
+
+```rust
+use ailang_core::ast::{Literal, Module, Pattern, Type};
+```
+```rust
+#[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:
+
+```rust
+    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:
+
+```toml
+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`:
+
+```rust
+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 `MirDef`s. 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:
+  ```rust
+  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:
+  ```rust
+  let val_ail = self.synth_arg_type(value)?;
+  ```
+  with:
+  ```rust
+  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`:
+
+```rust
+// 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:
+```rust
+let arg_ty = self.synth_arg_type(&args[0])?;
+```
+both become:
+```rust
+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`:
+  ```rust
+  match self.synth_arg_type(value) {
+      Ok(t) => { /* is_ptr && !is_str on t */ }
+      Err(_) => false,
+  }
+  ```
+  becomes (no `Result`):
+  ```rust
+  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`:
+
+```rust
+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:
+
+```rust
+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):
+
+```rust
+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.