AILang/docs/plans/0077-loop-recur.2.md

# loop-recur.2 — Typecheck Semantics (Component 4) — Implementation Plan

> **Parent spec:** `docs/specs/0034-loop-recur.md`
>
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
> to run this plan. Steps use `- [ ]` checkboxes for tracking.

**Goal:** Replace the iter-1 `synth` `CheckError::Internal` stub for
`Term::Loop` / `Term::Recur` with real typecheck semantics — binder
typing, positional `recur` arity + per-arg type checking via a
`loop_stack` frame, a new private `verify_loop_body` tail-position
pass, and the four `Recur*` diagnostics — so a `sum_to`-class loop
program passes `ail check` and the four negatives fire point-exactly.

**Architecture:** `synth` gains a `loop_stack: &mut Vec<Vec<Type>>`
param threaded exactly as mut.2's `mut_scope_stack` (stack of
*ordered binder-type vectors* — `recur` is positional, not
name-keyed, so unlike `mut` the frame is not an `IndexMap`; binder
*names* enter the ordinary `locals` scope exactly as `Term::Let`
binds its name). `Term::Loop` synths each binder init (later inits
+ body see earlier binder names via `locals`), pushes the ordered
binder types onto `loop_stack`, synths the body (loop's static type
= body's type), pops. `Term::Recur` reads `loop_stack.last()`:
empty → `RecurOutsideLoop`; arg-count ≠ binder-count →
`RecurArityMismatch`; per-arg subst-compare ≠ binder type →
`RecurTypeMismatch` (Assign-style structural pre-check, NOT
`unify`-propagate — see Boss call 1); `recur`'s own result is a
fresh metavar (it transfers control, never falls through). A NEW
private `verify_loop_body` (sibling of the spec-frozen
`verify_tail_positions`) enforces `recur` only in tail position of
its enclosing loop body (`RecurNotInTailPosition`); it runs in
`check_fn` *after* `synth`, so `RecurOutsideLoop`/arity/type (synth)
take code-precedence over the tail-position code by construction.

**Tech Stack:** `ailang-check` (lib.rs — `CheckError`, `code`,
`ctx`, `synth`, `check_fn`, new `verify_loop_body`); `examples/`
(4 negative `.ail.json` fixtures + 1 positive `.ail`);
`ailang-core/tests/carve_out_inventory.rs`; new
`ailang-check/tests/loop_recur_typecheck_pin.rs`;
`ail/tests/ct1_check_cli.rs`.

---

## Boss design calls baked into this plan (settled — do not re-litigate)

1. **`RecurTypeMismatch` is an Assign-style structural pre-check,
   not a `unify`-propagate.** The recon found two in-file
   precedents: mut.2 `Term::Mut`-init lets `unify(&v.ty,&init_ty,
   subst)?` propagate its own `CheckError::TypeMismatch` (code
   `type-mismatch`); mut.2 `Term::Assign` does NOT — it synths the
   value, `subst.apply`s both sides, structurally compares
   `applied_declared != applied_value`, and catch-wraps into the
   dedicated `AssignTypeMismatch`. The spec §"Error handling" +
   §"Acceptance criteria" mandate a dedicated `recur-type-mismatch`
   code that fires *point-exactly* on its negative fixture. Only
   the Assign-style mechanism satisfies that (a `unify`-propagate
   would surface `type-mismatch`, failing the acceptance). So
   `Term::Recur` per-arg checking mirrors the `Term::Assign` arm
   (`lib.rs:3716-3730`) verbatim in mechanism: synth the arg,
   `subst.apply` both the arg type and the binder type, structural
   `!=`, on mismatch `Err(RecurTypeMismatch{position,expected,got})`.
   Rationale is semantic (one in-repo mechanism for "declared-vs-
   actual at a binding site with its own point-exact code",
   consistent with `AssignTypeMismatch`), not effort.

2. **`loop_stack` element type is `Vec<Type>` (ordered binder
   types), NOT `IndexMap<String,Type>`.** mut.2's
   `mut_scope_stack: Vec<IndexMap<String,Type>>` is name-keyed
   because `assign`/`var` resolve mut-vars *by name*. `recur` has
   no by-name rebinding — it rebinds binders *positionally*. The
   frame must model exactly what `Term::Recur` consumes: the
   ordered binder types, for arity (`.len()`) and per-position type
   checks. Binder *names* enter the ordinary `locals: &mut
   IndexMap<String,Type>` exactly as `Term::Let` binds its name
   (`lib.rs:3205-3218` is the verbatim precedent) so later inits
   and the body resolve them through the normal locals/globals
   chain. The spec phrase "threaded exactly as mut.2's
   `mut_scope_stack`" governs the *threading discipline* (a
   `&mut Vec<…>` pushed/popped around the body, passed through
   every recursive `synth`), not the element type. Semantic, not
   effort.

3. **Diagnostic-code precedence is by pass ordering, already
   correct.** `RecurOutsideLoop` / `RecurArityMismatch` /
   `RecurTypeMismatch` are raised in `synth` (runs at
   `check_fn:1970`); `RecurNotInTailPosition` is raised in the new
   `verify_loop_body` (runs after, analogous to
   `verify_tail_positions` at `check_fn:1980`). A `recur` outside
   any loop therefore fires `RecurOutsideLoop` (synth, first), not
   `RecurNotInTailPosition` — exactly the spec-correct code. No
   explicit ordering logic is needed; the pass sequence is the
   mechanism. `verify_loop_body` is entered only on synth success,
   so by then every `recur` is known to be inside a loop with
   matching arity/types; the pass adds only the tail rule.

