diff --git a/bench/orchestrator-stats/2026-05-13-iter-bugfix-instance-body-unbound-var.json b/bench/orchestrator-stats/2026-05-13-iter-bugfix-instance-body-unbound-var.json new file mode 100644 index 0000000..a628d8e --- /dev/null +++ b/bench/orchestrator-stats/2026-05-13-iter-bugfix-instance-body-unbound-var.json @@ -0,0 +1,12 @@ +{ + "iter_id": "bugfix-instance-body-unbound-var", + "date": "2026-05-13", + "mode": "mini", + "outcome": "DONE", + "tasks_total": 1, + "tasks_completed": 1, + "reloops_per_task": { "1": 1 }, + "review_loops_spec": 0, + "review_loops_quality": 1, + "blocked_reason": null +} diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 9de2d67..7264283 100644 --- a/crates/ailang-check/src/lib.rs +++ b/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 `"::"`, 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, +) -> 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 = 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 = 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 diff --git a/docs/journals/2026-05-13-iter-bugfix-instance-body-unbound-var.md b/docs/journals/2026-05-13-iter-bugfix-instance-body-unbound-var.md new file mode 100644 index 0000000..f941c3d --- /dev/null +++ b/docs/journals/2026-05-13-iter-bugfix-instance-body-unbound-var.md @@ -0,0 +1,94 @@ +# iter bugfix-instance-body-unbound-var — instance method bodies now walk through check_fn + +**Date:** 2026-05-13 +**Started from:** 72f3f6541b3e41f2d4a7706dcad5bd784ec07d81 +**Status:** DONE +**Tasks completed:** 1 of 1 + +## Summary + +Fixes the bug surfaced by the 2026-05-13 form-a fieldtest: an unbound +identifier inside an `instance` method body slipped past `ail check` +and surfaced only at `ail build` as the degraded internal-error +diagnostic `monomorphise_workspace: unknown identifier: ...`. Root +cause: `check_def`'s `Def::Class(_) | Def::Instance(_)` arm at +`crates/ailang-check/src/lib.rs:1574-1595` early-returned `Ok(())` +without ever invoking the body walker — the comment claimed "instance- +body typechecking (with class-method substitution) land[s] in 22b.2", +but that wiring was never implemented. Workspace-load coherence checks +(`build_registry`'s Orphan/Duplicate/MissingMethod) only inspect +instance schema, not method-body identifier graphs. + +Fix is the minimum-scope change at that call site: split the combined +arm so `Def::Class(_)` continues to be schema-only, while +`Def::Instance(inst)` calls a new helper `check_instance` that, for +each `InstanceMethod`, lifts the body `Term::Lam` into a synthetic +`FnDef` (class-method-substituted via `substitute_rigids` / +`substitute_rigids_in_term` against the class's `param` name as +declared in `env.class_methods[(qualified_class, method)]`) and +hands it to the existing `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 the carrier's "minimal fix, no surrounding cleanup" constraint: +no widening to `Def::Class` (still schema-only); no changes to the +`monomorphise_workspace` diagnostic wording (the defence-in-depth +internal-error path stays as a backstop); no changes to mono.rs, +codegen, or any other crate. + +## Per-task notes + +- iter bugfix-instance-body-unbound-var.1: split the + `Def::Class(_) | Def::Instance(_)` arm into `Def::Class(_) => + Ok(())` and `Def::Instance(inst) => check_instance(inst, env, + out_warnings)`. New free fn `check_instance` reads + `env.class_methods[(qualify_class_ref_in_check(&inst.class, + &env.current_module), im.name)]` to recover the class's `param` + name, builds a `{class_param: inst.type_}` substitution, applies + it to the Lam's `param_tys` / `ret_ty` and to the Lam's body + Term (via the existing `substitute_rigids` / + `substitute_rigids_in_term` helpers), then constructs a synthetic + `FnDef` (`name = "::"`, `ty = + Type::fn_implicit(subst_param_tys, subst_ret_ty, + lam.effects)`, params from Lam, body = substituted Lam body) + and calls `check_fn` on it. + + First-attempt sketch wrapped the Lam's `param_tys` / `ret_ty` + unsubstituted on the assumption that the on-disk canonical form + was post-substitution — the `codegen_import_map_fallback_pin` + regression (and a sweep of the prelude `(typed x a) (typed y a)` + shape) immediately disproved that. The substitution step was + added at the second iteration of the implementer phase, before + reaching the spec / quality phases. + + Non-Lam method bodies are silently skipped — current schema + doesn't admit them and the pre-fix behaviour was also silent. + +## Concerns + +- None. + +## Known debt + +- `check_instance` does **not** verify that the substituted method + signature matches the corresponding `ClassMethodEntry.method_ty` + (with `class_param ↦ inst.type_`). The body-walk catches unbound + vars and effect-mismatches against the Lam's own declared types, + but a malformed instance whose Lam declares + `(typed x (con Int)) (typed y (con Int)) -> Bool` for an + `instance Eq Bool` body would currently typecheck cleanly. The + workspace-load `MissingMethod` / coherence checks only inspect + the (class, type) pair, not the method's declared type. Out of + scope per the carrier's "minimal fix" constraint; queued as a + follow-up roadmap candidate ("instance-method declared-type + vs class-method-type cross-check"). + +## Files touched + +- `crates/ailang-check/src/lib.rs` — `check_def` arm split, + new `check_instance` helper. + +## Stats + +bench/orchestrator-stats/2026-05-13-iter-bugfix-instance-body-unbound-var.json