diff --git a/bench/orchestrator-stats/2026-05-11-iter-23.4.json b/bench/orchestrator-stats/2026-05-11-iter-23.4.json
new file mode 100644
index 0000000..8eeaf25
--- /dev/null
+++ b/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)"
+  }
+}
diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs
index be5095f..7165e18 100644
--- a/crates/ail/src/main.rs
+++ b/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) => {
diff --git a/crates/ail/tests/mono_hash_stability.rs b/crates/ail/tests/mono_hash_stability.rs
new file mode 100644
index 0000000..4598332
--- /dev/null
+++ b/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");
+    }
+}
diff --git a/crates/ail/tests/mono_unification.rs b/crates/ail/tests/mono_unification.rs
new file mode 100644
index 0000000..ca95ecf
--- /dev/null
+++ b/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"
+    );
+}
diff --git a/crates/ail/tests/typeclass_22b3.rs b/crates/ail/tests/typeclass_22b3.rs
index e10d1ae..fd8f858 100644
--- a/crates/ail/tests/typeclass_22b3.rs
+++ b/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(),
diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs
index 8111e0b..e7b1e6b 100644
--- a/crates/ailang-check/src/builtins.rs
+++ b/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!(
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 0e5ffef..7c14bed 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/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)
         }
     }
 }
diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs
index da26324..c935f3a 100644
--- a/crates/ailang-check/src/lift.rs
+++ b/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))
     }
 }
diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs
index b4ef2b1..2f7ab59 100644
--- a/crates/ailang-check/src/mono.rs
+++ b/crates/ailang-check/src/mono.rs
@@ -70,7 +70,7 @@ pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> {
     // instance defs (no callable methods at concrete types), but
     // the body walks would still be a wasted traversal; the
     // class-free check is the cheap way to opt out.
-    if !workspace_has_typeclasses(ws) {
+    if !workspace_has_specialisable_targets(ws) {
         return Ok(ws.clone());
     }
 
@@ -115,35 +115,43 @@ pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> {
         // never mutates the registry.
         for t in &new {
             let key = mono_target_key(t);
-            // normalize to match Registry::normalize_type_for_lookup contract
-            let t_ty_norm = ws_owned.registry.normalize_type_for_lookup(&t.type_);
-            let registry_key =
-                (t.class.clone(), ailang_core::canonical::type_hash(&t_ty_norm));
-            let entry = ws_owned
-                .registry
-                .entries
-                .get(&registry_key)
-                .ok_or_else(|| {
-                    crate::CheckError::Internal(format!(
-                        "monomorphise_workspace: target `{} {}` has no registry entry",
-                        t.class,
-                        ailang_core::pretty::type_to_string(&t.type_),
-                    ))
-                })?;
-            let class_def = class_index.get(&t.class).ok_or_else(|| {
-                crate::CheckError::Internal(format!(
-                    "monomorphise_workspace: class `{}` not found",
-                    t.class
-                ))
-            })?;
-            let f = synthesise_mono_fn(t, class_def, &entry.instance)?;
+            let (f, defining_module) = match t {
+                MonoTarget::ClassMethod { class, type_, defining_module, .. } => {
+                    // normalize to match Registry::normalize_type_for_lookup contract
+                    let t_ty_norm = ws_owned.registry.normalize_type_for_lookup(type_);
+                    let registry_key =
+                        (class.clone(), ailang_core::canonical::type_hash(&t_ty_norm));
+                    let entry = ws_owned
+                        .registry
+                        .entries
+                        .get(&registry_key)
+                        .ok_or_else(|| {
+                            crate::CheckError::Internal(format!(
+                                "monomorphise_workspace: target `{} {}` has no registry entry",
+                                class,
+                                ailang_core::pretty::type_to_string(type_),
+                            ))
+                        })?;
+                    let class_def = class_index.get(class).ok_or_else(|| {
+                        crate::CheckError::Internal(format!(
+                            "monomorphise_workspace: class `{}` not found",
+                            class
+                        ))
+                    })?;
+                    (synthesise_mono_fn(t, class_def, &entry.instance)?, defining_module.clone())
+                }
+                MonoTarget::FreeFn { defining_module, .. } => (
+                    synthesise_mono_fn_for_free_fn(t, &ws_owned)?,
+                    defining_module.clone(),
+                ),
+            };
             let target_module = ws_owned
                 .modules
-                .get_mut(&t.defining_module)
+                .get_mut(&defining_module)
                 .ok_or_else(|| {
                     crate::CheckError::Internal(format!(
                         "monomorphise_workspace: defining module `{}` missing",
-                        t.defining_module
+                        defining_module
                     ))
                 })?;
             target_module.defs.push(Def::Fn(f));
@@ -165,16 +173,19 @@ pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> {
         // collection-phase walk (cursor alignment depends on it).
         let mut env_mod = env.clone();
         apply_per_module_types_overlay(&mut env_mod, &ws_owned, mname);
+        // Iter 23.4: precompute the per-module poly-free-fn name
+        // set used as the rewrite walker's second predicate.
+        let poly_free_fns = poly_free_fn_names_for_module(&ws_owned, &env_mod, mname);
         let n_defs = ws_owned.modules[mname].defs.len();
         for i in 0..n_defs {
             let ordered: Vec<Option<MonoTarget>> = {
                 let m = &ws_owned.modules[mname];
                 let d = &m.defs[i];
                 match d {
-                    Def::Fn(f) => collect_residuals_ordered(f, mname, &env_mod)?,
+                    Def::Fn(f) => collect_residuals_ordered(f, mname, &env_mod, &poly_free_fns)?,
                     Def::Const(c) => {
                         let pseudo = const_as_pseudo_fn(c);
-                        collect_residuals_ordered(&pseudo, mname, &env_mod)?
+                        collect_residuals_ordered(&pseudo, mname, &env_mod, &poly_free_fns)?
                     }
                     _ => continue,
                 }
@@ -185,13 +196,14 @@ pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> {
             let mut locals: BTreeSet<String> = BTreeSet::new();
             match d {
                 Def::Fn(f) => {
-                    // Top-level fn params shadow class-method names too.
+                    // Top-level fn params shadow class-method / poly-free-fn names too.
                     for p in &f.params {
                         locals.insert(p.clone());
                     }
-                    rewrite_class_method_calls(
+                    rewrite_mono_calls(
                         &mut f.body,
                         &env.class_methods,
+                        &poly_free_fns,
                         mname,
                         &ordered,
                         &mut cursor,
@@ -199,9 +211,10 @@ pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> {
                     );
                 }
                 Def::Const(c) => {
-                    rewrite_class_method_calls(
+                    rewrite_mono_calls(
                         &mut c.value,
                         &env.class_methods,
+                        &poly_free_fns,
                         mname,
                         &ordered,
                         &mut cursor,
@@ -269,6 +282,60 @@ fn const_as_pseudo_fn(c: &ConstDef) -> AstFnDef {
     }
 }
 
+/// Iter 23.4: compute the set of names (bare + dot-qualified) that
+/// `synth`'s Var arm would resolve to a polymorphic free fn when
+/// called from module `mname`. The rewrite walker and the slot
+/// collector both consult this set to decide whether a `Term::Var`
+/// site contributes a slot (i.e. needs cursor advancement and a
+/// potential mono-symbol rewrite).
+///
+/// The predicate must agree EXACTLY with `synth`'s Var arm's
+/// `free_fn_owner` derivation. Three sources contribute:
+///
+/// 1. Same-module poly `Def::Fn`s (bare names).
+/// 2. Implicitly-imported modules' poly `Def::Fn`s (bare names,
+///    via the iter-23.4-prep fall-through).
+/// 3. Dot-qualified `alias.name` forms for every import alias.
+///
+/// Builtins (`==`, `+`, etc.) are explicitly excluded — they live
+/// only in `env.globals`, never in `env.module_globals[<owner>]`,
+/// so they don't pass synth's "in module_globals" gate.
+fn poly_free_fn_names_for_module(
+    ws: &Workspace,
+    env: &crate::Env,
+    mname: &str,
+) -> BTreeSet<String> {
+    let mut out: BTreeSet<String> = BTreeSet::new();
+    // 1. Same-module poly fns.
+    if let Some(m) = ws.modules.get(mname) {
+        for d in &m.defs {
+            if let Def::Fn(f) = d {
+                if matches!(&f.ty, Type::Forall { .. }) {
+                    out.insert(f.name.clone());
+                }
+            }
+        }
+    }
+    // 2 + 3. Imported modules' poly fns: bare (via implicit-import
+    // fall-through) AND dot-qualified (alias.name).
+    if let Some(imports) = env.module_imports.get(mname) {
+        for (alias_or_name, target_mod) in imports {
+            if let Some(target_globals) = env.module_globals.get(target_mod) {
+                for (n, t) in target_globals {
+                    if matches!(t, Type::Forall { .. }) {
+                        // Implicit-import bare name (today only the
+                        // prelude is implicit; the loop is generic).
+                        out.insert(n.clone());
+                        // Dot-qualified form.
+                        out.insert(format!("{alias_or_name}.{n}"));
+                    }
+                }
+            }
+        }
+    }
+    out
+}
+
 /// Iter 22b.3: workspace-wide `class-name -> ClassDef` index.
 /// Used by the fixpoint to look up the matching class definition
 /// when synthesising a fn.
@@ -284,47 +351,78 @@ fn build_class_index(ws: &Workspace) -> BTreeMap<String, ClassDef> {
     idx
 }
 
-/// Iter 22b.3: returns `true` iff any module in `ws` declares at
-/// least one [`Def::Class`] or [`Def::Instance`]. Cheap workspace
-/// scan; the early-out keeps class-free workspaces byte-identical
-/// through the pass.
-fn workspace_has_typeclasses(ws: &Workspace) -> bool {
+/// Iter 22b.3 / iter 23.4: returns `true` iff any module in `ws`
+/// declares at least one specialisable target — a [`Def::Class`]
+/// or [`Def::Instance`] (class-method residuals) OR a
+/// `Type::Forall`-quantified [`Def::Fn`] (free-fn case). Cheap
+/// workspace scan; the early-out keeps target-free workspaces
+/// byte-identical through the pass.
+///
+/// Today the prelude is auto-injected into every workspace and
+/// brings its Eq/Ord classes along, so the predicate is effectively
+/// always true; the generalisation matters for principled
+/// correctness should a future workspace skip the prelude.
+fn workspace_has_specialisable_targets(ws: &Workspace) -> bool {
     ws.modules.values().any(|m| {
-        m.defs.iter().any(|d| matches!(d, Def::Class(_) | Def::Instance(_)))
+        m.defs.iter().any(|d| match d {
+            Def::Class(_) | Def::Instance(_) => true,
+            Def::Fn(f) => matches!(f.ty, Type::Forall { .. }),
+            _ => false,
+        })
     })
 }
 
-/// Iter 22b.3: deterministic mono-symbol name for a `(method,
-/// type)` pair. Primitive types (`Int`, `Bool`, `Str`, `Unit`)
-/// produce `<method>__<surface-name>` for diagnostic and
-/// ABI legibility. All other types — parameterised cons,
-/// user-defined ADTs, function types — fall to
-/// `<method>__<8-hex-prefix-of-canonical-type-hash>`. The hash
-/// route ensures uniqueness without requiring a flattened
-/// surface form for arbitrarily nested types.
+/// Iter 22b.3 / iter 23.4: deterministic mono-symbol name for a
+/// `(base-name, types...)` tuple. The N-ary form supports both
+/// single-type-var class methods (today's six primitive Eq/Ord
+/// symbols pass a one-element slice and produce identical output
+/// to the pre-iter-23.4 implementation — verified by the
+/// hash-stability pin in `crates/ail/tests/mono_hash_stability.rs`)
+/// AND N-ary free-fn instantiations (e.g. `Type::Forall.vars = ["a", "b"]`
+/// produces `<name>__<surface-a>__<surface-b>` in declaration order).
 ///
-/// Separator choice: `__` (double underscore) rather than the spec's
-/// recommended `#` — `#` terminates LLVM IR global identifiers (and
-/// breaks C-ABI symbol names on most targets), so the produced name
-/// has to survive codegen unaltered. The double underscore is
-/// already in use elsewhere in the codegen pipeline as a descriptor
-/// separator (see `emit_specialised_fn`), keeping the convention
-/// uniform. Iter 22b.3.7 documents the substitution at the e2e
-/// gate; Tasks 2/4 unit-tests are updated in lockstep.
+/// Per type, primitive `Type::Con` (`Int`, `Bool`, `Str`, `Unit`,
+/// `Float`) produces the surface name for diagnostic and ABI
+/// legibility. All other types — parameterised cons, user-defined
+/// ADTs, function types — fall to the 8-hex-prefix of
+/// `ailang_core::canonical::type_hash`. The hash route ensures
+/// uniqueness without requiring a flattened surface form for
+/// arbitrarily nested types.
+///
+/// Separator choice: `__` (double underscore) — `#` terminates LLVM
+/// IR global identifiers and breaks C-ABI symbol names on most
+/// targets, so the produced name has to survive codegen unaltered.
 ///
 /// Determinism: `ailang_core::canonical::type_hash` is the same
 /// function `workspace::build_registry` uses to key
 /// [`Registry::entries`], so a registry-key match implies a
 /// `mono_symbol` match.
-pub fn mono_symbol(method: &str, ty: &Type) -> String {
-    if let Some(prim) = primitive_surface_name(ty) {
-        return format!("{method}__{prim}");
+pub fn mono_symbol(base: &str, ty: &Type) -> String {
+    mono_symbol_n(base, std::slice::from_ref(ty))
+}
+
+/// Iter 23.4: N-ary variant of [`mono_symbol`]. The single-type
+/// public-API stays as [`mono_symbol`] (used by class-method
+/// emission) for surface compatibility; N-ary callers (free-fn
+/// emission with multi-arg type instantiations) use this form
+/// directly.
+pub fn mono_symbol_n(base: &str, types: &[Type]) -> String {
+    let mut parts: Vec<String> = Vec::with_capacity(1 + types.len());
+    parts.push(base.to_string());
+    for ty in types {
+        parts.push(type_to_mono_suffix(ty));
+    }
+    parts.join("__")
+}
+
+fn type_to_mono_suffix(ty: &Type) -> String {
+    match primitive_surface_name(ty) {
+        Some(p) => p.to_string(),
+        None => {
+            let h = ailang_core::canonical::type_hash(ty);
+            h[..8].to_string()
+        }
     }
-    let full_hash = ailang_core::canonical::type_hash(ty);
-    // 8-hex prefix is enough for low-collision keying across the
-    // workspace; the full hash remains in the registry for
-    // disambiguation should one ever be needed.
-    format!("{method}__{}", &full_hash[..8])
 }
 
 /// Returns the surface name iff `ty` is a zero-arity primitive
@@ -342,33 +440,60 @@ fn primitive_surface_name(ty: &Type) -> Option<&'static str> {
     }
 }
 
-/// Iter 22b.3: one synthesisation request — a fully-concrete
-/// `(class, method, type)` triple observed at a class-method call
-/// site, plus the registry's `defining_module` for the matching
-/// `InstanceDef` (the synthesised fn lives there). Equality of
-/// targets is compared via [`mono_target_key`] — `(class,
-/// method, type-hash)`.
+/// Iter 22b.3 / iter 23.4: a specialisation request. One synthesised
+/// monomorphic `Def::Fn` will be produced per unique
+/// [`mono_target_key`]. Two source-body kinds share one fixpoint:
+///
+/// - [`MonoTarget::ClassMethod`]: a class-constraint residual
+///   resolved to a concrete `(class, method, type)` triple. The
+///   body comes from `Registry::entries[(class, type-hash)]` (the
+///   instance body, or the class default if the instance omits the
+///   method).
+/// - [`MonoTarget::FreeFn`]: a call site to a polymorphic free
+///   `Def::Fn` with a fully-concrete substitution. The body comes
+///   directly from the polymorphic `Def::Fn`'s `body` after
+///   rigid-var substitution. Added in iter 23.4 to unify the
+///   typecheck-time and codegen-time specialisers.
 #[derive(Debug, Clone)]
-pub struct MonoTarget {
-    pub class: String,
-    pub method: String,
-    pub type_: Type,
-    pub defining_module: String,
+pub enum MonoTarget {
+    ClassMethod {
+        class: String,
+        method: String,
+        type_: Type,
+        defining_module: String,
+    },
+    FreeFn {
+        name: String,
+        /// Concrete type arguments in `Type::Forall.vars` declaration order.
+        type_args: Vec<Type>,
+        /// Module in which the polymorphic source `Def::Fn` is declared;
+        /// the synthesised mono `Def::Fn` is appended there.
+        defining_module: String,
+    },
 }
 
-/// Iter 22b.3: dedup key for a [`MonoTarget`] — the same triple
-/// `Registry::entries` uses for instance lookup, plus the method
-/// name. Two targets with the same key produce the same
-/// synthesised symbol and the same body. Consumed by the workspace
-/// fixpoint (Task 5) and the rewrite walker (Task 6); declared
-/// here in Task 3 so the dedup contract lives next to `MonoTarget`.
-#[allow(dead_code)]
-pub(crate) fn mono_target_key(t: &MonoTarget) -> (String, String, String) {
-    (
-        t.class.clone(),
-        t.method.clone(),
-        ailang_core::canonical::type_hash(&t.type_),
-    )
+/// Iter 22b.3 / iter 23.4: dedup key for a [`MonoTarget`]. Class-method
+/// targets key on `("class", "<class>.<method>", <type-hash>)`; free-fn
+/// targets key on `("free", "<name>", <joined-type-hashes>)`. The two
+/// kinds are guaranteed-disjoint by the first component, so a
+/// class-method and a free-fn with the same base name never collide.
+/// Consumed by the workspace fixpoint and the rewrite walker.
+pub fn mono_target_key(t: &MonoTarget) -> (String, String, String) {
+    match t {
+        MonoTarget::ClassMethod { class, method, type_, .. } => (
+            "class".into(),
+            format!("{class}.{method}"),
+            ailang_core::canonical::type_hash(type_),
+        ),
+        MonoTarget::FreeFn { name, type_args, .. } => {
+            let joined = type_args
+                .iter()
+                .map(ailang_core::canonical::type_hash)
+                .collect::<Vec<_>>()
+                .join("|");
+            ("free".into(), name.clone(), joined)
+        }
+    }
 }
 
 /// Thin wrapper over [`crate::build_check_env`]. The mono pass needs
@@ -474,6 +599,7 @@ pub fn collect_mono_targets(
     let mut subst = crate::Subst::default();
     let mut counter: u32 = 0;
     let mut residuals: Vec<crate::ResidualConstraint> = Vec::new();
+    let mut free_fn_calls: Vec<crate::FreeFnCall> = Vec::new();
     crate::synth(
         &f.body,
         &env,
@@ -483,6 +609,7 @@ pub fn collect_mono_targets(
         &mut subst,
         &mut counter,
         &mut residuals,
+        &mut free_fn_calls,
     )?;
 
     // Filter residuals to fully-concrete ones; look up
@@ -500,13 +627,47 @@ pub fn collect_mono_targets(
             Some(e) => e,
             None => continue, // no-instance — Task 10 of 22b.2 fires; skip silently here.
         };
-        out.push(MonoTarget {
+        out.push(MonoTarget::ClassMethod {
             class: r.class.clone(),
             method: r.method.clone(),
             type_: r_ty,
             defining_module: entry.defining_module.clone(),
         });
     }
+    // Iter 23.4 Task 4: free-fn arm. Each `FreeFnCall` observation
+    // recorded by `synth`'s Var arm carries the bare name, the
+    // owning module (resolved through synth's lookup ladder), the
+    // forall vars (declaration order), and the per-var fresh
+    // metavars. Post-`synth`, `subst.apply` each meta to recover
+    // the concrete type-arg at this call site. Unbound (metavar)
+    // vars default to `Type::unit()` — mirrors the pre-iter-23.4
+    // codegen-side `derive_substitution` behaviour at
+    // `crates/ailang-codegen/src/subst.rs:57-61`, where a forall
+    // var the args couldn't pin (e.g. `is_empty Nil` for
+    // `is_empty : forall a. (List<a>) -> Bool`) collapses to a
+    // single Unit-defaulted specialisation. The specialised body
+    // must not actually consume an `a`-typed value, or typecheck
+    // would have rejected; the Unit default is sound and
+    // deterministic.
+    for fc in free_fn_calls {
+        let type_args: Vec<Type> = fc
+            .metas
+            .iter()
+            .map(|m| {
+                let resolved = subst.apply(m);
+                if crate::is_fully_concrete(&resolved) {
+                    resolved
+                } else {
+                    Type::unit()
+                }
+            })
+            .collect();
+        out.push(MonoTarget::FreeFn {
+            name: fc.name.clone(),
+            type_args,
+            defining_module: fc.owner_module.clone(),
+        });
+    }
     Ok(out)
 }
 
@@ -541,35 +702,45 @@ pub fn synthesise_mono_fn(
     class_def: &ClassDef,
     instance: &InstanceDef,
 ) -> Result<AstFnDef> {
+    let (class_name, method, type_) = match target {
+        MonoTarget::ClassMethod { class, method, type_, .. } => (class, method, type_),
+        MonoTarget::FreeFn { .. } => {
+            return Err(crate::CheckError::Internal(
+                "synthesise_mono_fn: called with FreeFn variant; use \
+                 synthesise_mono_fn_for_free_fn instead"
+                    .into(),
+            ));
+        }
+    };
     // Locate the class method declaration.
     let class_method = class_def
         .methods
         .iter()
-        .find(|m| m.name == target.method)
+        .find(|m| &m.name == method)
         .ok_or_else(|| {
             crate::CheckError::Internal(format!(
                 "synthesise_mono_fn: class `{}` has no method `{}`",
-                class_def.name, target.method
+                class_def.name, method
             ))
         })?;
 
-    // Build the substitution `param := target.type_` and apply it
-    // to the method type. The result is a concrete `Type::Fn` (no
+    // Build the substitution `param := type_` and apply it to the
+    // method type. The result is a concrete `Type::Fn` (no
     // `Forall`).
     let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
-    mapping.insert(class_def.param.clone(), target.type_.clone());
+    mapping.insert(class_def.param.clone(), type_.clone());
     let concrete_method_ty = crate::substitute_rigids(&class_method.ty, &mapping);
 
     // Resolve the body — instance override first, then class default.
-    let body_term: Term = match instance.methods.iter().find(|im| im.name == target.method) {
+    let body_term: Term = match instance.methods.iter().find(|im| &im.name == method) {
         Some(im) => im.body.clone(),
         None => class_method.default.clone().ok_or_else(|| {
             crate::CheckError::Internal(format!(
                 "synthesise_mono_fn: instance `{} {}` omits method `{}` and class has no \
                  default (registry-build should have rejected this)",
-                target.class,
-                ailang_core::pretty::type_to_string(&target.type_),
-                target.method,
+                class_name,
+                ailang_core::pretty::type_to_string(type_),
+                method,
             ))
         })?,
     };
@@ -587,7 +758,7 @@ pub fn synthesise_mono_fn(
                 return Err(crate::CheckError::Internal(format!(
                     "synthesise_mono_fn: method `{}` has positional params but body is not \
                      a Lam: {:?}",
-                    target.method, other
+                    method, other
                 )));
             }
         }
@@ -596,7 +767,7 @@ pub fn synthesise_mono_fn(
     };
 
     Ok(AstFnDef {
-        name: mono_symbol(&target.method, &target.type_),
+        name: mono_symbol(method, type_),
         ty: concrete_method_ty,
         params,
         body,
@@ -605,38 +776,138 @@ pub fn synthesise_mono_fn(
     })
 }
 
-/// Iter 22b.3: rewrite every class-method call site in `body` to
-/// the corresponding mono symbol, using `ordered_targets` —
-/// the per-call-site resolved targets collected by a parallel
-/// synth-replay run on the same body.
+/// Iter 23.4: synthesise a monomorphic `FnDef` for a polymorphic
+/// free-fn target. The source body comes directly from the
+/// polymorphic `Def::Fn`'s `body` (NOT from `Registry::entries`);
+/// rigid-var substitution applies the `target.type_args` to the
+/// source `Type::Forall { body }`.
 ///
-/// The walker increments a positional counter at each
-/// class-method-named `Term::Var` it encounters that is NOT
-/// shadowed by a local binding. The counter must match the order
-/// in which `synth` pushes residuals (pre-order AST walk; child
-/// evaluation order matches the `match` arms in [`crate::synth`]).
-/// When this invariant holds, `ordered_targets[idx]` is the target
-/// resolved at the i-th class-method call site.
+/// The body is passed through unchanged — the rewrite walker
+/// (Task 6) handles inner class-method / poly-call rewrites in a
+/// subsequent fixpoint round, mirroring the class-method arm's
+/// body-passthrough pattern.
 ///
-/// `caller_module`: name of the module enclosing this body. If
-/// the target's `defining_module` differs, the rewritten name is
-/// qualified `<defining_module>.<mono_symbol>` (cross-module
-/// resolution path); otherwise unqualified.
+/// Errors are all [`crate::CheckError::Internal`] — caller-contract
+/// violations that cannot occur after typecheck has succeeded.
+pub fn synthesise_mono_fn_for_free_fn(
+    target: &MonoTarget,
+    ws: &Workspace,
+) -> Result<AstFnDef> {
+    let (name, type_args, defining_module) = match target {
+        MonoTarget::FreeFn { name, type_args, defining_module } => {
+            (name, type_args, defining_module)
+        }
+        MonoTarget::ClassMethod { .. } => {
+            return Err(crate::CheckError::Internal(
+                "synthesise_mono_fn_for_free_fn: called with ClassMethod variant; use \
+                 synthesise_mono_fn instead"
+                    .into(),
+            ));
+        }
+    };
+    let source_module = ws.modules.get(defining_module).ok_or_else(|| {
+        crate::CheckError::Internal(format!(
+            "synthesise_mono_fn_for_free_fn: defining module `{}` not in workspace",
+            defining_module
+        ))
+    })?;
+    let source_fn = source_module
+        .defs
+        .iter()
+        .find_map(|d| match d {
+            Def::Fn(f) if &f.name == name => Some(f),
+            _ => None,
+        })
+        .ok_or_else(|| {
+            crate::CheckError::Internal(format!(
+                "synthesise_mono_fn_for_free_fn: no source Def::Fn `{}` in module `{}`",
+                name, defining_module
+            ))
+        })?;
+
+    let (forall_vars, inner_ty) = match &source_fn.ty {
+        Type::Forall { vars, body, .. } => (vars.clone(), (**body).clone()),
+        other => {
+            return Err(crate::CheckError::Internal(format!(
+                "synthesise_mono_fn_for_free_fn: source fn `{}` is not Type::Forall; got {:?}",
+                name, other
+            )));
+        }
+    };
+    if forall_vars.len() != type_args.len() {
+        return Err(crate::CheckError::Internal(format!(
+            "synthesise_mono_fn_for_free_fn: arity mismatch for `{}` — {} forall vars vs {} \
+             type args",
+            name,
+            forall_vars.len(),
+            type_args.len()
+        )));
+    }
+    let mapping: BTreeMap<String, Type> = forall_vars
+        .iter()
+        .cloned()
+        .zip(type_args.iter().cloned())
+        .collect();
+
+    // Apply rigid-var substitution on the function type AND on the
+    // body (the latter required because a free-fn body may contain
+    // inner `Term::Lam` nodes whose `param_tys` / `ret_ty` reference
+    // the outer Forall vars; those references must be substituted
+    // so the post-mono body's re-synth in Phase 3 sees concrete
+    // types throughout).
+    //
+    // The class-method arm in `synthesise_mono_fn` doesn't need
+    // this because instance bodies are Lam-unwrapped during synth
+    // (the outer Lam's `param_tys` are dropped); a free-fn body
+    // can carry arbitrary nested Lams with `Type::Var`-bearing
+    // `param_tys`, which is the case for e.g. `std_list.length`
+    // (an inner accumulating lambda over `(b, a)`).
+    let new_type = crate::substitute_rigids(&inner_ty, &mapping);
+    let new_body = crate::substitute_rigids_in_term(&source_fn.body, &mapping);
+
+    Ok(AstFnDef {
+        name: mono_symbol_n(name, type_args.as_slice()),
+        ty: new_type,
+        params: source_fn.params.clone(),
+        body: new_body,
+        doc: source_fn.doc.clone(),
+        suppress: Vec::new(),
+    })
+}
+
+/// Iter 22b.3 / iter 23.4: rewrite every polymorphic call site in
+/// `body` to the corresponding mono symbol, using `ordered_targets`
+/// — the per-call-site resolved targets collected by a parallel
+/// synth-replay run on the same body via [`collect_residuals_ordered`].
 ///
-/// `locals` mirrors `synth`'s lookup-precedence rule: a `Term::Var`
-/// whose `name` is in `locals` resolves to the local binding and
-/// `synth` pushes NO residual for it, so the walker must NOT
-/// advance the cursor either. Each binding-form pushes its binders
-/// before recursing into the relevant scope and pops them after.
+/// Two kinds of call site trigger cursor advancement:
 ///
-/// `ordered_targets[idx]`:
-/// - `Some(t)` — concrete instance found; rewrite the name.
-/// - `None` — residual was non-concrete or had no instance; cursor
-///   still advances (to keep alignment) but the name is left
-///   unchanged.
-fn rewrite_class_method_calls(
+/// - **Class-method** sites: `Term::Var { name }` where `name` is in
+///   `class_methods`. Synth pushes a residual at such sites.
+/// - **Polymorphic free-fn** sites (iter 23.4): `Term::Var { name }`
+///   where `name` is in `poly_free_fns` (the set of bare + qualified
+///   names that resolve to a `Type::Forall`-quantified `Def::Fn` in
+///   `caller_module`'s scope per `synth`'s Var arm). Synth pushes a
+///   `FreeFnCall` observation at such sites.
+///
+/// Local-shadowed names are skipped in both kinds — synth's
+/// lookup-precedence rule resolves them to the local binding and
+/// pushes nothing, so the walker must not advance either.
+///
+/// At a matching cursor position, the slot's `MonoTarget` variant
+/// drives the rewrite:
+///
+/// - `ClassMethod`: `<method>__<typesurfacename>`, possibly
+///   `<defining_module>.<...>` if cross-module.
+/// - `FreeFn`: `<name>__<typesurfacename1>__<typesurfacename2>__…`,
+///   possibly `<defining_module>.<...>` if cross-module.
+/// - `None` (slot is None): residual was non-concrete or instance
+///   not registered; cursor still advances (to keep alignment) but
+///   the name is left unchanged.
+fn rewrite_mono_calls(
     body: &mut Term,
     class_methods: &BTreeMap<String, crate::ClassMethodEntry>,
+    poly_free_fns: &BTreeSet<String>,
     caller_module: &str,
     ordered_targets: &[Option<MonoTarget>],
     cursor: &mut usize,
@@ -644,83 +915,85 @@ fn rewrite_class_method_calls(
 ) {
     match body {
         Term::Var { name } => {
-            if class_methods.contains_key(name) {
-                // Mirror synth's lookup-precedence rule: if `name` is
-                // shadowed by a local, synth resolves to the local
-                // and pushes no residual — we must not advance.
-                if locals.contains(name) {
-                    return;
-                }
+            // Two-way predicate: cursor advances at any Term::Var
+            // whose name synth would resolve to either a class-method
+            // residual OR a poly-free-fn observation. Locally
+            // shadowed names match neither — synth pushes nothing.
+            let is_class_method = class_methods.contains_key(name);
+            let is_poly_free_fn = !is_class_method && poly_free_fns.contains(name);
+            let should_advance = (is_class_method || is_poly_free_fn) && !locals.contains(name);
+            if should_advance {
                 if let Some(slot) = ordered_targets.get(*cursor) {
                     if let Some(t) = slot {
-                        let sym = mono_symbol(&t.method, &t.type_);
-                        let new_name = if t.defining_module == caller_module {
+                        let (sym, defining_module) = match t {
+                            MonoTarget::ClassMethod { method, type_, defining_module, .. } => {
+                                (mono_symbol(method, type_), defining_module.as_str())
+                            }
+                            MonoTarget::FreeFn { name: fn_name, type_args, defining_module } => {
+                                (mono_symbol_n(fn_name, type_args.as_slice()), defining_module.as_str())
+                            }
+                        };
+                        let new_name = if defining_module == caller_module {
                             sym
                         } else {
-                            format!("{}.{}", t.defining_module, sym)
+                            format!("{}.{}", defining_module, sym)
                         };
                         *name = new_name;
                     }
-                    // else: residual was non-concrete → leave name unchanged.
+                    // else: residual / observation was non-concrete →
+                    // leave name unchanged.
                 }
                 *cursor += 1;
             }
         }
         Term::App { callee, args, .. } => {
-            rewrite_class_method_calls(callee, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(callee, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             for a in args {
-                rewrite_class_method_calls(a, class_methods, caller_module, ordered_targets, cursor, locals);
+                rewrite_mono_calls(a, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             }
         }
         Term::Let { name, value, body } => {
-            // synth: `value` is in the outer scope; `body` sees `name`.
-            rewrite_class_method_calls(value, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(value, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             let inserted = locals.insert(name.clone());
-            rewrite_class_method_calls(body, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(body, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             if inserted {
                 locals.remove(name);
             }
         }
         Term::LetRec { name, params, body, in_term, .. } => {
-            // synth: `name` is in scope in BOTH `body` (with `params`
-            // also in scope) AND `in_term` (without `params`).
             let name_inserted = locals.insert(name.clone());
-            // Body scope: name + params.
             let mut params_inserted: Vec<String> = Vec::new();
             for p in params {
                 if locals.insert(p.clone()) {
                     params_inserted.push(p.clone());
                 }
             }
-            rewrite_class_method_calls(body, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(body, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             for p in &params_inserted {
                 locals.remove(p);
             }
-            // In-clause scope: name only.
-            rewrite_class_method_calls(in_term, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(in_term, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             if name_inserted {
                 locals.remove(name);
             }
         }
         Term::If { cond, then, else_ } => {
-            rewrite_class_method_calls(cond, class_methods, caller_module, ordered_targets, cursor, locals);
-            rewrite_class_method_calls(then, class_methods, caller_module, ordered_targets, cursor, locals);
-            rewrite_class_method_calls(else_, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(cond, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(then, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(else_, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
         }
         Term::Do { args, .. } => {
             for a in args {
-                rewrite_class_method_calls(a, class_methods, caller_module, ordered_targets, cursor, locals);
+                rewrite_mono_calls(a, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             }
         }
         Term::Ctor { args, .. } => {
             for a in args {
-                rewrite_class_method_calls(a, class_methods, caller_module, ordered_targets, cursor, locals);
+                rewrite_mono_calls(a, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             }
         }
         Term::Match { scrutinee, arms } => {
-            // synth: scrutinee is in outer scope; each arm's body sees
-            // its pattern's binders.
-            rewrite_class_method_calls(scrutinee, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(scrutinee, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             for Arm { pat, body } in arms {
                 let binders = pattern_binders(pat);
                 let mut inserted: Vec<String> = Vec::new();
@@ -729,35 +1002,34 @@ fn rewrite_class_method_calls(
                         inserted.push(b.clone());
                     }
                 }
-                rewrite_class_method_calls(body, class_methods, caller_module, ordered_targets, cursor, locals);
+                rewrite_mono_calls(body, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
                 for b in &inserted {
                     locals.remove(b);
                 }
             }
         }
         Term::Lam { params, body, .. } => {
-            // synth: params are in scope in `body`.
             let mut inserted: Vec<String> = Vec::new();
             for p in params {
                 if locals.insert(p.clone()) {
                     inserted.push(p.clone());
                 }
             }
-            rewrite_class_method_calls(body, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(body, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
             for p in &inserted {
                 locals.remove(p);
             }
         }
         Term::Seq { lhs, rhs } => {
-            rewrite_class_method_calls(lhs, class_methods, caller_module, ordered_targets, cursor, locals);
-            rewrite_class_method_calls(rhs, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(lhs, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(rhs, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
         }
         Term::Clone { value } => {
-            rewrite_class_method_calls(value, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(value, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
         }
         Term::ReuseAs { source, body } => {
-            rewrite_class_method_calls(source, class_methods, caller_module, ordered_targets, cursor, locals);
-            rewrite_class_method_calls(body, class_methods, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(source, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
+            rewrite_mono_calls(body, class_methods, poly_free_fns, caller_module, ordered_targets, cursor, locals);
         }
         Term::Lit { .. } => {}
     }
@@ -794,6 +1066,7 @@ pub(crate) fn collect_residuals_ordered(
     f: &AstFnDef,
     module_name: &str,
     env: &crate::Env,
+    poly_free_fns: &BTreeSet<String>,
 ) -> Result<Vec<Option<MonoTarget>>> {
     let (rigids, inner_ty): (Vec<String>, Type) = match &f.ty {
         Type::Forall { vars, constraints: _, body } => (vars.clone(), (**body).clone()),
@@ -831,6 +1104,7 @@ pub(crate) fn collect_residuals_ordered(
     let mut subst = crate::Subst::default();
     let mut counter: u32 = 0;
     let mut residuals: Vec<crate::ResidualConstraint> = Vec::new();
+    let mut free_fn_calls: Vec<crate::FreeFnCall> = Vec::new();
     crate::synth(
         &f.body,
         &env,
@@ -840,31 +1114,207 @@ pub(crate) fn collect_residuals_ordered(
         &mut subst,
         &mut counter,
         &mut residuals,
+        &mut free_fn_calls,
     )?;
 
-    let mut out: Vec<Option<MonoTarget>> = Vec::new();
-    for r in residuals {
-        let r_ty = subst.apply(&r.type_);
-        if !crate::is_fully_concrete(&r_ty) {
-            out.push(None);
-            continue;
-        }
-        // normalize to match Registry::normalize_type_for_lookup contract
-        let r_ty_norm = env.workspace_registry.normalize_type_for_lookup(&r_ty);
-        let key = (r.class.clone(), ailang_core::canonical::type_hash(&r_ty_norm));
-        let entry = match env.workspace_registry.entries.get(&key) {
-            Some(e) => e,
-            None => {
-                out.push(None);
-                continue;
+    // Iter 23.4 Task 6: build two per-channel slot lists — one for
+    // class-method residuals, one for poly-free-fn observations —
+    // each in synth's push order. Then walk the AST in synth's
+    // traversal order, classifying each `Term::Var` site as
+    // class-method, poly-free-fn, or neither (and consuming from
+    // the appropriate channel). The output slot list interleaves
+    // the two channels in source-AST order; the rewrite walker
+    // consumes it with a single cursor.
+    let class_slots: Vec<Option<MonoTarget>> = residuals
+        .into_iter()
+        .map(|r| {
+            let r_ty = subst.apply(&r.type_);
+            if !crate::is_fully_concrete(&r_ty) {
+                return None;
             }
-        };
-        out.push(Some(MonoTarget {
-            class: r.class.clone(),
-            method: r.method.clone(),
-            type_: r_ty,
-            defining_module: entry.defining_module.clone(),
-        }));
-    }
+            let r_ty_norm = env.workspace_registry.normalize_type_for_lookup(&r_ty);
+            let key = (r.class.clone(), ailang_core::canonical::type_hash(&r_ty_norm));
+            let entry = env.workspace_registry.entries.get(&key)?;
+            Some(MonoTarget::ClassMethod {
+                class: r.class.clone(),
+                method: r.method.clone(),
+                type_: r_ty,
+                defining_module: entry.defining_module.clone(),
+            })
+        })
+        .collect();
+    let free_fn_slots: Vec<Option<MonoTarget>> = free_fn_calls
+        .iter()
+        .map(|fc| {
+            // Mirrors `collect_mono_targets`'s Unit-default for unpinned
+            // forall vars. Per-meta resolution: pinned → keep; unpinned
+            // → `Type::unit()`. This ensures the cursor-walker emits a
+            // Some(target) at every poly-free-fn call site, so the
+            // rewrite walker's cursor advancement maps to a real
+            // mono-symbol rewrite (no `None`-slots from this channel).
+            let type_args: Vec<Type> = fc
+                .metas
+                .iter()
+                .map(|m| {
+                    let resolved = subst.apply(m);
+                    if crate::is_fully_concrete(&resolved) {
+                        resolved
+                    } else {
+                        Type::unit()
+                    }
+                })
+                .collect();
+            Some(MonoTarget::FreeFn {
+                name: fc.name.clone(),
+                type_args,
+                defining_module: fc.owner_module.clone(),
+            })
+        })
+        .collect();
+
+    // Walk the AST in the same pre-order the rewrite walker uses
+    // (which mirrors synth's traversal order). At each Term::Var
+    // matching `class_methods` or `poly_free_fns` (and not locally
+    // shadowed), emit one slot consuming from the appropriate
+    // channel. The resulting Vec is in interleaved walker-order,
+    // ready for the rewrite walker's single-cursor consumption.
+    let mut out: Vec<Option<MonoTarget>> = Vec::new();
+    let mut class_cur = 0usize;
+    let mut free_cur = 0usize;
+    let mut walker_locals: BTreeSet<String> = f.params.iter().cloned().collect();
+    interleave_slots(
+        &f.body,
+        &env.class_methods,
+        poly_free_fns,
+        &class_slots,
+        &free_fn_slots,
+        &mut class_cur,
+        &mut free_cur,
+        &mut walker_locals,
+        &mut out,
+    );
     Ok(out)
 }
+
+/// Iter 23.4 helper for `collect_residuals_ordered`: walk a body
+/// in synth's traversal order, interleaving class-method and
+/// poly-free-fn slots in source-AST order. The walker MUST stay
+/// in lockstep with `rewrite_mono_calls` — same predicates, same
+/// shadowing handling.
+#[allow(clippy::too_many_arguments)]
+fn interleave_slots(
+    term: &Term,
+    class_methods: &BTreeMap<String, crate::ClassMethodEntry>,
+    poly_free_fns: &BTreeSet<String>,
+    class_slots: &[Option<MonoTarget>],
+    free_fn_slots: &[Option<MonoTarget>],
+    class_cur: &mut usize,
+    free_cur: &mut usize,
+    locals: &mut BTreeSet<String>,
+    out: &mut Vec<Option<MonoTarget>>,
+) {
+    match term {
+        Term::Var { name } => {
+            let is_class_method = class_methods.contains_key(name);
+            let is_poly_free_fn = !is_class_method && poly_free_fns.contains(name);
+            let advances = (is_class_method || is_poly_free_fn) && !locals.contains(name);
+            if advances {
+                if is_class_method {
+                    let slot = class_slots.get(*class_cur).cloned().unwrap_or(None);
+                    out.push(slot);
+                    *class_cur += 1;
+                } else {
+                    let slot = free_fn_slots.get(*free_cur).cloned().unwrap_or(None);
+                    out.push(slot);
+                    *free_cur += 1;
+                }
+            }
+        }
+        Term::App { callee, args, .. } => {
+            interleave_slots(callee, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            for a in args {
+                interleave_slots(a, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+        }
+        Term::Let { name, value, body } => {
+            interleave_slots(value, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            let inserted = locals.insert(name.clone());
+            interleave_slots(body, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            if inserted {
+                locals.remove(name);
+            }
+        }
+        Term::LetRec { name, params, body, in_term, .. } => {
+            let name_inserted = locals.insert(name.clone());
+            let mut params_inserted: Vec<String> = Vec::new();
+            for p in params {
+                if locals.insert(p.clone()) {
+                    params_inserted.push(p.clone());
+                }
+            }
+            interleave_slots(body, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            for p in &params_inserted {
+                locals.remove(p);
+            }
+            interleave_slots(in_term, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            if name_inserted {
+                locals.remove(name);
+            }
+        }
+        Term::If { cond, then, else_ } => {
+            interleave_slots(cond, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            interleave_slots(then, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            interleave_slots(else_, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::Do { args, .. } => {
+            for a in args {
+                interleave_slots(a, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+        }
+        Term::Ctor { args, .. } => {
+            for a in args {
+                interleave_slots(a, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+        }
+        Term::Match { scrutinee, arms } => {
+            interleave_slots(scrutinee, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            for Arm { pat, body } in arms {
+                let binders = pattern_binders(pat);
+                let mut inserted: Vec<String> = Vec::new();
+                for b in &binders {
+                    if locals.insert(b.clone()) {
+                        inserted.push(b.clone());
+                    }
+                }
+                interleave_slots(body, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+                for b in &inserted {
+                    locals.remove(b);
+                }
+            }
+        }
+        Term::Lam { params, body, .. } => {
+            let mut inserted: Vec<String> = Vec::new();
+            for p in params {
+                if locals.insert(p.clone()) {
+                    inserted.push(p.clone());
+                }
+            }
+            interleave_slots(body, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            for p in &inserted {
+                locals.remove(p);
+            }
+        }
+        Term::Seq { lhs, rhs } => {
+            interleave_slots(lhs, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            interleave_slots(rhs, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::Clone { value } => {
+            interleave_slots(value, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::ReuseAs { source, body } => {
+            interleave_slots(source, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            interleave_slots(body, class_methods, poly_free_fns, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::Lit { .. } => {}
+    }
+}
diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs
index 9455490..f68cea3 100644
--- a/crates/ailang-codegen/src/lib.rs
+++ b/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))
     }
diff --git a/crates/ailang-codegen/src/subst.rs b/crates/ailang-codegen/src/subst.rs
index b83d1eb..4b5509c 100644
--- a/crates/ailang-codegen/src/subst.rs
+++ b/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`).
diff --git a/crates/ailang-codegen/src/synth.rs b/crates/ailang-codegen/src/synth.rs
index daa8448..2baa01b 100644
--- a/crates/ailang-codegen/src/synth.rs
+++ b/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
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 40ecf9d..391ba83 100644
--- a/docs/DESIGN.md
+++ b/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
 
diff --git a/docs/journals/2026-05-11-iter-23.4.md b/docs/journals/2026-05-11-iter-23.4.md
new file mode 100644
index 0000000..3e87e2f
--- /dev/null
+++ b/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
diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md
index 8f6ae86..57ad1e0 100644
--- a/docs/journals/INDEX.md
+++ b/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
diff --git a/examples/cmp_max_smoke.ail.json b/examples/cmp_max_smoke.ail.json
new file mode 100644
index 0000000..8e56e42
--- /dev/null
+++ b/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 } }
+          ]
+        }]
+      }
+    }
+  ]
+}
diff --git a/examples/mono_hash_pin_smoke.ail.json b/examples/mono_hash_pin_smoke.ail.json
new file mode 100644
index 0000000..6a6aa2d
--- /dev/null
+++ b/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" } }
+                      ]
+                    }]
+                  }]
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  ]
+}