---

## Files this plan creates or modifies

- Modify: `crates/ailang-check/src/lib.rs`
  - `:705`-area — 4 new `CheckError` variants (after
    `MutVarCapturedByLambda` `:697`, before `Internal` `:703`).
  - `:751`-area — 4 new `code()` arms (after
    `MutVarCapturedByLambda` `:750`).
  - `:824`-area — 2 new `ctx()` arms (after
    `MutVarCapturedByLambda` `:822-824`, before the `_ =>`
    catch-all `:825`).
  - `:2772` — `synth` signature: add `loop_stack` param.
  - 22 internal recursive `synth(...)` call sites + `:1970`
    (check_fn) + `:2748` (check_const) + test-module callers —
    thread `loop_stack` (build-gated; see Task 2).
  - `:3740-3742` — replace the iter-1 Loop/Recur `Internal` stub
    with the two real arms.
  - `:1969`-adjacent + `:1970` + after `:1980` (check_fn) —
    declare `loop_stack`, thread into the synth call, invoke
    `verify_loop_body`.
  - new private `fn verify_loop_body` (place immediately after
    `verify_tail_positions`, which ends `:2725`).
- Create: `examples/test_recur_outside_loop.ail.json`
- Create: `examples/test_recur_arity_mismatch.ail.json`
- Create: `examples/test_recur_type_mismatch.ail.json`
- Create: `examples/test_recur_not_in_tail_position.ail.json`
- Reuse (no new file): `examples/loop_sum_to.ail` (shipped iter-1
  as the round-trip fixture) — now also the positive `ail check`
  evidence: it returned the `Internal` stub in iter-1, must
  typecheck clean in iter-2. One fixture, two properties
  (round-trips AND typechecks); no near-duplicate is created.
- Create: `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`
  (mirror of `mut_typecheck_pin.rs`).
- Modify: `crates/ailang-core/tests/carve_out_inventory.rs:6-40`
  (header prose refresh + 4 `EXPECTED` entries; 13 → 17).
- Modify: `crates/ail/tests/ct1_check_cli.rs` — add a sibling
  `check_human_mode_renders_recur_diagnostic_code_exactly_once`.
- No edit: `verify_tail_positions` (`:2607-2725`, spec-frozen
  tail-app role — its iter-1 Loop/Recur descent arms stay);
  the drift trio (`design_schema_drift`/`spec_drift`/
  `schema_coverage` — iter-2 adds no schema); `round_trip.rs`
  (auto-discovers `.ail` only; negatives are `.ail.json` carve-
  outs, exempt by construction).

---

## Task 1: The four `Recur*` `CheckError` variants + `code()` + `ctx()`

**Files:** Modify `crates/ailang-check/src/lib.rs`

- [ ] **Step 1: Write the failing code() unit test**

In `crates/ailang-check/src/lib.rs`, in the `#[cfg(test)] mod
tests` (near the mut-family unit tests), add:

```rust
    #[test]
    fn recur_checkerror_codes_are_exact() {
        assert_eq!(CheckError::RecurOutsideLoop.code(), "recur-outside-loop");
        assert_eq!(
            CheckError::RecurArityMismatch { expected: 2, got: 1 }.code(),
            "recur-arity-mismatch"
        );
        assert_eq!(
            CheckError::RecurTypeMismatch {
                position: 0,
                expected: "Int".into(),
                got: "Bool".into(),
            }
            .code(),
            "recur-type-mismatch"
        );
        assert_eq!(
            CheckError::RecurNotInTailPosition.code(),
            "recur-not-in-tail-position"
        );
    }
```

- [ ] **Step 2: Run test to verify it fails to compile**

Run: `cargo test -p ailang-check --lib recur_checkerror_codes_are_exact 2>&1 | tail -5`
Expected: FAIL — `error[E0599]: no variant ... RecurOutsideLoop` etc.

- [ ] **Step 3: Add the four variants**

In `crates/ailang-check/src/lib.rs`, immediately after the
`MutVarCapturedByLambda { name: String }` variant (ends `:697`),
before the `/// Iter 22b.3 …` doc + `Internal(String)` (`:699-704`),
add (bracket-`[code]`-free `#[error(...)]`, F2 convention,
mirroring the mut.2 variant style at `:661-697`):

```rust
    /// loop-recur iter 2: `Term::Recur` reached typecheck with no
    /// lexically-enclosing `Term::Loop` (the `loop_stack` was empty).
    #[error("`recur` is only valid inside a `loop` — there is no enclosing loop here")]
    RecurOutsideLoop,

    /// loop-recur iter 2: `Term::Recur`'s argument count differs from
    /// the enclosing loop's binder count. `recur` rebinds every loop
    /// binder positionally, so the counts must match exactly.
    #[error("`recur` passes {got} argument(s) but the enclosing loop has {expected} binder(s) — recur must rebind every binder positionally")]
    RecurArityMismatch { expected: usize, got: usize },

    /// loop-recur iter 2: a `recur` argument's type differs from the
    /// corresponding loop binder's declared type (0-based position).
    #[error("`recur` argument {position} has type `{got}` but the enclosing loop's binder at that position is `{expected}` — every recur argument must match its binder's type")]
    RecurTypeMismatch {
        position: usize,
        expected: String,
        got: String,
    },

    /// loop-recur iter 2: `Term::Recur` appears somewhere other than
    /// the tail position of its enclosing loop body. `recur` is a
    /// structural back-jump; it cannot be a sub-expression.
    #[error("`recur` must be in tail position of its enclosing `loop` body — it is a back-jump, not a value-producing sub-expression")]
    RecurNotInTailPosition,
```

