iter 23.4: mono-pass unification — class methods + polymorphic free fns in one fixpoint

Restructure ailang-check/src/mono.rs::monomorphise_workspace into a
single specialiser over every Type::Forall-quantified Def::Fn, covering
both class-method residuals AND polymorphic free-fn call sites in one
fixpoint pass. Remove the codegen-time specialiser (lower_polymorphic_call,
module_polymorphic_fns, mono_queue, mono_emitted, emit_specialised_fn,
plus the now-dead helpers apply_subst_to_term, descriptor_for_subst,
type_descriptor) entirely. Codegen sees only monomorphic Def::Fns after
this iter — no polymorphic call sites, no codegen-time queue.

Architecture changes:
- MonoTarget: struct → enum with ClassMethod / FreeFn variants; dedup
  keys are guaranteed-disjoint via 'class'/'free' first component.
- collect_mono_targets: new FreeFnCall channel through synth (cleaner
  than the plan's separate-walker proposal — one less data flow,
  substitution tracking comes 'for free' via fresh metavars +
  post-synth subst.apply). Plan Step 4.4 (polymorphic_free_fns env
  field) consequently obsolete.
- synthesise_mono_fn_for_free_fn: new free-fn entry point; substitutes
  rigid vars in BOTH the type AND the body (body substitution required
  because free-fn bodies carry inner Lams whose param_tys reference
  outer Forall vars — adapted from plan's 'body unchanged' sketch).
- mono_symbol_n: N-ary extension of mono_symbol; bit-stable for the
  single-type-var case (hash-stability pin Task 1 fires zero times
  through all eight refactor tasks).
- rewrite_class_method_calls → rewrite_mono_calls; interleaved-slot
  collector preserves the positional-cursor invariant across both
  channels.
- workspace_has_typeclasses → workspace_has_specialisable_targets
  (principled correctness; old predicate happened to already be true
  for every user workspace because the prelude is auto-injected).

Codegen cleanup:
- Two call sites of lower_polymorphic_call deleted (codegen/src/lib.rs
  lines ~1939-1945, ~1965-1973).
- lower_polymorphic_call body, module_polymorphic_fns field +
  population + Emitter wiring, mono_queue / mono_emitted, drain loop,
  emit_specialised_fn — all removed.
- is_static_callee collapsed to module_user_fns-only.
- subst.rs apply_subst_to_term + descriptor_for_subst removed; synth.rs
  type_descriptor removed (all dead post-removal).
- ail emit-ir command pipeline gains lift_letrecs + monomorphise_workspace
  pre-passes (pre-iter-23.4 the codegen-time poly path was masking
  this dependency — emit-ir is now consistent with build).
- Net codegen reduction: -285 lines lib.rs, -93 lines subst.rs.

Tests:
- mono_hash_stability.rs (new): regression pin for six primitive Eq/Ord
  mono-symbol body hashes; stayed bit-stable through all eight refactor
  tasks.
- mono_unification.rs (new): six tests covering variant-key disjointness,
  free-fn target emission, free-fn synthesis with rigid substitution,
  rewrite walker on free fns, identity for poly-free-fn-only workspaces,
  end-to-end cmp_max_smoke runtime correctness.
- typeclass_22b3.rs: three test sites updated to MonoTarget::ClassMethod
  enum form.
- 73 e2e + 18 typeclass + 81 codegen tests all green workspace-wide.

DESIGN.md §'Monomorphisation (post-typecheck, pre-codegen)' amended:
two-arm fixpoint described, disjoint-keyed dedup, cursor-aligned
walker, removed codegen-time path.

Bench check (all exit 0, 112 metrics stable): bench/check.py +
compile_check.py + cross_lang.py.

Plan parent: docs/plans/2026-05-11-iter-23.4.md (fab1685).
Spec parent: docs/specs/2026-05-11-23-eq-ord-prelude.md (841d65d).
Per-iter journal documents two adapted deviations from the plan
(synth-channel vs separate walker; body substitution; emit-ir fix);
no spec defects.

bench/orchestrator-stats/2026-05-11-iter-23.4.json

@@ -0,0 +1,34 @@
+{
+  "iter_id": "23.4",
+  "date": "2026-05-11",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 11,
+  "tasks_completed": 11,
+  "reloops_per_task": {
+    "1": 0,
+    "2": 0,
+    "3": 0,
+    "4": 1,
+    "5": 1,
+    "6": 0,
+    "7": 0,
+    "8": 1,
+    "9": 0,
+    "10": 0,
+    "11": 0
+  },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "bench_check_exit_code": 0,
+  "bench_compile_check_exit_code": 0,
+  "bench_cross_lang_exit_code": 0,
+  "bench_regressed_metrics": 0,
+  "bench_total_metrics": 112,
+  "notes_per_task": {
+    "4": "extended `synth` with new `&mut Vec<FreeFnCall>` channel instead of plan's separate-walker approach; bypassed plan Step 4.4 (`polymorphic_free_fns` env field unneeded under this approach); fixed builtin-discrimination bug (`==`-like operators in env.globals are filtered by `module_globals[<owner>].contains_key`)",
+    "5": "added `substitute_rigids_in_term` to substitute rigid vars in the body — required because free-fn bodies (e.g. std_list.length) carry inner Lams with `param_tys: [Type::Var \"a\"]`; class-method arm doesn't need this because instance bodies are Lam-unwrapped at synth time",
+    "8": "added Unit-default fallback for unpinned forall vars in `collect_mono_targets` + `collect_residuals_ordered` (mirrors pre-iter-23.4 codegen behaviour for sites like `is_empty(Nil)`); updated `ail emit-ir` command pipeline to include `lift_letrecs` + `monomorphise_workspace` (pre-iter-23.4 codegen-time poly path was masking this dependency)"
+  }
+}

crates/ail/src/main.rs

@@ -674,6 +674,27 @@ fn main() -> Result<()> {
                     std::process::exit(1);
                 }
             }
