//! Iter 22b.3: monomorphisation pass tests.
//!
//! Co-located with `typeclass_22b2.rs` so the typeclass-feature
//! coverage is browsable in one directory. Tests use the same
//! `examples_dir()` pattern — `cargo test`-cwd is the crate dir,
//! the fixtures live in `<repo>/examples/`.

use ailang_core::ast::Type;
use std::path::PathBuf;

fn examples_dir() -> PathBuf {
    // crates/ail/ → repo root → examples/
    let mut d = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
    d.pop();
    d.pop();
    d.join("examples")
}

#[test]
fn monomorphise_workspace_is_identity_on_class_free_workspace() {
    // Pick any class-free fixture; `examples/hello.ail.json` is
    // the canonical class-free smoke test.
    let entry = examples_dir().join("hello.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    let ws = ailang_check::monomorphise_workspace(&ws)
        .expect("mono on class-free workspace");

    // Module set unchanged.
    let before = ailang_core::load_workspace(&examples_dir().join("hello.ail.json"))
        .expect("re-load");
    assert_eq!(
        ws.modules.keys().collect::<Vec<_>>(),
        before.modules.keys().collect::<Vec<_>>(),
        "module set must be identical"
    );
    // Per-module def list unchanged (compare by canonical-JSON hash).
    for (mname, m) in &ws.modules {
        let before_m = &before.modules[mname];
        let h_after = ailang_core::module_hash(m);
        let h_before = ailang_core::module_hash(before_m);
        assert_eq!(
            h_after, h_before,
            "class-free module `{}` must hash-identical through mono",
            mname
        );
    }
}

/// Property: when a workspace has a class + instance but no concrete
/// class-method call sites, the mono pass produces a hash-identical
/// workspace — the early-out path is bypassed (typeclasses present)
/// but the fixpoint loop terminates on round 1 with zero new targets,
/// so no FnDefs are appended.
///
/// The fixture (`test_22b3_no_call_sites.ail.json`) declares
/// `class Show` + `instance Show Int` with a Lam-shaped instance
/// body, but `main` is a literal — there is no `show <x>` call at any
/// type. Updated in Task 5 from `test_22b2_instance_present.ail.json`,
/// which had a `show 42` call site that the real fixpoint now
/// (correctly) materialises into `show__Int`.
#[test]
fn monomorphise_workspace_is_identity_when_no_concrete_call_sites() {
    let entry = examples_dir().join("test_22b3_no_call_sites.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    let ws_after = ailang_check::monomorphise_workspace(&ws)
        .expect("mono on class-present workspace");

    // Module set unchanged.
    let before = ailang_core::load_workspace(&entry).expect("re-load");
    assert_eq!(
        ws_after.modules.keys().collect::<Vec<_>>(),
        before.modules.keys().collect::<Vec<_>>(),
        "module set must be identical"
    );
    // Each module hashes byte-identical — no synth fns appended
    // because no call site triggered a target.
    for (mname, m) in &ws_after.modules {
        let before_m = &before.modules[mname];
        let h_after = ailang_core::module_hash(m);
        let h_before = ailang_core::module_hash(before_m);
        assert_eq!(
            h_after, h_before,
            "class-present-but-no-call-site module `{}` must hash-identical",
            mname
        );
    }
}

#[test]
fn mono_symbol_primitive_types_use_surface_form() {
    // Primitive-type forms must be human-readable in diagnostics
    // and ABI symbols. Per the spec's mono-symbol naming guidance:
    // <method>#<surface-name> for primitives.
    let int_ty = Type::int();
    let bool_ty = Type::bool_();
    let str_ty = Type::str_();
    let unit_ty = Type::unit();

    assert_eq!(ailang_check::mono::mono_symbol("show", &int_ty), "show__Int");
    assert_eq!(ailang_check::mono::mono_symbol("eq", &bool_ty), "eq__Bool");
    assert_eq!(ailang_check::mono::mono_symbol("show", &str_ty), "show__Str");
    assert_eq!(ailang_check::mono::mono_symbol("foo", &unit_ty), "foo__Unit");
}

/// Property: collect_mono_targets returns exactly the set of
/// fully-concrete `(class, method, type)` triples observed at
/// class-method call sites in a fn body, with the registry's
/// `defining_module` attached to each. The fixture's `main` calls
/// `show 42` once with `Int`, and the workspace declares
/// `instance Show Int` in the same module — the expected output is
/// a single MonoTarget naming `Show`, `show`, `Int`, and that
/// module.
#[test]
fn collect_mono_targets_single_concrete_call_site() {
    use ailang_check::mono::collect_mono_targets;

    let entry = examples_dir().join("test_22b2_instance_present.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    // Build the workspace-wide env (class_methods, registry, ...)
    // exactly as `check_in_workspace` does. The mono pass exposes
    // this via `build_workspace_env`.
    let env = ailang_check::mono::build_workspace_env(&ws);

    // The fixture has one user fn — `main`. Locate it.
    let main_module = ws.modules.get("test_22b2_instance_present").expect("module");
    let main_fn = main_module
        .defs
        .iter()
        .find_map(|d| match d {
            ailang_core::ast::Def::Fn(f) if f.name == "main" => Some(f),
            _ => None,
        })
        .expect("main fn");

    let targets = collect_mono_targets(main_fn, "test_22b2_instance_present", &env)
        .expect("collect");

    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");
}

#[test]
fn mono_symbol_compound_type_uses_hash_suffix() {
    // Compound types fall through to canonical type_hash with an
    // 8-hex-char prefix. Stability matters more than legibility
    // here — same input must produce the same name across runs.
    let pair_ty = Type::Con {
        name: "Pair".into(),
        args: vec![Type::int(), Type::bool_()],
    };
    let name = ailang_check::mono::mono_symbol("show", &pair_ty);

    // Format: `show__<8-hex-chars>`.
    assert!(name.starts_with("show__"), "name = {name}");
    let suffix = &name["show__".len()..];
    assert_eq!(suffix.len(), 8, "compound suffix is 8 hex chars: {suffix}");
    assert!(
        suffix.chars().all(|c| c.is_ascii_hexdigit()),
        "compound suffix must be hex: {suffix}"
    );

    // Stability: a second call with the same type produces the same name.
    let again = ailang_check::mono::mono_symbol("show", &pair_ty);
    assert_eq!(name, again, "mono_symbol must be deterministic");
}

/// Property: synthesise_mono_fn copies the matching instance method's
/// body verbatim and produces a fully-concrete `FnDef` whose name uses
/// the `mono_symbol` form, whose `ty` is the class method's declared
/// type with the class param substituted to the target type, and whose
/// `params` / `body` come from the instance's `Term::Lam`.
#[test]
fn synthesise_mono_fn_uses_instance_body_lam() {
    use ailang_check::mono::{synthesise_mono_fn, MonoTarget};
    use ailang_core::ast::{ClassDef, ClassMethod, InstanceDef, InstanceMethod, Term};

    let class_def = ClassDef {
        name: "Foo".into(),
        param: "a".into(),
        superclass: None,
        methods: vec![ClassMethod {
            name: "bar".into(),
            ty: Type::Fn {
                params: vec![Type::Var { name: "a".into() }],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ailang_core::ast::ParamMode::Implicit,
            },
            default: None,
        }],
        doc: None,
    };
    let instance = InstanceDef {
        class: "Foo".into(),
        type_: Type::int(),
        methods: vec![InstanceMethod {
            name: "bar".into(),
            body: Term::Lam {
                params: vec!["i".into()],
                param_tys: vec![Type::Var { name: "a".into() }],
                ret_ty: Box::new(Type::int()),
                effects: vec![],
                body: Box::new(Term::Var { name: "i".into() }),
            },
        }],
        doc: None,
    };
    let target = MonoTarget {
        class: "Foo".into(),
        method: "bar".into(),
        type_: Type::int(),
        defining_module: "m".into(),
    };

    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
    assert_eq!(f.name, "bar__Int");
    assert!(
        matches!(
            &f.ty,
            Type::Fn { params, ret, .. }
                if params.len() == 1
                && matches!(&params[0], Type::Con { name, args } if name == "Int" && args.is_empty())
                && matches!(ret.as_ref(), Type::Con { name, args } if name == "Int" && args.is_empty())
        ),
        "ty = {:?}",
        f.ty
    );
    assert_eq!(f.params, vec!["i".to_string()]);
    assert!(
        matches!(&f.body, Term::Var { name } if name == "i"),
        "body = {:?}",
        f.body
    );
}

/// Property: when the instance omits a method that has a class-level
/// `default` body, synthesise_mono_fn falls back to that default and
/// uses its params/body verbatim — registry-build's `MissingMethod`
/// has already enforced that one of the two is present.
#[test]
fn synthesise_mono_fn_falls_back_to_class_default() {
    use ailang_check::mono::{synthesise_mono_fn, MonoTarget};
    use ailang_core::ast::{ClassDef, ClassMethod, InstanceDef, Literal, Term};

    let class_def = ClassDef {
        name: "Greet".into(),
        param: "a".into(),
        superclass: None,
        methods: vec![ClassMethod {
            name: "hello".into(),
            ty: Type::Fn {
                params: vec![Type::Var { name: "a".into() }],
                ret: Box::new(Type::str_()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ailang_core::ast::ParamMode::Implicit,
            },
            default: Some(Term::Lam {
                params: vec!["_x".into()],
                param_tys: vec![Type::Var { name: "a".into() }],
                ret_ty: Box::new(Type::str_()),
                effects: vec![],
                body: Box::new(Term::Lit {
                    lit: Literal::Str { value: "hi".into() },
                }),
            }),
        }],
        doc: None,
    };
    // Instance carries no `hello` body — must fall back to default.
    let instance = InstanceDef {
        class: "Greet".into(),
        type_: Type::int(),
        methods: vec![],
        doc: None,
    };
    let target = MonoTarget {
        class: "Greet".into(),
        method: "hello".into(),
        type_: Type::int(),
        defining_module: "m".into(),
    };

    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
    assert_eq!(f.name, "hello__Int");
    assert_eq!(
        f.params.len(),
        1,
        "default-fallback Lam carries 1 param: {:?}",
        f.params
    );
    assert!(matches!(&f.body, Term::Lit { .. }), "body = {:?}", f.body);
}

/// Zero-arg method (no positional params): body is used verbatim
/// without Lam-unwrapping. Class `Foo a where bar : Int` (note: no
/// arrow — the method is a constant), instance `Foo Int where bar
/// = 7`. synthesise_mono_fn must produce
/// `FnDef { name: "bar__Int", ty: Int, params: [], body: Lit 7 }`.
#[test]
fn synthesise_mono_fn_zero_arg_method_uses_body_verbatim() {
    use ailang_check::mono::{synthesise_mono_fn, MonoTarget};
    use ailang_core::ast::{ClassDef, ClassMethod, InstanceDef, InstanceMethod, Literal, Term};

    let class_def = ClassDef {
        name: "Foo".into(),
        param: "a".into(),
        superclass: None,
        methods: vec![ClassMethod {
            name: "bar".into(),
            // Zero-arg method: ty is the value type directly, not a Type::Fn.
            ty: Type::int(),
            default: None,
        }],
        doc: None,
    };
    let instance = InstanceDef {
        class: "Foo".into(),
        type_: Type::int(),
        methods: vec![InstanceMethod {
            name: "bar".into(),
            // Body is a value directly — no Lam wrapper.
            body: Term::Lit {
                lit: Literal::Int { value: 7 },
            },
        }],
        doc: None,
    };
    let target = MonoTarget {
        class: "Foo".into(),
        method: "bar".into(),
        type_: Type::int(),
        defining_module: "m".into(),
    };

    let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth");
    assert_eq!(f.name, "bar__Int");
    assert!(
        f.params.is_empty(),
        "zero-arg method must produce empty params"
    );
    assert!(
        matches!(&f.body, Term::Lit { lit: Literal::Int { value: 7 } }),
        "body must be the verbatim Lit, got {:?}",
        f.body
    );
}

/// Property: when two call sites of `show` apply at the same concrete
/// type (Int), the workspace fixpoint synthesises the matching FnDef
/// (`show__Int`) exactly once across the whole workspace. Verifies the
/// dedup contract — the pass must not emit one FnDef per call site.
#[test]
fn fixpoint_dedupes_repeated_calls_at_same_type() {
    let entry = examples_dir().join("test_22b3_dup_call_sites.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    let ws = ailang_check::monomorphise_workspace(&ws).expect("mono");

    // Count `show__Int` fns workspace-wide.
    let mut count = 0usize;
    for m in ws.modules.values() {
        for d in &m.defs {
            if let ailang_core::ast::Def::Fn(f) = d {
                if f.name == "show__Int" {
                    count += 1;
                }
            }
        }
    }
    assert_eq!(count, 1, "exactly one show__Int across the workspace");
}

/// Property: when a synthesised instance body itself calls another class
/// method (the canonical `Eq.ne x y = not (eq x y)` shape), the workspace
/// fixpoint closes over the chained call — Round 1 synthesises the outer
/// fn, Round 2 picks up the inner class-method residual on the freshly-
/// appended body and synthesises that. Without the multi-round loop, the
/// inner mono fn would be missing.
///
/// Fixture (`test_22b3_chained_calls`):
///   class B a where b_method : (a) -> Int
///   class A a where a_method : (a) -> Int  default \x. b_method x
///   instance B Int { b_method = \y. y }
///   instance A Int { /* uses class default */ }
///   main : () -> Int = a_method 5
///
/// Expected post-mono workspace contents: BOTH `a_method__Int` (Round 1,
/// from the class default) AND `b_method__Int` (Round 2, from instance B's
/// body).
#[test]
fn fixpoint_handles_chained_class_method_calls() {
    let entry = examples_dir().join("test_22b3_chained_calls.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    let ws = ailang_check::monomorphise_workspace(&ws).expect("mono");

    // Locate both synthesised fns workspace-wide.
    let mut has_a_method_int = false;
    let mut has_b_method_int = false;
    for m in ws.modules.values() {
        for d in &m.defs {
            if let ailang_core::ast::Def::Fn(f) = d {
                if f.name == "a_method__Int" {
                    has_a_method_int = true;
                }
                if f.name == "b_method__Int" {
                    has_b_method_int = true;
                }
            }
        }
    }
    assert!(
        has_a_method_int,
        "a_method__Int must be synthesised in Round 1 from main's call site"
    );
    assert!(
        has_b_method_int,
        "b_method__Int must be synthesised in Round 2 from a_method__Int's body \
         — multi-round fixpoint property"
    );
}

/// Property: when a fn's body locally shadows a class-method name
/// (here `show` is rebound by a `let`-binding), synth resolves the
/// shadowed `Var` against the local and pushes NO residual for it.
/// The rewrite walker must mirror that exact lookup-precedence rule
/// — when a `Term::Var { name }` is in the local scope, the walker
/// must NOT advance the per-callsite cursor. Otherwise a subsequent
/// (real) class-method call site is re-aligned to the wrong slot of
/// `ordered_targets`, and the user-visible diff is two corruptions:
/// the shadowed Var gets a wrong mono-symbol, and the next real call
/// site is left un-rewritten (or rewritten to yet another mismatched
/// target).
///
/// Body shape (`main`):
///   let _t = show 5 in                  -- residual #0: show@Int
///     let show = "shadow" in             -- shadow `show`
///       let _u = show in                  -- shadowed Var (no residual)
///         foo 7                            -- residual #1: foo@Int
///
/// `synth` pushes exactly two residuals (in order: show@Int, foo@Int).
/// The shadow-aware walker must:
///   - rewrite the outer `show` callee → `show__Int`,
///   - leave the inner shadowed `show` Var literally as `show`,
///   - rewrite the `foo` callee → `foo__Int`.
///
/// A shadow-blind walker would advance the cursor on the inner Var,
/// rewriting it to `foo__Int` (using residual #1) AND leaving the real
/// `foo 7` callee untouched (cursor walks off the end of the slice).
#[test]
fn rewrite_walker_skips_locally_shadowed_class_method() {
    use ailang_core::ast::{Def, Term};

    let entry = examples_dir().join("test_22b3_shadow_class_method.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    let ws = ailang_check::monomorphise_workspace(&ws).expect("mono");

    let main_module = ws.modules.get("test_22b3_shadow_class_method").unwrap();
    let main_fn = main_module
        .defs
        .iter()
        .find_map(|d| match d {
            Def::Fn(f) if f.name == "main" => Some(f),
            _ => None,
        })
        .expect("main");

    // Body: Let _t (= App show 5) (Let show "shadow" (Let _u (Var show) (App foo 7)))
    let (outer_value, outer_body): (&Term, &Term) = match &main_fn.body {
        Term::Let { value, body, .. } => (value.as_ref(), body.as_ref()),
        other => panic!("outer body is not Let: {:?}", other),
    };
    let outer_callee = match outer_value {
        Term::App { callee, .. } => match callee.as_ref() {
            Term::Var { name } => name.as_str(),
            other => panic!("outer callee is not Var: {:?}", other),
        },
        other => panic!("outer value is not App: {:?}", other),
    };
    assert_eq!(
        outer_callee, "show__Int",
        "the outer class-method call site must be rewritten to show__Int"
    );

    // Step inside `let show = "shadow" in <body>`.
    let shadow_let_body = match outer_body {
        Term::Let { name, body, .. } => {
            assert_eq!(name, "show", "expected shadowing let to bind `show`");
            body.as_ref()
        }
        other => panic!("expected shadowing Let, got {:?}", other),
    };
    // Step inside `let _u = <Var show> in <foo-call>`.
    let (inner_value, inner_body): (&Term, &Term) = match shadow_let_body {
        Term::Let { value, body, .. } => (value.as_ref(), body.as_ref()),
        other => panic!("expected inner Let, got {:?}", other),
    };
    let shadowed_var_name = match inner_value {
        Term::Var { name } => name.as_str(),
        other => panic!("inner value is not Var: {:?}", other),
    };
    // The locally-shadowed `show` Var must NOT be rewritten.
    assert_eq!(
        shadowed_var_name, "show",
        "locally-shadowed `show` Var must remain literal `show`, \
         not be re-aligned to a later residual slot"
    );
    // The real `foo 7` call site — the second residual — must be
    // rewritten correctly to `foo__Int`. A shadow-blind walker would
    // have spent residual #1 on the shadowed Var and left this Var
    // untouched.
    let foo_callee = match inner_body {
        Term::App { callee, .. } => match callee.as_ref() {
            Term::Var { name } => name.as_str(),
            other => panic!("foo callee is not Var: {:?}", other),
        },
        other => panic!("expected App for `foo 7`, got {:?}", other),
    };
    assert_eq!(
        foo_callee, "foo__Int",
        "the post-shadow `foo` call site must align to residual #1"
    );
}

/// Property: a class-method call site in module A whose `defining_module`
/// (per the registry's instance entry) is module B is rewritten to the
/// qualified name `<B>.<mono_symbol>` — defending the cross-module
/// resolution branch in the walker. Also asserts the synth-def
/// placement contract: the synthesised FnDef lives in B, not A.
#[test]
fn rewrite_uses_qualified_name_for_cross_module_call_site() {
    let entry = examples_dir().join("test_22b2_xmod_instance_present.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    let ws = ailang_check::monomorphise_workspace(&ws).expect("mono");

    let main_module = ws.modules.get("test_22b2_xmod_instance_present").unwrap();
    let main_fn = main_module
        .defs
        .iter()
        .find_map(|d| match d {
            ailang_core::ast::Def::Fn(f) if f.name == "main" => Some(f),
            _ => None,
        })
        .expect("main");

    let callee_name: &str = match &main_fn.body {
        ailang_core::ast::Term::App { callee, .. } => match callee.as_ref() {
            ailang_core::ast::Term::Var { name } => name.as_str(),
            other => panic!("callee is not Var: {:?}", other),
        },
        other => panic!("body is not App: {:?}", other),
    };
    // class+instance live in test_22b2_xmod_classmod; caller in
    // test_22b2_xmod_instance_present → qualified call.
    assert_eq!(callee_name, "test_22b2_xmod_classmod.show__Int");

    // Placement: the synthesised def must live in the defining module,
    // not the caller's module.
    let classmod = ws.modules.get("test_22b2_xmod_classmod").unwrap();
    let has_synth = classmod.defs.iter().any(|d| {
        matches!(d, ailang_core::ast::Def::Fn(f) if f.name == "show__Int")
    });
    assert!(
        has_synth,
        "show__Int must live in the instance's defining module"
    );
    let caller_has_synth = main_module.defs.iter().any(|d| {
        matches!(d, ailang_core::ast::Def::Fn(f) if f.name == "show__Int")
    });
    assert!(
        !caller_has_synth,
        "show__Int must NOT live in the caller's module"
    );
}

/// Iter 22b.3.7 GATING: the synthetic class+instance fixture must
/// typecheck cleanly under `check_workspace`. Pre-condition for the
/// end-to-end run gate (`synthetic_fixture_runs_and_prints_five`):
/// if the fixture is ill-typed, the run gate's failure mode would
/// be ambiguous between mono-pass bug and 22b.2 typecheck bug.
#[test]
fn synthetic_fixture_typechecks_clean() {
    let entry = examples_dir().join("test_22b3_mono_synthetic.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);
}

/// Iter 22b.3.7 GATING: the synthetic class+instance fixture must
/// build via `ail run` and emit `5\n` to stdout. This is the
/// spec's close-out criterion for 22b.3 — proves the full mono
/// pipeline (class declaration + instance + class-method call site
/// → synthesised concrete fn + rewritten call site → codegen + run)
/// is end-to-end-correct independently of the Prelude (22b.4).
#[test]
fn synthetic_fixture_runs_and_prints_five() {
    let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
    let ail_bin = std::env::var("CARGO_BIN_EXE_ail")
        .expect("CARGO_BIN_EXE_ail set by cargo test");
    let fixture = examples_dir().join("test_22b3_mono_synthetic.ail.json");

    let tmp = manifest_dir.join("target").join(format!(
        "test_22b3_synthetic_{}", std::process::id()
    ));
    std::fs::create_dir_all(&tmp).expect("mkdir temp");

    let output = std::process::Command::new(&ail_bin)
        .arg("run")
        .arg(&fixture)
        .current_dir(&tmp)
        .output()
        .expect("ail run");

    assert!(
        output.status.success(),
        "ail run failed: stdout={}, stderr={}",
        String::from_utf8_lossy(&output.stdout),
        String::from_utf8_lossy(&output.stderr),
    );
    let stdout = String::from_utf8_lossy(&output.stdout);
    assert_eq!(
        stdout.trim_end(), "5",
        "stdout = `{stdout}`, stderr = `{}`",
        String::from_utf8_lossy(&output.stderr)
    );
}

/// After the mono pass, the body of `main` in
/// test_22b2_instance_present must reference `show__Int` instead
/// of `show`.
#[test]
fn rewrite_replaces_class_method_var_with_mono_symbol_same_module() {
    let entry = examples_dir().join("test_22b2_instance_present.ail.json");
    let ws = ailang_core::load_workspace(&entry).expect("load");
    let diags = ailang_check::check_workspace(&ws);
    assert!(diags.is_empty(), "fixture must typecheck: {:?}", diags);

    let ws = ailang_check::monomorphise_workspace(&ws).expect("mono");

    let main_module = ws.modules.get("test_22b2_instance_present").unwrap();
    let main_fn = main_module
        .defs
        .iter()
        .find_map(|d| match d {
            ailang_core::ast::Def::Fn(f) if f.name == "main" => Some(f),
            _ => None,
        })
        .expect("main");

    // The body is `App { fn: Var "show", args: [Lit 42] }`. After
    // rewrite, the callee Var must be `show__Int`.
    let callee_name: &str = match &main_fn.body {
        ailang_core::ast::Term::App { callee, .. } => match callee.as_ref() {
            ailang_core::ast::Term::Var { name } => name.as_str(),
            other => panic!("callee is not Var: {:?}", other),
        },
        other => panic!("body is not App: {:?}", other),
    };
    assert_eq!(callee_name, "show__Int");
}

/// Helper: build & run a workspace via `ail run` and capture stdout
/// + stderr. The 22b.3 e2e tests below all funnel through this so the
/// failure-mode reporting is uniform.
fn ail_run(fixture_name: &str) -> (std::process::Output, String) {
    let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
    let ail_bin = std::env::var("CARGO_BIN_EXE_ail")
        .expect("CARGO_BIN_EXE_ail set by cargo test");
    let fixture = examples_dir().join(fixture_name);

    let tmp = manifest_dir.join("target").join(format!(
        "test_22b3_e2e_{}_{}",
        fixture_name.replace('.', "_"),
        std::process::id()
    ));
    std::fs::create_dir_all(&tmp).expect("mkdir temp");

    let output = std::process::Command::new(&ail_bin)
        .arg("run")
        .arg(&fixture)
        .current_dir(&tmp)
        .output()
        .expect("ail run");
    let stdout = String::from_utf8_lossy(&output.stdout).to_string();
    (output, stdout)
}

/// Property: when a single workspace declares two distinct instances of
/// the SAME class (`R Int` and `R Bool`), and `main` calls the class
/// method `r` at BOTH types, the binary picks the correct
/// monomorphised body for each call site. Coherence is preserved
/// end-to-end: instance `R Int { r _ = 11 }` reaches the `r 0` call,
/// instance `R Bool { r _ = 22 }` reaches the `r True` call. A
/// regression where coherence collapses (e.g. both call sites get
/// rewritten to the same `r__<X>`, or one synth body shadows the other)
/// would surface here as `11\n11\n`, `22\n22\n`, or build/runtime
/// failure — all observable at stdout. Defends mono-pass invariant 3.
#[test]
fn coherence_two_instances_pick_correct_body_at_runtime() {
    let (output, stdout) = ail_run("test_22b3_coherence_two_instances.ail.json");
    assert!(
        output.status.success(),
        "ail run failed: stdout={}, stderr={}",
        stdout,
        String::from_utf8_lossy(&output.stderr),
    );
    assert_eq!(
        stdout.trim_end_matches('\n'),
        "11\n22",
        "stdout = `{stdout}`, stderr = `{}`",
        String::from_utf8_lossy(&output.stderr),
    );
}

/// Property: a class method whose body comes from the class-level
/// `default` clause (the instance omits the override) is reachable
/// end-to-end through codegen and run. `class D a where dval : (a) ->
/// Int default \x. 99` + empty `instance D Int {}` + `main` calling
/// `dval 0` must produce `99\n`. Currently only `synthesise_mono_fn`'s
/// unit test covers the default-fallback branch; this fixture pins
/// down the *binary-level* property — the synthesised fn must lower
/// and link, the call site must be rewritten to `dval__Int`, the
/// constant 99 must reach stdout. Defends mono-pass invariant 4.
#[test]
fn class_default_method_runs_and_prints_default_value() {
    let (output, stdout) = ail_run("test_22b3_default_e2e.ail.json");
    assert!(
        output.status.success(),
        "ail run failed: stdout={}, stderr={}",
        stdout,
        String::from_utf8_lossy(&output.stderr),
    );
    assert_eq!(
        stdout.trim_end(),
        "99",
        "stdout = `{stdout}`, stderr = `{}`",
        String::from_utf8_lossy(&output.stderr),
    );
}

/// Property: a class+instance declared in module A, called from module
/// B's `main`, links and runs end-to-end. The mono pass appends the
/// synthesised fn to module A (the instance's defining module), the
/// call-site rewrite in module B emits the qualified name
/// `<A>.<mono_symbol>`, and the linker resolves the reference across
/// module boundaries. The AST-level property is already protected by
/// `rewrite_uses_qualified_name_for_cross_module_call_site`, but the
/// emit + link + run path is otherwise untested at the binary level.
/// A regression that left the synthesised fn unemitted or the call
/// site unqualified would surface as a link error or wrong stdout.
/// Defends mono-pass invariant 6.
#[test]
fn cross_module_class_method_runs_and_prints_correct_value() {
    let (output, stdout) = ail_run("test_22b3_xmod_e2e_main.ail.json");
    assert!(
        output.status.success(),
        "ail run failed: stdout={}, stderr={}",
        stdout,
        String::from_utf8_lossy(&output.stderr),
    );
    assert_eq!(
        stdout.trim_end(),
        "7",
        "stdout = `{stdout}`, stderr = `{}`",
        String::from_utf8_lossy(&output.stderr),
    );
}