- [ ] **Step 4: Add the four `code()` arms**

In `pub fn code(&self)`'s `match self`, immediately after
`CheckError::MutVarCapturedByLambda { .. } => "mut-var-captured-by-lambda",`
(`:750`), before `CheckError::Internal(_) => "internal",` (`:751`),
add:

```rust
            CheckError::RecurOutsideLoop => "recur-outside-loop",
            CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
            CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
            CheckError::RecurNotInTailPosition => "recur-not-in-tail-position",
```

- [ ] **Step 5: Add the two `ctx()` arms**

In `pub fn ctx(&self)`'s `match self`, immediately after
`CheckError::MutVarCapturedByLambda { name } => { … }` (ends
`:824`), before the `_ => serde_json::Value::Object(...)`
catch-all (`:825`), add (arity mirrors the `ArityMismatch`
`{expected, actual}` precedent at `:763-765`; type mirrors
`AssignTypeMismatch`'s `{name?,expected,actual}` shape at
`:816-818` but positional; `RecurOutsideLoop` /
`RecurNotInTailPosition` deliberately use the `{}` catch-all —
no actionable structured context beyond the message):

```rust
            CheckError::RecurArityMismatch { expected, got } => {
                serde_json::json!({"expected": expected, "actual": got})
            }
            CheckError::RecurTypeMismatch { position, expected, got } => {
                serde_json::json!({"position": position, "expected": expected, "actual": got})
            }
```

- [ ] **Step 6: Run the code() test to verify it passes**

Run: `cargo test -p ailang-check --lib recur_checkerror_codes_are_exact 2>&1 | tail -5`
Expected: PASS — `test result: ok. 1 passed`. (The crate compiles:
`code()` is exhaustive and now has all four arms; the `synth`
Loop/Recur stub still returns `Internal` and does not yet use the
new variants — that is Task 3.)

---

## Task 2: `synth` signature + `loop_stack` threading

**Files:** Modify `crates/ailang-check/src/lib.rs`

Pure mechanical param threading. The `synth` Loop/Recur arm is
still the iter-1 `Internal` stub after this task (it does not
reference `loop_stack`), so the crate compiles once threading is
complete. The compiler is the exhaustive completeness oracle: a
missed caller is a hard `error[E0061] this function takes N
arguments`.

- [ ] **Step 1: Add the `loop_stack` parameter to `synth`**

In `pub(crate) fn synth(`, immediately after the
`mut_scope_stack: &mut Vec<IndexMap<String, Type>>,` parameter
(`:2772`), add:

```rust
    // loop-recur iter 2: per-walk loop-binder-type stack. Each frame
    // is one `Term::Loop`'s binder types in declaration order
    // (positional — `recur` rebinds binders by position, not name,
    // so this is `Vec<Type>` not name-keyed like `mut_scope_stack`).
    // Pushed on `Term::Loop` body entry, popped on exit; consulted
    // innermost-first by `Term::Recur` for arity + per-position type.
    // Position: mut_scope_stack-adjacent — both are per-fn-body
    // lexical-control scope state threaded identically.
    loop_stack: &mut Vec<Vec<Type>>,
```

- [ ] **Step 2: Thread `loop_stack` at every recursive call site**

The threading rule is uniform: in every `synth(...)` call, insert
the `loop_stack` argument **immediately after the `mut_scope_stack`
argument** (positionally matching the signature). For the 22
recursive call sites inside `fn synth` (the in-scope `loop_stack`
param is threaded through): `:3161`, `:3197`, `:3206`, `:3208`,
`:3220`, `:3222`, `:3223`, `:3241`, `:3336`, `:3345`, `:3363`,
`:3438`, `:3440`, `:3474`, `:3562`, `:3589`, `:3605`, `:3619`,
`:3649`, and the three multi-line calls headed at `:3674`,
`:3683`, `:3717`. Example transform (the `Term::Let` arm at
`:3206`/`:3208`):

```rust
// before:
let v = synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
// after:
let v = synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
```

- [ ] **Step 3: Thread `loop_stack` at the external (non-recursive) callers**

- `check_fn` `:1970`: handled in Task 4 Step 4 (it declares its
  own fresh `loop_stack`).
- `check_const` `:2748`: a const value has no enclosing loop.
  Immediately before the `synth(&c.value, …)` call, add
  `let mut loop_stack: Vec<Vec<Type>> = Vec::new();` and pass
  `&mut loop_stack` immediately after `&mut mut_scope_stack` in
  that call. (Any `recur` in a const value then correctly fires
  `RecurOutsideLoop`.)

- [ ] **Step 4: Build-gated completeness sweep**

