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

    #[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):

    /// 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:

            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):

            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:

    // 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):

// 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:

//! 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):

        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):

        // 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):

{
  "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:

#[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):

/// 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:

    // 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,:

// 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):

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

{
  "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

{
  "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

{
  "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:

#[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:

    // 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):

/// 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:

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