diff --git a/crates/ail/tests/typeclass_22b3.rs b/crates/ail/tests/typeclass_22b3.rs
index 6b4a626..bca5745 100644
--- a/crates/ail/tests/typeclass_22b3.rs
+++ b/crates/ail/tests/typeclass_22b3.rs
@@ -443,6 +443,165 @@ fn fixpoint_handles_chained_class_method_calls() {
);
}
+/// 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
`.
+ 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 = in `.
+ 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 `.` — 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"
+ );
+}
+
/// After the mono pass, the body of `main` in
/// test_22b2_instance_present must reference `show#Int` instead
/// of `show`.
diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs
index 3e9bfd4..3cfdd21 100644
--- a/crates/ailang-check/src/mono.rs
+++ b/crates/ailang-check/src/mono.rs
@@ -51,7 +51,7 @@
//! the implementation so the constraint is visible to anyone
//! extending the skeleton.
-use ailang_core::ast::{Arm, ClassDef, Def, FnDef as AstFnDef, InstanceDef, Term, Type};
+use ailang_core::ast::{Arm, ClassDef, ConstDef, Def, FnDef as AstFnDef, InstanceDef, Pattern, Term, Type};
use ailang_core::workspace::Workspace;
use crate::Result;
use indexmap::IndexMap;
@@ -156,47 +156,35 @@ pub fn monomorphise_workspace(ws: &Workspace) -> Result {
for mname in &module_names {
let n_defs = ws_owned.modules[mname].defs.len();
for i in 0..n_defs {
- let (ordered, defining_module_name): (Vec