Run: `cargo build -p ailang-check 2>&1 | grep -E 'this function takes|error\[E0061\]' | sort -u`
Expected first run: a list of remaining `synth(...)` callers in
the `#[cfg(test)]` module (the `let err = synth(`/`let ty = synth(`/
`let _ = synth(` sites the recon located at `:4123`, `:4165`,
`:4208`, `:4313`, `:4353`, `:4392`, `:4494`, `:7233`). For each:
these are loop-free unit-test call sites — insert a
`let mut loop_stack: Vec<Vec<Type>> = Vec::new();` before the call
(or reuse one already in scope) and pass `&mut loop_stack`
immediately after the `mut_scope_stack`/`&mut mut_scope_stack`
argument, exactly as Step 3.

Re-run the command until it prints nothing.
Then run: `cargo build -p ailang-check 2>&1 | tail -2`
Expected: PASS — `Finished` (0 errors). The threading is
complete iff the crate compiles; this is the exhaustive gate.

- [ ] **Step 5: Confirm the suite still green (stub intact)**

Run: `cargo test -p ailang-check --lib 2>&1 | grep -E '^test result:' | tail -1`
Expected: PASS — the `synth` Loop/Recur arm is still the iter-1
`Internal` stub (unchanged); no behaviour changed, only an unused
threaded param was added.

---

## Task 3: Real `synth` `Term::Loop` + `Term::Recur` arms

**Files:** Modify `crates/ailang-check/src/lib.rs`

- [ ] **Step 1: Write the failing positive-typecheck pin**

Create `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`
with the harness mirrored verbatim from `mut_typecheck_pin.rs`
(same `examples_dir()` + `check_fixture()` helpers) and this first
test:

```rust
//! loop-recur iter 2: pin tests that the loop/recur typecheck
//! fixtures produce the expected diagnostic codes (or zero
//! diagnostics for the positive sum_to-class case). Mirrors
//! `mut_typecheck_pin.rs`; negative fixtures live as `.ail.json`
//! so the diagnostic code is the load-bearing assertion.

use ailang_check::check_workspace;
use ailang_surface::load_workspace;
use std::path::PathBuf;

fn examples_dir() -> PathBuf {
    let manifest = env!("CARGO_MANIFEST_DIR");
    PathBuf::from(manifest)
        .parent().expect("crates/ailang-check parent")
        .parent().expect("crates/ parent")
        .join("examples")
}

fn check_fixture(fixture_name: &str) -> Vec<String> {
    let path = examples_dir().join(fixture_name);
    let ws = load_workspace(&path)
        .unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}"));
    let diags = check_workspace(&ws);
    diags.iter().map(|d| d.code.clone()).collect()
}

#[test]
fn loop_sum_to_typechecks_clean() {
    // examples/loop_sum_to.ail shipped in iter-1 as the round-trip
    // fixture; in iter-2 it must ALSO typecheck clean (it returned
    // the synth Internal stub in iter-1). One fixture, two
    // properties — no near-duplicate corpus file.
    let codes = check_fixture("loop_sum_to.ail");
    assert!(codes.is_empty(), "expected zero diagnostics, got {codes:?}");
}
```

(The four negative tests are added in Task 5 Step 4 — same file.)