+            // Iter 23.4: 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 = ailang_codegen::lower_workspace(&ws)?;
             match out {
                 Some(p) => {

crates/ail/tests/mono_hash_stability.rs

@@ -0,0 +1,52 @@
+//! Regression pin for primitive Eq/Ord mono-symbol body hashes.
+//!
+//! Locks the six primitive mono symbols (`eq__Int`, `eq__Bool`, `eq__Str`,
+//! `compare__Int`, `compare__Bool`, `compare__Str`) to their pre-iter-23.4
+//! body hashes. The unified mono pass MUST produce bit-identical bodies.
+
+use ailang_core::ast::Def;
+use ailang_core::hash::def_hash;
+use ailang_core::workspace::load_workspace;
+use std::path::PathBuf;
+
+fn fixture_path() -> PathBuf {
+    let mut d = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
+    d.pop();
+    d.pop();
+    d.join("examples").join("mono_hash_pin_smoke.ail.json")
+}
+
+#[test]
+fn primitive_eq_ord_mono_symbol_hashes_stay_bit_identical() {
+    let ws = load_workspace(&fixture_path()).expect("workspace loads");
+    let diags = ailang_check::check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
+    let post_mono = ailang_check::monomorphise_workspace(&ws).expect("mono green");
+
+    // Mono symbols for class methods are appended to the instance's
+    // `defining_module` — i.e. the prelude module, since all six
+    // primitive Eq/Ord instances live there.
+    let prelude_mod = post_mono
+        .modules
+        .get("prelude")
+        .expect("prelude module present");
+
+    let pins: &[(&str, &str)] = &[
+        ("eq__Int",       "81d59ac38ab3663d"),
+        ("eq__Bool",      "11da98a358b5979b"),
+        ("eq__Str",       "277516bb7f195b2a"),
+        ("compare__Int",  "d5d3f66b86c7e758"),
+        ("compare__Bool", "676e3ea0298a8795"),
+        ("compare__Str",  "a532710899cf14fe"),
+    ];
+
+    for (sym, pin) in pins {
+        let def = prelude_mod
+            .defs
+            .iter()
+            .find(|d| matches!(d, Def::Fn(f) if f.name == *sym))
+            .unwrap_or_else(|| panic!("mono symbol {sym} not found in prelude module"));
+        let h = def_hash(def);
+        assert_eq!(&h, pin, "{sym} body hash drifted");
+    }
+}

crates/ail/tests/mono_unification.rs

@@ -0,0 +1,221 @@
+//! Tests for the unified mono pass over polymorphic free fns (iter 23.4).
+//!
+//! These tests assert workspace-level invariants AFTER
+//! `monomorphise_workspace` has run: synthesised mono `Def::Fn`s for
+//! both class-method residuals AND polymorphic free-fn calls live in
+//! the post-mono workspace.
+
+use ailang_check::mono::{mono_target_key, MonoTarget};
+use ailang_core::ast::{Def, Type};
+use ailang_core::workspace::load_workspace;
+use std::path::PathBuf;
+
+fn fixture(name: &str) -> PathBuf {
+    let mut d = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
+    d.pop();
+    d.pop();
+    d.join("examples").join(name)
+}
+
+#[test]
+fn cmp_max_smoke_produces_both_mono_symbols_in_one_fixpoint() {
+    let ws = load_workspace(&fixture("cmp_max_smoke.ail.json"))
+        .expect("workspace loads");
+    let diags = ailang_check::check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
+    let post_mono = ailang_check::monomorphise_workspace(&ws).expect("mono green");
+
+    // Free-fn mono symbols are appended to their owner module
+    // (where the polymorphic Def::Fn lives) — for cmp_max, that is
+    // `cmp_max_smoke`. Class-method mono symbols (compare__Int) are
+    // appended to the instance's defining module (`prelude`).
+    let main_mod = post_mono
+        .modules
+        .get("cmp_max_smoke")
+        .expect("main module present");
+    let prelude_mod = post_mono
+        .modules
+        .get("prelude")
+        .expect("prelude module present");
+
+    let main_names: Vec<&str> = main_mod
+        .defs
+        .iter()
+        .filter_map(|d| if let Def::Fn(f) = d { Some(f.name.as_str()) } else { None })
+        .collect();
+    let prelude_names: Vec<&str> = prelude_mod
+        .defs
+        .iter()
+        .filter_map(|d| if let Def::Fn(f) = d { Some(f.name.as_str()) } else { None })
+        .collect();
+
+    assert!(
+        main_names.contains(&"cmp_max__Int"),
+        "post-mono workspace must contain free-fn mono symbol cmp_max__Int in module cmp_max_smoke; got {main_names:?}"
+    );
+    assert!(
+        prelude_names.contains(&"compare__Int"),
+        "post-mono workspace must contain class-method mono symbol compare__Int in prelude (closed transitively from cmp_max__Int body); got {prelude_names:?}"
+    );
+}
+
+#[test]
+fn collect_mono_targets_emits_free_fn_target_for_cmp_max_at_int() {
+    use ailang_check::mono::collect_mono_targets;
+    let ws = load_workspace(&fixture("cmp_max_smoke.ail.json")).expect("workspace loads");
+    let diags = ailang_check::check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
+    let env = ailang_check::build_check_env(&ws);
+
+    let main_mod = ws.modules.get("cmp_max_smoke").expect("main module");
+    let main_fn = main_mod.defs.iter().find_map(|d| {
+        if let Def::Fn(f) = d { (f.name == "main").then_some(f) } else { None }
+    }).expect("main fn");
+
+    let targets = collect_mono_targets(main_fn, "cmp_max_smoke", &env)
+        .expect("collector runs");
+
+    let has_free_fn_target = targets.iter().any(|t| matches!(
+        t, MonoTarget::FreeFn { name, type_args, .. }
+        if name == "cmp_max" && type_args.len() == 1
+            && matches!(&type_args[0], Type::Con { name, args } if name == "Int" && args.is_empty())
+    ));
+    assert!(
+        has_free_fn_target,
+        "expected MonoTarget::FreeFn {{ name: \"cmp_max\", type_args: [Int] }}; got {targets:?}"
+    );
+}
+
+#[test]
+fn cmp_max_smoke_runs_end_to_end() {
+    // Compile + run the cmp_max_smoke fixture, prove it prints 7
+    // (cmp_max(3, 7) at Int via Ord Int).
+    use std::process::Command;
+    let manifest_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"));
+    let workspace = manifest_dir.parent().unwrap().parent().unwrap();
+    let src = workspace.join("examples").join("cmp_max_smoke.ail.json");
+    let tmp = std::env::temp_dir().join(format!(
+        "ailang_cmp_max_smoke_{}",
+        std::process::id()
+    ));
+    std::fs::create_dir_all(&tmp).unwrap();
+    let out = tmp.join("bin");
+    let status = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .args(["build", src.to_str().unwrap(), "-o"])
+        .arg(&out)
+        .status()
+        .expect("ail build failed to run");
+    assert!(status.success(), "ail build failed for cmp_max_smoke");
+    let output = Command::new(&out).output().expect("run cmp_max_smoke binary");
+    assert!(output.status.success(), "binary exited non-zero");
+    let stdout = String::from_utf8(output.stdout).expect("stdout utf8");
+    assert_eq!(stdout.trim(), "7", "cmp_max(3, 7) at Int prints 7");
+}
+
+#[test]
+fn workspace_with_only_poly_free_fn_and_no_classes_still_monomorphises() {
+    // poly_id has a Type::Forall free fn and NO class/instance defs
+    // in the user module. The prelude (auto-injected) has classes,
+    // but for early-out purposes we test the user-module gate.
+    // Today the workspace-has-typeclasses early-out checks the
+    // WHOLE workspace including the prelude, so it actually fires
+    // on every user workspace. The Task-7 generalisation widens
+    // the predicate to also include `Def::Fn` with `Type::Forall`
+    // as a specialisable target — which makes the predicate true
+    // for any workspace with poly free fns (regardless of classes).
+    let ws = load_workspace(&fixture("poly_id.ail.json")).expect("workspace loads");
+    let diags = ailang_check::check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
+    let post_mono = ailang_check::monomorphise_workspace(&ws).expect("mono green");
+
+    // After the unified pass, the workspace contains synthesised
+    // mono fn defs for `id` at Int and at Bool — both invoked from
+    // `main`.
+    let names: Vec<String> = post_mono.modules.values()
+        .flat_map(|m| m.defs.iter().filter_map(|d| {
+            if let Def::Fn(f) = d { Some(f.name.clone()) } else { None }
+        }))
+        .collect();
+    assert!(names.iter().any(|n| n == "id__Int"),
+        "poly_id must produce id__Int via unified mono; got {names:?}");
+    assert!(names.iter().any(|n| n == "id__Bool"),
+        "poly_id must produce id__Bool via unified mono; got {names:?}");
+}
+
+#[test]
+fn rewrite_mono_calls_rewrites_bare_poly_free_fn_to_mono_symbol() {
+    let ws = load_workspace(&fixture("cmp_max_smoke.ail.json")).expect("workspace loads");
+    let diags = ailang_check::check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
+    let post_mono = ailang_check::monomorphise_workspace(&ws).expect("mono green");
+
+    let main_mod = post_mono.modules.get("cmp_max_smoke").expect("main module");
+    let main_fn = main_mod.defs.iter().find_map(|d| {
+        if let Def::Fn(f) = d { (f.name == "main").then_some(f) } else { None }
+    }).expect("main fn");
+
+    let body_str = format!("{:?}", main_fn.body);
+    assert!(
+        body_str.contains("cmp_max__Int"),
+        "main body must call cmp_max__Int after rewrite; got: {body_str}"
+    );
+    // The bare-name `cmp_max` (as a Term::Var.name) must NOT appear
+    // anywhere in main's body post-rewrite.
+    assert!(
+        !body_str.contains("Var { name: \"cmp_max\""),
+        "main body must NOT still call bare cmp_max after rewrite; got: {body_str}"
+    );
+}
+
+#[test]
+fn synthesise_mono_fn_free_fn_arm_substitutes_rigid_vars() {
+    use ailang_check::mono::synthesise_mono_fn_for_free_fn;
+    let ws = load_workspace(&fixture("cmp_max_smoke.ail.json")).expect("workspace loads");
+    let diags = ailang_check::check_workspace(&ws);
+    assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
+
+    let int_ty = Type::Con { name: "Int".into(), args: vec![] };
+    let target = MonoTarget::FreeFn {
+        name: "cmp_max".into(),
+        type_args: vec![int_ty.clone()],
+        defining_module: "cmp_max_smoke".into(),
+    };
+    let synth = synthesise_mono_fn_for_free_fn(&target, &ws)
+        .expect("synthesis succeeds");
+
+    assert_eq!(synth.name, "cmp_max__Int");
+    // Body must still reference `compare` (pre-rewrite); Task 6
+    // rewrites it to `compare__Int` during the walker pass.
+    let body_str = format!("{:?}", synth.body);
+    assert!(body_str.contains("compare"), "body still references compare bare-name pre-rewrite: {body_str}");
+    // Param types must be Int after rigid substitution.
+    assert!(matches!(
+        &synth.ty,
+        Type::Fn { params, ret, .. }
+            if params.len() == 2
+            && matches!(&params[0], Type::Con { name, args } if name == "Int" && args.is_empty())
+            && matches!(&params[1], Type::Con { name, args } if name == "Int" && args.is_empty())
+            && matches!(ret.as_ref(), Type::Con { name, args } if name == "Int" && args.is_empty())
+    ), "synth.ty = {:?}", synth.ty);
+}
+
+#[test]
+fn mono_target_free_fn_variant_keys_distinctly_from_class_method() {
+    let int_ty = Type::Con { name: "Int".into(), args: vec![] };
+    let class_tgt = MonoTarget::ClassMethod {
+        class: "Eq".into(),
+        method: "eq".into(),
+        type_: int_ty.clone(),
+        defining_module: "prelude".into(),
+    };
+    let free_tgt = MonoTarget::FreeFn {
+        name: "cmp_max".into(),
+        type_args: vec![int_ty.clone()],
+        defining_module: "prelude".into(),
+    };
+    assert_ne!(
+        mono_target_key(&class_tgt),
+        mono_target_key(&free_tgt),
+        "class-method and free-fn targets must have distinct dedup keys"
+    );
+}

crates/ail/tests/typeclass_22b3.rs

@@ -146,14 +146,19 @@ fn collect_mono_targets_single_concrete_call_site() {
 
     assert_eq!(targets.len(), 1, "one target expected: {:?}", targets);
     let t = &targets[0];
-    assert_eq!(t.class, "Show");
-    assert_eq!(t.method, "show");
-    assert!(
-        matches!(&t.type_, ailang_core::ast::Type::Con { name, args } if name == "Int" && args.is_empty()),
-        "type must be Int, got {:?}",
-        t.type_
-    );
-    assert_eq!(t.defining_module, "test_22b2_instance_present");
+    match t {
+        ailang_check::mono::MonoTarget::ClassMethod { class, method, type_, defining_module } => {
+            assert_eq!(class, "Show");
+            assert_eq!(method, "show");
+            assert!(
+                matches!(type_, ailang_core::ast::Type::Con { name, args } if name == "Int" && args.is_empty()),
+                "type must be Int, got {:?}",
+                type_
+            );
+            assert_eq!(defining_module, "test_22b2_instance_present");
+        }
+        other => panic!("expected ClassMethod target, got {other:?}"),
+    }
 }
 
 #[test]
@@ -223,7 +228,7 @@ fn synthesise_mono_fn_uses_instance_body_lam() {
         }],
         doc: None,
     };
