iter bugfix-instance-body-unbound-var: GREEN — walk instance method bodies through check_fn

Fixes the bug RED-pinned in 72f3f65: an unbound identifier inside an
instance method body slipped past `ail check` (false-OK exit 0) and
surfaced only at `ail build` as the degraded internal-error diagnostic
`monomorphise_workspace: unknown identifier: <name>` with no source
location, symbol kind, or "did you mean" candidates.

Root cause: `check_def` in `crates/ailang-check/src/lib.rs:1574-1595`
early-returned `Ok(())` for `Def::Class(_) | Def::Instance(_)` without
ever invoking the body walker. The arm's comment claimed iter 22b.2
landed instance-body typechecking; that wiring was never implemented.
Only the workspace-load coherence checks (Orphan/Duplicate/
MissingMethod) touched instance defs, and they inspect schema only,
not the method-body identifier graph.

Fix: split the combined arm so `Def::Class(_)` stays schema-only at
this layer, while `Def::Instance(inst)` routes through a new helper
`check_instance` that lifts each `InstanceMethod`'s `Term::Lam` body
into a synthetic `FnDef`, applies class-method substitution (class
param -> instance type, via the existing `substitute_rigids` /
`substitute_rigids_in_term` helpers), and hands it to `check_fn`.
The reuse of `check_fn` is what gets the body walked through the
same identifier-resolution path as fn bodies, so an unbound name
fires `[unbound-var]` at `ail check` with exit 1 and the standard
structured diagnostic.

Per "minimal fix, no surrounding cleanup" constraint: no widening
to Def::Class (still schema-only); no changes to the
monomorphise_workspace diagnostic wording (defence-in-depth
internal-error path stays as backstop); no changes to mono.rs,
codegen, or any other crate.

Tests: 557 baseline + 2 new RED -> 559 green. Both RED pins in
unbound_in_instance_method_pin.rs now PASS. fn-body level
unbound-var path stays green. All 8 carve-out fixtures classify
unchanged.

Known debt (out of scope per carrier; queued in journal):
`check_instance` does not yet cross-check the substituted method
signature against the class's `ClassMethodEntry.method_ty` — a
malformed instance declaring wrong types in its Lam would still
typecheck cleanly. The body-walk catches unbound vars and
effect-mismatches against the Lam's own declared types, but not
class-method-signature mismatch.

crates/ailang-check/src/lib.rs

@@ -1580,20 +1580,107 @@ fn check_def(
         Def::Fn(f) => check_fn(f, env, out_warnings),
         Def::Const(c) => check_const(c, env, out_warnings),
         Def::Type(td) => check_type_def(td, env),
-        // Iter 22b.1: schema-only landing for class/instance defs.
-        // Class-schema validation (InvalidSuperclassParam,
-        // ConstraintReferencesUnboundTypeVar) and instance-body
-        // typechecking (with class-method substitution) land in 22b.2.
-        // ctt.3: KindMismatch retired — the malformed-class-param
-        // shape now fires BareCrossModuleTypeRef from the canonical-
-        // form validator instead.
-        // Workspace-load coherence checks (Orphan / Duplicate /
-        // MissingMethod) already fire from `workspace::build_registry`,
-        // so a malformed instance never reaches this point.
-        Def::Class(_) | Def::Instance(_) => Ok(()),
+        // bugfix-instance-body-unbound-var (2026-05-13): each instance
+        // method body is walked through `check_fn` via a synthetic
+        // `FnDef` lifted from the `Term::Lam` the InstanceMethod body
+        // carries. This routes instance bodies through the same
+        // identifier-resolution path as fn bodies, so an unbound
+        // identifier inside an instance method fires `[unbound-var]`
+        // at `ail check` instead of slipping past and surfacing as a
+        // degraded "monomorphise_workspace: unknown identifier"
+        // diagnostic at `ail build`. Class-method substitution
+        // (class param → instance type) happens inside
+        // `check_instance` before the body-walk. Class-schema
+        // validation (InvalidSuperclassParam, etc.) and the workspace-
+        // load coherence checks (Orphan / Duplicate / MissingMethod)
+        // fire from `workspace::build_registry` independently, so a
+        // malformed instance never reaches this body-walk. `Def::Class`
+        // remains schema-only at this layer.
+        Def::Class(_) => Ok(()),
+        Def::Instance(inst) => check_instance(inst, env, out_warnings),
     }
 }
 