- [ ] **Step 2: Run the positive pin RED (no fixture creation — reuse iter-1's)**

`examples/loop_sum_to.ail` already exists (shipped iter-1,
commit `a179ec3`); do NOT create a new fixture.

Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin loop_sum_to_typechecks_clean 2>&1 | tail -6`
Expected: FAIL — `codes == ["internal"]` (the iter-1 `synth`
Loop/Recur stub returns `CheckError::Internal`; `ail check`
surfaces it as code `internal`, so the list is non-empty).

- [ ] **Step 3: Replace the `Internal` stub with the real arms**

In `crates/ailang-check/src/lib.rs`, replace the iter-1 stub
(`:3740-3742`, verbatim):

```rust
        Term::Loop { .. } | Term::Recur { .. } => Err(CheckError::Internal(
            "Term::Loop/Term::Recur typecheck lands in loop-recur iter 2".into(),
        )),
```

with the two real arms (binder-name scoping mirrors the
`Term::Let` arm `:3205-3218` verbatim; per-arg type check mirrors
the `Term::Assign` arm `:3716-3730` verbatim per Boss call 1;
fresh metavar via `Subst::fresh(counter)` per `:57-61` /
`:3038`):

```rust
        // loop-recur iter 2: each binder init is synthed in the
        // outer scope plus already-declared binder names of THIS
        // loop (declaration order; later inits + body see earlier
        // binders via `locals`, exactly as `Term::Let` binds its
        // name). The loop's static type is the body's type. The
        // ordered binder types are pushed onto `loop_stack` for the
        // body walk so an inner `Term::Recur` can position-check
        // against them; popped on exit. Binder names are NOT in
        // `loop_stack` (recur is positional, not by-name).
        Term::Loop { binders, body } => {
            let mut binder_tys: Vec<Type> = Vec::new();
            let mut restore: Vec<(String, Option<Type>)> = Vec::new();
            for b in binders {
                let init_ty = synth(
                    &b.init, env, locals, mut_scope_stack, loop_stack, effects,
                    in_def, subst, counter, residuals, free_fn_calls, warnings,
                )?;
                unify(&b.ty, &init_ty, subst)?;
                binder_tys.push(b.ty.clone());
                let prev = locals.insert(b.name.clone(), b.ty.clone());
                restore.push((b.name.clone(), prev));
            }
            loop_stack.push(binder_tys);
            let body_result = synth(
                body, env, locals, mut_scope_stack, loop_stack, effects,
                in_def, subst, counter, residuals, free_fn_calls, warnings,
            );
            loop_stack.pop();
            for (name, prev) in restore.into_iter().rev() {
                match prev {
                    Some(p) => {
                        locals.insert(name, p);
                    }
                    None => {
                        locals.shift_remove(&name);
                    }
                }
            }
            body_result
        }
        // loop-recur iter 2: recur re-enters the innermost enclosing
        // loop, rebinding its binders positionally. RecurOutsideLoop
        // when `loop_stack` is empty; RecurArityMismatch on count
        // disagreement; RecurTypeMismatch via the Assign-style
        // subst-apply-then-structural-compare (Boss call 1) so the
        // dedicated code fires point-exactly. recur's OWN type is a
        // fresh metavar — it transfers control and never falls
        // through, so it unifies with whatever sibling branch the
        // enclosing if/match requires.
        Term::Recur { args } => {
            let binder_tys = match loop_stack.last() {
                None => return Err(CheckError::RecurOutsideLoop),
                Some(tys) => tys.clone(),
            };
            if args.len() != binder_tys.len() {
                return Err(CheckError::RecurArityMismatch {
                    expected: binder_tys.len(),
                    got: args.len(),
                });
            }
            for (i, a) in args.iter().enumerate() {
                let arg_ty = synth(
                    a, env, locals, mut_scope_stack, loop_stack, effects,
                    in_def, subst, counter, residuals, free_fn_calls, warnings,
                )?;
                let applied_binder = subst.apply(&binder_tys[i]);
                let applied_arg = subst.apply(&arg_ty);
                if applied_binder != applied_arg {
                    return Err(CheckError::RecurTypeMismatch {
                        position: i,
                        expected: ailang_core::pretty::type_to_string(&applied_binder),
                        got: ailang_core::pretty::type_to_string(&applied_arg),
                    });
                }
            }
            Ok(Subst::fresh(counter))
        }
```

- [ ] **Step 4: Run the positive pin to verify it passes**

Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin loop_sum_to_typechecks_clean 2>&1 | tail -6`
Expected: PASS — zero diagnostics (binder typing succeeds; `recur`
arity 2 == 2 binders, both `Int`, fresh-metavar result unifies
with the `if`'s `acc` branch which is `Int`).

---

## Task 4: `verify_loop_body` private pass + `check_fn` wiring

**Files:** Modify `crates/ailang-check/src/lib.rs`

- [ ] **Step 1: Write the failing tail-position fixture + pin**

Create `examples/test_recur_not_in_tail_position.ail.json` (the
spec §"Concrete code shapes" `bad_recur` program, canonical JSON;
envelope mirrors `examples/test_mut_assign_outside_mut.ail.json`):

```json
{
  "schema": "ailang/v0",
  "name": "test_recur_not_in_tail_position",
  "imports": [],
  "defs": [
    {
      "kind": "fn",
      "name": "bad_recur",
      "type": {
        "k": "fn",
        "params": [ { "k": "con", "name": "Int" } ],
        "ret": { "k": "con", "name": "Int" },
        "effects": []
      },
      "params": [ "n" ],
      "doc": "loop-recur iter 2: recur as an argument to + is NOT in tail position -> recur-not-in-tail-position.",
      "body": {
        "t": "loop",
        "binders": [
          { "name": "i", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }
        ],
        "body": {
          "t": "app",
          "fn": { "t": "var", "name": "+" },
          "args": [
            { "t": "lit", "lit": { "kind": "int", "value": 1 } },
            { "t": "recur", "args": [ { "t": "app", "fn": { "t": "var", "name": "+" }, "args": [ { "t": "var", "name": "i" }, { "t": "lit", "lit": { "kind": "int", "value": 1 } } ] } ] }
          ]
        }
      }
    }
  ]
}
```

Add to `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`:

```rust
#[test]
fn recur_not_in_tail_position_emits_recur_not_in_tail_position() {
    let codes = check_fixture("test_recur_not_in_tail_position.ail.json");
    assert_eq!(codes, vec!["recur-not-in-tail-position".to_string()]);
}
```

Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin recur_not_in_tail_position 2>&1 | tail -6`
Expected: FAIL — synth accepts it (arity 1 == 1, type `Int`),
returns a fresh metavar; nothing yet checks tail-position, so
`codes` is empty (or carries an unrelated code), not
`["recur-not-in-tail-position"]`.

- [ ] **Step 2: Add the `verify_loop_body` private pass**

In `crates/ailang-check/src/lib.rs`, immediately after
`pub fn verify_tail_positions` ends (`:2725`), add (structure
mirrors `verify_tail_positions`; `in_loop_tail` = "this position
is a tail position of the innermost enclosing loop body", false
outside any loop or in a non-tail sub-position; runs after synth so
every `Recur` reached here is already inside a valid loop):

```rust
/// loop-recur iter 2: enforces that every `Term::Recur` occurs in
/// tail position of its lexically-innermost enclosing `Term::Loop`
/// body. A NEW private pass — a *sibling* of
/// `verify_tail_positions` (which is spec-frozen for its tail-app
/// role and unchanged). Invoked from `check_fn` *after* `synth`, so
/// `RecurOutsideLoop`/arity/type (raised in `synth`) take code-
/// precedence; by the time a `Recur` is reached here it is known to
/// be inside a loop with matching arity/types — this pass adds only
/// the tail-position rule. `in_loop_tail` is the loop analogue of
/// `verify_tail_positions`' `is_tail`, scoped to the innermost loop.
fn verify_loop_body(t: &Term, in_loop_tail: bool) -> Result<()> {
    match t {
        Term::Lit { .. } | Term::Var { .. } => Ok(()),
        Term::Recur { args } => {
            if !in_loop_tail {
                return Err(CheckError::RecurNotInTailPosition);
            }
            // recur args are evaluated in non-tail position; a recur
            // nested inside a recur arg is itself non-tail.
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Loop { binders, body } => {
            // Binder inits run once on loop entry — not in the
            // loop's tail scope. The loop body opens a FRESH
            // innermost-loop tail scope (independent of where the
            // loop itself sits — the loop's tail scope is intrinsic).
            for b in binders {
                verify_loop_body(&b.init, false)?;
            }
            verify_loop_body(body, true)
        }
        Term::App { callee, args, .. } => {
            verify_loop_body(callee, false)?;
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Do { args, .. } => {
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Let { value, body, .. } => {
            verify_loop_body(value, false)?;
            verify_loop_body(body, in_loop_tail)
        }
        Term::If { cond, then, else_ } => {
            verify_loop_body(cond, false)?;
            verify_loop_body(then, in_loop_tail)?;
            verify_loop_body(else_, in_loop_tail)
        }
        Term::Seq { lhs, rhs } => {
            verify_loop_body(lhs, false)?;
            verify_loop_body(rhs, in_loop_tail)
        }
        Term::Match { scrutinee, arms } => {
            verify_loop_body(scrutinee, false)?;
            for arm in arms {
                verify_loop_body(&arm.body, in_loop_tail)?;
            }
            Ok(())
        }
        Term::Ctor { args, .. } => {
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Lam { body, .. } => {
            // A `recur` cannot cross a lambda boundary (different
            // control frame). Reset: a recur inside a lam is outside
            // every enclosing loop's tail scope — and synth's
            // loop_stack likewise does not cross the lam, so such a
            // recur is already a synth `RecurOutsideLoop`.
            verify_loop_body(body, false)
        }
        Term::LetRec { body, in_term, .. } => {
            verify_loop_body(body, false)?;
            verify_loop_body(in_term, in_loop_tail)
        }
        Term::Clone { value } => verify_loop_body(value, in_loop_tail),
        Term::ReuseAs { source, body } => {
            verify_loop_body(source, false)?;
            verify_loop_body(body, in_loop_tail)
        }
        Term::Mut { vars, body } => {
            for v in vars {
                verify_loop_body(&v.init, false)?;
            }
            verify_loop_body(body, in_loop_tail)
        }
        Term::Assign { value, .. } => verify_loop_body(value, false),
    }
}
```

- [ ] **Step 3: Declare `loop_stack` in `check_fn`**

In `check_fn`, immediately after the `mut_scope_stack`
declaration (`:1969`,
`let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();`),
add:

```rust
    // loop-recur iter 2: fresh per-fn-body loop-binder-type stack.
    // Empty at fn entry; pushed/popped by `Term::Loop` arms during
    // the synth walk; discarded after the body type-checks.
    let mut loop_stack: Vec<Vec<Type>> = Vec::new();
```

- [ ] **Step 4: Thread `loop_stack` into the `check_fn` synth call + invoke `verify_loop_body`**

In `check_fn`, the `synth(&f.body, …)` call (`:1970`): insert
`&mut loop_stack,` immediately after `&mut mut_scope_stack,`:

```rust
// before:
let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
// after:
let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
```

Immediately after `verify_tail_positions(&f.body, true)?;`
(`:1980`), add (sibling pass; fn body is not itself inside any
loop → `false`):

```rust
    // loop-recur iter 2: recur-in-tail-position verification. Runs
    // after synth (so RecurOutsideLoop/arity/type take code-
    // precedence) and alongside verify_tail_positions (sibling, not
    // a repurpose — verify_tail_positions' tail-app role is frozen).
    verify_loop_body(&f.body, false)?;
```

- [ ] **Step 5: Run the tail-position pin to verify it passes**

Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin recur_not_in_tail_position 2>&1 | tail -6`
Expected: PASS — `codes == ["recur-not-in-tail-position"]` (the
`recur` is an argument to `+`, a non-tail position).

Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin loop_sum_to_typechecks_clean 2>&1 | tail -3`
Expected: PASS — the positive `sum_to` loop still clean (its
`recur` IS in the `if` else-branch tail).

---

## Task 5: Three remaining negative fixtures + carve-out + ct1 F2 + pin completion

**Files:** Create 3 `.ail.json`; modify
`carve_out_inventory.rs`, `ct1_check_cli.rs`,
`loop_recur_typecheck_pin.rs`.

- [ ] **Step 1: Create `test_recur_outside_loop.ail.json`**

```json
{
  "schema": "ailang/v0",
  "name": "test_recur_outside_loop",
  "imports": [],
  "defs": [
    {
      "kind": "fn",
      "name": "main",
      "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] },
      "params": [],
      "doc": "loop-recur iter 2: recur with no enclosing loop -> recur-outside-loop.",
      "body": { "t": "recur", "args": [ { "t": "lit", "lit": { "kind": "int", "value": 1 } } ] }
    }
  ]
}
```

- [ ] **Step 2: Create `test_recur_arity_mismatch.ail.json`**

```json
{
  "schema": "ailang/v0",
  "name": "test_recur_arity_mismatch",
  "imports": [],
  "defs": [
    {
      "kind": "fn",
      "name": "bad_arity",
      "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] },
      "params": [],
      "doc": "loop-recur iter 2: 2 binders, recur passes 1 arg -> recur-arity-mismatch.",
      "body": {
        "t": "loop",
        "binders": [
          { "name": "a", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } },
          { "name": "b", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 1 } } }
        ],
        "body": { "t": "recur", "args": [ { "t": "var", "name": "a" } ] }
      }
    }
  ]
}
```

- [ ] **Step 3: Create `test_recur_type_mismatch.ail.json`**

```json
{
  "schema": "ailang/v0",
  "name": "test_recur_type_mismatch",
  "imports": [],
  "defs": [
    {
      "kind": "fn",
      "name": "bad_type",
      "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] },
      "params": [],
      "doc": "loop-recur iter 2: binder is Int, recur arg is Bool -> recur-type-mismatch.",
      "body": {
        "t": "loop",
        "binders": [
          { "name": "i", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }
        ],
        "body": { "t": "recur", "args": [ { "t": "lit", "lit": { "kind": "bool", "value": true } } ] }
      }
    }
  ]
}
```

- [ ] **Step 4: Complete the pin file**

Append to `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`:

```rust
#[test]
fn recur_outside_loop_emits_recur_outside_loop() {
    let codes = check_fixture("test_recur_outside_loop.ail.json");
    assert_eq!(codes, vec!["recur-outside-loop".to_string()]);
}

#[test]
fn recur_arity_mismatch_emits_recur_arity_mismatch() {
    let codes = check_fixture("test_recur_arity_mismatch.ail.json");
    assert_eq!(codes, vec!["recur-arity-mismatch".to_string()]);
}

#[test]
fn recur_type_mismatch_emits_recur_type_mismatch() {
    let codes = check_fixture("test_recur_type_mismatch.ail.json");
    assert_eq!(codes, vec!["recur-type-mismatch".to_string()]);
}
```

Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin 2>&1 | grep -E '^test result:'`
Expected: PASS — all 5 tests green (1 positive + 4 negatives,
each code point-exact via `assert_eq!`, non-vacuous).

- [ ] **Step 5: Extend `carve_out_inventory.rs` (13 → 17 + refresh stale header)**

In `crates/ailang-core/tests/carve_out_inventory.rs`, in
`const EXPECTED`, immediately after the
`"test_mut_var_captured_by_lambda.ail.json",` line (the
`// Iter mut.4-tidy` entry), add:

```rust
    // loop-recur iter 2 — negative typecheck fixtures
    "test_recur_arity_mismatch.ail.json",
    "test_recur_not_in_tail_position.ail.json",
    "test_recur_outside_loop.ail.json",
    "test_recur_type_mismatch.ail.json",
```

In the module doc-comment header (`:6-19`), replace the stale
line `//! Twelve carve-outs post iter mut.2 (2026-05-15):` with:

```
//! Seventeen carve-outs post iter loop-recur.2 (2026-05-17):
```

and immediately after the `//! - §C4 (b) compile-time-embed: …`
bullet block (ends `:19`), add a new bullet:

```
//! - loop-recur iter 2: 4 negative typecheck fixtures for the
//!   four `Recur*` diagnostics (recur-outside-loop /
//!   recur-arity-mismatch / recur-type-mismatch /
//!   recur-not-in-tail-position) — the diagnostic code is the
//!   load-bearing assertion, mirroring the §C4(a) / mut.2
//!   negative-fixture convention.
```

(The pre-existing "Twelve"-vs-13 mut.4-tidy drift is corrected by
this same refresh to the true post-iter-2 count of 17.)

Run: `cargo test -p ailang-core --test carve_out_inventory 2>&1 | tail -3`
Expected: PASS — `examples/*.ail.json` inventory == EXPECTED (17).

- [ ] **Step 6: Add the ct1 F2 human-mode sibling test**

In `crates/ail/tests/ct1_check_cli.rs`, immediately after
`fn check_human_mode_renders_mut_diagnostic_code_exactly_once`
(ends ~`:252`), add a sibling (verbatim same body shape, recur
cases, recur-appropriate name):

```rust
/// loop-recur iter 2: the four `Recur*` Display bodies must be
/// bracket-`[code]`-free (F2 convention) — the human-mode
/// formatter supplies `[<code>]` exactly once. Same observable
/// property as the mut sibling, over the four recur negatives.
#[test]
fn check_human_mode_renders_recur_diagnostic_code_exactly_once() {
    let cases = [
        ("test_recur_outside_loop.ail.json", "recur-outside-loop"),
        ("test_recur_arity_mismatch.ail.json", "recur-arity-mismatch"),
        ("test_recur_type_mismatch.ail.json", "recur-type-mismatch"),
        (
            "test_recur_not_in_tail_position.ail.json",
            "recur-not-in-tail-position",
        ),
    ];
    for (fixture_name, code) in cases {
        let fixture = examples_dir().join(fixture_name);
        let output = Command::new(ail_bin())
            .args(["check", fixture.to_str().unwrap()])
            .output()
            .expect("ail binary must launch");
        assert!(
            !output.status.success(),
            "ail check (human mode) must fail on {fixture_name}"
        );
        let stderr = String::from_utf8(output.stderr).expect("stderr is utf-8");
        let needle = format!("[{code}]");
        let occurrences = stderr.matches(&needle).count();
        assert_eq!(
            occurrences, 1,
            "expected `[{code}]` exactly once in human stderr, found {occurrences}; \
             full stderr:\n{stderr}"
        );
    }
}
```

Run: `cargo test -p ail --test ct1_check_cli check_human_mode_renders_recur 2>&1 | tail -4`
Expected: PASS — each recur Display body is bracket-free; the
formatter prefixes `[<code>]` exactly once. (If FAIL with
"found 2": a Display `#[error(...)]` string in Task 1 Step 3
wrongly embedded the bracket — it must not; the bodies as
specified are bracket-free, so this stays green.)

---

## Task 6: Infinite-loop acceptance + full suite + tail-app non-regression

**Files:** Create `examples/loop_forever.ail`; no source changes.

- [ ] **Step 1: Infinite-loop typechecks (no termination claim)**

Create `examples/loop_forever.ail` (a `loop` whose only path is
`recur` — no non-`recur` exit; must typecheck, asserting the spec
"no termination claim is made or enforced"):

```
(module loop_forever
  (fn spin
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params n)
    (body
      (loop (i (con Int) 0)
        (recur (app + i 1))))))
```

Add to `crates/ailang-check/tests/loop_recur_typecheck_pin.rs`:

```rust
#[test]
fn infinite_loop_typechecks_clean_no_termination_claim() {
    let codes = check_fixture("loop_forever.ail");
    assert!(codes.is_empty(), "infinite loop must typecheck (no totality claim), got {codes:?}");
}
```

Run: `cargo test -p ailang-check --test loop_recur_typecheck_pin infinite_loop 2>&1 | tail -4`
Expected: PASS — zero diagnostics. (`recur` is the loop body's
sole expression = tail position; arity 1 == 1; type `Int`;
`verify_loop_body` accepts; no guardedness/totality pass exists,
per spec deliberate boundary. The fn return type `Int` unifies
with `recur`'s fresh metavar.)

- [ ] **Step 2: Full workspace suite**

Run: `cargo test --workspace 2>&1 | grep -E '^test result: ok' | awk '{p+=$4} END {print p" passed"}'; cargo test --workspace 2>&1 | grep -E 'FAILED|error\[|^test result: FAILED' | head`
Expected: passed count ≥ the loop-recur.1 baseline (608) + the new
loop-recur.2 tests; zero `FAILED`/`error[`.

- [ ] **Step 3: `tail-app` non-regression (Boss-call-1 carryover evidence)**

Run: `cargo test --workspace tail 2>&1 | grep -E '^test result:' | tail -4`
Expected: PASS — every `tail-app`/`tail-do`/`verify_tail_positions`
test byte-identical (iter-2 added a *sibling* `verify_loop_body`
and did not touch `verify_tail_positions`; this re-confirms the
spec's frozen-tail-app-role acceptance criterion).

---

## Acceptance criteria (this iteration)

- `synth` types `Term::Loop` (binder typing; loop type = body type;
  binder names in `locals` scope for later inits + body) and
  `Term::Recur` (positional rebinding; fresh-metavar result);
  the iter-1 `CheckError::Internal` stub is gone.
- The four `Recur*` codes fire **point-exactly** on their negative
  fixtures (`assert_eq!`, non-vacuous): `recur-outside-loop`,
  `recur-arity-mismatch`, `recur-type-mismatch`,
  `recur-not-in-tail-position`. `recur` outside tail position is a
  compile error.
- A `sum_to`-class loop passes `ail check` (it did not in iter-1);
  an infinite `loop` (no non-`recur` exit) typechecks — **no
  termination claim is made or enforced**.
- `verify_tail_positions` / `tail-app` / `tail-do` / Decision 8
  byte-unchanged (verify_loop_body is a sibling, not a repurpose);
  NO `Diverge`, NO `verify_structural_recursion`, NO
  `NonStructuralRecursion`; codegen still the iter-1 `lower_term`
  `CodegenError::Internal` stub (real lowering = iter 3).
- The four Display bodies are bracket-`[code]`-free (F2);
  `carve_out_inventory` is 17 and its header prose is truthful
  (the pre-existing "Twelve"-vs-13 drift corrected in passing).
- `cargo test --workspace` green.

## Cross-references

- Parent spec `docs/specs/0034-loop-recur.md`
  (Component 4 = this iter; Component 5 codegen + the positive
  RUN-to-a-value / deep-`n` E2E = iter 3).
- iter-1 (`a179ec3`) shipped the additive nodes + the `synth` /
  `lower_term` `Internal` stubs this iter's `synth` arm replaces
  (codegen stub stays).
- mut.2 (`docs/specs/0029-mut-local.md`) is the structural
  precedent: `mut_scope_stack` threading discipline, the
  variant/`code()`/`ctx()`/bracket-free-Display pattern, the
  `.ail.json` negative-fixture + `carve_out_inventory` +
  `*_typecheck_pin.rs` + ct1-F2 convention. loop-recur.2 mirrors
  the *mechanics*; the *frame element type* differs by Boss
  call 2 (positional `Vec<Type>`, not name-keyed).
- Boss calls 1-3 (RecurTypeMismatch mechanism; loop_stack element
  type; diagnostic-code precedence by pass ordering) are recorded
  here and must be mirrored into the per-iter journal at iter
  close.