feat(codegen): switch the lowering walk from &Term to typed &MTerm (mir.1b)

Atomic completion of spec iteration mir.1 (docs/specs/0060-typed-mir.md):
codegen now consumes the typed MIR produced by `lower_to_mir` instead of
re-deriving types from the bare `ast::Term`. Every codegen helper that
took `&Term` (lower_term, lower_app, drop.rs, match_lower.rs) takes
`&MTerm` and reads each node's checker-proved type off `MTerm::ty()`.
The build path is `Workspace -> elaborate_workspace -> MirWorkspace ->
lower_workspace`; the public `lower_workspace*` entry points and their 18
call sites thread `&MirWorkspace`. The codegen-side type re-derivers
`synth_with_extras` + `synth_arg_type` (and the `builtin_ail_type` /
`builtin_effect_op_ret` mirror tables) are deleted — grep-clean. The
three re-derivers the spec keeps until mir.2/mir.3 (`type_home_module`,
`is_static_callee`, the second `infer_module_with_cross`) stay.

The mechanical Term->MTerm match-arm conversion was straightforward and
compiler-enforced. The substance was a set of producer-side correctness
gaps that only surface once codegen reads `MTerm::ty()` and once the
build path re-synthesises the post-mono AST through the canonical
`synth` (which, unlike the old codegen, fully re-unifies). Each was
root-caused against a failing e2e fixture:

1. `qualify_local_types` stripped fn-type modes (rebuilt `Type::Fn` with
   empty `param_modes` / `Implicit` `ret_mode`), so a monomorphised
   polymorphic intrinsic (`RawBuf.set`) lost its `Own` ret-mode and the
   owned temporary leaked at the call site. Made mode-preserving, like
   its sister `qualify_workspace_types` and `Subst::apply` (449df13).

2. `lower_to_mir::synth_pure` synthesises each node in isolation, so a
   nullary polymorphic ctor (`Nil : List<a>`) left its element type an
   unbound `$m` metavar that the canonical synth never pins. Codegen's
   mono unifier (`unify_for_subst`) already has a wildcard for exactly
   this — `$u`, the spelling the now-deleted codegen synth used — so the
   typed-MIR boundary normalises every residual `$m` to `$u` once
   (`wildcard_residual_metavars`), rather than teaching each consumer to
   tolerate a raw metavar.

3. The class-method mono arm (`synthesise_mono_fn`) substituted the
   registry-canonical *qualified* instance type into a method appended to
   the instance's own module, minting a `show_user_adt.IntBox` param
   against a bare-`IntBox` body. Localised to bare before substitution,
   symmetric to the free-fn arm (600565d).

4. Monomorphisation synthesises *downward* class-dispatch references —
   prelude's `print__<IntBox>` names the instance module `show_user_adt`
   that prelude never imports. The post-mono re-synth in `lower_module`
   seeds every workspace module name as an identity import (excluding the
   current module, to keep own types bare) so the qualified-var path
   resolves these; the canonical `synth` used by `check_workspace` stays
   strict.

5. Post-mono, a cross-module callee can name the consumer's *own* ADT
   qualified (`show_user_adt.IntBox`) where the consumer synthesises it
   bare — a spelling split that cannot exist pre-mono (the param is
   polymorphic there). synth's App arm strips the current module's own
   qualifier from both sides before unifying (`strip_own_module_qual`),
   a no-op pre-mono.

Acceptance: whole workspace suite green (698 tests); `e2e` 98/98 and
`show_print_e2e` 3/3; `synth_with_extras`/`synth_arg_type` grep-clean in
codegen; #51/#53 fixtures build and run; lower_to_mir_ty pins green. The
#49 heap-Str loop-binder leak remains ignored (lifts at mir.4).

Builds on the standalone producer fix (600565d, free-fn own-ADT
localisation) and the two standalone mode-preservation fixes
(449df13 Subst::apply); those landed separately as they are
independently correct and inert on the old codegen.

Cargo.lock

