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.

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<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.