# 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>` 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` (ordered binder types), NOT `IndexMap`.** mut.2's `mut_scope_stack: Vec>` 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` 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>,` 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` 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>, ``` - [ ] **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::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::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 { 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 = Vec::new(); let mut restore: Vec<(String, Option)> = 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> = 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::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 `[]` 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 `[]` 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`, 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.