From bc9f5120034f2552ad7e78454bb198472404d4b1 Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 15 May 2026 14:50:22 +0200 Subject: [PATCH] =?UTF-8?q?plan:=20it.2=20guardedness=20checker=20+=20Dive?= =?UTF-8?q?rge=20effect=20=E2=80=94=206=20tasks?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Boss-resolved design decisions (DD-1 standalone post-synth pass sibling of verify_tail_positions; DD-2 the smaller-set structural algorithm with implicit position inference; DD-3 self = callee==in_def, mutual = ADT-family connected-components union-find admitting D1's tree/forest set; DD-4 term_contains_loop stopping at Term::Lam, reuse UndeclaredEffect, callee-propagation free). it.2-only tail==true grandfather keeps the 21-fixture corpus alive until it.3. Nothing tail-related removed. Spec fda9b78. --- docs/plans/2026-05-15-iter-it.2.md | 663 +++++++++++++++++++++++++++++ 1 file changed, 663 insertions(+) create mode 100644 docs/plans/2026-05-15-iter-it.2.md diff --git a/docs/plans/2026-05-15-iter-it.2.md b/docs/plans/2026-05-15-iter-it.2.md new file mode 100644 index 0000000..8bda409 --- /dev/null +++ b/docs/plans/2026-05-15-iter-it.2.md @@ -0,0 +1,663 @@ +# it.2 — guardedness checker + Diverge effect — Implementation Plan + +> **Parent spec:** `docs/specs/2026-05-15-iteration-discipline.md` +> +> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement` +> to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Make non-structural recursion-by-call a compile error +(`NonStructuralRecursion`), keeping the accumulator-carrying +structural walk classified as structural (pure, total), the 21 +`tail-app` corpus fixtures grandfathered, and any `loop`-bearing +function forced to declare the now-real `Diverge` effect. + +**Architecture:** All work is in `crates/ailang-check` plus a +DESIGN.md prose sync and fixtures. One new whole-body verification +pass `verify_structural_recursion` runs as a sibling of +`verify_tail_positions` in `check_fn`'s post-synth region; one new +`CheckError::NonStructuralRecursion`; one `term_contains_loop` +syntactic check that injects `"Diverge"` into the raised effect set +so the *existing* `UndeclaredEffect` reconciliation does the rest. +No AST variant is added, so there is no walker-arm/schema-coverage +fan-out. Nothing `tail`-related is removed (that is it.3). + +**Tech Stack:** `ailang-check` (`lib.rs`: `CheckError`, +`check_fn`, a new module-or-fn for the guardedness pass), DESIGN.md, +`examples/` fixtures, `crates/ailang-check/tests/`, the carve-out +inventory test. + +--- + +## Design decisions (Boss-resolved; not implementer judgement calls) + +- **DD-1 — standalone post-synth pass.** `verify_structural_recursion( + f: &FnDef, env: &Env) -> Result<(), CheckError>` is a new + whole-body walk invoked in `check_fn` immediately after the + `verify_tail_positions` call (recon HEAD: `lib.rs:2021`), before + the declared-vs-raised effect reconciliation (`lib.rs:2023-2028`). + It is the structural sibling of `verify_tail_positions` / + `verify_loop_body` (recon: `lib.rs:2627`/`:2769`), which already + bind `Term::App { tail }`. It is NOT folded into the `synth` + `Term::App` arm (`lib.rs:3255`, which discards `tail` via `..`): + guardedness is a body-shape invariant, not a type-synthesis fact, + and it needs (a) the whole body to build the provenance map before + judging any call and (b) the `tail` binding the synth arm drops. +- **DD-2 — the `smaller` set algorithm (the structural check).** For + a recursive `FnDef`, for each candidate structural parameter + position `i` (every parameter whose declared type is a + `Type::Con` ADT — not a primitive, not a function type): walk the + body maintaining `smaller: HashSet` = variables known + strictly structurally smaller than the parameter bound at position + `i`. `smaller` starts empty. At `Term::Match { scrutinee, arms }` + where `scrutinee` is `Term::Var { name }` and (`name` == the + parameter-`i` binder name OR `name ∈ smaller`): for each arm, the + variables bound by a constructor sub-pattern + (`Pattern::Ctor { fields }`, recon `ast.rs:611-626`, + `type_check_pattern` `lib.rs:3994`) are added to a per-arm copy of + `smaller` while walking that arm's body. A recursive call (DD-3) + is *guarded at position i* iff its argument expression at position + `i` is `Term::Var { name }` with `name ∈ smaller` at that call + site. The def is **structural** iff there exists at least one + candidate position `i` guarded at *every* recursive call site + (implicit inference per spec D1 — no annotation). Accumulator + positions are never examined, so they are unconstrained (spec D1: + the foldl-shape accumulator walk is structural). If no candidate + position is guarded at all recursive call sites ⇒ + `NonStructuralRecursion`. +- **DD-3 — recursive-call identification + mutual grouping.** + Self-recursion: a `Term::App` whose `callee_name(callee)` + (recon `lib.rs:4127-4132`) equals the enclosing def name (`f.name`; + `in_def` is already threaded but unused for this — the new pass + takes `f` directly). `Term::LetRec` clause bodies use the clause + name as the recursion name. Mutual recursion: a module-level + pre-pass computes ADT **families** as connected components of the + ADT type-reference graph (nodes = `type` decl names; an undirected + edge between `T` and `U` iff `U` appears in a constructor field + type of `T` or vice versa; union-find). A set of `FnDef`s forms a + *mutual structural group* iff they call each other (direct + `Term::App`→`Term::Var`), every member has a structural parameter + whose type head lies in **one** family component, and every + self/cross recursive call passes, at the callee's structural + position, a variable in the caller's `smaller` set. This admits + exactly spec-D1's named set (even/odd-over-`Nat` — one family; + mutual `JSON` — one family; tree/forest — one component via the + cross-reference edge). A general lexicographic/size-measure + ordering is **out of scope** (spec D1, deferred). +- **DD-4 — Diverge injection.** In `check_fn`, before the + `:2023-2028` reconcile loop: if `term_contains_loop(&f.body)` then + insert `"Diverge"` into the raised `effects` `BTreeSet`. + `term_contains_loop` recurses structurally but **stops at + `Term::Lam` boundaries** (a lambda is a value with its own arrow + effect row — a loop inside it executes on closure call, not here; + this mirrors exactly how `!IO` inside a lam does not leak to the + enclosing fn). The "calls a `Diverge`-declaring callee" half needs + **no new code**: a callee's `Type::Fn.effects` already flows into + the raised set at `lib.rs:3295-3297`, identically to `IO`. The + lam-arrow case (a `loop` inside a `Term::Lam` body ⇒ the lam's + arrow type carries `Diverge`) is wired at the existing lam + sub-effect reconcile site (recon `lib.rs:3582-3585`) with the same + `term_contains_loop`-stops-at-inner-lam check applied to the lam + body. The existing `UndeclaredEffect` (recon `lib.rs:438`, code + arm `:751`, raised at `:2026`) does the enforcement — **no new + diagnostic variant for Diverge**. Structural recursion injects + nothing. + +> Recon line numbers are HEAD-at-recon and may have drifted. Drive +> every edit site off `grep`/`cargo build`, not the literal numbers +> (cf. memory: recon misindexing recurs; the numbers are anchors, +> the symbols are authoritative). + +--- + +## Files this plan creates or modifies + +**Create:** +- Test: `crates/ailang-check/tests/structural_recursion_pin.rs` — + driver mirroring `loop_recur_pin.rs`; positives + negatives +- Test: `examples/struct_rec_list_len.ail` — positive: structural + list length (recurse on tail) +- Test: `examples/struct_rec_foldl_sum.ail` — positive: accumulator + (foldl-shape) over a list — structural, Diverge-free +- Test: `examples/struct_rec_tree_forest.ail` — positive: mutual + tree/forest, same family +- Test: `examples/loop_needs_diverge.ail` — positive: a fn that + declares `!Diverge` and contains a `loop` +- Test: `examples/test_non_structural_recursion.ail.json` — + negative: self-call on a non-decreasing arg, not `tail`-marked +- Test: `examples/test_mutual_cross_family.ail.json` — negative: + mutual recursion across two unrelated ADT families +- Test: `examples/test_loop_missing_diverge.ail.json` — negative: + `loop`-bearing fn that omits `!Diverge` + +**Modify:** +- `crates/ailang-check/src/lib.rs` — `CheckError` enum + (recon `:401-735`), `code()` (`:743-787`), `ctx()` (`:791-867`), + `check_fn` post-synth region (`:2011-2028`), the new pass + + helpers (new code, sited next to `verify_tail_positions` + `:2627`/`verify_loop_body` `:2769`), the lam sub-effect reconcile + (`:3582-3585`) +- `crates/ailang-core/tests/carve_out_inventory.rs` — `EXPECTED` + 17 → 20 (three new `.ail.json` negatives) + the stale "Twelve" + header comment (`:6`) +- `docs/DESIGN.md` — Decision 3 (`:163-168`), the Data-model it.2 + hook sentence (`:2449-2451`) + +--- + +## Task 1: `NonStructuralRecursion` diagnostic plumbing + +**Files:** `crates/ailang-check/src/lib.rs`. + +- [ ] **Step 1.1: RED — assert the code string exists.** + +In `crates/ailang-check/tests/structural_recursion_pin.rs` (new; +copy the harness preamble of `crates/ailang-check/tests/loop_recur_pin.rs` +verbatim — same `check_fixture`/`check_workspace`→`Vec` +helper): + +```rust +mod common; // if loop_recur_pin uses an inline helper, inline it identically here instead +#[test] +fn non_structural_recursion_code_is_registered() { + // A CheckError::NonStructuralRecursion must map to the kebab code. + // Construct it directly and assert code(); mirrors how the it.1 + // Recur* variants are unit-tested if such a test exists, else + // assert via a fixture in Task 2. This step only pins the code() + // arm exists and returns the exact string. + use ailang_check::CheckError; + let e = CheckError::NonStructuralRecursion { + callee: "f".into(), + arg: "n".into(), + }; + assert_eq!(e.code(), "non-structural-recursion"); +} +``` + +Run: `cargo test --workspace -p ailang-check non_structural_recursion_code_is_registered` +Expected: FAIL — `CheckError::NonStructuralRecursion` does not exist +(compile error: no variant). + +- [ ] **Step 1.2: Add the variant.** + +In `crates/ailang-check/src/lib.rs` `CheckError` enum, beside the +it.1 `RecurTypeMismatch`/`RecurNotInTailPosition` variants (recon +`:716-727`), add — Display body **bracket-`[code]`-free** (the CLI +formatter prepends `[code]`; F2 convention; mirror the it.1 `Recur*` +variants' exact attribute/field style): + +```rust +#[error("recursive call to `{callee}` is not on a structurally-smaller argument (`{arg}`); express this iteration as `(loop …)` / `recur`")] +NonStructuralRecursion { callee: String, arg: String }, +``` + +- [ ] **Step 1.3: `code()` + `ctx()` arms.** + +In `fn code()` (recon `:743-787`), beside the +`RecurNotInTailPosition => "recur-not-in-tail-position"` arm, add: + +```rust +CheckError::NonStructuralRecursion { .. } => "non-structural-recursion", +``` + +In `fn ctx()` (recon `:791-867`), before the `_ =>` empty-Object +fallthrough (`:865`), add a structured arm mirroring +`RecurTypeMismatch`'s ctx shape (recon `:862-864`): + +```rust +CheckError::NonStructuralRecursion { callee, arg } => { + serde_json::json!({ "callee": callee, "arg": arg }) +} +``` + +Do **not** add anything to `diagnostic.rs` — there is no doc-list +there; `code()` is the authoritative registry (memory: +plan-pseudo-vs-reality). + +- [ ] **Step 1.4: GREEN.** + +Run: `cargo test --workspace -p ailang-check non_structural_recursion_code_is_registered` +Expected: PASS. + +Run: `cargo test --workspace 2>&1 | tail -3` +Expected: green (additive variant; existing exhaustive `CheckError` +matches — if any non-`_` exhaustive match over `CheckError` fails to +compile, add the mirror arm there; drive off `cargo build` E0004). + +--- + +## Task 2: Self-structural-recursion pass + it.2-only grandfather + +**Files:** `crates/ailang-check/src/lib.rs`, +`examples/struct_rec_list_len.ail`, +`examples/struct_rec_foldl_sum.ail`, +`examples/test_non_structural_recursion.ail.json`, +`crates/ailang-check/tests/structural_recursion_pin.rs`, +`crates/ailang-core/tests/carve_out_inventory.rs`. + +- [ ] **Step 2.1: RED — fixtures + pins.** + +Create (Form-A spellings copied verbatim from an existing list +fixture — read `examples/std_list.ail` and match its `type`/`match`/ +ctor surface; do not invent surface): + +`examples/struct_rec_list_len.ail` — `len(xs)` recursing on the +tail bound by a `Cons` pattern (structural, Diverge-free). +`examples/struct_rec_foldl_sum.ail` — `go(xs, acc)` recursing on +tail with `acc` threaded (accumulator; structural by the tail +position; D1 — must pass clean, no Diverge). +`examples/test_non_structural_recursion.ail.json` — a self-call +where the structural-position arg is NOT a match-bound sub-component +(e.g. `f(n) = … f(n) …` or `f(xs) = … f(xs) …`), and the call is +**not** `tail`-marked. + +Add to `structural_recursion_pin.rs`: + +```rust +#[test] +fn structural_list_len_is_clean() { + assert!(check_fixture("examples/struct_rec_list_len.ail").is_empty()); +} +#[test] +fn foldl_accumulator_is_structural_and_clean() { + assert!(check_fixture("examples/struct_rec_foldl_sum.ail").is_empty()); +} +#[test] +fn non_structural_self_call_is_rejected() { + assert!(check_fixture("examples/test_non_structural_recursion.ail.json") + .contains(&"non-structural-recursion".to_string())); +} +``` + +Add the one new `.ail.json` to `carve_out_inventory.rs` `EXPECTED` +(17 → 18; fix the stale `:6` header comment count too). + +Run: `cargo test --workspace -p ailang-check --test structural_recursion_pin` +Expected: FAIL — no guardedness pass exists; all three fail +(positives clean only by accident, negative not rejected). + +- [ ] **Step 2.2: The pass — self-recursion + `smaller` algorithm (DD-2/DD-3).** + +Add next to `verify_tail_positions` (recon `:2627`): + +```rust +/// it.2: structural-recursion guardedness. A recursive call must +/// pass a structurally-smaller argument at some inferable parameter +/// position. Accumulator positions are unconstrained (spec D1). +/// it.2-only: a `tail: true`-marked recursive call is grandfathered +/// (spec it.2 "Transitional grandfather"; it.3 removes this). +fn verify_structural_recursion(f: &FnDef, env: &Env) -> Result<(), CheckError> { + let rec_name = &f.name; + // candidate structural positions: params whose decl type is an ADT Con + let cand: Vec = adt_param_positions(&f.ty, env); + let calls = collect_rec_calls(&f.body, rec_name); // Vec<&[Term]> arg-lists of unguarded-eligible calls + if calls.is_empty() { return Ok(()); } + for &i in &cand { + if calls.iter().all(|c| call_guarded_at(c, i, f, env)) { + return Ok(()); // some position is structural at every call + } + } + // not structural at any position — but grandfather tail-marked calls + let offending = first_unguarded_non_tail_call(&f.body, rec_name, &cand, f, env); + match offending { + None => Ok(()), // every unguarded call was tail:true (grandfathered) + Some((callee, arg)) => Err(CheckError::NonStructuralRecursion { callee, arg }), + } +} +``` + +Implement the helpers in the same module, fully: + +- `adt_param_positions(ty, env)` — from the fn's `Type::Fn { params, .. }`, + the indices whose `Type` is a `Type::Con { name, .. }` resolving + (via `env`) to a `type` decl (not a primitive `Int/Float/Bool/ + Unit/Str`, not `Type::Fn`). Use the existing env type-lookup + (grep how `synth` resolves a `Type::Con` to its decl). +- `collect_rec_calls(body, name)` — walk `body`; collect the + argument slice of every `Term::App { callee, args, tail }` where + `callee_name(callee) == name` (recon `callee_name` `:4127-4132`) + **and** `tail == false` (the grandfather: `tail == true` recursive + calls are not collected, hence never cause rejection). Also walk + into `Term::LetRec` clause bodies with the clause name. Stop at + `Term::Lam` (a lambda body is a separate def's territory; its own + `FnDef`-equivalent check covers it — keep it.2 conservative and + consistent with DD-4's lam boundary). +- `call_guarded_at(arg_slice, i, f, env)` — `arg_slice.get(i)` is + `Some(Term::Var { name })` and `name` is in the `smaller` set in + effect at that syntactic position. Implement `smaller` by a single + recursive walk `walk(term, smaller: &HashSet)` that, at + `Term::Match { scrutinee: Term::Var { name }, arms }` where + `name == param_i_name || smaller.contains(name)`, extends a clone + of `smaller` with every `Pattern::Ctor`-bound field variable of + each arm (recon: patterns are flat post-desugar — `Pattern::Ctor + { fields }` fields are `Pattern::Var`/`Pattern::Wild`, `ast.rs:611- + 626`) before recursing into that arm body. The recursive-call + argument check consults the `smaller` set live during this walk + (fold the call-collection and the guardedness test into the one + `smaller`-threaded walk rather than two passes, so position + context is exact). +- `first_unguarded_non_tail_call(...)` — same walk; returns the + `(callee_name, arg_display)` of the first non-`tail` recursive + call not guarded at any candidate position, for the diagnostic. + +(Use the real `Env`, `Type`, `Pattern`, `Term`, `callee_name` +identifiers from the neighbouring code — grep each before use; do +not invent. `arg_display` = the pretty/short form the it.1 `Recur*` +diagnostics use for an argument.) + +- [ ] **Step 2.3: Wire into `check_fn`.** + +In `check_fn`, immediately after the `verify_tail_positions(...)` +call (recon `:2021`) and before the effect reconcile (`:2023`): + +```rust +verify_structural_recursion(f, &env)?; +``` + +(Match the exact `env`/binding names in scope at that point — grep +the `verify_tail_positions` call site and mirror its argument +sourcing.) + +- [ ] **Step 2.4: GREEN.** + +Run: `cargo test --workspace -p ailang-check --test structural_recursion_pin` +Expected: PASS — list_len + foldl clean, non-structural rejected. + +Run: `cargo test --workspace 2>&1 | tail -3` +Expected: green. **Critical:** the 21 `tail-app` corpus fixtures +must still pass — they recurse non-structurally but are +`tail:true`-marked, so `collect_rec_calls` skips them (grandfather). +If any `tail-app` fixture now fails `non-structural-recursion`, the +grandfather is wrong — fix `collect_rec_calls`'s `tail == false` +guard, do not weaken the structural check. + +--- + +## Task 3: Mutual recursion — ADT-family components + +**Files:** `crates/ailang-check/src/lib.rs`, +`examples/struct_rec_tree_forest.ail`, +`examples/test_mutual_cross_family.ail.json`, +`crates/ailang-check/tests/structural_recursion_pin.rs`, +`crates/ailang-core/tests/carve_out_inventory.rs`. + +- [ ] **Step 3.1: RED.** + +`examples/struct_rec_tree_forest.ail` — mutual `tree_size`/ +`forest_size` over `type Tree = Node(Int, Forest)` / +`type Forest = Nil | Cons(Tree, Forest)` (the cross-reference makes +them one family component). `examples/test_mutual_cross_family.ail.json` +— `f`/`g` mutually recursive where `f`'s structural param is a +`List` and `g`'s is an unrelated `Tree` (distinct components). + +Add pins: `tree_forest_mutual_is_clean` (empty), and +`mutual_cross_family_is_rejected` +(`contains "non-structural-recursion"`). Add the new `.ail.json` to +`carve_out_inventory.rs` `EXPECTED` (18 → 19). + +Run: `cargo test --workspace -p ailang-check --test structural_recursion_pin` +Expected: FAIL — tree/forest rejected (cross-calls not recognised +as same-group) and/or cross-family not rejected. + +- [ ] **Step 3.2: ADT-family components + mutual grouping.** + +Add: + +```rust +/// Connected components of the ADT type-reference graph. +/// Two `type` names share a family iff one transitively appears in +/// the other's constructor field types (undirected, union-find). +fn adt_families(env: &Env) -> UnionFind { /* … */ } + +/// FnDefs that (a) directly call each other and (b) each have a +/// structural param whose type head is in one family component. +fn mutual_structural_group<'a>(f: &'a FnDef, module: &'a [FnDef], fams: &UnionFind) -> Vec<&'a FnDef> { /* … */ } +``` + +Extend `verify_structural_recursion`: if `f` is in a +`mutual_structural_group`, a cross-call to a group member is +treated like a self-call for the `smaller`/`call_guarded_at` test +(the callee's structural arg must be in the *caller's* `smaller` +set), and `collect_rec_calls` collects cross-group callees too +(still `tail == false` only — grandfather still applies). A mutual +fn whose group fails the family-component test, or whose cross-call +arg is not smaller, yields `NonStructuralRecursion`. + +(`UnionFind` — use a tiny inline `BTreeMap`-backed union-find in +this module; do not add a dependency. The module FnDef list: grep +how `check_fn` is iterated per workspace module and pass the +sibling `FnDef`s in; if `check_fn` is called per-def without the +sibling list, thread the module's `&[FnDef]` into +`verify_structural_recursion` from the same caller that has the +module — recon: confirm the workspace-check loop's module handle.) + +- [ ] **Step 3.3: GREEN.** + +Run: `cargo test --workspace -p ailang-check --test structural_recursion_pin` +Expected: PASS — tree/forest clean, cross-family rejected. + +Run: `cargo test --workspace 2>&1 | tail -3` +Expected: green; `tail-app` corpus still grandfathered-clean. + +--- + +## Task 4: Diverge effect injection (DD-4) + +**Files:** `crates/ailang-check/src/lib.rs`, +`examples/loop_needs_diverge.ail`, +`examples/test_loop_missing_diverge.ail.json`, +`crates/ailang-check/tests/structural_recursion_pin.rs`, +`crates/ailang-core/tests/carve_out_inventory.rs`. + +- [ ] **Step 4.1: RED.** + +`examples/loop_needs_diverge.ail` — a fn whose body contains a +`(loop …)` and whose signature **declares** `!Diverge` (copy the +`loop_counter.ail` shape from it.1; add `Diverge` to its effect +row — grep how `!IO` is written in a Form-A fn signature and mirror +it for `Diverge`). `examples/test_loop_missing_diverge.ail.json` — +the same fn but **without** `Diverge` in the declared effect row. + +Pins: + +```rust +#[test] +fn loop_fn_declaring_diverge_is_clean() { + assert!(check_fixture("examples/loop_needs_diverge.ail").is_empty()); +} +#[test] +fn loop_fn_missing_diverge_is_rejected() { + assert!(check_fixture("examples/test_loop_missing_diverge.ail.json") + .contains(&"undeclared-effect".to_string())); +} +#[test] +fn structural_recursion_is_diverge_free() { + // struct_rec_list_len has no loop, no Diverge declared → clean + assert!(check_fixture("examples/struct_rec_list_len.ail").is_empty()); +} +``` + +Add the `.ail.json` to `carve_out_inventory.rs` `EXPECTED` (19 → 20). + +Run: `cargo test --workspace -p ailang-check --test structural_recursion_pin` +Expected: FAIL — `loop_fn_missing_diverge_is_rejected` fails (loop +does not yet inject Diverge, so no `undeclared-effect`). + +- [ ] **Step 4.2: `term_contains_loop` + injection.** + +Add: + +```rust +/// True iff `t` syntactically contains a `Term::Loop`, NOT +/// descending into `Term::Lam` bodies (a lambda's loop runs on +/// closure call; it carries Diverge on the lam's own arrow type, +/// not on the enclosing fn — coherent with how !IO scopes to lam). +fn term_contains_loop(t: &Term) -> bool { + match t { + Term::Loop { .. } => true, + Term::Lam { .. } => false, + // recurse into every other child; mirror the child set of + // the existing structural Term walks (grep verify_tail_positions + // arms for the exhaustive child list) + _ => term_children(t).iter().any(|c| term_contains_loop(c)), + } +} +``` + +(If no `term_children` helper exists, write the explicit match over +all `Term` variants — drive the variant list off `cargo build` +exhaustiveness, mirror `verify_tail_positions`' arm set; `Term::Lam` +returns `false`, `Term::Loop` returns `true`, all others recurse +their children incl. `Term::Recur` args, `Term::Match` arms, +`Term::Let/If/Seq/App/Do/Mut/Assign/...`.) + +In `check_fn`, before the `:2023-2028` declared-vs-raised reconcile +loop, after the raised `effects` set is populated: + +```rust +if term_contains_loop(&f.body) { + effects.insert("Diverge".to_string()); +} +``` + +(Use the exact raised-set identifier and type the reconcile loop +reads — recon: a `BTreeSet` named `effects`; grep the +`UndeclaredEffect`-raising loop at `:2023-2028` and match its source +set name exactly.) + +- [ ] **Step 4.3: Lam-arrow Diverge coherence.** + +At the `Term::Lam` sub-effect reconcile site (recon `:3582-3585`): +if the lam body `term_contains_loop`, ensure `"Diverge"` is in the +lam's reconciled raised-effect set before it is checked against the +lam's declared arrow effects (same `term_contains_loop`, applied to +the lam body; the helper's own `Term::Lam => false` correctly stops +at a *further-nested* lam). Mirror the existing `!IO`-through-lam +reconcile shape verbatim, only adding the loop→Diverge insert. + +- [ ] **Step 4.4: GREEN.** + +Run: `cargo test --workspace -p ailang-check --test structural_recursion_pin` +Expected: PASS — declaring-Diverge clean, missing-Diverge rejected +with `undeclared-effect`, structural recursion still Diverge-free. + +Run: `cargo test --workspace 2>&1 | tail -3` +Expected: green. The it.1 `loop_counter.ail`/`loop_in_lambda_e2e.ail` +fixtures: if they have a `(loop …)` but no declared `!Diverge`, +they now (correctly) require it — **update those two it.1 fixtures' +signatures to declare `!Diverge`** (this is the first iteration +where a bare loop is an error; it is in-scope: the spec's it.2 says +loop-bearing fns carry `!Diverge`, and the it.1 fixtures are loop- +bearing). Record the fixture-signature update in the journal. Do +NOT instead weaken the injection. + +--- + +## Task 5: DESIGN.md prose sync + +**Files:** `docs/DESIGN.md`. + +- [ ] **Step 5.1: Decision 3 amendment.** + +Edit `docs/DESIGN.md` Decision 3 (recon `:163-168`). Current text +calls `Diverge` a nominally-wired MVP effect. Replace the relevant +sentence so it states: `Diverge` is the effect carried by any +function whose body contains a `loop` (or that calls a +`Diverge`-declaring function); structural recursion is pure and +total and carries no effect. Keep `IO` description intact. + +- [ ] **Step 5.2: Data-model it.2 hook sentence.** + +Edit the §"Data model" `loop`/`recur` block sentence (recon +`:2449-2451`) that says "The structural-recursion restriction and +the Diverge effect land in it.2" → state they are now in effect +(present tense), `tail-app`/`tail-do` retirement remains it.3. + +- [ ] **Step 5.3: Drift-anchor regression check.** + +Run: `cargo test --workspace -p ailang-core design_schema_drift schema_coverage spec_drift` +Expected: PASS — it.2 adds no AST variant; §"Data model" `loop`/ +`recur` anchors are unchanged (only the trailing status sentence +inside the block is reworded; verify the anchor strings the test +greps are not the reworded substring). If the drift test scans a +substring you changed, restore that exact substring and move the +status note to an adjacent line. + +--- + +## Task 6: it.2 acceptance gate + +**Files:** none (verification only). + +- [ ] **Step 6.1: Full workspace.** + +Run: `cargo test --workspace 2>&1 | tail -3` +Expected: all green. + +- [ ] **Step 6.2: Spec it.2 acceptance bullets (verbatim).** + +Verify each, by the named pin: +- structural list/tree/JSON walk + foldl accumulator clean, + Diverge-free → `structural_list_len_is_clean`, + `foldl_accumulator_is_structural_and_clean`, + `structural_recursion_is_diverge_free`, `tree_forest_mutual_is_clean` +- non-structural recursion-by-call → `non_structural_self_call_is_rejected` +- loop-bearing fn missing `!Diverge` → `loop_fn_missing_diverge_is_rejected` +- mutual same-family passes, cross-family fails → + `tree_forest_mutual_is_clean`, `mutual_cross_family_is_rejected` +- `mut_counter`/`mut_sum_floats` not migrated, still grandfathered: + Run `ail run examples/mut_counter.ail` → still `55` (they use + `tail-app`; grandfathered; unchanged) +- `cargo test --workspace` green → Step 6.1 + +- [ ] **Step 6.3: tail-app corpus grandfather proof.** + +Run: `ail check examples/bench_compute_intsum.ail examples/list_map_poly.ail examples/sort.ail` +Expected: all clean (non-structural but `tail:true`-marked → +grandfathered; this is the load-bearing it.2 invariant that keeps +the corpus alive until it.3 migrates it). + +--- + +## Self-review (planner Step 5) + +1. **Spec coverage.** Spec §Components it.2 (a) guardedness → T2/T3; + (b) grandfather → T2.2 (`collect_rec_calls` `tail==false`); (c) + Diverge → T4; (d) DESIGN.md → T5. §Error-handling + `NonStructuralRecursion` (one new variant, `UndeclaredEffect` + reused) → T1/T4. §Data-flow steps 3–4 → T2/T3 (pass) + T4 + (effect reconcile). §Testing-strategy it.2 + acceptance bullets + → T2/T3/T4 pins + T6. D1 (implicit, foldl=structural, + same-family) → DD-2/DD-3 + the foldl pin. D2 (Diverge, no new + variant) → DD-4 + T4. All it.2 sections covered; it.3 explicitly + excluded everywhere. +2. **Placeholder scan.** No "TBD/TODO/implement later/similar to + Task/add appropriate". The pass helpers are specified with + signatures + the exact algorithm (DD-2/DD-3) + the + grep-the-real-identifier instruction; that is an exact + transformation, not a placeholder. Per memory + (plan-pseudo-vs-reality): no prose round-trip is scripted + anywhere; no `diagnostic.rs` doc-list claim (Step 1.3 explicitly + says `code()` is the registry, do not touch diagnostic.rs); + recon line numbers are flagged drift-prone with "drive off + grep/cargo build" in the DD preamble. +3. **Type/name consistency.** `NonStructuralRecursion {callee,arg}`, + code `non-structural-recursion`, `verify_structural_recursion`, + `term_contains_loop`, `adt_families`, `mutual_structural_group`, + `collect_rec_calls`, `call_guarded_at`, + `structural_recursion_pin.rs`, the eight fixtures — consistent + across all tasks and the files section. +4. **Step granularity.** Each step is one action (one fixture set / + one helper / one wire-in / one command) in the 2–5-min band; the + largest (T2.2, the pass) is one cohesive algorithm with the + algorithm given. +5. **No commit steps.** None. Work stays in the working tree; Boss + commits the whole it.2 diff at iter end. + +Recorded risk (named, with decision rule — not a placeholder): if +`check_fn` is invoked per-`FnDef` without the sibling module +`&[FnDef]` in scope (T3.2 needs it for mutual grouping), thread the +module slice from the workspace-check loop that already owns it +(recon flagged this as the one unconfirmed handle); the self-only +path (T2) is unaffected and lands first, so T3 can be re-scoped to +"self + same-file siblings via the existing module iteration" if +the workspace handle proves awkward — T2's value ships regardless.