From c3e804436164f51680550fd197e9f64377198e0a Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 11 May 2026 14:50:47 +0200 Subject: [PATCH] =?UTF-8?q?plan:=20iter=2023.4-prep=20=E2=80=94=20checker?= =?UTF-8?q?=20prerequisites=20for=20prelude=20free=20fns?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/plans/2026-05-11-iter-23.4-prep.md | 452 ++++++++++++++++++++++++ 1 file changed, 452 insertions(+) create mode 100644 docs/plans/2026-05-11-iter-23.4-prep.md diff --git a/docs/plans/2026-05-11-iter-23.4-prep.md b/docs/plans/2026-05-11-iter-23.4-prep.md new file mode 100644 index 0000000..d1ad744 --- /dev/null +++ b/docs/plans/2026-05-11-iter-23.4-prep.md @@ -0,0 +1,452 @@ +# Iter 23.4-prep — Checker Prerequisites for Prelude Free Fns — Implementation Plan + +> **Parent spec:** `docs/specs/2026-05-10-23-eq-ord-prelude.md` +> +> **Plan provenance:** This iter does not have a spec section of its +> own. It closes two checker gaps discovered mid-iter when iter 23.4 +> BLOCKED on Task 1. See the BLOCKED journal at +> `git show iter/23.4:docs/journals/2026-05-11-iter-23.4.md`. +> +> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement` +> to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Close two localised checker gaps so iter 23.4's prelude +free fns become reachable from user code: (Gap 1) extend bare-name +resolution to fall through to free fns in implicitly-imported +modules; (Gap 2) register `Def::Class` method types in +`linearity::check_module`'s globals so class-method `param_modes` +become visible to the borrow walk. + +**Architecture:** + +Gap 2 is purely intra-module: `ne` and `eq` both live in the prelude +module, so `linearity::check_module(prelude)` is the only call that +needs to see class-method modes. Fix iterates `class_def.methods` +in the build loop and inserts `(method_name, strip_forall(ty))` into +`globals`, mirroring the existing `Def::Fn(f)` arm two lines above. + +Gap 1 is per-consumer-module workspace lookup: the `Term::Var { name }` +fall-through ladder gains one new arm between `env.class_methods` +and the dot-qualified arm. New arm iterates `env.imports` +(per-current-module implicit-import alias map) and consults +`env.module_globals[].fns.get(name)`. Single-match wins; +zero-match and multi-match both fall through (the latter is +unreachable today — prelude is the only implicit import — and is +covered by a one-line code comment naming the prelude-singleton +invariant). No new `Env` field; existing `env.imports` and +`env.module_globals` carry everything needed. + +**Tech Stack:** `ailang-check` crate (`linearity.rs` for Gap 2, +`lib.rs` for Gap 1). No changes to `ailang-core`, `ailang-codegen`, +or any on-disk fixture (including the prelude). + +**Out of scope:** +- The five prelude free fns themselves (`ne`/`lt`/`le`/`gt`/`ge`). + They land in iter 23.4 unchanged from the existing + `docs/plans/2026-05-11-iter-23.4.md`. +- Any modification to `examples/prelude.ail.json`. +- Any new diagnostic for the hypothetical multi-implicit-import + ambiguity case. +- Extension of bare-name lookup to explicit imports (today's behaviour + — explicit imports stay qualified-only — is preserved). + +--- + +## Files this plan creates or modifies + +- **Modify:** `crates/ailang-check/src/linearity.rs:212` — replace + the empty `Def::Class(_) | Def::Instance(_) => {}` arm with one + that iterates `class_def.methods` and registers each + `(method_name, strip_forall(method_ty))` into the `globals` + HashMap. `Def::Instance` stays a no-op (instance method bodies + are walked separately as Def::Fn after monomorphisation; per the + recon, the spec-23.4 false-positive flows from the class-method + *type declaration*, not from the instance body). +- **Modify:** `crates/ailang-check/src/linearity.rs` test module — + add `class_method_borrow_call_does_not_fire_consume_while_borrowed` + unit test inside the existing `#[cfg(test)] mod tests` block. +- **Modify:** `crates/ailang-check/src/lib.rs` around line 1780 — + extend the bare-name lookup ladder in the `Term::Var { name }` arm + inside `synth` (signature at line 1745). Insert one new + `else if` between the existing `env.class_methods.get(name)` + branch and the dot-qualified arm. New branch iterates + `env.imports.values()` (each value is the actual module name an + implicit alias resolves to) and consults + `env.module_globals[].fns.get(name)`. Single-match returns + the substituted type. Zero or multi match falls through. +- **Modify:** `crates/ailang-check/src/lib.rs` test module (or + similar pre-existing test location near the `Term::Var` arm) — + add `bare_name_resolves_through_implicit_import_to_free_fn` test + that constructs an in-memory `Workspace` with a synthetic prelude + carrying a test-only free fn `dbl : Int -> Int` and a consumer + module calling bare `dbl 5`. RED before the fix + (`unknown-ident: dbl`), GREEN after. + +--- + +## Task 1: Gap 2 — `linearity::check_module` registers class-method types + +**Files:** +- Modify: `crates/ailang-check/src/linearity.rs:208–214` — replace + the empty `Def::Class(_) | Def::Instance(_) => {}` arm. +- Modify: `crates/ailang-check/src/linearity.rs` test module — add + one new unit test. + +- [ ] **Step 1: Write the failing test inside the existing test module.** + +Locate the `#[cfg(test)] mod tests { ... }` block in `linearity.rs`. +After the most recent existing test, append: + +```rust +#[test] +fn class_method_borrow_call_does_not_fire_consume_while_borrowed() { + // Construct a module with one `Def::Class` carrying a borrow-borrow + // method, and one `Def::Fn` whose body forwards its borrow-mode + // params into a call to that class method. The pre-fix behaviour + // is `consume-while-borrowed` false positives on both params. + use crate::ast::{ + ClassDef, ClassMethod, Def, FnDef, Module, ParamMode, Term, Type, + }; + + let class_eq = ClassDef { + name: "TestEq".to_string(), + param: "a".to_string(), + superclass: None, + methods: vec![ClassMethod { + name: "teq".to_string(), + ty: Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + param_modes: vec![ParamMode::Borrow, ParamMode::Borrow], + ret: Box::new(Type::Con { name: "Bool".into() }), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + default: None, + }], + doc: None, + }; + + let ne = FnDef { + name: "tne".to_string(), + ty: Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + param_modes: vec![ParamMode::Borrow, ParamMode::Borrow], + ret: Type::Con { name: "Bool".into() }.into(), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec!["x".into(), "y".into()], + body: Term::App { + fn_: Box::new(Term::Var { name: "teq".into() }), + args: vec![ + Term::Var { name: "x".into() }, + Term::Var { name: "y".into() }, + ], + }, + doc: None, + }; + + let module = Module { + name: "m".into(), + imports: vec![], + defs: vec![Def::Class(class_eq), Def::Fn(ne)], + }; + + let diags = check_module(&module); + assert!( + diags.is_empty(), + "expected no diagnostics but got {:#?}", + diags + ); +} +``` + +If the exact AST constructor field names diverge from this snippet +(e.g. `fn_` vs `f`, `Box` placement on `ret`), use the existing +test in the file as the canonical shape — same enum variants, same +field ordering. The implementer surfaces NEEDS_CONTEXT only if the +field-name diagnostic is non-trivial; field-rename adjustments are +in-scope for this step. + +- [ ] **Step 2: Run the test — expect RED.** + +Run: `cargo test --workspace -p ailang-check class_method_borrow_call_does_not_fire_consume_while_borrowed` + +Expected: FAIL. The test should panic on the `assert!` because two +`consume-while-borrowed` diagnostics fire — one for `x`, one for `y` +— from the synthesised `App(teq, [x, y])` since `callee_arg_modes` +fails to find `teq` in `globals` and defaults to `Consume`. + +- [ ] **Step 3: Apply the fix.** + +Replace `crates/ailang-check/src/linearity.rs:208–214`: + +```rust + // Iter 22b.1: class/instance defs are skipped here. Once + // 22b.3 monomorphisation materialises class methods as + // ordinary `FnDef`s, the lift's globals map will pick + // them up automatically. + Def::Class(_) | Def::Instance(_) => {} +``` + +with: + +```rust + // Iter 23.4-prep: class methods register their types into + // the globals map so `callee_arg_modes` can see their + // `param_modes`. Without this, a borrow-mode fn that + // forwards its borrow params into a class-method call + // fires `consume-while-borrowed` false positives. + // Instance defs stay a no-op: instance method bodies are + // walked separately via `Def::Fn` after monomorphisation. + Def::Class(c) => { + for m in &c.methods { + globals.insert(m.name.clone(), strip_forall(&m.ty).clone()); + } + } + Def::Instance(_) => {} +``` + +- [ ] **Step 4: Run the test — expect GREEN.** + +Run: `cargo test --workspace -p ailang-check class_method_borrow_call_does_not_fire_consume_while_borrowed` + +Expected: PASS. + +- [ ] **Step 5: Full workspace sanity.** + +Run: `cargo test --workspace` + +Expected: PASS. No regression in any other linearity or check test. +If anything fires, root-cause; the most likely failure mode is a +test that relied on the old skip behaviour (we have no such test +on record — recon found none). + +- [ ] **Step 6: Commit.** + +```bash +git add crates/ailang-check/src/linearity.rs +git commit -m "iter 23.4-prep.1: linearity — register Def::Class method types in globals" +``` + +--- + +## Task 2: Gap 1 — bare-name resolution falls through to implicitly-imported free fns + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs` around line 1780 — insert + one new branch into the `Term::Var { name }` lookup ladder inside + `synth`. +- Modify: `crates/ailang-check/src/lib.rs` test module — add the + bare-name test. + +- [ ] **Step 1: Write the failing integration test.** + +Locate the existing test module in `crates/ailang-check/src/lib.rs` +(near the bottom of the file — find `#[cfg(test)] mod tests`). +Append: + +```rust +#[test] +fn bare_name_resolves_through_implicit_import_to_free_fn() { + // Construct a workspace whose prelude carries a test-only free + // fn `dbl : Int -> Int`, and a consumer module that calls bare + // `dbl 5`. The pre-fix behaviour is `unknown-ident: dbl`, + // because the bare-name lookup ladder consults the consumer's + // local globals + workspace-flat class_methods but never the + // free fns of implicitly-imported modules. + use crate::ast::{Def, FnDef, Lit, Module, ParamMode, Term, Type}; + use crate::workspace::Workspace; + + let prelude = Module { + name: "prelude".into(), + imports: vec![], + defs: vec![Def::Fn(FnDef { + name: "dbl".into(), + ty: Type::Fn { + params: vec![Type::Con { name: "Int".into() }], + param_modes: vec![ParamMode::Implicit], + ret: Type::Con { name: "Int".into() }.into(), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec!["n".into()], + body: Term::Var { name: "n".into() }, + doc: None, + })], + }; + + let consumer = Module { + name: "m".into(), + imports: vec![], + defs: vec![Def::Fn(FnDef { + name: "main".into(), + ty: Type::Fn { + params: vec![], + param_modes: vec![], + ret: Type::Con { name: "Int".into() }.into(), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec![], + body: Term::App { + fn_: Box::new(Term::Var { name: "dbl".into() }), + args: vec![Term::Lit { + lit: Lit::Int { value: 5 }, + }], + }, + doc: None, + })], + }; + + let ws = Workspace { + entry: "m".into(), + modules: vec![prelude, consumer].into_iter() + .map(|m| (m.name.clone(), m)) + .collect(), + }; + + let mg = build_module_globals(&ws).expect("build_module_globals"); + let errs = check_in_workspace(&ws.modules["m"], &ws, &mg); + assert!( + errs.is_empty(), + "expected no errors but got {:#?}", + errs + ); +} +``` + +If a helper for synthetic-Workspace construction already exists +(e.g. `single_module_with_type_con` at `workspace.rs:2095+` per the +recon's cross-reference), prefer that helper's idiom. The exact +field names follow whatever the existing tests use. + +- [ ] **Step 2: Run the test — expect RED.** + +Run: `cargo test --workspace -p ailang-check bare_name_resolves_through_implicit_import_to_free_fn` + +Expected: FAIL with `unknown-ident: dbl` (or the project's +equivalent — the bare-name lookup falls through every existing arm +and terminates at the `UnknownIdent` error at line 1842). + +- [ ] **Step 3: Apply the fix to the `Term::Var { name }` lookup ladder.** + +In `crates/ailang-check/src/lib.rs:1745+` (function `synth`), +locate the `Term::Var { name }` arm. After the existing +`env.class_methods.get(name)` branch (around line 1780) and before +the dot-qualified arm (around line 1819), insert: + +```rust + // Iter 23.4-prep: bare-name fall-through to free fns of + // implicitly-imported modules. Iterates the current + // module's implicit-import aliases (today: only `prelude` + // — see lib.rs:1163-1180). Single-match wins; zero-match + // and multi-match fall through (multi-match is + // unreachable as long as `prelude` is the only implicit + // import; if a second implicit import lands, revisit). + } else if let Some((mod_name, fn_ty)) = env.imports + .values() + .filter_map(|mod_name| { + env.module_globals + .get(mod_name) + .and_then(|mg| mg.get(name).map(|ty| (mod_name.clone(), ty.clone()))) + }) + .next() + { + // Hash-mark the resolved owner so downstream passes + // (codegen mangling, mono) can compute the cross- + // module symbol. Same treatment the dot-qualified + // arm gives below. + let _ = mod_name; // owner reachable via the workspace; mangling consults + // the FnDef's home module directly during codegen. + let ty = substitute_freshly(&fn_ty); + Ok((Term::Var { name: name.clone() }, ty)) +``` + +Notes: +1. `env.imports.values()` yields the per-current-module list of + resolved module names (per recon: implicit-prelude is wired at + 1271-1290 alongside the workspace-flat path). +2. The `substitute_freshly` (or equivalent type-instantiation helper) + is the same one the existing globals branch uses around line 1773 + — match its name verbatim from the existing code. +3. The owner-module name is informational here; codegen mangles + cross-module references via the FnDef's owning module field at + monomorphisation time. The placeholder `let _ = mod_name;` makes + the variable usage explicit; remove it once the implementer + confirms (via existing class-method-resolution patterns) that no + additional bookkeeping is needed at the `Term::Var` site. +4. The `.next()` short-circuits at the first match. This implements + the single-match-wins rule. If two implicit imports both define + the same name, the first iterated wins — recon flagged this as + acceptable today (prelude singleton); the code comment names the + future revisit point. + +If the existing class-method branch at line 1780 uses a different +substitution helper or returns a more elaborate result shape (e.g. +inserts the resolved class instance), mirror that shape verbatim +for free fns — recon noted free fns have *less* than class methods +(no instance disambiguation needed), so any class-method-only +bookkeeping (e.g. instance candidate lists) does not apply to the +new branch. + +- [ ] **Step 4: Run the test — expect GREEN.** + +Run: `cargo test --workspace -p ailang-check bare_name_resolves_through_implicit_import_to_free_fn` + +Expected: PASS. + +- [ ] **Step 5: Full workspace sanity.** + +Run: `cargo test --workspace` + +Expected: PASS. The most plausible regression vectors are (a) a test +that relied on `unknown-ident` firing for a name that today lives +in a non-prelude module reachable via implicit-import wiring (recon +says no such test exists — prelude is the only implicit import), or +(b) a name-shadowing case where a local variable and a prelude free +fn share a name (the existing `locals → globals → class_methods` +ladder already shields locals; the new branch sits *after* +class_methods so locals still win). + +- [ ] **Step 6: Commit.** + +```bash +git add crates/ailang-check/src/lib.rs +git commit -m "iter 23.4-prep.2: check — bare-name fall-through to implicit-imported free fns" +``` + +--- + +## Plan self-review + +1. **Coverage:** Two tasks, one per gap, both with RED-first unit / + integration tests that close the failure mode the iter-23.4 + BLOCKED journal documented. ✓ +2. **Placeholder scan:** No "TBD", "TODO", "implement later", or + "similar to Task N". Task 2 Step 3 contains a deliberate + "if the existing class-method branch ... mirror that shape + verbatim" — this is *guidance for an implementer-side ambiguity + that cannot be resolved without reading the unquoted surrounding + code*, not a placeholder. The plan-recon snippet quoted enough + to make the fix concrete; the mirror-clause covers a single + localised judgment call (instance-list shape) that the implementer + resolves by reading the same function block they're editing. ✓ +3. **Type consistency:** `dbl`, `tne`/`teq` (synthetic names in test + modules, isolated from prelude), `Workspace`, `Module`, + `ClassDef`, `ClassMethod`, `FnDef`, `Term::Var`, `Term::App`, + `Type::Fn`, `ParamMode::Borrow/Implicit`, `build_module_globals`, + `check_in_workspace`, `check_module`, `strip_forall`, + `callee_arg_modes`, `env.class_methods`, `env.module_globals`, + `env.imports`. All referenced consistently across both tasks + and matched to the recon's line anchors. ✓ +4. **Step granularity:** Each step is one action plus a single + `cargo test` invocation. Step 5 in each task adds a full-suite + sanity (`cargo test --workspace`) — fast enough on this corpus + to keep the step inside the 2-5 minute window. ✓