+/// bugfix-instance-body-unbound-var (2026-05-13): route each
+/// `InstanceMethod` body through `check_fn` by wrapping it in a
+/// synthetic `FnDef`. The InstanceMethod body is conventionally a
+/// `Term::Lam` (the post-mq.3 shape; see iter mq.3 journal
+/// "instance-method body shape ... existing-convention is `Term::Lam`
+/// with paramTypes/retType"); we extract its `param_tys` / `ret_ty`
+/// / `params` / `body` into an `FnDef` shape and reuse the existing
+/// fn-body-check machinery.
+///
+/// Class-method substitution: the on-disk Lam's `param_tys` / `ret_ty`
+/// reference the class's type parameter directly (e.g. the prelude
+/// `instance Eq Int` body declares `(typed x a) (typed y a)` with `a`
+/// being `Eq`'s class param). Before handing to `check_fn` we look up
+/// the class's `param` name via `env.class_methods` and substitute it
+/// to the instance's concrete `type_`, using the existing
+/// `substitute_rigids` helper on type positions and
+/// `substitute_rigids_in_term` on the body (which targets any embedded
+/// Type annotations on nested Lams / LetRecs). Without this step
+/// `check_fn` would fire `polymorphic-not-supported` on the class
+/// param appearing in non-Forall position.
+///
+/// The synthetic fn name is `"<class>::<method>"`, used only for
+/// diagnostic strings.
+///
+/// Non-Lam method bodies are not part of the current schema (all
+/// fixtures in the corpus and the convention reaffirmed in iter mq.3
+/// use `Term::Lam`); they are silently skipped here. If a future
+/// schema admits non-Lam shapes, this arm must be extended to walk
+/// them — silent skip is the conservative choice today because
+/// the pre-fix behaviour was also silent.
+fn check_instance(
+    inst: &InstanceDef,
+    env: &Env,
+    out_warnings: &mut Vec<Diagnostic>,
+) -> Result<()> {
+    let qualified_class = qualify_class_ref_in_check(&inst.class, &env.current_module);
+    for im in &inst.methods {
+        // Look up the class's param name. Workspace-load's MissingMethod
+        // gates this — if the (class, method) pair isn't in the table,
+        // the instance was structurally rejected upstream and we never
+        // get here in practice. Defensive fallback: skip substitution
+        // (body walks without class-param resolution).
+        let subst_map: BTreeMap<String, Type> = env
+            .class_methods
+            .get(&(qualified_class.clone(), im.name.clone()))
+            .map(|entry| {
+                let mut m = BTreeMap::new();
+                m.insert(entry.class_param.clone(), inst.type_.clone());
+                m
+            })
+            .unwrap_or_default();
+
+        let Term::Lam { params, param_tys, ret_ty, effects, body } = &im.body else {
+            // Non-Lam method body: skip (see fn-level doc-comment).
+            continue;
+        };
+        let subst_param_tys: Vec<Type> = param_tys
+            .iter()
+            .map(|t| substitute_rigids(t, &subst_map))
+            .collect();
+        let subst_ret_ty = substitute_rigids(ret_ty, &subst_map);
+        let subst_body = substitute_rigids_in_term(body, &subst_map);
+        let fn_ty = Type::fn_implicit(
+            subst_param_tys,
+            subst_ret_ty,
+            effects.clone(),
+        );
+        let synthetic = FnDef {
+            name: format!("{}::{}", inst.class, im.name),
+            ty: fn_ty,
+            params: params.clone(),
+            body: subst_body,
+            doc: None,
+            suppress: Vec::new(),
+        };
+        check_fn(&synthetic, env, out_warnings)?;
+    }
+    Ok(())
+}
+
 fn check_type_def(td: &TypeDef, env: &Env) -> Result<()> {
     // Iter 13a: a parameterised ADT (`vars` non-empty) installs its
     // type parameters as rigid vars while checking the ctor field