@@ -37,6 +37,7 @@ version = "0.0.1"
 dependencies = [
  "ailang-check",
  "ailang-core",
+ "ailang-mir",
  "ailang-surface",
  "indexmap",
  "thiserror",

crates/ail/src/main.rs

@@ -648,53 +648,10 @@ fn main() -> Result<()> {
             // workspace lowering. For single-module programs the
             // workspace is effectively a trivial workspace with one module.
             let ws = load_workspace_human(&path)?;
-            let diags = ailang_check::check_workspace(&ws);
-            if !diags.is_empty() {
-                for d in &diags {
-                    eprintln!(
-                        "{}: [{}] {}{}",
-                        match d.severity {
-                            ailang_check::Severity::Error => "error",
-                            ailang_check::Severity::Warning => "warning",
-                        },
-                        d.code,
-                        d.def
-                            .as_ref()
-                            .map(|n| format!("{n}: "))
-                            .unwrap_or_default(),
-                        d.message,
-                    );
-                }
-                // only Error-severity blocks codegen.
-                if diags
-                    .iter()
-                    .any(|d| matches!(d.severity, ailang_check::Severity::Error))
-                {
-                    std::process::exit(1);
-                }
-            }
-            // emit-ir must run the same pre-codegen pipeline
-            // as `build` — `lift_letrecs` per module, then
-            // `monomorphise_workspace`. Pre-iter-23.4 this was implicit:
-            // codegen's poly-call path handled specialisation internally.
-            // With that path removed, emit-ir must produce the
-            // post-mono workspace explicitly, same shape as `build`.
-            let mut lifted_modules = std::collections::BTreeMap::new();
-            for (mname, m) in &ws.modules {
-                let desugared = ailang_core::desugar::desugar_module(m);
-                let lifted = ailang_check::lift_letrecs(&desugared)
-                    .map_err(|e| anyhow::anyhow!("lift_letrecs in module `{mname}`: {e}"))?;
-                lifted_modules.insert(mname.clone(), lifted);
-            }
-            let ws = ailang_core::Workspace {
-                entry: ws.entry.clone(),
-                modules: lifted_modules,
-                root_dir: ws.root_dir.clone(),
-                registry: ws.registry.clone(),
-            };
-            let ws = ailang_check::monomorphise_workspace(&ws)
-                .map_err(|e| anyhow::anyhow!("monomorphise_workspace: {e}"))?;
-            let ir = if emit == "staticlib" {
+            // staticlib needs ≥1 export — checked on the source AST
+            // (structural; survives elaborate). Done before elaborate so
+            // the message is clear rather than a missing-main lowering.
+            if emit == "staticlib" {
                 let has_export = ws.modules.values().any(|m| m.defs.iter().any(|d|
                     matches!(d, ailang_core::Def::Fn(f) if f.export.is_some())));
                 if !has_export {
@@ -702,9 +659,22 @@ fn main() -> Result<()> {
                         "staticlib target needs at least one `(export \"<sym>\")` fn"
                     );
                 }
-                ailang_codegen::lower_workspace_staticlib(&ws)?
+            }
+            // mir.1b OQ4: emit-ir runs the same single front-end as
+            // `build` via `elaborate_workspace` (check → desugar+lift →
+            // mono → lower_to_mir), driving error diagnostics from its
+            // `Err` rather than a separate `check_workspace` call.
+            let mir = match ailang_check::elaborate_workspace(&ws) {
+                Ok(mir) => mir,
+                Err(diags) => {
+                    print_build_diagnostics(&diags);
+                    std::process::exit(1);
+                }
+            };
+            let ir = if emit == "staticlib" {
+                ailang_codegen::lower_workspace_staticlib(&mir)?
             } else {
-                ailang_codegen::lower_workspace(&ws)?
+                ailang_codegen::lower_workspace(&mir)?
             };
             match out {
                 Some(p) => {
@@ -2264,19 +2234,35 @@ fn locate_str_runtime() -> Result<PathBuf> {
     )
 }
 
+/// print build-time diagnostics to stderr in the `ail check` human
+/// format (severity / code / optional def name / message). Used by the
+/// build paths to surface the `Err(diags)` from `elaborate_workspace`
+/// before exiting with code 1.
+fn print_build_diagnostics(diags: &[ailang_check::Diagnostic]) {
+    for d in diags {
+        eprintln!(
+            "{}: [{}] {}{}",
+            match d.severity {
+                ailang_check::Severity::Error => "error",
+                ailang_check::Severity::Warning => "warning",
+            },
+            d.code,
+            d.def
+                .as_ref()
+                .map(|n| format!("{n}: "))
+                .unwrap_or_default(),
+            d.message,
+        );
+    }
+}
+
 /// shared build helper for `Cmd::Build` and `Cmd::Run`.
-/// Loads the workspace, runs the typechecker, emits IR, and links via
-/// clang. On typecheck failure, prints diagnostics to stderr and exits
-/// the process with code 1. On clang failure, returns a Result error
+/// Loads the workspace, elaborates it to MIR (check → desugar+lift →
+/// monomorphise → lower_to_mir), emits IR, and links via clang. On
+/// typecheck failure, prints diagnostics to stderr and exits the
+/// process with code 1. On clang failure, returns a Result error
 /// (the .ll path is preserved for post-mortem inspection).
 ///
-/// between `check_workspace` and `lower_workspace` we run
-/// `ailang_check::lift_letrecs` per module. The lift eliminates any
-/// `Term::LetRec` that the desugar pass left in place (specifically:
-/// LetRecs that capture `Term::Let`-bound names, whose types are
-/// only known after typecheck). The lifted workspace then goes to
-/// codegen unchanged.
-///
 /// `alloc` selects the heap allocator the emitted IR targets.
 /// Default `Rc` is the canonical production path: declares
 /// `@ailang_rc_alloc` (with `ailang_rc_inc` / `ailang_rc_dec`
@@ -2290,62 +2276,20 @@ fn build_to(
     alloc: ailang_codegen::AllocStrategy,
 ) -> Result<PathBuf> {
     let ws = load_workspace_human(path)?;
-    let diags = ailang_check::check_workspace(&ws);
-    if !diags.is_empty() {
-        for d in &diags {
-            eprintln!(
-                "{}: [{}] {}{}",
-                match d.severity {
-                    ailang_check::Severity::Error => "error",
-                    ailang_check::Severity::Warning => "warning",
-                },
-                d.code,
-                d.def
-                    .as_ref()
-                    .map(|n| format!("{n}: "))
-                    .unwrap_or_default(),
-                d.message,
-            );
-        }
-        // only Error-severity blocks the build. Warning-
-        // severity diagnostics (e.g. `over-strict-mode`) print but
-        // do not abort.
-        if diags
-            .iter()
-            .any(|d| matches!(d.severity, ailang_check::Severity::Error))
-        {
+    // mir.1b OQ4: one check, not two. `elaborate_workspace` runs the
+    // full front-end (check → desugar+lift → monomorphise →
+    // lower_to_mir) and returns `Err(diags)` on a type error; the
+    // build path no longer runs its own `check_workspace`. The error
+    // diagnostics drive the same human-format print + exit(1) the
+    // separate check used to.
+    let mir = match ailang_check::elaborate_workspace(&ws) {
+        Ok(mir) => mir,
+        Err(diags) => {
+            print_build_diagnostics(&diags);
             std::process::exit(1);
         }
-    }
-    // run `lift_letrecs` per module on the post-desugar
-    // form. Codegen's internal desugar pass is idempotent on a
-    // module that contains no `Term::LetRec`, so the lifted output
-    // can be handed directly to `lower_workspace`.
-    let mut lifted_modules = std::collections::BTreeMap::new();
-    for (mname, m) in &ws.modules {
-        let desugared = ailang_core::desugar::desugar_module(m);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .map_err(|e| anyhow::anyhow!("lift_letrecs in module `{mname}`: {e}"))?;
-        lifted_modules.insert(mname.clone(), lifted);
-    }
-    let ws = ailang_core::Workspace {
-        entry: ws.entry.clone(),
-        modules: lifted_modules,
-        root_dir: ws.root_dir.clone(),
-        // pass the registry through the lift pass. Lift
-        // only rewrites `Term::LetRec` into top-level fns; it does
-        // not touch class/instance defs, so the registry built at
-        // load-time remains valid.
-        registry: ws.registry.clone(),
     };
-    // monomorphisation pass. After `lift_letrecs` and
-    // before codegen, every (class-method, concrete-type) call-site
-    // pair becomes a synthesised top-level fn; user call sites are
-    // rewritten to target those names. Class-free workspaces flow
-    // through bit-identically; see `ailang_check::monomorphise_workspace`.
-    let ws = ailang_check::monomorphise_workspace(&ws)
-        .map_err(|e| anyhow::anyhow!("monomorphise_workspace: {e}"))?;
-    let ir = ailang_codegen::lower_workspace_with_alloc(&ws, alloc)?;
+    let ir = ailang_codegen::lower_workspace_with_alloc(&mir, alloc)?;
     let tmpdir = std::env::temp_dir().join(format!("ailang-{}", std::process::id()));
     std::fs::create_dir_all(&tmpdir)?;
     let ll_path = tmpdir.join(format!("{}.ll", ws.entry));
@@ -2459,43 +2403,12 @@ fn build_staticlib(
     opt: &str,
     alloc: ailang_codegen::AllocStrategy,
 ) -> Result<(PathBuf, PathBuf)> {
-    // ---- shared front matter: identical to build_to:2239-2294 ----
+    // ---- shared front matter: elaborate to MIR (one check) ----
     let ws = load_workspace_human(path)?;
-    let diags = ailang_check::check_workspace(&ws);
-    if !diags.is_empty() {
-        for d in &diags {
-            eprintln!(
-                "{}: [{}] {}{}",
-                match d.severity {
-                    ailang_check::Severity::Error => "error",
-                    ailang_check::Severity::Warning => "warning",
-                },
-                d.code,
-                d.def.as_ref().map(|n| format!("{n}: ")).unwrap_or_default(),
-                d.message,
-            );
-        }
-        if diags.iter().any(|d| matches!(d.severity, ailang_check::Severity::Error)) {
-            std::process::exit(1);
-        }
-    }
-    let mut lifted_modules = std::collections::BTreeMap::new();
-    for (mname, m) in &ws.modules {
-        let desugared = ailang_core::desugar::desugar_module(m);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .map_err(|e| anyhow::anyhow!("lift_letrecs in module `{mname}`: {e}"))?;
-        lifted_modules.insert(mname.clone(), lifted);
-    }
-    let ws = ailang_core::Workspace {
-        entry: ws.entry.clone(),
-        modules: lifted_modules,
-        root_dir: ws.root_dir.clone(),
-        registry: ws.registry.clone(),
-    };
-    let ws = ailang_check::monomorphise_workspace(&ws)
-        .map_err(|e| anyhow::anyhow!("monomorphise_workspace: {e}"))?;
-
-    // ---- staticlib-specific: require ≥1 export, then lower ----
+    // require ≥1 export on the source AST (structural; export survives
+    // desugar/lift/mono unchanged). Checked before elaborate so a
+    // no-export staticlib fails with the clear message rather than on a
+    // missing-`@main`-free lowering.
     let has_export = ws.modules.values().any(|m| m.defs.iter().any(|d|
         matches!(d, ailang_core::Def::Fn(f) if f.export.is_some())));
     if !has_export {
@@ -2509,7 +2422,14 @@ fn build_staticlib(
              leak-only bench instrument, not swarm-safe; use `--alloc=rc`"
         );
     }
-    let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(&ws, alloc)?;
+    let mir = match ailang_check::elaborate_workspace(&ws) {
+        Ok(mir) => mir,
+        Err(diags) => {
+            print_build_diagnostics(&diags);
+            std::process::exit(1);
+        }
+    };
+    let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(&mir, alloc)?;
 
     let tmpdir = std::env::temp_dir().join(format!("ailang-{}", std::process::id()));
     std::fs::create_dir_all(&tmpdir)?;

crates/ail/tests/e2e.rs

@@ -1515,27 +1515,12 @@ fn reuse_as_demo_under_rc_uses_inplace_rewrite() {
     //     extension-dispatching `ailang_surface::load_workspace` so
     //     the `.ail` entry is accepted.
     let ws = ailang_surface::load_workspace(&ail_path).expect("load workspace");
-    let mut lifted_modules = std::collections::BTreeMap::new();
-    for (mname, m) in &ws.modules {
-        let desugared = ailang_core::desugar::desugar_module(m);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .unwrap_or_else(|e| panic!("lift_letrecs in module `{mname}`: {e:?}"));
-        lifted_modules.insert(mname.clone(), lifted);
-    }
-    let lifted_ws = ailang_core::Workspace {
-        entry: ws.entry.clone(),
-        modules: lifted_modules,
-        root_dir: ws.root_dir.clone(),
-        registry: ws.registry.clone(),
-    };
-    // post-print-migration, fixtures use `(app print x)`
-    // which monomorphises to `print__<T>`. Adding the mono pass here
-    // mirrors `ail build`'s pipeline (desugar -> lift -> mono ->
-    // lower); without it, lowering errors with `UnknownVar("print")`.
-    let mono_ws = ailang_check::monomorphise_workspace(&lifted_ws)
-        .expect("monomorphise_workspace");
+    // mir.1b: the desugar→lift→mono→lower bridge collapses into the
+    // single `elaborate_workspace` front-end, which produces the typed
+    // MIR codegen now consumes.
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_with_alloc(
-        &mono_ws,
+        &mir,
         ailang_codegen::AllocStrategy::Rc,
     )
     .expect("lower workspace under rc");
@@ -1686,27 +1671,12 @@ fn alloc_rc_borrow_only_recursive_list_drop() {
     let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
     let json_path = workspace.join("examples").join(example);
     let ws = ailang_surface::load_workspace(&json_path).expect("load workspace");
-    let mut lifted_modules = std::collections::BTreeMap::new();
-    for (mname, m) in &ws.modules {
-        let desugared = ailang_core::desugar::desugar_module(m);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .unwrap_or_else(|e| panic!("lift_letrecs in module `{mname}`: {e:?}"));
-        lifted_modules.insert(mname.clone(), lifted);
-    }
-    let lifted_ws = ailang_core::Workspace {
-        entry: ws.entry.clone(),
-        modules: lifted_modules,
-        root_dir: ws.root_dir.clone(),
-        registry: ws.registry.clone(),
-    };
-    // post-print-migration, fixtures use `(app print x)`
-    // which monomorphises to `print__<T>`. Adding the mono pass here
-    // mirrors `ail build`'s pipeline (desugar -> lift -> mono ->
-    // lower); without it, lowering errors with `UnknownVar("print")`.
-    let mono_ws = ailang_check::monomorphise_workspace(&lifted_ws)
-        .expect("monomorphise_workspace");
+    // mir.1b: the desugar→lift→mono→lower bridge collapses into the
+    // single `elaborate_workspace` front-end, which produces the typed
+    // MIR codegen now consumes.
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_with_alloc(
-        &mono_ws,
+        &mir,
         ailang_codegen::AllocStrategy::Rc,
     )
     .expect("lower workspace under rc");
@@ -1760,27 +1730,12 @@ fn alloc_rc_partial_drop_skips_moved_keeps_wildcarded() {
     let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
     let json_path = workspace.join("examples").join(example);
     let ws = ailang_surface::load_workspace(&json_path).expect("load workspace");
-    let mut lifted_modules = std::collections::BTreeMap::new();
-    for (mname, m) in &ws.modules {
-        let desugared = ailang_core::desugar::desugar_module(m);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .unwrap_or_else(|e| panic!("lift_letrecs in module `{mname}`: {e:?}"));
-        lifted_modules.insert(mname.clone(), lifted);
-    }
-    let lifted_ws = ailang_core::Workspace {
-        entry: ws.entry.clone(),
-        modules: lifted_modules,
-        root_dir: ws.root_dir.clone(),
-        registry: ws.registry.clone(),
-    };
-    // post-print-migration, fixtures use `(app print x)`
-    // which monomorphises to `print__<T>`. Adding the mono pass here
-    // mirrors `ail build`'s pipeline (desugar -> lift -> mono ->
-    // lower); without it, lowering errors with `UnknownVar("print")`.
-    let mono_ws = ailang_check::monomorphise_workspace(&lifted_ws)
-        .expect("monomorphise_workspace");
+    // mir.1b: the desugar→lift→mono→lower bridge collapses into the
+    // single `elaborate_workspace` front-end, which produces the typed
+    // MIR codegen now consumes.
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_with_alloc(
-        &mono_ws,
+        &mir,
         ailang_codegen::AllocStrategy::Rc,
     )
     .expect("lower workspace under rc");
@@ -1849,27 +1804,12 @@ fn alloc_rc_own_param_dec_at_fn_return() {
     let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
     let json_path = workspace.join("examples").join(example);
     let ws = ailang_surface::load_workspace(&json_path).expect("load workspace");
-    let mut lifted_modules = std::collections::BTreeMap::new();
-    for (mname, m) in &ws.modules {
-        let desugared = ailang_core::desugar::desugar_module(m);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .unwrap_or_else(|e| panic!("lift_letrecs in module `{mname}`: {e:?}"));
-        lifted_modules.insert(mname.clone(), lifted);
-    }
-    let lifted_ws = ailang_core::Workspace {
-        entry: ws.entry.clone(),
-        modules: lifted_modules,
-        root_dir: ws.root_dir.clone(),
-        registry: ws.registry.clone(),
-    };
-    // post-print-migration, fixtures use `(app print x)`
-    // which monomorphises to `print__<T>`. Adding the mono pass here
-    // mirrors `ail build`'s pipeline (desugar -> lift -> mono ->
-    // lower); without it, lowering errors with `UnknownVar("print")`.
-    let mono_ws = ailang_check::monomorphise_workspace(&lifted_ws)
-        .expect("monomorphise_workspace");
+    // mir.1b: the desugar→lift→mono→lower bridge collapses into the
+    // single `elaborate_workspace` front-end, which produces the typed
+    // MIR codegen now consumes.
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_with_alloc(
-        &mono_ws,
+        &mir,
         ailang_codegen::AllocStrategy::Rc,
     )
     .expect("lower workspace under rc");
@@ -1972,27 +1912,12 @@ fn iter18e_drop_iterative_emits_worklist_body_no_self_recursion() {
     let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
     let json_path = workspace.join("examples").join(example);
     let ws = ailang_surface::load_workspace(&json_path).expect("load workspace");
-    let mut lifted_modules = std::collections::BTreeMap::new();
-    for (mname, m) in &ws.modules {
-        let desugared = ailang_core::desugar::desugar_module(m);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .unwrap_or_else(|e| panic!("lift_letrecs in module `{mname}`: {e:?}"));
-        lifted_modules.insert(mname.clone(), lifted);
-    }
-    let lifted_ws = ailang_core::Workspace {
-        entry: ws.entry.clone(),
-        modules: lifted_modules,
-        root_dir: ws.root_dir.clone(),
-        registry: ws.registry.clone(),
-    };
-    // post-print-migration, fixtures use `(app print x)`
-    // which monomorphises to `print__<T>`. Adding the mono pass here
-    // mirrors `ail build`'s pipeline (desugar -> lift -> mono ->
-    // lower); without it, lowering errors with `UnknownVar("print")`.
-    let mono_ws = ailang_check::monomorphise_workspace(&lifted_ws)
-        .expect("monomorphise_workspace");
+    // mir.1b: the desugar→lift→mono→lower bridge collapses into the
+    // single `elaborate_workspace` front-end, which produces the typed
+    // MIR codegen now consumes.
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_with_alloc(
-        &mono_ws,
+        &mir,
         ailang_codegen::AllocStrategy::Rc,
     )
     .expect("lower workspace under rc");
@@ -2055,7 +1980,9 @@ fn iter18e_no_annotation_keeps_recursive_drop_body() {
     let workspace = Path::new(manifest_dir).parent().unwrap().parent().unwrap();
     let json_path = workspace.join("examples").join(example);
     let ws = ailang_surface::load_workspace(&json_path).expect("load workspace");
-    // Mutate every TypeDef in every module to clear the annotation.
+    // Mutate every TypeDef in every module to clear the annotation,
+    // then elaborate the mutated source workspace to MIR (mir.1b: the
+    // single front-end replaces the explicit desugar→lift→mono bridge).
     let mut modules = std::collections::BTreeMap::new();
     for (mname, m) in &ws.modules {
         let mut mc = m.clone();
@@ -2064,25 +1991,17 @@ fn iter18e_no_annotation_keeps_recursive_drop_body() {
                 td.drop_iterative = false;
             }
         }
-        let desugared = ailang_core::desugar::desugar_module(&mc);
-        let lifted = ailang_check::lift_letrecs(&desugared)
-            .unwrap_or_else(|e| panic!("lift_letrecs in module `{mname}`: {e:?}"));
-        modules.insert(mname.clone(), lifted);
+        modules.insert(mname.clone(), mc);
     }
-    let lifted_ws = ailang_core::Workspace {
+    let mutated_ws = ailang_core::Workspace {
         entry: ws.entry.clone(),
         modules,
         root_dir: ws.root_dir.clone(),
         registry: ws.registry.clone(),
     };
-    // post-print-migration, fixtures use `(app print x)`
-    // which monomorphises to `print__<T>`. Adding the mono pass here
-    // mirrors `ail build`'s pipeline (desugar -> lift -> mono ->
-    // lower); without it, lowering errors with `UnknownVar("print")`.
-    let mono_ws = ailang_check::monomorphise_workspace(&lifted_ws)
-        .expect("monomorphise_workspace");
+    let mir = ailang_check::elaborate_workspace(&mutated_ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_with_alloc(
-        &mono_ws,
+        &mir,
         ailang_codegen::AllocStrategy::Rc,
     )
     .expect("lower workspace under rc");

crates/ail/tests/typeclass_22b3.rs

@@ -236,7 +236,7 @@ fn synthesise_mono_fn_uses_instance_body_lam() {
         defining_module: "m".into(),
     };
 
-    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
+    let f = synthesise_mono_fn(&target, &class_def, &instance, &std::collections::BTreeSet::new()).expect("synth");
     assert_eq!(f.name, "bar__Int");
     assert!(
         matches!(
@@ -305,7 +305,7 @@ fn synthesise_mono_fn_falls_back_to_class_default() {
         defining_module: "m".into(),
     };
 
-    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
+    let f = synthesise_mono_fn(&target, &class_def, &instance, &std::collections::BTreeSet::new()).expect("synth");
     assert_eq!(f.name, "hello__Int");
     assert_eq!(
         f.params.len(),
@@ -357,7 +357,7 @@ fn synthesise_mono_fn_zero_arg_method_uses_body_verbatim() {
         defining_module: "m".into(),
     };
 
-    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
+    let f = synthesise_mono_fn(&target, &class_def, &instance, &std::collections::BTreeSet::new()).expect("synth");
     assert_eq!(f.name, "bar__Int");
     assert!(
         f.params.is_empty(),

crates/ailang-check/src/lib.rs

@@ -3757,7 +3757,15 @@ pub(crate) fn synth(
             }
             for (a, exp) in args.iter().zip(params.iter()) {
                 let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
-                unify(exp, &actual, subst)?;
+                // Reconcile the post-mono own-module spelling split: a
+                // cross-module callee may name the consumer's own ADT
+                // qualified (`<current_module>.T`) where the consumer
+                // synthesises it bare (`T`). Both denote the same type
+                // within this module; strip the own qualifier from each
+                // side before unifying. Pre-mono this is a no-op.
+                let exp = strip_own_module_qual(exp, &env.current_module);
+                let actual = strip_own_module_qual(&actual, &env.current_module);
+                unify(&exp, &actual, subst)?;
             }
             for e in fx {
                 effects.insert(e);
@@ -4563,6 +4571,51 @@ fn maybe_instantiate(t: Type, counter: &mut u32) -> Type {
 /// Already-qualified names, primitives (`Int`, `Bool`, `Unit`, `Str`),
 /// rigid type vars, and type names that are not in `local_types` pass
 /// through unchanged.
+/// Strip a leading `<module>.` qualifier from every `Type::Con` whose
+/// qualifier is exactly `module`, recursing structurally. Within module
+/// `m`, `m.T` and the bare `T` denote the same type.
+///
+/// Used to reconcile a post-monomorphisation spelling split: a
+/// cross-module callee whose polymorphic parameter was specialised to
+/// the *consumer's own* ADT carries that type *qualified* in its
+/// signature (e.g. prelude's `print__<IntBox>` takes
+/// `show_user_adt.IntBox`), while the consumer synthesises the same type
+/// *bare* under the own-module-types-stay-bare invariant
+/// (`IntBox`). Stripping the consumer module's own qualifier from both
+/// sides before unification makes the two spellings agree. A no-op
+/// outside post-mono re-synth: a cross-module signature never references
+/// the consumer's own type before monomorphisation, so nothing carries a
+/// `<current_module>.` qualifier there. The trailing-dot check keeps a
+/// longer module name with a shared prefix (`m2.T` vs module `m`) intact.
+fn strip_own_module_qual(t: &Type, module: &str) -> Type {
+    match t {
+        Type::Con { name, args } => {
+            let stripped = name
+                .strip_prefix(module)
+                .and_then(|rest| rest.strip_prefix('.'))
+                .map(str::to_string)
+                .unwrap_or_else(|| name.clone());
+            Type::Con {
+                name: stripped,
+                args: args.iter().map(|a| strip_own_module_qual(a, module)).collect(),
+            }
+        }
+        Type::Fn { params, param_modes, ret, ret_mode, effects } => Type::Fn {
+            params: params.iter().map(|p| strip_own_module_qual(p, module)).collect(),
+            param_modes: param_modes.clone(),
+            ret: Box::new(strip_own_module_qual(ret, module)),
+            ret_mode: ret_mode.clone(),
+            effects: effects.clone(),
+        },
+        Type::Var { .. } => t.clone(),
+        Type::Forall { vars, constraints, body } => Type::Forall {
+            vars: vars.clone(),
+            constraints: constraints.clone(),
+            body: Box::new(strip_own_module_qual(body, module)),
+        },
+    }
+}
+
 fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap<String, TypeDef>) -> Type {
     match t {
         Type::Con { name, args } => {
@@ -4588,15 +4641,25 @@ fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap<Stri
                     .collect(),
             }
         }
-        Type::Fn { params, ret, effects, .. } => Type::Fn {
+        // Qualification only renames `Con` type-cons; it never changes
+        // the fn's arity, so the positional `param_modes` stay aligned.
+        // Preserve them (and `ret_mode`): this transform must be
+        // mode-preserving, mirroring the sister `qualify_workspace_types`
+        // and `Subst::apply`. The typed-MIR boundary qualifies a
+        // cross-module callee sig through here, and the codegen drop path
+        // reads `ret_mode == Own` off that node to decide RC trackability;
+        // stripping the mode here erased the Own signal for a
+        // monomorphised polymorphic intrinsic (e.g. `RawBuf.set`), leaking
+        // the owned temporary at the call site.
+        Type::Fn { params, param_modes, ret, ret_mode, effects } => Type::Fn {
             params: params
                 .iter()
                 .map(|p| qualify_local_types(p, owner_module, local_types))
                 .collect(),
             ret: Box::new(qualify_local_types(ret, owner_module, local_types)),
             effects: effects.clone(),
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
+            param_modes: param_modes.clone(),
+            ret_mode: ret_mode.clone(),
         },
         Type::Forall { vars, constraints, body } => Type::Forall {
             vars: vars.clone(),

crates/ailang-check/src/lower_to_mir.rs

@@ -50,7 +50,53 @@ impl<'a> Ctx<'a> {
             &mut free_fn_calls,
             &mut warnings,
         )?;
-        Ok(subst.apply(&ty))
+        Ok(wildcard_residual_metavars(&subst.apply(&ty)))
+    }
+}
+
+/// Rewrite every residual `$m`-prefixed inference metavar to the
+/// `$u` wildcard codegen's monomorphisation unifier expects.
+///
+/// `synth_pure` synthesises each node's type in isolation, so a
+/// type-arg that the full program would pin only through a *sibling*
+/// node stays an unbound metavar here — e.g. a bare `Nil`'s element
+/// type in `(Cons 3 Nil)`: synthesised alone, `Nil : List<$m0>`,
+/// because nothing in the `Nil` node itself constrains the element.
+/// Post-monomorphisation any such residual is, by construction, an
+/// unconstrained *phantom* position (a nullary ctor carries no value
+/// of that type, so no runtime representation depends on it) — every
+/// rep-bearing type was already pinned by its own value or by mono.
+/// Codegen already has a wildcard for exactly this: `$u`, which
+/// `subst::unify_for_subst` accepts on either side without binding, so
+/// a sibling arg pins the type var instead (`Cons`'s declared
+/// `List<a>` field unifies against `List<$u>` without the head's
+/// `a := Int` binding then clashing on `$u`). The canonical checker
+/// emits `$m` metavars, never `$u` — `$u` was the now-deleted
+/// codegen-side synth's own spelling — so the typed-MIR boundary
+/// normalises to it here, once, rather than teaching every node-type
+/// consumer to also tolerate a raw `$m`.
+fn wildcard_residual_metavars(t: &Type) -> Type {
+    match t {
+        Type::Var { name } if name.starts_with("$m") => Type::Var {
+            name: name.replacen("$m", "$u", 1),
+        },
+        Type::Var { .. } => t.clone(),
+        Type::Con { name, args } => Type::Con {
+            name: name.clone(),
+            args: args.iter().map(wildcard_residual_metavars).collect(),
+        },
+        Type::Fn { params, param_modes, ret, ret_mode, effects } => Type::Fn {
+            params: params.iter().map(wildcard_residual_metavars).collect(),
+            param_modes: param_modes.clone(),
+            ret: Box::new(wildcard_residual_metavars(ret)),
+            ret_mode: ret_mode.clone(),
+            effects: effects.clone(),
+        },
+        Type::Forall { vars, constraints, body } => Type::Forall {
+            vars: vars.clone(),
+            constraints: constraints.clone(),
+            body: Box::new(wildcard_residual_metavars(body)),
+        },
     }
 }
 
@@ -300,6 +346,36 @@ pub fn lower_module(module: &Module, env: &Env) -> Result<MirModule> {
     if let Some(im) = env.module_imports.get(&module.name).cloned() {
         env.imports = im;
     }
+    // Post-mono permissive seeding. Monomorphisation synthesises
+    // `<module>.<def>` references that do NOT obey user-source import
+    // discipline — in particular *downward* class-method dispatch: a
+    // method mono'd into the class's home module (e.g. prelude's
+    // `print__IntBox`) references the *instance's* module
+    // (`show_user_adt`) that the home module never imports. The code has
+    // already passed `check_workspace`; this re-synth only re-derives
+    // types, it does not re-check import discipline, so resolution may
+    // reach any workspace module. Seed every module name as an identity
+    // import — without overwriting a real author alias — so the canonical
+    // `synth`'s qualified-var path (lib.rs ~3556, which otherwise resolves
+    // only via TypeDef-home or `env.imports`) resolves these synthesised
+    // cross-module references. The canonical `synth` itself stays strict:
+    // only this post-mono producer is permissive, mirroring the
+    // module-name fallback the now-deleted codegen `synth_arg_type` carried
+    // for exactly this case.
+    // Skip the current module: a module does not import itself, and
+    // seeding a self-import would route its own type-cons through the
+    // cross-module qualification path (`show_user_adt.IntBox`),
+    // violating the own-module-types-stay-bare invariant the canonical
+    // `synth` upholds (`IntBox` stays bare in its home module).
+    let all_modules: Vec<String> = env
+        .module_globals
+        .keys()
+        .filter(|m| *m != &module.name)
+        .cloned()
+        .collect();
+    for m in all_modules {
+        env.imports.entry(m.clone()).or_insert(m);
+    }
     let mut defs = Vec::new();
     let mut consts = Vec::new();
     for def in &module.defs {

crates/ailang-check/src/mono.rs

@@ -153,7 +153,27 @@ pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> {
                             class
                         ))
                     })?;
-                    (synthesise_mono_fn(t, class_def, &entry.instance)?, defining_module.clone())
+                    // own ADT names of the module the synthesised
+                    // method is appended to — so its instance type, if
+                    // that module's own ADT, is localised back to bare
+                    // before substitution (see `synthesise_mono_fn`).
+                    let own_type_names: BTreeSet<String> = ws_owned
+                        .modules
+                        .get(defining_module)
+                        .map(|m| {
+                            m.defs
+                                .iter()
+                                .filter_map(|d| match d {
+                                    Def::Type(td) => Some(td.name.clone()),
+                                    _ => None,
+                                })
+                                .collect()
+                        })
+                        .unwrap_or_default();
+                    (
+                        synthesise_mono_fn(t, class_def, &entry.instance, &own_type_names)?,
+                        defining_module.clone(),
+                    )
                 }
                 MonoTarget::FreeFn { defining_module, .. } => (
                     synthesise_mono_fn_for_free_fn(t, &ws_owned)?,
@@ -960,9 +980,12 @@ pub fn synthesise_mono_fn(
     target: &MonoTarget,
     class_def: &ClassDef,
     instance: &InstanceDef,
+    own_type_names: &BTreeSet<String>,
 ) -> Result<AstFnDef> {
-    let (class_name, method, type_) = match target {
-        MonoTarget::ClassMethod { class, method, type_, .. } => (class, method, type_),
+    let (class_name, method, type_, defining_module) = match target {
+        MonoTarget::ClassMethod { class, method, type_, defining_module } => {
+            (class, method, type_, defining_module)
+        }
         MonoTarget::FreeFn { .. } => {
             return Err(crate::CheckError::Internal(
                 "synthesise_mono_fn: called with FreeFn variant; use \
@@ -986,8 +1009,26 @@ pub fn synthesise_mono_fn(
     // Build the substitution `param := type_` and apply it to the
     // method type. The result is a concrete `Type::Fn` (no
     // `Forall`).
+    //
+    // `type_` is registry-canonical: an instance whose type is the
+    // *defining module's own* ADT carries the qualified
+    // `<defining_module>.<T>` spelling (mono normalises every observed
+    // instance type through `Registry::normalize_type_for_lookup` for
+    // dedup + symbol naming). The synthesised method is appended to that
+    // same `defining_module`, whose own type-cons stay bare under the
+    // own-module-types-stay-bare invariant — so substituting the
+    // qualified `type_` into the method signature mints a param typed
+    // `<defining_module>.<T>` against a body that pattern-matches the
+    // bare ctor, and the post-mono `synth` re-entry in `lower_to_mir`
+    // rejects the clash (`expected show_user_adt.IntBox, got IntBox`).
+    // Localise `type_` back to the defining module's bare convention
+    // before substitution, symmetric to `synthesise_mono_fn_for_free_fn`.
+    // (Primitives and cross-module instance types are untouched —
+    // `localize_own_types` only strips `<defining_module>.<T>` for `T` in
+    // that module's own ADTs.)
+    let local_type = localize_own_types(type_, defining_module, own_type_names);
     let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
-    mapping.insert(class_def.param.clone(), type_.clone());
+    mapping.insert(class_def.param.clone(), local_type);
     let concrete_method_ty = crate::substitute_rigids(&class_method.ty, &mapping);
 
     // Resolve the body — instance override first, then class default.

crates/ailang-codegen/Cargo.toml

@@ -6,6 +6,7 @@ license.workspace = true
 
 [dependencies]
 ailang-core.workspace = true
+ailang-mir.workspace = true
 ailang-check.workspace = true
 thiserror.workspace = true
 indexmap.workspace = true

crates/ailang-codegen/src/drop.rs

@@ -25,7 +25,8 @@
 //! this submodule into the parent's private `Emitter` fields works
 //! through the standard descendant-module privacy lane.
 
-use ailang_core::ast::*;
+use ailang_core::ast::{ParamMode, Type, TypeDef};
+use ailang_mir::{Callee, MTerm};
 use std::collections::BTreeSet;
 
 use super::synth::llvm_type;
@@ -454,16 +455,16 @@ impl<'a> Emitter<'a> {
     /// here. A `Term::Var` returning an RC-allocated box would already
     /// be tracked by an earlier let-binder; tracking it again here
     /// would double-dec.
-    pub(crate) fn is_rc_heap_allocated(&self, value: &Term) -> bool {
+    pub(crate) fn is_rc_heap_allocated(&self, value: &MTerm) -> bool {
         if !matches!(self.alloc, AllocStrategy::Rc) {
             return false;
         }
         match value {
-            Term::Ctor { .. } | Term::Lam { .. } => {
-                let term_ptr = (value as *const Term) as usize;
+            MTerm::Ctor { .. } | MTerm::Lam { .. } => {
+                let term_ptr = (value as *const MTerm) as usize;
                 !self.non_escape.contains(&term_ptr)
             }
-            Term::App { callee, .. } => {
+            MTerm::App { callee, .. } => {
                 // a call whose callee carries
                 // `ret_mode == Own` hands a fresh heap allocation to
                 // the caller's frame. Trackable. `Borrow` and
@@ -475,7 +476,7 @@ impl<'a> Emitter<'a> {
                     .map(|m| matches!(m, ParamMode::Own))
                     .unwrap_or(false)
             }
-            Term::Loop { .. } => {
+            MTerm::Loop { .. } => {
                 // Loop result is owned-and-untracked (seeds are moved in).
                 // Track iff its static type is boxed/heap (llvm `ptr`) AND not
                 // Str. Str is excluded: a loop can return a *static* Str (a seed
@@ -484,20 +485,16 @@ impl<'a> Emitter<'a> {
                 // never return a static Str, which is why the App arm may track Str
                 // but the Loop arm must not. Unboxed primitives (Int/Bool/Float/Unit)
                 // lower to non-`ptr` and are correctly excluded by the `ptr` gate.
-                match self.synth_arg_type(value) {
-                    Ok(t) => {
-                        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
-                    }
-                    Err(_) => false,
-                }
+                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
             }
             _ => false,
         }
@@ -510,8 +507,11 @@ impl<'a> Emitter<'a> {
     /// is defensive). Used by [`Self::is_rc_heap_allocated`] and the
     /// [`Self::drop_symbol_for_binder`] App-arm to decide both
     /// trackability and the drop-fn symbol.
-    fn synth_callee_ret_mode(&self, callee: &Term) -> Option<ParamMode> {
-        let cty = self.synth_arg_type(callee).ok()?;
+    fn synth_callee_ret_mode(&self, callee: &Callee) -> Option<ParamMode> {
+        let cty = match callee {
+            Callee::Indirect(inner) => inner.ty(),
+            Callee::Static { .. } => return None,
+        };
         match cty {
             Type::Fn { ret_mode, .. } => Some(ret_mode),
             _ => None,
@@ -530,9 +530,9 @@ impl<'a> Emitter<'a> {
     /// unreachable since `is_rc_heap_allocated` only returns `true`
     /// for `Term::Ctor` / `Term::Lam`, but a defensive fallback
     /// keeps the IR well-formed even if the predicate ever widens.
-    pub(crate) fn drop_symbol_for_binder(&self, value: &Term, val_ssa: &str) -> String {
+    pub(crate) fn drop_symbol_for_binder(&self, value: &MTerm, val_ssa: &str) -> String {
         match value {
-            Term::Ctor { type_name, .. } => {
+            MTerm::Ctor { type_name, .. } => {
                 if type_name.matches('.').count() == 1 {
                     let (prefix, suffix) =
                         type_name.split_once('.').expect("checked");
@@ -543,7 +543,7 @@ impl<'a> Emitter<'a> {
                 }
                 format!("drop_{m}_{type_name}", m = self.module_name)
             }
-            Term::Lam { .. } => self
+            MTerm::Lam { .. } => self
                 .closure_drops
                 .get(val_ssa)
                 .cloned()
@@ -557,8 +557,8 @@ impl<'a> Emitter<'a> {
             // the ret-type is not a `Type::Con` (e.g. a bare type
             // var on an as-yet-unmonomorphised polymorphic call —
             // the monomorphised copies will resolve correctly).
-            Term::App { .. } | Term::Loop { .. } => {
-                if let Ok(Type::Con { name, .. }) = self.synth_arg_type(value) {
+            MTerm::App { .. } | MTerm::Loop { .. } => {
+                if let Type::Con { name, .. } = value.ty() {
                     // Symmetric to `field_drop_call`'s Str arm: Str is a
                     // built-in pointer type with no per-type drop fn. Both
                     // heap-Str (rc_header at payload-8) and static-Str
@@ -843,25 +843,22 @@ impl<'a> Emitter<'a> {
     /// the runtime tag and dec's only the unmoved fields.
     pub(crate) fn emit_inlined_partial_drop(
         &mut self,
-        value: &Term,
+        value: &MTerm,
         val_ssa: &str,
         moved: &BTreeSet<usize>,
     ) -> Result<()> {
         let (type_name, ctor_name) = match value {
-            Term::Ctor { type_name, ctor, .. } => (type_name.as_str(), ctor.as_str()),
+            MTerm::Ctor { type_name, ctor, .. } => (type_name.as_str(), ctor.as_str()),
             _ => {
                 // dynamic-tag partial-drop via the
-                // per-type helper. `value` is `Term::App` (Own-
+                // per-type helper. `value` is `MTerm::App` (Own-
                 // returning) — the binder's static type is the App's
-                // ret type, recovered through `synth_arg_type` /
-                // `partial_drop_symbol_for_type`. `Term::Lam` shapes
+                // ret type, read off `value.ty()` and mapped through
+                // `partial_drop_symbol_for_type`. `MTerm::Lam` shapes
                 // never reach here with a non-empty `moved` (you can't
                 // pattern-match a closure-pair); the fallback below
                 // handles them defensively.
-                let sym = self
-                    .synth_arg_type(value)
-                    .ok()
-                    .and_then(|ty| self.partial_drop_symbol_for_type(&ty));
+                let sym = self.partial_drop_symbol_for_type(&value.ty());
                 if let (Some(sym), Some(mask)) =
                     (sym, Self::build_moved_mask(moved))
                 {

crates/ailang-codegen/src/escape.rs

@@ -80,7 +80,8 @@
 //! Precision can be improved later; correctness is the priority for
 //! this iter.
 
-use ailang_core::ast::{NewArg, Pattern, Term};
+use ailang_core::ast::Pattern;
+use ailang_mir::{Callee, MNewArg, MTerm};
 use std::collections::BTreeSet;
 
 /// Set of allocation sites (identified by raw pointer address cast to
@@ -94,7 +95,7 @@ pub type NonEscapeSet = BTreeSet<usize>;
 /// Run the analysis over a fn body. Returns the set of allocation
 /// sites (pointers to `Term::Ctor` / `Term::Lam` nodes) that may
 /// be safely lowered with `alloca` instead of the runtime allocator.
-pub fn analyze_fn_body(body: &Term) -> NonEscapeSet {
+pub fn analyze_fn_body(body: &MTerm) -> NonEscapeSet {
     let mut out = NonEscapeSet::new();
     walk(body, &mut out);
     out
@@ -107,13 +108,13 @@ pub fn analyze_fn_body(body: &Term) -> NonEscapeSet {
 ///
 /// Then recurse into all sub-terms so that nested let-allocations and
 /// lambdas are analyzed too.
-fn walk(t: &Term, out: &mut NonEscapeSet) {
+fn walk(t: &MTerm, out: &mut NonEscapeSet) {
     match t {
-        Term::Let { name, value, body } => {
+        MTerm::Let { name, init, body, .. } => {
             // Candidate shape: let X = Ctor|Lam in B.
-            let alloc_kind = match value.as_ref() {
-                Term::Ctor { .. } => Some("ctor"),
-                Term::Lam { .. } => Some("lam"),
+            let alloc_kind = match init.as_ref() {
+                MTerm::Ctor { .. } => Some("ctor"),
+                MTerm::Lam { .. } => Some("lam"),
                 _ => None,
             };
             if alloc_kind.is_some() {
@@ -126,46 +127,48 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
                 // tainted name, it escapes the let, which transitively
                 // escapes the fn.
                 if !escapes(body, &tainted, true) {
-                    let ptr = (value.as_ref() as *const Term) as usize;
+                    let ptr = (init.as_ref() as *const MTerm) as usize;
                     out.insert(ptr);
                 }
             }
             // Recurse into value and body for any nested allocations.
-            walk(value, out);
+            walk(init, out);
             walk(body, out);
         }
-        Term::App { callee, args, .. } => {
-            walk(callee, out);
+        MTerm::App { callee, args, .. } => {
+            if let Callee::Indirect(inner) = callee {
+                walk(inner, out);
+            }
             for a in args {
-                walk(a, out);
+                walk(&a.term, out);
             }
         }
-        Term::Do { args, .. } => {
+        MTerm::Do { args, .. } => {
             for a in args {
-                walk(a, out);
+                walk(&a.term, out);
             }
         }
-        Term::Ctor { args, .. } => {
+        MTerm::Ctor { args, .. } => {
             for a in args {
-                walk(a, out);
+                walk(&a.term, out);
             }
         }
-        Term::Match { scrutinee, arms } => {
+        MTerm::Match { scrutinee, arms, .. } => {
             walk(scrutinee, out);
             for arm in arms {
                 walk(&arm.body, out);
             }
         }
-        Term::If { cond, then, else_ } => {
+        MTerm::If { cond, then, else_, .. } => {
             walk(cond, out);
             walk(then, out);
             walk(else_, out);
         }
-        Term::Seq { lhs, rhs } => {
+        MTerm::Seq { lhs, rhs, .. } => {
             walk(lhs, out);
             walk(rhs, out);
         }
-        Term::Lam { body, .. } => {
+        MTerm::Lam { body, .. } => {
             // Recurse into the lambda body — it is itself a fn frame
             // for our analysis purposes (each lifted thunk runs the
             // same analysis when emit_fn is called for it; for
@@ -173,47 +176,47 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
             // allocations).
             walk(body, out);
         }
-        Term::LetRec { body, in_term, .. } => {
+        MTerm::LetRec { body, in_term, .. } => {
             // LetRec is normally eliminated before codegen.
             // Still walk for completeness.
             walk(body, out);
             walk(in_term, out);
         }
-        Term::Clone { value } => {
+        MTerm::Clone { value, .. } => {
             // clone is identity at IR level — only walk
             // sub-terms looking for Let-allocation candidates.
             walk(value, out);
         }
-        Term::ReuseAs { source, body } => {
+        MTerm::ReuseAs { source, body, .. } => {
             // identity at IR level (codegen lowers `body`,
             // ignores `source`). Walk both children for completeness.
             walk(source, out);
             walk(body, out);
         }
-        Term::Loop { binders, body } => {
+        MTerm::Loop { binders, body, .. } => {
             for b in binders {
                 walk(&b.init, out);
             }
             walk(body, out);
         }
-        Term::Recur { args } => {
+        MTerm::Recur { args, .. } => {
             for a in args {
-                walk(a, out);
+                walk(&a.term, out);
             }
         }
         // prep.2 (kernel-extension-mechanics): walker through
-        // NewArg::Value subterms; Term::New does not yet have a
+        // MNewArg::Value subterms; MTerm::New does not yet have a
         // direct codegen path (lower_term returns an Internal error
         // via Pattern D until the raw-buf milestone lands).
-        Term::New { args, .. } => {
+        MTerm::New { args, .. } => {
             for arg in args {
-                if let NewArg::Value(v) = arg {
+                if let MNewArg::Value(v) = arg {
                     walk(v, out);
                 }
             }
         }
-        Term::Lit { .. } | Term::Var { .. } => {}
-        Term::Intrinsic => {}
+        MTerm::Lit { .. } | MTerm::Str { .. } | MTerm::Var { .. } => {}
+        MTerm::Intrinsic { .. } => {}
     }
 }
 
@@ -224,69 +227,71 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
 /// initial call from `walk`, we set `in_tail = true` for the let's
 /// body because the body's value is the let's value, which we cannot
 /// see beyond — better to assume escape.
-fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
+fn escapes(t: &MTerm, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
     match t {
-        Term::Lit { .. } => false,
-        Term::Var { name } => {
+        MTerm::Lit { .. } | MTerm::Str { .. } => false,
+        MTerm::Var { name, .. } => {
             // A bare Var reference whose value flows to tail = escape.
             in_tail && tainted.contains(name)
         }
-        Term::App { callee, args, .. } => {
+        MTerm::App { callee, args, .. } => {
             // Callee position. Special case: a direct call to a
             // tainted Var (calling the bound closure) is not escape;
             // the closure pair is loaded and invoked locally.
-            match callee.as_ref() {
-                Term::Var { name: cname } if tainted.contains(cname) => {
-                    // Calling locally is fine; don't flag the callee as escape.
-                }
-                _ => {
-                    if escapes(callee, tainted, false) {
-                        return true;
+            if let Callee::Indirect(inner) = callee {
+                match inner.as_ref() {
+                    MTerm::Var { name: cname, .. } if tainted.contains(cname) => {
+                        // Calling locally is fine; don't flag the callee as escape.
+                    }
+                    _ => {
+                        if escapes(inner, tainted, false) {
+                            return true;
+                        }
                     }
                 }
             }
             // Args: any tainted Var as arg = escape. Sub-expressions
             // recurse with in_tail=false.
             for a in args {
-                if let Term::Var { name } = a {
+                if let MTerm::Var { name, .. } = &a.term {
                     if tainted.contains(name) {
                         return true;
                     }
                 }
-                if escapes(a, tainted, false) {
+                if escapes(&a.term, tainted, false) {
                     return true;
                 }
             }
             false
         }
-        Term::Do { args, .. } => {
+        MTerm::Do { args, .. } => {
             for a in args {
-                if let Term::Var { name } = a {
+                if let MTerm::Var { name, .. } = &a.term {
                     if tainted.contains(name) {
                         return true;
                     }
                 }
-                if escapes(a, tainted, false) {
+                if escapes(&a.term, tainted, false) {
                     return true;
                 }
             }
             false
         }
-        Term::Ctor { args, .. } => {
+        MTerm::Ctor { args, .. } => {
             for a in args {
-                if let Term::Var { name } = a {
+                if let MTerm::Var { name, .. } = &a.term {
                     if tainted.contains(name) {
                         return true;
                     }
                 }
-                if escapes(a, tainted, false) {
+                if escapes(&a.term, tainted, false) {
                     return true;
                 }
             }
             false
         }
-        Term::Let { name, value, body } => {
-            if escapes(value, tainted, false) {
+        MTerm::Let { name, init, body, .. } => {
+            if escapes(init, tainted, false) {
                 return true;
             }
             // If the let's value is a tainted Var, the new binding
@@ -295,7 +300,7 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             // taint flowing through computation. Conservative cut:
             // only direct Var aliasing propagates.)
             let mut local = tainted.clone();
-            if let Term::Var { name: vn } = value.as_ref() {
+            if let MTerm::Var { name: vn, .. } = init.as_ref() {
                 if tainted.contains(vn) {
                     local.insert(name.clone());
                 }
@@ -303,14 +308,14 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             // Body: tail position propagates from the enclosing let.
             escapes(body, &local, in_tail)
         }
-        Term::Match { scrutinee, arms } => {
+        MTerm::Match { scrutinee, arms, .. } => {
             if escapes(scrutinee, tainted, false) {
                 return true;
             }
             // If the scrutinee is a tainted Var, propagate taint to
             // pattern bindings (each arm independently).
             let scrutinee_tainted = match scrutinee.as_ref() {
-                Term::Var { name } => tainted.contains(name),
+                MTerm::Var { name, .. } => tainted.contains(name),
                 _ => false,
             };
             for arm in arms {
@@ -328,7 +333,7 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             false
         }
-        Term::If { cond, then, else_ } => {
+        MTerm::If { cond, then, else_, .. } => {
             if escapes(cond, tainted, false) {
                 return true;
             }
@@ -340,13 +345,13 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             false
         }
-        Term::Seq { lhs, rhs } => {
+        MTerm::Seq { lhs, rhs, .. } => {
             if escapes(lhs, tainted, false) {
                 return true;
             }
             escapes(rhs, tainted, in_tail)
         }
-        Term::Lam { params, body, .. } => {
+        MTerm::Lam { params, body, .. } => {
             // A lambda captures free vars. If any free var is tainted,
             // the closure escapes the value via its env. (Even if the
             // closure pair itself doesn't escape, capturing creates a
@@ -366,19 +371,19 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             false
         }
-        Term::LetRec { .. } => {
+        MTerm::LetRec { .. } => {
             // LetRec is normally eliminated by the lift-pass before
             // codegen. If one slips through, be conservative and
             // declare escape.
             true
         }
-        Term::Clone { value } => {
+        MTerm::Clone { value, .. } => {
             // clone is identity. The wrapper's escape
             // verdict is exactly that of its inner term, threaded
             // through with the same `in_tail` context.
             escapes(value, tainted, in_tail)
         }
-        Term::ReuseAs { source, body } => {
+        MTerm::ReuseAs { source, body, .. } => {
             // identity at IR level. The whole expression's
             // value is `body`, so its escape verdict is the body's
             // (threaded through `in_tail`). The `source` is evaluated
@@ -390,7 +395,7 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             escapes(body, tainted, in_tail)
         }
-        Term::Loop { binders, body } => {
+        MTerm::Loop { binders, body, .. } => {
             for b in binders {
                 if escapes(&b.init, tainted, false) {
                     return true;
@@ -398,22 +403,22 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             escapes(body, tainted, in_tail)
         }
-        Term::Recur { args } => {
+        MTerm::Recur { args, .. } => {
             for a in args {
-                if escapes(a, tainted, false) {
+                if escapes(&a.term, tainted, false) {
                     return true;
                 }
             }
             false
         }
-        // prep.2 (kernel-extension-mechanics): walk every NewArg::Value
-        // in non-tail mode (call-arg semantics). Term::New itself does
+        // prep.2 (kernel-extension-mechanics): walk every MNewArg::Value
+        // in non-tail mode (call-arg semantics). MTerm::New itself does
         // not yet codegen; the analysis stays conservative against the
         // future codegen by treating each value-arg as a non-tail
         // expression whose tainted-name flow matters.
-        Term::New { args, .. } => {
+        MTerm::New { args, .. } => {
             for arg in args {
-                if let NewArg::Value(v) = arg {
+                if let MNewArg::Value(v) = arg {
                     if escapes(v, tainted, false) {
                         return true;
                     }
@@ -421,7 +426,7 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             false
         }
-        Term::Intrinsic => false,
+        MTerm::Intrinsic { .. } => false,
     }
 }
 
@@ -443,44 +448,46 @@ fn pattern_bound_names(p: &Pattern, out: &mut Vec<String>) {
 /// only to check whether a Lam captures any tainted name. Mirrors
 /// `Emitter::collect_captures` in lib.rs but without the builtin /
 /// top-level filter (those don't matter for taint).
-fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<String>) {
+fn collect_free_vars(t: &MTerm, bound: &mut BTreeSet<String>, out: &mut BTreeSet<String>) {
     match t {
-        Term::Lit { .. } => {}
-        Term::Var { name } => {
+        MTerm::Lit { .. } | MTerm::Str { .. } => {}
+        MTerm::Var { name, .. } => {
             if !bound.contains(name) {
                 out.insert(name.clone());
             }
         }
-        Term::App { callee, args, .. } => {
-            collect_free_vars(callee, bound, out);
+        MTerm::App { callee, args, .. } => {
+            if let Callee::Indirect(inner) = callee {
+                collect_free_vars(inner, bound, out);
+            }
             for a in args {
-                collect_free_vars(a, bound, out);
+                collect_free_vars(&a.term, bound, out);
             }
         }
-        Term::Do { args, .. } => {
+        MTerm::Do { args, .. } => {
             for a in args {
-                collect_free_vars(a, bound, out);
+                collect_free_vars(&a.term, bound, out);
             }
         }
-        Term::Ctor { args, .. } => {
+        MTerm::Ctor { args, .. } => {
             for a in args {
-                collect_free_vars(a, bound, out);
+                collect_free_vars(&a.term, bound, out);
             }
         }
-        Term::Let { name, value, body } => {
-            collect_free_vars(value, bound, out);
+        MTerm::Let { name, init, body, .. } => {
+            collect_free_vars(init, bound, out);
             let inserted = bound.insert(name.clone());
             collect_free_vars(body, bound, out);
             if inserted {
                 bound.remove(name);
             }
         }
-        Term::If { cond, then, else_ } => {
+        MTerm::If { cond, then, else_, .. } => {
             collect_free_vars(cond, bound, out);
             collect_free_vars(then, bound, out);
             collect_free_vars(else_, bound, out);
         }
-        Term::Match { scrutinee, arms } => {
+        MTerm::Match { scrutinee, arms, .. } => {
             collect_free_vars(scrutinee, bound, out);
             for arm in arms {
                 let mut binds = Vec::new();
@@ -497,7 +504,7 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
                 }
             }
         }
-        Term::Lam { params, body, .. } => {
+        MTerm::Lam { params, body, .. } => {
             let mut newly = Vec::new();
             for p in params {
                 if bound.insert(p.clone()) {
@@ -509,24 +516,24 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
                 bound.remove(&n);
             }
         }
-        Term::Seq { lhs, rhs } => {
+        MTerm::Seq { lhs, rhs, .. } => {
             collect_free_vars(lhs, bound, out);
             collect_free_vars(rhs, bound, out);
         }
-        Term::LetRec { body, in_term, .. } => {
+        MTerm::LetRec { body, in_term, .. } => {
             collect_free_vars(body, bound, out);
             collect_free_vars(in_term, bound, out);
         }
-        Term::Clone { value } => {
+        MTerm::Clone { value, .. } => {
             // clone is identity for free-var collection.
             collect_free_vars(value, bound, out);
         }
-        Term::ReuseAs { source, body } => {
+        MTerm::ReuseAs { source, body, .. } => {
             // free vars are the union of source and body.
             collect_free_vars(source, bound, out);
             collect_free_vars(body, bound, out);
         }
-        Term::Loop { binders, body } => {
+        MTerm::Loop { binders, body, .. } => {
             let mut newly: Vec<String> = Vec::new();
             for b in binders {
                 collect_free_vars(&b.init, bound, out);
@@ -539,43 +546,49 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
                 bound.remove(&n);
             }
         }
-        Term::Recur { args } => {
+        MTerm::Recur { args, .. } => {
             for a in args {
-                collect_free_vars(a, bound, out);
+                collect_free_vars(&a.term, bound, out);
             }
         }
         // prep.2 (kernel-extension-mechanics): free vars of a
         // `(new T args)` are the union of free vars of every
-        // NewArg::Value; NewArg::Type carries no term.
-        Term::New { args, .. } => {
+        // MNewArg::Value; MNewArg::Type carries no term.
+        MTerm::New { args, .. } => {
             for arg in args {
-                if let NewArg::Value(v) = arg {
+                if let MNewArg::Value(v) = arg {
                     collect_free_vars(v, bound, out);
                 }
             }
         }
-        Term::Intrinsic => {}
+        MTerm::Intrinsic { .. } => {}
     }
 }
 
 #[cfg(test)]
 mod tests {
     use super::*;
-    use ailang_core::ast::{Arm, Literal, Type};
+    use ailang_core::ast::{Literal, Type};
+    use ailang_mir::{MArg, MArm, Mode};
 
-    fn lit_int(v: i64) -> Term {
-        Term::Lit {
+    fn marg(term: MTerm) -> MArg {
+        MArg { term, mode: Mode::Owned, consume_count: 1 }
+    }
+    fn lit_int(v: i64) -> MTerm {
+        MTerm::Lit {
             lit: Literal::Int { value: v },
+            ty: Type::int(),
         }
     }
-    fn var(s: &str) -> Term {
-        Term::Var { name: s.into() }
+    fn var(s: &str) -> MTerm {
+        MTerm::Var { name: s.into(), ty: Type::int() }
     }
-    fn ctor(ty: &str, c: &str, args: Vec<Term>) -> Term {
-        Term::Ctor {
+    fn ctor(ty: &str, c: &str, args: Vec<MTerm>) -> MTerm {
+        MTerm::Ctor {
             type_name: ty.into(),
             ctor: c.into(),
-            args,
+            args: args.into_iter().map(marg).collect(),
+            ty: Type::Con { name: ty.into(), args: vec![] },
         }
     }
 
@@ -589,25 +602,28 @@ mod tests {
             "Cons",
             vec![lit_int(1), ctor("L", "Nil", vec![])],
         );
-        let alloc_ptr = (&alloc as *const Term) as usize;
-        let body = Term::Let {
+        let alloc_ptr = (&alloc as *const MTerm) as usize;
+        let body = MTerm::Let {
             name: "xs".into(),
-            value: Box::new(alloc.clone()),
-            body: Box::new(Term::Match {
+            mode: Mode::Owned,
+            init: Box::new(alloc.clone()),
+            body: Box::new(MTerm::Match {
                 scrutinee: Box::new(var("xs")),
-                arms: vec![Arm {
+                arms: vec![MArm {
                     pat: Pattern::Wild,
                     body: lit_int(0),
                 }],
+                ty: Type::int(),
             }),
+            ty: Type::int(),
         };
         let neset = analyze_fn_body(&body);
-        // The allocation site we care about is the `value` field of
+        // The allocation site we care about is the `init` field of
         // the Let. Since `body` was constructed inline (the Let's
-        // value is a Box copy of `alloc`), use the boxed copy's addr.
+        // init is a Box copy of `alloc`), use the boxed copy's addr.
         // Walk the AST to find it.
         let let_value_ptr = match &body {
-            Term::Let { value, .. } => (value.as_ref() as *const Term) as usize,
+            MTerm::Let { init, .. } => (init.as_ref() as *const MTerm) as usize,
             _ => unreachable!(),
         };
         assert!(
@@ -628,14 +644,16 @@ mod tests {
             "Cons",
             vec![lit_int(1), ctor("L", "Nil", vec![])],
         );
-        let body = Term::Let {
+        let body = MTerm::Let {
             name: "xs".into(),
-            value: Box::new(alloc),
+            mode: Mode::Owned,
+            init: Box::new(alloc),
             body: Box::new(var("xs")),
+            ty: Type::int(),
         };
         let neset = analyze_fn_body(&body);
         let let_value_ptr = match &body {
-            Term::Let { value, .. } => (value.as_ref() as *const Term) as usize,
+            MTerm::Let { init, .. } => (init.as_ref() as *const MTerm) as usize,
             _ => unreachable!(),
         };
         assert!(
@@ -649,18 +667,21 @@ mod tests {
     #[test]
     fn ctor_passed_as_arg_escapes() {
         let alloc = ctor("L", "Nil", vec![]);
-        let body = Term::Let {
+        let body = MTerm::Let {
             name: "xs".into(),
-            value: Box::new(alloc),
-            body: Box::new(Term::App {
-                callee: Box::new(var("length")),
-                args: vec![var("xs")],
+            mode: Mode::Owned,
+            init: Box::new(alloc),
+            body: Box::new(MTerm::App {
+                callee: Callee::Indirect(Box::new(var("length"))),
+                args: vec![marg(var("xs"))],
                 tail: false,
+                ty: Type::int(),
             }),
+            ty: Type::int(),
         };
         let neset = analyze_fn_body(&body);
         let let_value_ptr = match &body {
-            Term::Let { value, .. } => (value.as_ref() as *const Term) as usize,
+            MTerm::Let { init, .. } => (init.as_ref() as *const MTerm) as usize,
             _ => unreachable!(),
         };
         assert!(
@@ -674,18 +695,20 @@ mod tests {
     #[test]
     fn ctor_stored_in_ctor_field_escapes() {
         let h_alloc = ctor("X", "Mk", vec![lit_int(1)]);
-        let body = Term::Let {
+        let body = MTerm::Let {
             name: "h".into(),
-            value: Box::new(h_alloc),
+            mode: Mode::Owned,
+            init: Box::new(h_alloc),
             body: Box::new(ctor(
                 "L",
                 "Cons",
                 vec![var("h"), ctor("L", "Nil", vec![])],
             )),
+            ty: Type::int(),
         };
         let neset = analyze_fn_body(&body);
         let let_value_ptr = match &body {
-            Term::Let { value, .. } => (value.as_ref() as *const Term) as usize,
+            MTerm::Let { init, .. } => (init.as_ref() as *const MTerm) as usize,
             _ => unreachable!(),
         };
         assert!(
@@ -704,13 +727,14 @@ mod tests {
             "Cons",
             vec![lit_int(1), ctor("L", "Nil", vec![])],
         );
-        let body = Term::Let {
+        let body = MTerm::Let {
             name: "xs".into(),
-            value: Box::new(alloc),
-            body: Box::new(Term::Match {
+            mode: Mode::Owned,
+            init: Box::new(alloc),
+            body: Box::new(MTerm::Match {
                 scrutinee: Box::new(var("xs")),
                 arms: vec![
-                    Arm {
+                    MArm {
                         pat: Pattern::Ctor {
                             ctor: "Cons".into(),
                             fields: vec![
@@ -720,7 +744,7 @@ mod tests {
                         },
                         body: var("h"),
                     },
-                    Arm {
+                    MArm {
                         pat: Pattern::Ctor {
                             ctor: "Nil".into(),
                             fields: vec![],
@@ -728,11 +752,13 @@ mod tests {
                         body: lit_int(0),
                     },
                 ],
+                ty: Type::int(),
             }),
+            ty: Type::int(),
         };
         let neset = analyze_fn_body(&body);
         let let_value_ptr = match &body {
-            Term::Let { value, .. } => (value.as_ref() as *const Term) as usize,
+            MTerm::Let { init, .. } => (init.as_ref() as *const MTerm) as usize,
             _ => unreachable!(),
         };
         assert!(
@@ -745,25 +771,29 @@ mod tests {
     /// callee. Expected: alloca-eligible.
     #[test]
     fn local_lam_call_only() {
-        let lam = Term::Lam {
+        let lam = MTerm::Lam {
             params: vec!["x".into()],
             param_tys: vec![Type::int()],
-            ret_ty: Box::new(Type::int()),
+            ret_ty: Type::int(),
             effects: vec![],
             body: Box::new(var("x")),
+            ty: Type::int(),
         };
-        let body = Term::Let {
+        let body = MTerm::Let {
             name: "f".into(),
-            value: Box::new(lam),
-            body: Box::new(Term::App {
-                callee: Box::new(var("f")),
-                args: vec![lit_int(42)],
+            mode: Mode::Owned,
+            init: Box::new(lam),
+            body: Box::new(MTerm::App {
+                callee: Callee::Indirect(Box::new(var("f"))),
+                args: vec![marg(lit_int(42))],
                 tail: false,
+                ty: Type::int(),
             }),
+            ty: Type::int(),
         };
         let neset = analyze_fn_body(&body);
         let let_value_ptr = match &body {
-            Term::Let { value, .. } => (value.as_ref() as *const Term) as usize,
+            MTerm::Let { init, .. } => (init.as_ref() as *const MTerm) as usize,
             _ => unreachable!(),
         };
         assert!(
@@ -777,25 +807,29 @@ mod tests {
     /// as arg. Expected: NOT alloca-eligible.
     #[test]
     fn lam_passed_as_arg_escapes() {
-        let lam = Term::Lam {
+        let lam = MTerm::Lam {
             params: vec!["x".into()],
             param_tys: vec![Type::int()],
-            ret_ty: Box::new(Type::int()),
+            ret_ty: Type::int(),
             effects: vec![],
             body: Box::new(var("x")),
+            ty: Type::int(),
         };
-        let body = Term::Let {
+        let body = MTerm::Let {
             name: "f".into(),
-            value: Box::new(lam),
-            body: Box::new(Term::App {
-                callee: Box::new(var("map")),
-                args: vec![var("f"), var("xs")],
+            mode: Mode::Owned,
+            init: Box::new(lam),
+            body: Box::new(MTerm::App {
+                callee: Callee::Indirect(Box::new(var("map"))),
+                args: vec![marg(var("f")), marg(var("xs"))],
                 tail: false,
+                ty: Type::int(),
             }),
+            ty: Type::int(),
         };
         let neset = analyze_fn_body(&body);
         let let_value_ptr = match &body {
-            Term::Let { value, .. } => (value.as_ref() as *const Term) as usize,
+            MTerm::Let { init, .. } => (init.as_ref() as *const MTerm) as usize,
             _ => unreachable!(),
         };
         assert!(

crates/ailang-codegen/src/lambda.rs

@@ -23,7 +23,8 @@
 //!   - `synth::llvm_type`, `synth::fn_sig_from_type`: free-function
 //!     helpers for IR shaping.
 
-use ailang_core::ast::*;
+use ailang_core::ast::{ParamMode, Pattern, Type};
+use ailang_mir::{Callee, MNewArg, MTerm};
 use std::collections::BTreeSet;
 
 use super::escape;
@@ -41,7 +42,7 @@ impl<'a> Emitter<'a> {
         lam_params: &[String],
         lam_param_tys: &[Type],
         lam_ret_ty: &Type,
-        lam_body: &Term,
+        lam_body: &MTerm,
         term_ptr: usize,
     ) -> Result<(String, String)> {
         let llvm_param_tys: Vec<String> =
@@ -370,7 +371,7 @@ impl<'a> Emitter<'a> {
     /// are excluded — they're globally accessible. Qualified names
     /// (`prefix.def`) are excluded too.
     fn collect_captures(
-        t: &Term,
+        t: &MTerm,
         bound: &mut BTreeSet<String>,
         captures: &mut Vec<String>,
         captures_set: &mut BTreeSet<String>,
@@ -378,8 +379,8 @@ impl<'a> Emitter<'a> {
         top_level: &BTreeSet<String>,
     ) {
         match t {
-            Term::Lit { .. } => {}
-            Term::Var { name } => {
+            MTerm::Lit { .. } | MTerm::Str { .. } => {}
+            MTerm::Var { name, .. } => {
                 if name.contains('.') {
                     return; // qualified ref is module-level
                 }
@@ -396,36 +397,38 @@ impl<'a> Emitter<'a> {
                     captures.push(name.clone());
                 }
             }
-            Term::App { callee, args, .. } => {
-                Self::collect_captures(callee, bound, captures, captures_set, builtins, top_level);
+            MTerm::App { callee, args, .. } => {
+                if let Callee::Indirect(inner) = callee {
+                    Self::collect_captures(inner, bound, captures, captures_set, builtins, top_level);
+                }
                 for a in args {
-                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
+                    Self::collect_captures(&a.term, bound, captures, captures_set, builtins, top_level);
                 }
             }
-            Term::Let { name, value, body } => {
-                Self::collect_captures(value, bound, captures, captures_set, builtins, top_level);
+            MTerm::Let { name, init, body, .. } => {
+                Self::collect_captures(init, bound, captures, captures_set, builtins, top_level);
                 let inserted = bound.insert(name.clone());
                 Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
                 if inserted {
                     bound.remove(name);
                 }
             }
-            Term::If { cond, then, else_ } => {
+            MTerm::If { cond, then, else_, .. } => {
                 Self::collect_captures(cond, bound, captures, captures_set, builtins, top_level);
                 Self::collect_captures(then, bound, captures, captures_set, builtins, top_level);
                 Self::collect_captures(else_, bound, captures, captures_set, builtins, top_level);
             }
-            Term::Do { args, .. } => {
+            MTerm::Do { args, .. } => {
                 for a in args {
-                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
+                    Self::collect_captures(&a.term, bound, captures, captures_set, builtins, top_level);
                 }
             }
-            Term::Ctor { args, .. } => {
+            MTerm::Ctor { args, .. } => {
                 for a in args {
-                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
+                    Self::collect_captures(&a.term, bound, captures, captures_set, builtins, top_level);
                 }
             }
-            Term::Match { scrutinee, arms } => {
+            MTerm::Match { scrutinee, arms, .. } => {
                 Self::collect_captures(scrutinee, bound, captures, captures_set, builtins, top_level);
                 for arm in arms {
                     let mut pat_bindings = Vec::new();
@@ -442,7 +445,7 @@ impl<'a> Emitter<'a> {
                     }
                 }
             }
-            Term::Lam { params, body, .. } => {
+            MTerm::Lam { params, body, .. } => {
                 // Inner lambda's params don't escape; its free vars
                 // (relative to the outer) DO contribute to outer captures.
                 let mut newly_bound = Vec::new();
@@ -456,25 +459,25 @@ impl<'a> Emitter<'a> {
                     bound.remove(&n);
                 }
             }
-            Term::Seq { lhs, rhs } => {
+            MTerm::Seq { lhs, rhs, .. } => {
                 Self::collect_captures(lhs, bound, captures, captures_set, builtins, top_level);
                 Self::collect_captures(rhs, bound, captures, captures_set, builtins, top_level);
             }
-            Term::LetRec { .. } => {
+            MTerm::LetRec { .. } => {
                 // eliminated by desugar before codegen.
-                unreachable!("Term::LetRec eliminated by desugar")
+                unreachable!("MTerm::LetRec eliminated by desugar")
             }
-            Term::Clone { value } => {
+            MTerm::Clone { value, .. } => {
                 // clone is identity for capture analysis —
                 // free vars of `(clone X)` are exactly the free vars of `X`.
                 Self::collect_captures(value, bound, captures, captures_set, builtins, top_level);
             }
-            Term::ReuseAs { source, body } => {
+            MTerm::ReuseAs { source, body, .. } => {
                 // free vars are the union of source and body.
                 Self::collect_captures(source, bound, captures, captures_set, builtins, top_level);
                 Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
             }
-            Term::Loop { binders, body } => {
+            MTerm::Loop { binders, body, .. } => {
                 let mut newly_bound: Vec<String> = Vec::new();
                 for b in binders {
                     Self::collect_captures(&b.init, bound, captures, captures_set, builtins, top_level);
@@ -487,22 +490,22 @@ impl<'a> Emitter<'a> {
                     bound.remove(&n);
                 }
             }
-            Term::Recur { args } => {
+            MTerm::Recur { args, .. } => {
                 for a in args {
-                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
+                    Self::collect_captures(&a.term, bound, captures, captures_set, builtins, top_level);
                 }
             }
             // prep.2 (kernel-extension-mechanics): captures of a
             // `(new T args)` are the union of captures of every
-            // NewArg::Value; NewArg::Type carries no runtime term.
-            Term::New { args, .. } => {
+            // MNewArg::Value; MNewArg::Type carries no runtime term.
+            MTerm::New { args, .. } => {
                 for arg in args {
-                    if let NewArg::Value(v) = arg {
+                    if let MNewArg::Value(v) = arg {
                         Self::collect_captures(v, bound, captures, captures_set, builtins, top_level);
                     }
                 }
             }
-            Term::Intrinsic => {}
+            MTerm::Intrinsic { .. } => {}
         }
     }
 

crates/ailang-codegen/src/match_lower.rs

@@ -15,13 +15,14 @@
 //! to the lookup-table family.
 //!
 //! Cross-references back into the parent module:
-//!   - `synth_arg_type`, `lookup_ctor_by_type`,
-//!     `lookup_ctor_in_pattern`, `collect_owner_local_types`,
-//!     `field_drop_call`: lookup helpers, all `pub(crate)`.
+//!   - `lookup_ctor_by_type`, `lookup_ctor_in_pattern`,
+//!     `collect_owner_local_types`, `field_drop_call`: lookup helpers,
+//!     all `pub(crate)`. Per-node types are read off `MTerm::ty()`.
 //!   - `lower_term`, `start_block`, `fresh_ssa`, `fresh_id`:
 //!     lowering primitives, all `pub(crate)`.
 
-use ailang_core::ast::*;
+use ailang_core::ast::{ParamMode, Pattern, Type};
+use ailang_mir::{MArg, MArm, MTerm};
 use std::collections::{BTreeMap, BTreeSet};
 
 use super::synth::llvm_type;
@@ -43,7 +44,7 @@ impl<'a> Emitter<'a> {
         &mut self,
         type_name: &str,
         ctor_name: &str,
-        args: &[Term],
+        args: &[MArg],
         term_ptr: usize,
     ) -> Result<(String, String)> {
         let cref = self.lookup_ctor_by_type(type_name, ctor_name)?;
@@ -79,8 +80,8 @@ impl<'a> Emitter<'a> {
         } else {
             let arg_ail_tys: Vec<Type> = args
                 .iter()
-                .map(|a| self.synth_arg_type(a))
-                .collect::<Result<_>>()?;
+                .map(|a| a.term.ty())
+                .collect::<Vec<_>>();
             let var_set: BTreeSet<&str> =
                 cref.type_vars.iter().map(|s| s.as_str()).collect();
             let mut subst: BTreeMap<String, Type> = BTreeMap::new();
@@ -96,7 +97,7 @@ impl<'a> Emitter<'a> {
         // together.
         let mut compiled = Vec::new();
         for (a, exp) in args.iter().zip(expected_llvm_tys.iter()) {
-            let (v, vty) = self.lower_term(a)?;
+            let (v, vty) = self.lower_term(&a.term)?;
             if &vty != exp {
                 return Err(CodegenError::Internal(format!(
                     "ctor `{ctor_name}` field type {vty} != expected {exp}"
@@ -178,10 +179,10 @@ impl<'a> Emitter<'a> {
     /// fields. The shape check ensures that path is unreachable.
     pub(crate) fn lower_reuse_as_rc(
         &mut self,
-        source: &Term,
+        source: &MTerm,
         body_type_name: &str,
         body_ctor_name: &str,
-        body_args: &[Term],
+        body_args: &[MArg],
     ) -> Result<(String, String)> {
         // 1. Lower the source. Linearity (18d.1) guarantees this is a
         //    bare Var of an in-scope binder; lower_term resolves it
@@ -198,7 +199,7 @@ impl<'a> Emitter<'a> {
         // ensures `source` is `Term::Var` here; the var-resolution
         // is just defensive.
         let source_binder: Option<String> = match source {
-            Term::Var { name } => {
+            MTerm::Var { name, .. } => {
                 if self.locals.iter().any(|(n, _, _, _)| n == name) {
                     Some(name.clone())
                 } else {
@@ -228,7 +229,7 @@ impl<'a> Emitter<'a> {
         // pattern in Lean 4's reset/reuse codegen: the
         // refcount-decrement is the contract; the drop fn cascade
         // is owned by the last release, not by intermediate ones.
-        let _ = source; // synth_arg_type not needed for shallow dec
+        let _ = source; // source type not needed for a shallow dec
         let src_drop_call = "ailang_rc_dec".to_string();
 
         // 2. Resolve the body ctor and its expected per-field LLVM
@@ -260,8 +261,8 @@ impl<'a> Emitter<'a> {
         } else {
             let arg_ail_tys: Vec<Type> = body_args
                 .iter()
-                .map(|a| self.synth_arg_type(a))
-                .collect::<Result<_>>()?;
+                .map(|a| a.term.ty())
+                .collect::<Vec<_>>();
             let var_set: BTreeSet<&str> =
                 cref.type_vars.iter().map(|s| s.as_str()).collect();
             let mut subst: BTreeMap<String, Type> = BTreeMap::new();
@@ -285,7 +286,7 @@ impl<'a> Emitter<'a> {
         //    on refcount.
         let mut compiled = Vec::new();
         for (a, exp) in body_args.iter().zip(expected_llvm_tys.iter()) {
-            let (v, vty) = self.lower_term(a)?;
+            let (v, vty) = self.lower_term(&a.term)?;
             if &vty != exp {
                 return Err(CodegenError::Internal(format!(
                     "reuse-as body ctor `{body_ctor_name}` field type {vty} != expected {exp}"
@@ -439,10 +440,10 @@ impl<'a> Emitter<'a> {
 
     pub(crate) fn lower_match(
         &mut self,
-        scrutinee: &Term,
-        arms: &[Arm],
+        scrutinee: &MTerm,
+        arms: &[MArm],
     ) -> Result<(String, String)> {
-        let s_ail = self.synth_arg_type(scrutinee)?;
+        let s_ail = scrutinee.ty();
         let (s_val, s_ty) = self.lower_term(scrutinee)?;
         if s_ty != "ptr" {
             return Err(CodegenError::Internal(format!(
@@ -457,7 +458,7 @@ impl<'a> Emitter<'a> {
         // fallback). Only record when the var actually resolves to a
         // local binder.
         let scrutinee_binder: Option<String> = match scrutinee {
-            Term::Var { name } => {
+            MTerm::Var { name, .. } => {
                 if self.locals.iter().any(|(n, _, _, _)| n == name) {
                     Some(name.clone())
                 } else {
@@ -473,8 +474,8 @@ impl<'a> Emitter<'a> {
             .push_str(&format!("  {tag} = load i64, ptr {s_val}, align 8\n"));
 
         // Separate arms.
-        let mut ctor_arms: Vec<(CtorRef, &Arm, Vec<Option<String>>)> = Vec::new();
-        let mut open_arm: Option<&Arm> = None;
+        let mut ctor_arms: Vec<(CtorRef, &MArm, Vec<Option<String>>)> = Vec::new();
+        let mut open_arm: Option<&MArm> = None;
         let mut open_var: Option<String> = None;
         for arm in arms {
             match &arm.pat {
@@ -698,7 +699,7 @@ impl<'a> Emitter<'a> {
             // up to prevent.
             let arm_body_is_tail_call = matches!(
                 &arm.body,
-                Term::App { tail: true, .. } | Term::Do { tail: true, .. }
+                MTerm::App { tail: true, .. } | MTerm::Do { tail: true, .. }
             );
             if matches!(self.alloc, AllocStrategy::Rc)
                 && arm_body_is_tail_call

crates/ailang-codegen/src/subst.rs

@@ -1,66 +1,20 @@
 //! Type substitution + unification helpers for monomorphisation.
 //!
 //! Free functions extracted from `lib.rs` during the 18g tidy split.
-//! The four-step pipeline is: `derive_substitution` walks declared
-//! params against actual arg types, calling `unify_for_subst` to bind
-//! `Type::Var`s; `apply_subst_to_type` / `apply_subst_to_term`
-//! specialise a polymorphic def under that binding;
-//! `qualify_local_types_codegen` rewrites bare ADT names into
-//! `module.Type` form when a sig crosses an import boundary;
-//! `descriptor_for_subst` produces the stable mangling suffix used in
-//! the specialised symbol's name.
+//! `unify_for_subst` walks declared params against actual arg types and
+//! binds `Type::Var`s; `apply_subst_to_type` specialises a polymorphic
+//! type under that binding; `qualify_local_types_codegen` rewrites bare
+//! ADT names into `module.Type` form when a sig crosses an import
+//! boundary. (The mir.1b switch deleted the codegen-side type-mirror,
+//! the only caller of the former `derive_substitution` entry; its
+//! callers in `match_lower` build the substitution directly via
+//! `unify_for_subst`.)
 
 use ailang_core::ast::*;
 use std::collections::{BTreeMap, BTreeSet};
 
 use super::{CodegenError, Result};
 
-/// derive a name → concrete-type substitution from the
-/// declared params of a `Forall` body and the actual arg types at a
-/// call site. Walks both sides in parallel; whenever a `Type::Var`
-/// (rigid name) appears on the params side, binds it to the
-/// corresponding concrete type. Conflicts (same var bound to two
-/// different types) surface as an internal error — the typechecker
-/// would already have rejected such a call.
-pub(crate) fn derive_substitution(
-    vars: &[String],
-    params: &[Type],
-    arg_tys: &[Type],
-) -> Result<BTreeMap<String, Type>> {
-    if params.len() != arg_tys.len() {
-        return Err(CodegenError::Internal(format!(
-            "derive_substitution: arity mismatch ({} params vs {} args)",
-            params.len(),
-            arg_tys.len(),
-        )));
-    }
-    let var_set: BTreeSet<&str> = vars.iter().map(|s| s.as_str()).collect();
-    let mut subst: BTreeMap<String, Type> = BTreeMap::new();
-    for (p, a) in params.iter().zip(arg_tys.iter()) {
-        unify_for_subst(p, a, &var_set, &mut subst)?;
-    }
-    // Any forall var not pinned by the args is left unbound. For the
-    // MVP this is an error — we can't specialise without a concrete
-    // type. The typechecker's body should have constrained it already
-    // through return-type unification, but at the call site we only
-    // see args; if needed, callers can extend this with expected-ret
-    // info.
-    // a forall var that the args couldn't pin (e.g.
-    // `is_none(Nothing) : forall a. (Maybe a) -> Bool` — `a` is
-    // genuinely unobservable from the args alone) defaults to `Unit`.
-    // The specialised body must not actually read an `a`-typed value,
-    // or it would have failed type-checking; a dummy concrete type is
-    // sound and lets monomorphisation proceed deterministically. The
-    // descriptor uses the same default, so all such call sites
-    // converge on a single specialisation.
-    for v in vars {
-        if !subst.contains_key(v) {
-            subst.insert(v.clone(), Type::unit());
-        }
-    }
-    Ok(subst)
-}
-
 /// Walks `param` and `arg` in parallel, treating any `Type::Var { name }`
 /// on the param side whose name is in `vars` as an unknown to be bound
 /// in `subst`. Identical concrete shapes pass through; structural
@@ -72,7 +26,7 @@ pub(crate) fn unify_for_subst(
     subst: &mut BTreeMap<String, Type>,
 ) -> Result<()> {
     // A `$u`-prefixed var is a
-    // synth-only wildcard produced by `synth_arg_type` for nullary
+    // synth-only wildcard the checker emits for nullary
     // ctors of a parameterised ADT (e.g. `Nil : List<$u>`). It
     // carries no real constraint — accept without binding so a
     // sibling arg can pin the type var instead. Without this,

crates/ailang-codegen/src/synth.rs

@@ -56,142 +56,11 @@ pub(crate) fn fn_sig_from_type(t: &Type) -> Option<FnSig> {
     None
 }
 
-/// AILang type of a builtin operator. Used by
-/// `synth_arg_type` for arg-type inference at polymorphic call sites.
-/// Mirrors what the typechecker installs in its env via `builtins`.
-pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
-    // same widening as `crates/ailang-check/src/
-    // builtins.rs` — `+`/`-`/`*`/`/` and `!=`/`<`/`<=`/`>`/`>=` are
-    // polymorphic. `%` stays monomorphic-Int. Codegen lowering for
-    // these ops still goes through `builtin_binop` (Int-only) in
-    // iter 3; iter 4 converts that to type-dispatched.
-    let poly_a_a_to_a = || Type::Forall {
-        vars: vec!["a".into()],
-        constraints: vec![],
-        body: Box::new(Type::Fn {
-            params: vec![
-                Type::Var { name: "a".into() },
-                Type::Var { name: "a".into() },
-            ],
-            ret: Box::new(Type::Var { name: "a".into() }),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
-        }),
-    };
-    // 2026-05-21 operator-routing-eq-ord: `poly_a_a_to_bool` was
-    // shared by the six comparator builtins. With those names
-    // deleted from the surface, the helper is dead.
-    let int_int_int = || Type::Fn {
-        params: vec![Type::int(), Type::int()],
-        ret: Box::new(Type::int()),
-        effects: vec![],
-        param_modes: vec![],
-        ret_mode: ParamMode::Implicit,
-    };
-    Some(match name {
-        "+" | "-" | "*" | "/" => poly_a_a_to_a(),
-        "%" => int_int_int(),
-        // 2026-05-21 operator-routing-eq-ord: the six comparator
-        // names (`==` / `!=` / `<` / `<=` / `>` / `>=`) are no
-        // longer surface identifiers. Equality / ordering route
-        // through the class methods `eq` / `compare` (prelude.Eq /
-        // Ord); Float comparison routes through the named fns
-        // `float_eq` / `float_lt` / etc. Neither path needs an
-        // entry in this codegen-side mirror table.
-        "not" => Type::Fn {
-            params: vec![Type::bool_()],
-            ret: Box::new(Type::bool_()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
-        },
-        // `__unreachable__` is the polymorphic bottom value
-        // (`forall a. a`). Mirrors the typechecker's `builtins::install`.
-        "__unreachable__" => Type::Forall {
-            vars: vec!["a".into()],
-            constraints: vec![],
-            body: Box::new(Type::Var { name: "a".into() }),
-        },
-        // Float-conversion and inspection builtins.
-        // Same lockstep with `crates/ailang-check/src/builtins.rs`.
-        "neg" => Type::Forall {
-            vars: vec!["a".into()],
-            constraints: vec![],
-            body: Box::new(Type::Fn {
-                params: vec![Type::Var { name: "a".into() }],
-                ret: Box::new(Type::Var { name: "a".into() }),
-                effects: vec![],
-                param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
-            }),
-        },
-        "int_to_float" => Type::Fn {
-            params: vec![Type::int()],
-            ret: Box::new(Type::float()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
-        },
-        "float_to_int_truncate" => Type::Fn {
-            params: vec![Type::float()],
-            ret: Box::new(Type::int()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
-        },
-        "float_to_str" => Type::Fn {
-            params: vec![Type::float()],
-            ret: Box::new(Type::str_()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Own,
-        },
-        "int_to_str" => Type::Fn {
-            params: vec![Type::int()],
-            ret: Box::new(Type::str_()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Own,
-        },
-        "bool_to_str" => Type::Fn {
-            params: vec![Type::bool_()],
-            ret: Box::new(Type::str_()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Own,
-        },
-        "str_clone" => Type::Fn {
-            params: vec![Type::str_()],
-            ret: Box::new(Type::str_()),
-            effects: vec![],
-            param_modes: vec![ParamMode::Borrow],
-            ret_mode: ParamMode::Own,
-        },
-        "is_nan" => Type::Fn {
-            params: vec![Type::float()],
-            ret: Box::new(Type::bool_()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
-        },
-        // Float bit-pattern constants. Bare values,
-        // not fns — referenced via `Term::Var`. Mirrors the
-        // typechecker's `builtins::install`. Codegen emits LLVM hex-
-        // float literals at the use site in iter 4.
-        "nan" | "inf" | "neg_inf" => Type::float(),
-        _ => return None,
-    })
-}
-
-/// AILang return type of a built-in effect op. The op's
-/// param signature is irrelevant here since we only consume the ret.
-pub(crate) fn builtin_effect_op_ret(op: &str) -> Option<Type> {
-    Some(match op {
-        "io/print_str" => Type::unit(),
-        _ => return None,
-    })
-}
+// mir.1b: `builtin_ail_type` (the codegen-side mirror of a builtin's
+// AILang type) and `builtin_effect_op_ret` were read only by the
+// codegen-side type re-derivation deleted in this iteration. Codegen
+// now reads `MTerm::ty()` off the typed MIR, so the mirror table is
+// gone — both definitions removed.
 
 // iter 23.4: `type_descriptor` was the helper that mangled a `Type`
 // into an identifier-safe suffix for the codegen-side mono mangling
@@ -200,8 +69,8 @@ pub(crate) fn builtin_effect_op_ret(op: &str) -> Option<Type> {
 // via 8-hex hash) — see `ailang_check::mono::mono_symbol_n`.
 
 /// Floats iter 4.2: arithmetic / comparison ops are type-dispatched
-/// over `{Int, Float}`. Caller (`lower_app`) resolves the arg type
-/// via `synth_arg_type` and passes it here. Returns the
+/// over `{Int, Float}`. Caller (`lower_app`) reads the arg type off
+/// `MTerm::ty()` and passes it here. Returns the
 /// `(instruction, operand_llvm_type, result_llvm_type)` triple to
 /// emit. `%` stays Int-only.
 ///

crates/ailang-codegen/tests/embed_record_layout_pin.rs

@@ -25,8 +25,9 @@ fn load(file: &str) -> Workspace {
 
 fn lower_carrier_ir() -> String {
     let ws = load("embed_record_layout_carrier.ail");
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     ailang_codegen::lower_workspace_with_alloc(
-        &ws, ailang_codegen::AllocStrategy::Rc).unwrap()
+        &mir, ailang_codegen::AllocStrategy::Rc).unwrap()
 }
 
 #[test]

crates/ailang-codegen/tests/embed_staticlib_lowering.rs

@@ -20,8 +20,9 @@ fn load(file: &str) -> Workspace {
 #[test]
 fn staticlib_emits_forwarder_no_main() {
     let ws = load("embed_backtest_step.ail");
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(
-        &ws, ailang_codegen::AllocStrategy::Rc).unwrap();
+        &mir, ailang_codegen::AllocStrategy::Rc).unwrap();
     assert!(!ir.contains("define i32 @main()"),
         "staticlib IR must not emit the @main trampoline");
     assert!(ir.contains("@backtest_step("),
@@ -55,8 +56,9 @@ fn staticlib_emits_forwarder_no_main() {
 #[test]
 fn staticlib_record_forwarder_is_ptr_passthrough() {
     let ws = load("embed_backtest_step_record.ail");
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(
-        &ws, ailang_codegen::AllocStrategy::Rc).unwrap();
+        &mir, ailang_codegen::AllocStrategy::Rc).unwrap();
     // record param + ret cross as bare ptr; ctx leading; M2 TLS shape.
     assert!(ir.contains("define ptr @backtest_step(ptr %ctx, ptr %a0, double %a1)"),
         "record fwd: ptr ret, leading ptr %ctx, ptr record param, double sample;\nIR:\n{ir}");
@@ -75,8 +77,9 @@ fn executable_target_still_emits_main() {
     let ws = load("embed_backtest_step.ail");
     // Default executable lowering is unaffected by the new field;
     // backtest has no `main`, so exe-target lowering still rejects.
+    let mir = ailang_check::elaborate_workspace(&ws).expect("elaborates");
     let err = ailang_codegen::lower_workspace_with_alloc(
-        &ws, ailang_codegen::AllocStrategy::Rc).unwrap_err();
+        &mir, ailang_codegen::AllocStrategy::Rc).unwrap_err();
     assert!(format!("{err}").contains("has no `main` def"),
         "exe target must still surface MissingEntryMain; got {err}");
 }

crates/ailang-codegen/tests/eq_primitives_pin.rs

@@ -6,7 +6,7 @@
 //! extension-dispatching superset), so the post-iter `.ail` corpus is
 //! loaded from Form A rather than the deleted `.ail.json` siblings.
 
-use ailang_check::{check_workspace, monomorphise_workspace, Severity};
+use ailang_check::elaborate_workspace;
 use ailang_codegen::lower_workspace;
 use ailang_surface::load_workspace;
 use std::path::Path;
@@ -21,13 +21,8 @@ fn eq_primitives_smoke_path() -> std::path::PathBuf {
 fn lower_eq_primitives_smoke() -> String {
     let entry = eq_primitives_smoke_path();
     let ws = load_workspace(&entry).expect("load workspace");
-    let diags = check_workspace(&ws);
-    assert!(
-        diags.iter().all(|d| !matches!(d.severity, Severity::Error)),
-        "unexpected check_workspace errors: {diags:?}"
-    );
-    let ws = monomorphise_workspace(&ws).expect("monomorphise");
-    lower_workspace(&ws).expect("lower")
+    let mir = elaborate_workspace(&ws).expect("elaborates");
+    lower_workspace(&mir).expect("lower")
 }
 
 /// integration with the auto-loaded prelude. Compiling a