-    let target = MonoTarget {
+    let target = MonoTarget::ClassMethod {
         class: "Foo".into(),
         method: "bar".into(),
         type_: Type::int(),
@@ -292,7 +297,7 @@ fn synthesise_mono_fn_falls_back_to_class_default() {
         methods: vec![],
         doc: None,
     };
-    let target = MonoTarget {
+    let target = MonoTarget::ClassMethod {
         class: "Greet".into(),
         method: "hello".into(),
         type_: Type::int(),
@@ -344,7 +349,7 @@ fn synthesise_mono_fn_zero_arg_method_uses_body_verbatim() {
         }],
         doc: None,
     };
-    let target = MonoTarget {
+    let target = MonoTarget::ClassMethod {
         class: "Foo".into(),
         method: "bar".into(),
         type_: Type::int(),

crates/ailang-check/src/builtins.rs

@@ -328,6 +328,7 @@ mod tests {
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
         let mut residuals = Vec::new();
+        let mut free_fn_calls = Vec::new();
         let ty = crate::synth(
             t,
             &env,
@@ -337,6 +338,7 @@ mod tests {
             &mut subst,
             &mut counter,
             &mut residuals,
+            &mut free_fn_calls,
         )
         .expect("synth");
         subst.apply(&ty)
@@ -493,6 +495,7 @@ mod tests {
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
         let mut residuals = Vec::new();
+        let mut free_fn_calls = Vec::new();
         let ret = crate::synth(
             &do_term,
             &env,
@@ -502,6 +505,7 @@ mod tests {
             &mut subst,
             &mut counter,
             &mut residuals,
+            &mut free_fn_calls,
         )
         .expect("synth");
         let ret = subst.apply(&ret);
@@ -538,6 +542,7 @@ mod tests {
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
         let mut residuals = Vec::new();
+        let mut free_fn_calls = Vec::new();
         let err = crate::synth(
             &term,
             &env,
@@ -547,6 +552,7 @@ mod tests {
             &mut subst,
             &mut counter,
             &mut residuals,
+            &mut free_fn_calls,
         )
         .expect_err("must reject");
         assert!(

crates/ailang-check/src/lib.rs

@@ -154,6 +154,88 @@ pub(crate) fn substitute_rigids(t: &Type, mapping: &BTreeMap<String, Type>) -> T
     }
 }
 
+/// Iter 23.4: substitute named rigid vars throughout a `Term`,
+/// recursing into every sub-Term and applying [`substitute_rigids`]
+/// to every embedded `Type` (in `Term::Lam.param_tys`,
+/// `Term::Lam.ret_ty`). All other Term variants carry no inline
+/// types and recurse structurally.
+///
+/// Used by `mono::synthesise_mono_fn_for_free_fn` to specialise a
+/// polymorphic free-fn body for a specific instantiation. The
+/// class-method arm doesn't need this — instance bodies are
+/// Lam-unwrapped during synthesis, dropping their `param_tys` —
+/// but a free-fn body may carry arbitrary nested Lams whose
+/// `param_tys` reference the outer Forall vars.
+pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Type>) -> Term {
+    use ailang_core::ast::Arm;
+    match t {
+        Term::Lit { .. } | Term::Var { .. } => t.clone(),
+        Term::App { callee, args, tail } => Term::App {
+            callee: Box::new(substitute_rigids_in_term(callee, mapping)),
+            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
+            tail: *tail,
+        },
+        Term::Let { name, value, body } => Term::Let {
+            name: name.clone(),
+            value: Box::new(substitute_rigids_in_term(value, mapping)),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+        Term::LetRec { name, ty, params, body, in_term } => Term::LetRec {
+            name: name.clone(),
+            ty: substitute_rigids(ty, mapping),
+            params: params.clone(),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+            in_term: Box::new(substitute_rigids_in_term(in_term, mapping)),
+        },
+        Term::If { cond, then, else_ } => Term::If {
+            cond: Box::new(substitute_rigids_in_term(cond, mapping)),
+            then: Box::new(substitute_rigids_in_term(then, mapping)),
+            else_: Box::new(substitute_rigids_in_term(else_, mapping)),
+        },
+        Term::Do { op, args, tail } => Term::Do {
+            op: op.clone(),
+            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
+            tail: *tail,
+        },
+        Term::Ctor { type_name, ctor, args } => Term::Ctor {
+            type_name: type_name.clone(),
+            ctor: ctor.clone(),
+            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
+        },
+        Term::Match { scrutinee, arms } => Term::Match {
+            scrutinee: Box::new(substitute_rigids_in_term(scrutinee, mapping)),
+            arms: arms
+                .iter()
+                .map(|a| Arm {
+                    pat: a.pat.clone(),
+                    body: substitute_rigids_in_term(&a.body, mapping),
+                })
+                .collect(),
+        },
+        Term::Lam { params, param_tys, ret_ty, effects, body } => Term::Lam {
+            params: params.clone(),
+            param_tys: param_tys
+                .iter()
+                .map(|t| substitute_rigids(t, mapping))
+                .collect(),
+            ret_ty: Box::new(substitute_rigids(ret_ty, mapping)),
+            effects: effects.clone(),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+        Term::Seq { lhs, rhs } => Term::Seq {
+            lhs: Box::new(substitute_rigids_in_term(lhs, mapping)),
+            rhs: Box::new(substitute_rigids_in_term(rhs, mapping)),
+        },
+        Term::Clone { value } => Term::Clone {
+            value: Box::new(substitute_rigids_in_term(value, mapping)),
+        },
+        Term::ReuseAs { source, body } => Term::ReuseAs {
+            source: Box::new(substitute_rigids_in_term(source, mapping)),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+    }
+}
+
 /// Returns true if metavar `id` occurs in `t` (after applying the
 /// current substitution). Used as the occurs check during unification.
 fn occurs(id: u32, t: &Type, subst: &Subst) -> bool {
@@ -1459,7 +1541,8 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
     // inside the body pushes a [`ResidualConstraint`] here; after the
     // body finishes, we compare against the expanded declared set.
     let mut residuals: Vec<ResidualConstraint> = Vec::new();
-    let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals)?;
+    let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+    let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls)?;
     unify(&ret_ty, &body_ty, &mut subst)?;
 
     // Iter 14e: tail-position verification (Decision 8). Runs after
@@ -1575,6 +1658,37 @@ pub(crate) struct ResidualConstraint {
     pub method: String,
 }
 
+/// Iter 23.4: per-call-site polymorphic-free-fn observation recorded by
+/// [`synth`] when a `Term::Var` resolves to a `Type::Forall`-quantified
+/// top-level def (NOT a class method — those are pushed to
+/// [`ResidualConstraint`] instead). Carries the bare name, the owning
+/// module (resolved through the same lookup ladder as `synth`'s Var arm),
+/// the polymorphic source's `Forall.vars` (declaration order), and the
+/// fresh metavars instantiated for those vars at the call site.
+///
+/// Consumed by the mono pass: after `synth` completes a body, each
+/// `metas[i]` is `subst.apply`'d to recover the concrete type at vars[i].
+/// Fully-concrete observations become [`crate::mono::MonoTarget::FreeFn`]
+/// targets; non-concrete observations are silently dropped (covered by
+/// the missing-constraint check on residuals if relevant).
+#[derive(Debug, Clone)]
+pub struct FreeFnCall {
+    /// Bare name of the polymorphic def at the call site.
+    pub name: String,
+    /// Module in which the polymorphic `Def::Fn` is declared, resolved
+    /// through `synth`'s lookup ladder (current module's globals,
+    /// implicitly-imported module's globals, or the dot-qualified
+    /// `prefix.name` path's target module).
+    pub owner_module: String,
+    /// The `Forall.vars` of the source def (declaration order).
+    pub forall_vars: Vec<String>,
+    /// Fresh metavars instantiated at this call site — same length as
+    /// `forall_vars`, same order. Post-`synth`, `subst.apply(&metas[i])`
+    /// yields the concrete type for `forall_vars[i]` iff the call site's
+    /// substitution was fully pinned.
+    pub metas: Vec<Type>,
+}
+
 /// Iter 22b.2 (Task 9): expand a list of declared class constraints
 /// with their one-step superclass closure (Decision 11). For every
 /// declared `(C, t)`, append `(S, t)` if class `C` has a superclass
@@ -1731,7 +1845,8 @@ fn check_const(c: &ConstDef, env: &Env) -> Result<()> {
     // Task 10's no-instance arm will pick those up. We thread an
     // accumulator only to keep `synth`'s signature uniform.
     let mut residuals: Vec<ResidualConstraint> = Vec::new();
-    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals)?;
+    let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls)?;
     unify(&c.ty, &v, &mut subst)?;
     if !effects.is_empty() {
         return Err(CheckError::ConstHasEffects(
@@ -1751,6 +1866,7 @@ pub(crate) fn synth(
     subst: &mut Subst,
     counter: &mut u32,
     residuals: &mut Vec<ResidualConstraint>,
+    free_fn_calls: &mut Vec<FreeFnCall>,
 ) -> Result<Type> {
     match t {
         Term::Lit { lit } => Ok(match lit {
@@ -1773,10 +1889,38 @@ pub(crate) fn synth(
             // class param with a fresh metavar and record a residual
             // class constraint — `check_fn` later compares the residual
             // set against the declared `Forall.constraints`.
-            let raw = if let Some(t) = locals.get(name) {
-                t.clone()
+            // Iter 23.4: alongside the bare type, capture
+            //   (owner_module, unqualified_name_in_owner_module)
+            // for any non-local resolution that lands on a
+            // `Type::Forall` AND is a real workspace-declared
+            // `Def::Fn` (NOT a builtin operator like `==`). The
+            // discriminator is whether the name appears in
+            // `env.module_globals[<owner>]` — builtins are installed
+            // into `env.globals` only. The unqualified-name capture
+            // matters for dot-qualified call sites: the FreeFnCall
+            // records the suffix (e.g. `length`), not the full
+            // `std_list.length`, so `synthesise_mono_fn_for_free_fn`
+            // can look up the source def by its bare name in the
+            // owner module's def list.
+            //
+            // After the resolution ladder, if `raw` is a `Type::Forall`
+            // AND a `free_fn_owner` is known, push a `FreeFnCall`
+            // observation; the mono pass `subst.apply`s the metas
+            // post-synth to recover concrete type-args at each
+            // polymorphic free-fn call site.
+            let (raw, free_fn_owner): (Type, Option<(String, String)>) = if let Some(t) = locals.get(name) {
+                (t.clone(), None)
             } else if let Some(t) = env.globals.get(name) {
-                t.clone()
+                // Same-module global. Owner is the current module IFF
+                // the name is in this module's declared globals
+                // (i.e. it's a `Def::Fn`, not a builtin). The bare
+                // `name` works as the in-module key.
+                let owner = env
+                    .module_globals
+                    .get(&env.current_module)
+                    .filter(|m| m.contains_key(name))
+                    .map(|_| (env.current_module.clone(), name.clone()));
+                (t.clone(), owner)
             } else if let Some(cm) = env.class_methods.get(name) {
                 // Iter 22b.2 (Task 9): instantiate the class param with
                 // a fresh metavar; the body's unification at the call
@@ -1833,7 +1977,10 @@ pub(crate) fn synth(
                     .get(&owner_module)
                     .cloned()
                     .unwrap_or_default();
-                qualify_local_types(&raw_ty, &owner_module, &owner_types)
+                let qualified = qualify_local_types(&raw_ty, &owner_module, &owner_types);
+                // Bare name resolves through implicit import; the
+                // unqualified name in the owner module is the same `name`.
+                (qualified, Some((owner_module, name.clone())))
             } else if name.matches('.').count() == 1 {
                 let (prefix, suffix) = name.split_once('.').expect("checked");
                 let target_module = match env.imports.get(prefix) {
@@ -1865,14 +2012,39 @@ pub(crate) fn synth(
                     .get(&target_module)
                     .cloned()
                     .unwrap_or_default();
-                qualify_local_types(&raw_ty, &target_module, &owner_types)
+                let qualified = qualify_local_types(&raw_ty, &target_module, &owner_types);
+                // Dot-qualified `prefix.suffix`: the unqualified name in
+                // the owner module is `suffix`.
+                (qualified, Some((target_module, suffix.to_string())))
             } else {
                 return Err(CheckError::UnknownIdent(name.clone()));
             };
+            // Iter 23.4: if raw is `Type::Forall` AND we know the
+            // owner module (i.e. the resolution went through a non-
+            // local branch), record a FreeFnCall observation BEFORE
+            // instantiating. The metas are the fresh metavars we
+            // about to use; the mono pass `subst.apply`s them later.
+            // Note: `unqualified_name` is the name as seen inside the
+            // owner module (so the mono pass can find the `Def::Fn`
+            // by bare name); the source-level `name` may be a
+            // dot-qualified form (`prefix.suffix`) the synth started
+            // with.
+            if let (Type::Forall { vars, constraints: _, body }, Some((owner, unqualified_name))) =
+                (&raw, &free_fn_owner)
+            {
+                let (metas, inst) = instantiate(vars, body, counter);
+                free_fn_calls.push(FreeFnCall {
+                    name: unqualified_name.clone(),
+                    owner_module: owner.clone(),
+                    forall_vars: vars.clone(),
+                    metas: metas.clone(),
+                });
+                return Ok(inst);
+            }
             Ok(maybe_instantiate(raw, counter))
         }
         Term::App { callee, args, .. } => {
-            let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals)?;
+            let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             let cty = subst.apply(&cty);
             let (params, ret, fx) = match &cty {
                 Type::Fn { params, ret, effects: fx, .. } => {
@@ -1908,7 +2080,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
                 unify(exp, &actual, subst)?;
             }
             for e in fx {
@@ -1917,9 +2089,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&ret))
         }
         Term::Let { name, value, body } => {
-            let v = synth(value, env, locals, effects, in_def, subst, counter, residuals)?;
+            let v = synth(value, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             let prev = locals.insert(name.clone(), v);
-            let r = synth(body, env, locals, effects, in_def, subst, counter, residuals)?;
+            let r = synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             match prev {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -1931,10 +2103,10 @@ pub(crate) fn synth(
             Ok(r)
         }
         Term::If { cond, then, else_ } => {
-            let c = synth(cond, env, locals, effects, in_def, subst, counter, residuals)?;
+            let c = synth(cond, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             unify(&Type::bool_(), &c, subst)?;
-            let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals)?;
-            let t2 = synth(else_, env, locals, effects, in_def, subst, counter, residuals)?;
+            let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
+            let t2 = synth(else_, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             unify(&t1, &t2, subst)?;
             Ok(subst.apply(&t1))
         }
@@ -1952,7 +2124,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(sig.params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
                 unify(exp, &actual, subst)?;
             }
             effects.insert(sig.effect.clone());
@@ -2047,7 +2219,7 @@ pub(crate) fn synth(
             }
             for (a, exp) in args.iter().zip(qualified_fields.iter()) {
                 let exp_inst = substitute_rigids(exp, &mapping);
-                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
                 unify(&exp_inst, &actual, subst)?;
             }
             Ok(Type::Con {
@@ -2056,7 +2228,7 @@ pub(crate) fn synth(
             })
         }
         Term::Match { scrutinee, arms } => {
-            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter, residuals)?;
+            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             if arms.is_empty() {
                 return Err(CheckError::NonExhaustive {
                     ty: ailang_core::pretty::type_to_string(&s_ty),
@@ -2074,7 +2246,7 @@ pub(crate) fn synth(
                     let prev = locals.insert(n.clone(), t.clone());
                     pushed.push((n.clone(), prev));
                 }
-                let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter, residuals)?;
+                let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
                 for (n, prev) in pushed.into_iter().rev() {
                     match prev {
                         Some(p) => {
@@ -2149,9 +2321,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
         }
         Term::Seq { lhs, rhs } => {
-            let lty = synth(lhs, env, locals, effects, in_def, subst, counter, residuals)?;
+            let lty = synth(lhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             unify(&Type::unit(), &lty, subst)?;
-            synth(rhs, env, locals, effects, in_def, subst, counter, residuals)
+            synth(rhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)
         }
         Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
             let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
@@ -2160,7 +2332,7 @@ pub(crate) fn synth(
                 pushed.push((n.clone(), prev));
             }
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals);
+            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls);
             for (n, prev) in pushed.into_iter().rev() {
                 match prev {
                     Some(p) => {
@@ -2248,7 +2420,7 @@ pub(crate) fn synth(
             // subset rule against `declared_effs` — exactly like
             // `Term::Lam`.
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals);
+            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls);
 
             // Restore body-scope locals (params + name).
             for (n, prev) in pushed.into_iter().rev() {
@@ -2275,7 +2447,7 @@ pub(crate) fn synth(
             // scope (params are not visible here; only the recursive
             // binding is).
             let prev_in = locals.insert(name.clone(), ty.clone());
-            let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter, residuals);
+            let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls);
             match prev_in {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -2291,7 +2463,7 @@ pub(crate) fn synth(
             // No constraint generated, no environment change. The
             // wrapper records author intent for the future RC inc/dec
             // emission pass (18c.3); typing is pure passthrough.
-            synth(value, env, locals, effects, in_def, subst, counter, residuals)
+            synth(value, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)
         }
         Term::ReuseAs { source, body } => {
             // Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to
@@ -2305,7 +2477,7 @@ pub(crate) fn synth(
             // shape-compatibility check (18d.2 will add a
             // `reuse-as-shape-mismatch` diagnostic when codegen has
             // the actual size info).
-            let _ = synth(source, env, locals, effects, in_def, subst, counter, residuals)?;
+            let _ = synth(source, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
             match body.as_ref() {
                 Term::Ctor { .. } | Term::Lam { .. } => {}
                 other => {
@@ -2331,7 +2503,7 @@ pub(crate) fn synth(
             }
             // Body's type is the result type of the whole reuse-as
             // expression.
-            synth(body, env, locals, effects, in_def, subst, counter, residuals)
+            synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)
         }
     }
 }

crates/ailang-check/src/lift.rs

@@ -691,7 +691,10 @@ impl<'a> Lifter<'a> {
         // fn during `check_fn`. Threading the accumulator only keeps
         // `synth`'s signature uniform.
         let mut residuals: Vec<crate::ResidualConstraint> = Vec::new();
-        let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter, &mut residuals)?;
+        // Iter 23.4: free-fn-call observations are similarly discarded
+        // here — the mono pass will re-synth bodies post-lift.
+        let mut free_fn_calls: Vec<crate::FreeFnCall> = Vec::new();
+        let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls)?;
         Ok(subst.apply(&ty))
     }
 }

crates/ailang-codegen/src/lib.rs

@@ -49,7 +49,7 @@ mod synth;
 
 use escape::NonEscapeSet;
 use subst::{
-    apply_subst_to_term, apply_subst_to_type, derive_substitution, descriptor_for_subst,
+    apply_subst_to_type, derive_substitution,
     qualify_local_types_codegen, unify_for_subst,
 };
 use synth::{
@@ -285,16 +285,16 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String>
 
     // Pass 1: per-module top-level symbol tables.
     // - `module_user_fns`: LLVM-typed FnSig for monomorphic fns. Used by
-    //   the call resolver. Polymorphic fns are deliberately excluded —
-    //   they don't have a single LLVM signature; specialised entries
-    //   appear here on demand during monomorphisation (Iter 12b).
-    // - `module_def_ail_types`: AILang `Type` for every fn-typed def
-    //   (poly or mono). Used by the codegen-side type tracker to derive
-    //   substitutions at polymorphic call sites and to look up the
-    //   original `Forall` body when specialising.
+    //   the call resolver. Post-iter-23.4 the workspace contains ONLY
+    //   monomorphic `Def::Fn`s (the typecheck-time mono pass synthesises
+    //   one per concrete instantiation); any residual `Type::Forall` ty
+    //   is a stale source def kept for round-trip / `ail diff` purposes
+    //   and is intentionally not lowered.
+    // - `module_def_ail_types`: AILang `Type` for every fn-typed def.
+    //   Retained for codegen-side type-tracking utilities (e.g.
+    //   `synth_arg_type` for ctor-arg type inference).
     let mut module_user_fns: BTreeMap<String, BTreeMap<String, FnSig>> = BTreeMap::new();
     let mut module_def_ail_types: BTreeMap<String, BTreeMap<String, Type>> = BTreeMap::new();
-    let mut module_polymorphic_fns: BTreeMap<String, BTreeMap<String, FnDef>> = BTreeMap::new();
     // Iter 15a: cross-module ctor table. Maps module name → ctor name →
     // CtorRef (with `type_name` *unqualified*, since the ctor is defined
     // in that module). Cross-module ctor lookups resolve through this
@@ -309,26 +309,20 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String>
     for (mname, m) in &ws.modules {
         let mut user_fns = BTreeMap::new();
         let mut ail_types = BTreeMap::new();
-        let mut poly_fns = BTreeMap::new();
         let mut ctors = BTreeMap::new();
         for def in &m.defs {
             if let Def::Fn(f) = def {
                 ail_types.insert(f.name.clone(), f.ty.clone());
-                match &f.ty {
-                    Type::Fn { params, ret, .. } => {
-                        let psig: Result<Vec<String>> = params.iter().map(llvm_type).collect();
-                        let rsig = llvm_type(ret);
-                        if let (Ok(params), Ok(ret)) = (psig, rsig) {
-                            user_fns.insert(f.name.clone(), FnSig { params, ret });
-                        }
+                if let Type::Fn { params, ret, .. } = &f.ty {
+                    let psig: Result<Vec<String>> = params.iter().map(llvm_type).collect();
+                    let rsig = llvm_type(ret);
+                    if let (Ok(params), Ok(ret)) = (psig, rsig) {
+                        user_fns.insert(f.name.clone(), FnSig { params, ret });
                     }
-                    Type::Forall { .. } => {
-                        // Polymorphic def — no LLVM sig now; specialised
-                        // versions get queued as call sites are lowered.
-                        poly_fns.insert(f.name.clone(), f.clone());
-                    }
-                    _ => {}
                 }
+                // iter 23.4: `Type::Forall`-quantified defs are
+                // intentionally skipped — the mono pass has already
+                // produced their monomorphic counterparts.
             }
             if let Def::Type(td) = def {
                 for (i, c) in td.ctors.iter().enumerate() {
@@ -360,7 +354,6 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String>
         }
         module_user_fns.insert(mname.clone(), user_fns);
         module_def_ail_types.insert(mname.clone(), ail_types);
-        module_polymorphic_fns.insert(mname.clone(), poly_fns);
         module_ctor_index.insert(mname.clone(), ctors);
         module_consts.insert(mname.clone(), consts);
     }
@@ -396,7 +389,6 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String>
             mname,
             &module_user_fns,
             &module_def_ail_types,
-            &module_polymorphic_fns,
             &module_ctor_index,
             &module_consts,
             import_map,
@@ -555,15 +547,6 @@ struct Emitter<'a> {
     /// `Forall` for polymorphic defs (used to derive substitutions at
     /// monomorphic call sites). Populated in pass 1 of `lower_workspace`.
     module_def_ail_types: &'a BTreeMap<String, BTreeMap<String, Type>>,
-    /// Polymorphic defs per module — full FnDef so we can specialise
-    /// the body when monomorphising. Mono fns aren't included.
-    module_polymorphic_fns: &'a BTreeMap<String, BTreeMap<String, FnDef>>,
-    /// Iter 12b: queue of (module, def, substitution) tuples that need
-    /// to be emitted as specialised versions of polymorphic defs.
-    /// `mono_emitted` tracks the same keys to deduplicate. The descriptor
-    /// string is the deterministic name suffix (`Int`, `Int_Bool`, ...).
-    mono_queue: Vec<(String, String, BTreeMap<String, Type>, String)>,
-    mono_emitted: BTreeSet<(String, String, String)>, // (module, def, descriptor)
     /// Import map of the current module (alias/module name → actual module name).
     import_map: BTreeMap<String, String>,
     /// ADT table: type_name -> list of ctors in definition order.
@@ -723,7 +706,6 @@ impl<'a> Emitter<'a> {
         module_name: &'a str,
         module_user_fns: &'a BTreeMap<String, BTreeMap<String, FnSig>>,
         module_def_ail_types: &'a BTreeMap<String, BTreeMap<String, Type>>,
-        module_polymorphic_fns: &'a BTreeMap<String, BTreeMap<String, FnDef>>,
         module_ctor_index: &'a BTreeMap<String, BTreeMap<String, CtorRef>>,
         module_consts: &'a BTreeMap<String, BTreeMap<String, ConstDef>>,
         import_map: BTreeMap<String, String>,
@@ -774,9 +756,6 @@ impl<'a> Emitter<'a> {
             str_counter: 0,
             module_user_fns,
             module_def_ail_types,
-            module_polymorphic_fns,
-            mono_queue: Vec::new(),
-            mono_emitted: BTreeSet::new(),
             import_map,
             types,
             module_ctor_index,
@@ -836,18 +815,13 @@ impl<'a> Emitter<'a> {
                 Def::Class(_) | Def::Instance(_) => {}
             }
         }
-        // Drain the monomorphisation queue. Specialised fns may
-        // themselves invoke polymorphic defs and queue further entries,
-        // so iterate until empty.
-        while let Some((owner_module, def_name, subst, descriptor)) = self.mono_queue.pop() {
-            self.emit_specialised_fn(&owner_module, &def_name, &subst, &descriptor)
-                .map_err(|e| {
-                    CodegenError::Def(
-                        format!("{def_name}__{descriptor}"),
-                        Box::new(e),
-                    )
-                })?;
-        }
+        // iter 23.4: the monomorphisation queue is gone — the
+        // typecheck-time mono pass synthesises every specialised
+        // `Def::Fn` before codegen runs (see
+        // `ailang_check::mono::monomorphise_workspace`). Codegen
+        // sees only monomorphic defs; the drain loop and
+        // `emit_specialised_fn` have been removed.
+
         // Iter 18c.4: per-ADT drop functions. Emitted only under
         // `--alloc=rc`. One `void @drop_<module>_<TypeName>(ptr)` per
         // `Def::Type` in the current module — the call site for
@@ -890,65 +864,6 @@ impl<'a> Emitter<'a> {
     /// calls `emit_fn` against a synthetic FnDef whose `name` already
     /// contains the descriptor — the existing mangling concatenates
     /// `ail_<module>_<name>` and produces the desired symbol.
-    fn emit_specialised_fn(
-        &mut self,
-        owner_module: &str,
-        def_name: &str,
-        subst: &BTreeMap<String, Type>,
-        descriptor: &str,
-    ) -> Result<()> {
-        let fdef = self
-            .module_polymorphic_fns
-            .get(owner_module)
-            .and_then(|m| m.get(def_name))
-            .cloned()
-            .ok_or_else(|| {
-                CodegenError::Internal(format!(
-                    "emit_specialised_fn: `{owner_module}.{def_name}` not registered"
-                ))
-            })?;
-        let inner_ty = match &fdef.ty {
-            Type::Forall { body, .. } => (**body).clone(),
-            other => other.clone(),
-        };
-        let mono_ty = apply_subst_to_type(&inner_ty, subst);
-        let mono_body = apply_subst_to_term(&fdef.body, subst);
-        let synthetic = FnDef {
-            name: format!("{def_name}__{descriptor}"),
-            ty: mono_ty,
-            params: fdef.params.clone(),
-            body: mono_body,
-            suppress: vec![],
-            doc: fdef.doc.clone(),
-        };
-        // Specialised def belongs to the polymorphic def's owner
-        // module, not necessarily self.module_name. Swap module_name
-        // briefly so mangling stays correct.
-        let saved_module = self.module_name;
-        // SAFETY: we rebind module_name through a raw pointer cast
-        // because the field is `&'a str`. Equivalent: hand
-        // emit_fn the mangling target via a parameter. Simpler to
-        // restore.
-        // Instead of unsafe, we just call emit_fn directly — the
-        // mangling uses self.module_name which is &'a str but the
-        // owner_module string lives inside self.module_polymorphic_fns,
-        // also borrowed for 'a, so we can re-borrow it.
-        let owner_ref: &'a str = self
-            .module_polymorphic_fns
-            .keys()
-            .find(|k| k.as_str() == owner_module)
-            .map(|s| s.as_str())
-            .ok_or_else(|| {
-                CodegenError::Internal(format!(
-                    "owner module `{owner_module}` not in module_polymorphic_fns"
-                ))
-            })?;
-        self.module_name = owner_ref;
-        let r = self.emit_fn(&synthetic);
-        self.module_name = saved_module;
-        r
-    }
-
     fn emit_const(&mut self, c: &ConstDef) -> Result<()> {
         // Iter 15b: non-literal const values (e.g. ctor expressions) are
         // not emitted as globals. They are inlined at every `Term::Var`
@@ -1935,14 +1850,12 @@ impl<'a> Emitter<'a> {
                     "cross-module call `{name}`: prefix `{prefix}` not in import map"
                 ))
             })?;
-            // Polymorphic def in target module? Monomorphise on demand.
-            if self
-                .module_polymorphic_fns
-                .get(&target_module)
-                .is_some_and(|m| m.contains_key(suffix))
-            {
-                return self.lower_polymorphic_call(&target_module, suffix, args, tail);
-            }
+            // iter 23.4: codegen-time poly-call dispatch removed. Post-mono
+            // every poly call site has been rewritten by `rewrite_mono_calls`
+            // to a monomorphic symbol, so the lookup-ladder below sees only
+            // user fns / consts / builtins. The pre-iter-23.4 path checked
+            // `module_polymorphic_fns` and dispatched to `lower_polymorphic_call`;
+            // both are gone (and the supporting Emitter fields with them).
             let target_fns = self
                 .module_user_fns
                 .get(&target_module)
@@ -1962,15 +1875,7 @@ impl<'a> Emitter<'a> {
             return self.emit_call(&target_module, suffix, &sig, args, tail);
         }
 
-        // Polymorphic def in the current module?
-        if self
-            .module_polymorphic_fns
-            .get(self.module_name)
-            .is_some_and(|m| m.contains_key(name))
-        {
-            let owner = self.module_name.to_string();
-            return self.lower_polymorphic_call(&owner, name, args, tail);
-        }
+        // iter 23.4: codegen-time poly-call dispatch removed (see above).
 
         // User function in the current module?
         if let Some(sig) = self
@@ -1987,122 +1892,6 @@ impl<'a> Emitter<'a> {
         )))
     }
 
-    /// Iter 12b: lower a direct call to a polymorphic def. Derives the
-    /// substitution from the actual arg types, queues the (def,
-    /// substitution) pair for specialisation if not yet emitted, and
-    /// emits a direct call to the mangled name `@ail_<m>_<def>__<descr>`.
-    fn lower_polymorphic_call(
-        &mut self,
-        owner_module: &str,
-        def_name: &str,
-        args: &[Term],
-        tail: bool,
-    ) -> Result<(String, String)> {
-        let fdef = self
-            .module_polymorphic_fns
-            .get(owner_module)
-            .and_then(|m| m.get(def_name))
-            .cloned()
-            .ok_or_else(|| {
-                CodegenError::Internal(format!(
-                    "lower_polymorphic_call: `{owner_module}.{def_name}` not registered"
-                ))
-            })?;
-        let (forall_vars, params, ret) = match &fdef.ty {
-            Type::Forall { vars, constraints: _, body } => match body.as_ref() {
-                Type::Fn { params, ret, .. } => {
-                    (vars.clone(), params.clone(), (**ret).clone())
-                }
-                _ => {
-                    return Err(CodegenError::Internal(format!(
-                        "lower_polymorphic_call: `{def_name}` Forall body is not Fn"
-                    )));
-                }
-            },
-            _ => {
-                return Err(CodegenError::Internal(format!(
-                    "lower_polymorphic_call: `{def_name}` is not polymorphic"
-                )));
-            }
-        };
-        // Iter 15a: when we're calling into another module, the fn's
-        // params and ret reference local type names that — from this
-        // call site's perspective — are qualified `module.T`. Qualify
-        // before deriving the substitution so the unification mirrors
-        // what the typechecker has already validated.
-        let (params, ret) = if owner_module != self.module_name {
-            let owner_types = self.collect_owner_local_types(owner_module);
-            (
-                params
-                    .iter()
-                    .map(|p| qualify_local_types_codegen(p, owner_module, &owner_types))
-                    .collect::<Vec<_>>(),
-                qualify_local_types_codegen(&ret, owner_module, &owner_types),
-            )
-        } else {
-            (params, ret)
-        };
-
-        // Derive the substitution by comparing the declared param
-        // types against the actual arg types.
-        let arg_ail_tys: Vec<Type> = args
-            .iter()
-            .map(|a| self.synth_arg_type(a))
-            .collect::<Result<_>>()?;
-        let subst = derive_substitution(&forall_vars, &params, &arg_ail_tys)?;
-
-        // Specialised types and signature.
-        let mono_params: Vec<Type> = params
-            .iter()
-            .map(|p| apply_subst_to_type(p, &subst))
-            .collect();
-        let mono_ret = apply_subst_to_type(&ret, &subst);
-        let llvm_params: Vec<String> = mono_params.iter().map(llvm_type).collect::<Result<_>>()?;
-        let llvm_ret = llvm_type(&mono_ret)?;
-        let descriptor = descriptor_for_subst(&forall_vars, &subst);
-        let mangled = format!("ail_{owner_module}_{def_name}__{descriptor}");
-
-        // Queue specialisation (deduplicated).
-        let key = (owner_module.to_string(), def_name.to_string(), descriptor.clone());
-        if self.mono_emitted.insert(key) {
-            self.mono_queue.push((
-                owner_module.to_string(),
-                def_name.to_string(),
-                subst.clone(),
-                descriptor,
-            ));
-        }
-
-        // Lower args and emit a direct call to the mangled name.
-        let mut compiled_args = Vec::new();
-        for (a, exp_ty) in args.iter().zip(llvm_params.iter()) {
-            let (v, vty) = self.lower_term(a)?;
-            if &vty != exp_ty {
-                return Err(CodegenError::Internal(format!(
-                    "poly call `{owner_module}.{def_name}` arg type mismatch: expected {exp_ty}, got {vty}"
-                )));
-            }
-            compiled_args.push((v, vty));
-        }
-        let arglist = compiled_args
-            .iter()
-            .map(|(v, t)| format!("{t} {v}"))
-            .collect::<Vec<_>>()
-            .join(", ");
-        let dst = self.fresh_ssa();
-        let call_kw = if tail { "musttail call" } else { "call" };
-        self.body.push_str(&format!(
-            "  {dst} = {call_kw} {ret} @{mangled}({arglist})\n",
-            ret = llvm_ret,
-        ));
-        if tail {
-            self.body
-                .push_str(&format!("  ret {ret} {dst}\n", ret = llvm_ret));
-            self.block_terminated = true;
-        }
-        Ok((dst, llvm_ret))
-    }
-
     fn emit_call(
         &mut self,
         target_module: &str,
@@ -2250,14 +2039,10 @@ impl<'a> Emitter<'a> {
         if name.matches('.').count() == 1 {
             return true;
         }
-        if self
-            .module_user_fns
-            .get(self.module_name)
-            .is_some_and(|m| m.contains_key(name))
-        {
-            return true;
-        }
-        self.module_polymorphic_fns
+        // iter 23.4: poly-def arm dropped — post-mono there are no
+        // `Type::Forall` defs in `module_user_fns` to begin with, and
+        // `module_polymorphic_fns` no longer exists.
+        self.module_user_fns
             .get(self.module_name)
             .is_some_and(|m| m.contains_key(name))
     }

crates/ailang-codegen/src/subst.rs

@@ -14,7 +14,6 @@ use ailang_core::ast::*;
 use std::collections::{BTreeMap, BTreeSet};
 
 use super::{CodegenError, Result};
-use crate::synth::type_descriptor;
 
 /// Iter 12b: derive a name → concrete-type substitution from the
 /// declared params of a `Forall` body and the actual arg types at a
@@ -233,89 +232,9 @@ pub(crate) fn apply_subst_to_type(t: &Type, subst: &BTreeMap<String, Type>) -> T
     }
 }
 
-/// Iter 12b: substitute rigid type vars throughout a Term. Only
-/// `Term::Lam` carries types in the AST (params/ret), so most arms
-/// just recurse. `Term::Var` contains a name string only and is
-/// left untouched.
-pub(crate) fn apply_subst_to_term(t: &Term, subst: &BTreeMap<String, Type>) -> Term {
-    match t {
-        Term::Lit { .. } | Term::Var { .. } => t.clone(),
-        Term::App { callee, args, tail } => Term::App {
-            callee: Box::new(apply_subst_to_term(callee, subst)),
-            args: args.iter().map(|a| apply_subst_to_term(a, subst)).collect(),
-            tail: *tail,
-        },
-        Term::Let { name, value, body } => Term::Let {
-            name: name.clone(),
-            value: Box::new(apply_subst_to_term(value, subst)),
-            body: Box::new(apply_subst_to_term(body, subst)),
-        },
-        Term::If { cond, then, else_ } => Term::If {
-            cond: Box::new(apply_subst_to_term(cond, subst)),
-            then: Box::new(apply_subst_to_term(then, subst)),
-            else_: Box::new(apply_subst_to_term(else_, subst)),
-        },
-        Term::Do { op, args, tail } => Term::Do {
-            op: op.clone(),
-            args: args.iter().map(|a| apply_subst_to_term(a, subst)).collect(),
-            tail: *tail,
-        },
-        Term::Ctor { type_name, ctor, args } => Term::Ctor {
-            type_name: type_name.clone(),
-            ctor: ctor.clone(),
-            args: args.iter().map(|a| apply_subst_to_term(a, subst)).collect(),
-        },
-        Term::Match { scrutinee, arms } => Term::Match {
-            scrutinee: Box::new(apply_subst_to_term(scrutinee, subst)),
-            arms: arms
-                .iter()
-                .map(|a| Arm {
-                    pat: a.pat.clone(),
-                    body: apply_subst_to_term(&a.body, subst),
-                })
-                .collect(),
-        },
-        Term::Lam { params, param_tys, ret_ty, effects, body } => Term::Lam {
-            params: params.clone(),
-            param_tys: param_tys
-                .iter()
-                .map(|t| apply_subst_to_type(t, subst))
-                .collect(),
-            ret_ty: Box::new(apply_subst_to_type(ret_ty, subst)),
-            effects: effects.clone(),
-            body: Box::new(apply_subst_to_term(body, subst)),
-        },
-        Term::Seq { lhs, rhs } => Term::Seq {
-            lhs: Box::new(apply_subst_to_term(lhs, subst)),
-            rhs: Box::new(apply_subst_to_term(rhs, subst)),
-        },
-        Term::LetRec { .. } => {
-            // Iter 16b.1: eliminated by desugar before any
-            // monomorphisation pass runs.
-            unreachable!("Term::LetRec eliminated by desugar")
-        }
-        Term::Clone { value } => Term::Clone {
-            // Iter 18c.1: structural recursion through the wrapper.
-            value: Box::new(apply_subst_to_term(value, subst)),
-        },
-        Term::ReuseAs { source, body } => Term::ReuseAs {
-            // Iter 18d.1: structural recursion through both children.
-            source: Box::new(apply_subst_to_term(source, subst)),
-            body: Box::new(apply_subst_to_term(body, subst)),
-        },
-    }
-}
-
-/// Iter 12b: deterministic descriptor string for a substitution. Used
-/// as the suffix in the mangled name `@ail_<m>_<def>__<descriptor>`.
-/// Vars are emitted in the order given by the FnDef's forall vars
-/// (so two call sites with the same instantiation map to the same
-/// descriptor regardless of internal BTreeMap ordering).
-pub(crate) fn descriptor_for_subst(vars: &[String], subst: &BTreeMap<String, Type>) -> String {
-    let mut parts: Vec<String> = Vec::with_capacity(vars.len());
-    for v in vars {
-        let ty = subst.get(v).cloned().unwrap_or_else(|| Type::unit());
-        parts.push(type_descriptor(&ty));
-    }
-    parts.join("_")
-}
+// iter 23.4: `apply_subst_to_term` and `descriptor_for_subst` were
+// the codegen-side body-substitution and symbol-mangling helpers used
+// by `lower_polymorphic_call` / `emit_specialised_fn`. Both are gone:
+// the typecheck-time mono pass synthesises every monomorphic body
+// (via `ailang_check::substitute_rigids_in_term`) and produces
+// surface-named mono symbols (via `ailang_check::mono::mono_symbol_n`).

crates/ailang-codegen/src/synth.rs

@@ -196,48 +196,11 @@ pub(crate) fn builtin_effect_op_ret(op: &str) -> Option<Type> {
     })
 }
 
-/// Iter 12b: a stable, identifier-safe descriptor for a `Type`.
-/// Maps `Int → I`, `Bool → B`, `Unit → U`, `Str → S`, ADT name `Foo →
-/// FFoo`, fn → `F<params...>R<ret>` (no recursion guard since types in
-/// the MVP are non-recursive at the type level).
-pub(crate) fn type_descriptor(t: &Type) -> String {
-    match t {
-        Type::Con { name, args } => {
-            let head = match name.as_str() {
-                "Int" => "I".into(),
-                "Bool" => "B".into(),
-                "Unit" => "U".into(),
-                "Str" => "S".into(),
-                "Float" => "Fl".into(),
-                other => format!("F{other}"),
-            };
-            if args.is_empty() {
-                head
-            } else {
-                // Iter 13a: parameterised ADTs get their type-arg
-                // descriptors appended, e.g. `FBox` of `Int` → `FBox_I`.
-                let mut s = head;
-                for a in args {
-                    s.push('_');
-                    s.push_str(&type_descriptor(a));
-                }
-                s
-            }
-        }
-        Type::Fn { params, ret, .. } => {
-            let mut s = String::from("Fn");
-            for p in params {
-                s.push('_');
-                s.push_str(&type_descriptor(p));
-            }
-            s.push_str("__r_");
-            s.push_str(&type_descriptor(ret));
-            s
-        }
-        Type::Var { name } => format!("V{name}"),
-        Type::Forall { .. } => "FORALL".into(),
-    }
-}
+// iter 23.4: `type_descriptor` was the helper that mangled a `Type`
+// into an identifier-safe suffix for the codegen-side mono mangling
+// (`Int → I`, `Bool → B`, etc.). The unified mono pass produces
+// surface-named mono symbols instead (`Int → "Int"`, parameterised
+// 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

docs/DESIGN.md

@@ -1511,21 +1511,49 @@ constraint context — which the user MUST have declared explicitly
 (per axis 2). No constraint is implicitly hoisted.
 
 **Monomorphisation (post-typecheck, pre-codegen).** A pass between
-typechecking and codegen replaces every resolved class-method call
-with a call to a synthesised monomorphic `FnDef`. For each unique
-`(method, concrete-type)` pair encountered, the pass:
+typechecking and codegen replaces every call to a
+`Type::Forall`-quantified `Def::Fn` with a call to a synthesised
+monomorphic `FnDef`. Two source-body entry points share the same
+mechanics in one fixpoint:
 
-1. Synthesises a top-level `FnDef` named deterministically from the
-   method name and the canonical hash of the instance type. Body is
-   the resolved instance method (or default body), with the class
-   parameter substituted to the concrete type.
-2. Caches the synthesised def by `(method, type-hash)` so the same
-   pair is not emitted twice.
-3. Rewrites the original `Call` to target the synthesised name.
+1. **Class-method entry.** For each unique `(method, concrete-type)`
+   pair produced by a class-constraint residual, the pass looks up
+   the resolved instance body via `Registry::entries[(class,
+   type-hash)]`, substitutes the class parameter to the concrete
+   type, and synthesises a top-level `FnDef` named
+   `<method>__<type-surface-name>`.
+2. **Free-fn entry.** For each call site to a polymorphic free
+   `Def::Fn` with a fully-concrete substitution, the pass takes the
+   source body directly from the polymorphic `Def::Fn`, applies
+   rigid-var substitution on both the type AND the body (the body
+   may contain inner `Term::Lam`s whose `param_tys` reference the
+   outer Forall vars), and synthesises a top-level `FnDef` named
+   `<name>__<type-surface-name-1>__<type-surface-name-2>__…`
+   (concatenated in `Type::Forall.vars` declaration order; the
+   N-ary case extends the single-type-var class-method shape
+   bit-stably).
 
-After this pass, the IR contains no class machinery — only ordinary
-monomorphic functions and direct calls. Codegen sees no difference
-between a hand-written `show_int` and a synthesised `show__Int`.
+Both arms share:
+
+- A fixpoint loop that keeps collecting targets until a round adds
+  nothing new (a synthesised free-fn body may invoke class methods
+  at concrete types, scheduling new class-method targets; a
+  class-method body may invoke polymorphic free fns at concrete
+  types, scheduling new free-fn targets).
+- A dedup cache keyed by `(kind, base-name,
+  type-hash-or-joined-hashes)` where the first component
+  (`"class"` / `"free"`) guarantees disjoint keying across the
+  two kinds.
+- A call-site rewrite walker that rewrites bare polymorphic call
+  sites — class-method-named OR poly-free-fn-named — to their
+  mono symbols before codegen runs. The walker advances a single
+  cursor over interleaved class-method and free-fn slots emitted
+  in synth's traversal order.
+
+After this pass, the IR contains no polymorphism, no class
+machinery, no polymorphic call sites — only ordinary monomorphic
+functions and direct calls. Codegen sees no difference between a
+hand-written `show_int` and a synthesised `show__Int`.
 
 **Why mono, not virtual dispatch.** Monomorphisation makes the call
 target visible to the optimiser, unlocking inlining and downstream
@@ -1548,11 +1576,14 @@ unambiguously into `<method>__<type-surface-name>` because neither
 component contains `__` by project convention.
 
 **No runtime dispatch, no dictionary passing.** The monomorphisation
-pass is the ONLY mechanism for class-method calls. A call that
-cannot be monomorphised — for instance, because a constraint remains
-unresolved at the entry point — is a static error, not a runtime one.
-This is the LLVM-friendly form and is consistent with Decision 10's
-performance commitment.
+pass is the ONLY specialiser. Codegen sees only monomorphic
+`Def::Fn`s and direct calls; the pre-iter-23.4 codegen-time
+specialiser (`lower_polymorphic_call` + `module_polymorphic_fns` +
+`mono_queue`) was removed in iter 23.4. A call that cannot be
+monomorphised — for instance, because a constraint remains
+unresolved at the entry point — is a static error, not a runtime
+one. This is the LLVM-friendly form and is consistent with
+Decision 10's performance commitment.
 
 ### Defaults and superclasses
 

docs/journals/2026-05-11-iter-23.4.md

@@ -0,0 +1,68 @@
+# iter 23.4 — Mono-Pass Unification
+
+**Date:** 2026-05-11
+**Started from:** fab1685
+**Status:** DONE
+**Tasks completed:** 11 of 11
+
+## Summary
+
+Restructured `crates/ailang-check/src/mono.rs::monomorphise_workspace`
+into a single specialiser over every `Type::Forall`-quantified
+`Def::Fn` in one fixpoint pass, covering both class-method residuals
+and polymorphic free-fn call sites. Removed the codegen-time
+specialiser entirely (`lower_polymorphic_call`, `module_polymorphic_fns`,
+`mono_queue`, `mono_emitted`, `emit_specialised_fn`, plus the dead
+helpers `apply_subst_to_term`, `descriptor_for_subst`, `type_descriptor`).
+Codegen now sees only monomorphic `Def::Fn`s — no polymorphic call
+sites, no codegen-time queue.
+
+The unified pass produces bit-identical mono-symbol bodies for the
+six existing primitive Eq/Ord symbols (hash-stability pin Task 1,
+`crates/ail/tests/mono_hash_stability.rs`) and produces new free-fn
+mono symbols on demand for fixtures like `cmp_max_smoke` (Tasks 2,
+6, 9). All 73 e2e tests + 18 typeclass tests + 81 codegen tests pass
+end-to-end against the new architecture.
+
+## Per-task notes
+
+- iter 23.4.1: hash-stability regression pin — `examples/mono_hash_pin_smoke.ail.json` + `mono_hash_stability.rs` with six pinned hashes (`eq__Int`/`Bool`/`Str`, `compare__Int`/`Bool`/`Str`).
+- iter 23.4.2: `cmp_max_smoke` fixture + RED workspace-level acceptance gate.
+- iter 23.4.3: `MonoTarget` struct → enum with `ClassMethod` / `FreeFn` variants; `mono_target_key` widened with `"class"` / `"free"` first component (guaranteed-disjoint keys).
+- iter 23.4.4: free-fn arm in `collect_mono_targets`. NOTE: the plan's Step 4.3 sketch proposed a separate walker over `Term::App` plus a new `env.polymorphic_free_fns` index; instead I extended `synth` itself with a parallel `&mut Vec<FreeFnCall>` channel (mirroring the existing `&mut Vec<ResidualConstraint>` mechanism). One less data flow, one less helper; substitution tracking comes "for free" via fresh metavars + post-synth `subst.apply`. Plan's Step 4.4 (adding `polymorphic_free_fns` to `Env`) is therefore obsolete; not landed.
+- iter 23.4.5: `synthesise_mono_fn_for_free_fn` + N-ary `mono_symbol_n`. One substantive deviation from the plan's sketch: I also substitute rigid vars in the BODY via a new `crate::substitute_rigids_in_term` helper. The plan said "passes through unchanged" mirroring the class-method arm — but free-fn bodies (e.g. `std_list.length`) carry inner `Term::Lam`s whose `param_tys` reference outer Forall vars; without body substitution, Phase 3's re-synth would fail unification on unbound rigid `a`.
+- iter 23.4.6: `rewrite_class_method_calls` renamed to `rewrite_mono_calls`; new helper `poly_free_fn_names_for_module` builds the per-module set of bare + qualified poly-fn names; `collect_residuals_ordered` walks the AST emitting interleaved slots via new `interleave_slots` helper. The walker and slot collector share the same predicate so the cursor invariant survives across the two channels.
+- iter 23.4.7: `workspace_has_typeclasses` → `workspace_has_specialisable_targets`. NOTE: the plan's expected "FAIL → PASS after generalisation" was incorrect because the auto-injected prelude (iter 23.1) already keeps the old predicate true for every user workspace. The generalisation is principled-correctness only; documented in the predicate docstring.
+- iter 23.4.8: codegen cleanup — removed `lower_polymorphic_call`, both call sites, the Emitter fields (`module_polymorphic_fns`, `mono_queue`, `mono_emitted`), `emit_specialised_fn`, Pass-1 poly population, and the unused dead helpers (`apply_subst_to_term`, `descriptor_for_subst`, `type_descriptor`). `is_static_callee` collapsed to its mono-only path. Two follow-on fixes were required beyond the plan: (a) Unit-default fallback for unpinned forall vars in the mono pass — mirrors pre-iter-23.4 codegen behaviour for sites like `is_empty(Nil)` where the elem type is unobservable from the args alone; (b) updated the `ail emit-ir` command pipeline to include `lift_letrecs` + `monomorphise_workspace` (pre-iter-23.4 the codegen-time poly path was masking this dependency — `emit-ir` was broken for poly fixtures without the explicit mono call now that codegen no longer handles it).
+- iter 23.4.9: end-to-end verification — `cmp_max_smoke_runs_end_to_end` proves `cmp_max(3, 7)` at Int prints 7; the three existing poly fixtures (`polymorphic_id_at_int_and_bool`, `polymorphic_apply_with_fn_param`, `poly_rec_capture_demo`) still run.
+- iter 23.4.10: `docs/DESIGN.md` §"Monomorphisation (post-typecheck, pre-codegen)" amended to describe the two-arm fixpoint, the dedup key with disjoint `"class"` / `"free"` prefixes, the cursor-aligned walker, and the removed codegen-time path.
+- iter 23.4.11: bench-regression check — `bench/check.py`, `bench/compile_check.py`, `bench/cross_lang.py` all exit 0; no metrics regressed.
+
+## Concerns
+
+- Plan Step 4.4 was bypassed (no `env.polymorphic_free_fns` field added). The synth-channel approach is structurally cleaner; the plan's index is unneeded. If a future iter needs an O(1) "is this name a poly free fn" predicate at non-synth call sites, the helper `poly_free_fn_names_for_module` (in mono.rs) builds the set on demand.
+- Plan Steps 5.3 / 7's "body unchanged" / "early-out fires for class-free workspaces" assumptions were both wrong against the actual codebase shape (free-fn bodies carry rigid vars in inner Lams; prelude is auto-injected so no workspace is class-free). Both were caught and adapted during implementation — no spec defect, just plan-draft drift against the live codebase.
+
+## Known debt
+
+- None tracked; all out-of-scope items from the plan (five prelude free fns ne/lt/le/gt/ge, `examples/prelude.ail.json` edits, the negative E2E fixtures `eq_ord_polymorphic` / `eq_ord_user_adt`, DESIGN.md §"Decision 11" amendment, Float-NoInstance diagnostic wording, roadmap update) remain owned by iter 23.5 as planned.
+
+## Files touched
+
+- `crates/ailang-check/src/lib.rs` — new `FreeFnCall` struct; `synth` signature gains `&mut Vec<FreeFnCall>`; Var arm tracks `(owner_module, unqualified_name)` and pushes `FreeFnCall` for `Type::Forall`-resolved non-local refs; new `substitute_rigids_in_term` helper.
+- `crates/ailang-check/src/mono.rs` — `MonoTarget` struct → enum (`ClassMethod` / `FreeFn`); `mono_target_key` widened; new `mono_symbol_n` (N-ary); new `synthesise_mono_fn_for_free_fn`; new `poly_free_fn_names_for_module`; new `interleave_slots`; rename `rewrite_class_method_calls` → `rewrite_mono_calls`; `workspace_has_typeclasses` → `workspace_has_specialisable_targets`; fixpoint loop matches on target variants.
+- `crates/ailang-check/src/lift.rs`, `crates/ailang-check/src/builtins.rs` — synth call sites pass new `&mut free_fn_calls` Vec.
+- `crates/ailang-codegen/src/lib.rs` — deletions per Task 8 (Emitter fields, `lower_polymorphic_call`, `emit_specialised_fn`, mono drain loop, Pass-1 poly population, `is_static_callee` poly arm). `use` import shrunk.
+- `crates/ailang-codegen/src/subst.rs` — `apply_subst_to_term` and `descriptor_for_subst` removed (dead post-Task-8).
+- `crates/ailang-codegen/src/synth.rs` — `type_descriptor` removed (dead post-Task-8).
+- `crates/ail/src/main.rs` — `emit-ir` command gains `lift_letrecs` + `monomorphise_workspace` pre-passes (matches `build` shape).
+- `crates/ail/tests/typeclass_22b3.rs` — updated three test sites to `MonoTarget::ClassMethod` enum form.
+- `crates/ail/tests/mono_hash_stability.rs` (new) — regression pin for six primitive Eq/Ord mono-symbol body hashes.
+- `crates/ail/tests/mono_unification.rs` (new) — six tests covering variant key disjointness, free-fn target emission, free-fn synthesis with rigid substitution, rewrite walker on free fns, identity for poly-free-fn-only workspaces, and end-to-end `cmp_max_smoke` runtime correctness.
+- `examples/cmp_max_smoke.ail.json` (new) — `cmp_max : forall a. Ord a => (a, a) -> a` composition fixture.
+- `examples/mono_hash_pin_smoke.ail.json` (new) — fixture exercising the six primitive Eq/Ord mono symbols for hash-stability pinning.
+- `docs/DESIGN.md` — §"Monomorphisation (post-typecheck, pre-codegen)" amended.
+
+## Stats
+
+bench/orchestrator-stats/2026-05-11-iter-23.4.json

docs/journals/INDEX.md

@@ -13,3 +13,4 @@
 - 2026-05-11 — iter 23.4-prep: checker prerequisites for prelude free fns → 2026-05-11-iter-23.4-prep.md
 - 2026-05-11 — iter gc.1: grounding-check agent + brainstorm Step 7.5 → 2026-05-11-iter-gc.1.md
 - 2026-05-11 — iter disc.1: boss-only commits + main-as-quarantine (no branches in implement) → 2026-05-11-iter-disc.1.md
+- 2026-05-11 — iter 23.4: mono-pass unification (class methods + polymorphic free fns in one fixpoint; codegen-time specialiser removed) → 2026-05-11-iter-23.4.md

examples/cmp_max_smoke.ail.json

@@ -0,0 +1,55 @@
+{
+  "schema": "ailang/v0",
+  "name": "cmp_max_smoke",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "cmp_max",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "constraints": [{ "class": "Ord", "type": { "k": "var", "name": "a" } }],
+        "body": {
+          "k": "fn",
+          "params": [{ "k": "var", "name": "a" }, { "k": "var", "name": "a" }],
+          "ret": { "k": "var", "name": "a" },
+          "effects": []
+        }
+      },
+      "params": ["x", "y"],
+      "body": {
+        "t": "match",
+        "scrutinee": {
+          "t": "app",
+          "fn": { "t": "var", "name": "compare" },
+          "args": [{ "t": "var", "name": "x" }, { "t": "var", "name": "y" }]
+        },
+        "arms": [
+          { "pat": { "p": "ctor", "type": "prelude.Ordering", "ctor": "LT", "fields": [] }, "body": { "t": "var", "name": "y" } },
+          { "pat": { "p": "wild" }, "body": { "t": "var", "name": "x" } }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "do", "op": "io/print_int",
+        "args": [{
+          "t": "app",
+          "fn": { "t": "var", "name": "cmp_max" },
+          "args": [
+            { "t": "lit", "lit": { "kind": "int", "value": 3 } },
+            { "t": "lit", "lit": { "kind": "int", "value": 7 } }
+          ]
+        }]
+      }
+    }
+  ]
+}

examples/mono_hash_pin_smoke.ail.json

@@ -0,0 +1,120 @@
+{
+  "schema": "ailang/v0",
+  "name": "mono_hash_pin_smoke",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "ord_to_int",
+      "type": {
+        "k": "fn",
+        "params": [{ "k": "con", "name": "prelude.Ordering" }],
+        "ret": { "k": "con", "name": "Int" },
+        "effects": []
+      },
+      "params": ["o"],
+      "body": {
+        "t": "match",
+        "scrutinee": { "t": "var", "name": "o" },
+        "arms": [
+          { "pat": { "p": "ctor", "type": "prelude.Ordering", "ctor": "LT", "fields": [] }, "body": { "t": "lit", "lit": { "kind": "int", "value": -1 } } },
+          { "pat": { "p": "ctor", "type": "prelude.Ordering", "ctor": "EQ", "fields": [] }, "body": { "t": "lit", "lit": { "kind": "int", "value": 0 } } },
+          { "pat": { "p": "ctor", "type": "prelude.Ordering", "ctor": "GT", "fields": [] }, "body": { "t": "lit", "lit": { "kind": "int", "value": 1 } } }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "body": {
+        "t": "seq",
+        "lhs": {
+          "t": "do", "op": "io/print_bool",
+          "args": [{
+            "t": "app", "fn": { "t": "var", "name": "eq" },
+            "args": [
+              { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+              { "t": "lit", "lit": { "kind": "int", "value": 1 } }
+            ]
+          }]
+        },
+        "rhs": {
+          "t": "seq",
+          "lhs": {
+            "t": "do", "op": "io/print_bool",
+            "args": [{
+              "t": "app", "fn": { "t": "var", "name": "eq" },
+              "args": [
+                { "t": "lit", "lit": { "kind": "bool", "value": true } },
+                { "t": "lit", "lit": { "kind": "bool", "value": true } }
+              ]
+            }]
+          },
+          "rhs": {
+            "t": "seq",
+            "lhs": {
+              "t": "do", "op": "io/print_bool",
+              "args": [{
+                "t": "app", "fn": { "t": "var", "name": "eq" },
+                "args": [
+                  { "t": "lit", "lit": { "kind": "str", "value": "a" } },
+                  { "t": "lit", "lit": { "kind": "str", "value": "a" } }
+                ]
+              }]
+            },
+            "rhs": {
+              "t": "seq",
+              "lhs": {
+                "t": "do", "op": "io/print_int",
+                "args": [{
+                  "t": "app", "fn": { "t": "var", "name": "ord_to_int" },
+                  "args": [{
+                    "t": "app", "fn": { "t": "var", "name": "compare" },
+                    "args": [
+                      { "t": "lit", "lit": { "kind": "int", "value": 1 } },
+                      { "t": "lit", "lit": { "kind": "int", "value": 2 } }
+                    ]
+                  }]
+                }]
+              },
+              "rhs": {
+                "t": "seq",
+                "lhs": {
+                  "t": "do", "op": "io/print_int",
+                  "args": [{
+                    "t": "app", "fn": { "t": "var", "name": "ord_to_int" },
+                    "args": [{
+                      "t": "app", "fn": { "t": "var", "name": "compare" },
+                      "args": [
+                        { "t": "lit", "lit": { "kind": "bool", "value": false } },
+                        { "t": "lit", "lit": { "kind": "bool", "value": true } }
+                      ]
+                    }]
+                  }]
+                },
+                "rhs": {
+                  "t": "do", "op": "io/print_int",
+                  "args": [{
+                    "t": "app", "fn": { "t": "var", "name": "ord_to_int" },
+                    "args": [{
+                      "t": "app", "fn": { "t": "var", "name": "compare" },
+                      "args": [
+                        { "t": "lit", "lit": { "kind": "str", "value": "a" } },
+                        { "t": "lit", "lit": { "kind": "str", "value": "b" } }
+                      ]
+                    }]
+                  }]
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  ]
+}