plan: it.2 guardedness checker + Diverge effect — 6 tasks

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.
2026-05-15 14:50:22 +02:00
parent 96db54d15d
commit bc9f512003
1 changed files with 663 additions and 0 deletions
@@ -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<String>` = 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<String>`
 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<usize> = 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<String>)` 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<String> { /* … */ }
 /// 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<String>) -> 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<String>` 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.