# iter loop-recur.2 — Typecheck Semantics (Component 4) **Date:** 2026-05-17 **Started from:** 5ac57fe8dec2d83ba135dd5ff6dd9caa1165c700 **Status:** DONE **Tasks completed:** 6 of 6 ## Summary The iter-1 `synth` `CheckError::Internal` stub for `Term::Loop` / `Term::Recur` is replaced with real typecheck semantics: binder typing (each init synthed in outer scope + already-declared binder names of THIS loop; loop's static type = body type), positional `recur` arity + per-arg type checking via a new `loop_stack: &mut Vec>` frame threaded exactly as mut.2's `mut_scope_stack`, the four `Recur*` `CheckError` variants (bracket-`[code]`-free Display per F2) + `code()` + two `ctx()` arms, and a NEW private `verify_loop_body` tail-position pass (a *sibling* of the spec-frozen `verify_tail_positions`, run after `synth` in `check_fn` so synth-raised codes take precedence by pass ordering). Four negative `.ail.json` fixtures fire their codes point-exactly (`assert_eq!`, non-vacuous); the iter-1 `loop_sum_to.ail` round-trip fixture now ALSO typechecks clean; an infinite `loop` typechecks (no termination claim). NO codegen this iter (the iter-1 `lower_term` `CodegenError::Internal` stub stays — iter 3); NO `Diverge`/`verify_structural_recursion`/guardedness (spec deliberate boundary). `verify_tail_positions` is byte-frozen (0 deletions). `cargo test --workspace` 616 green / 0 red (iter-1 baseline 608). ## Per-task notes - iter loop-recur.2.1: the four `Recur*` `CheckError` variants (`RecurOutsideLoop`, `RecurArityMismatch{expected,got}`, `RecurTypeMismatch{position,expected,got}`, `RecurNotInTailPosition`) + 4 `code()` arms + 2 `ctx()` arms (Arity/Type only; OutsideLoop/NotInTailPosition use the `{}` catch-all). RED-first via `recur_checkerror_codes_are_exact` (observed 4× E0599); GREEN exact. Bracket-`[code]`-free Display. - iter loop-recur.2.2: `synth` signature gains `loop_stack: &mut Vec>` after `mut_scope_stack`; threaded at every recursive call site (17 single-line canonical + 3 multi-line `Term::Mut`-init/body & `Term::Assign`-value + 2 letrec-capture `&mut body_effects`-shape) + `check_const` (fresh empty stack) + cross-module callers + test-module callers. The compile-driven sweep (`cargo build`/`cargo test --no-run`) was the exhaustive caller oracle as the plan specifies; iterated to 0 errors. Stub intact, lib suite green. - iter loop-recur.2.3: iter-1 `Internal` stub replaced with the two real `Term::Loop`/`Term::Recur` arms. Binder-name save/restore mirrors `Term::Let` (`lib.rs:3205-3218`) verbatim; per-arg type check mirrors `Term::Assign` (`lib.rs:3716-3730`) verbatim per Boss call 1; `recur`'s own type = `Subst::fresh(counter)`. RED `loop_sum_to_typechecks_clean` observed `["internal"]`; GREEN zero diagnostics. - iter loop-recur.2.4: new private `verify_loop_body(t, in_loop_tail)` immediately after `verify_tail_positions`'s closing brace — exhaustive no-`_` match over all 16 `Term` variants (verified equal to `verify_tail_positions`' variant set). Invoked from `check_fn` after `verify_tail_positions(&f.body, true)?;`. RED `recur_not_in_tail_position` observed `left: []`; GREEN `["recur-not-in-tail-position"]`, positive still clean. - iter loop-recur.2.5: 3 remaining negative fixtures (`test_recur_outside_loop` / `_arity_mismatch` / `_type_mismatch`) + 3 pins (all 5 green) + `carve_out_inventory` 13→17 with header refresh (`Twelve…mut.2` → `Seventeen…loop-recur.2`, pre-existing Twelve-vs-13 mut.4-tidy drift corrected in passing) + ct1 F2 sibling `check_human_mode_renders_recur_diagnostic_code_exactly_once`. - iter loop-recur.2.6: `examples/loop_forever.ail` (loop whose only path is `recur`, no exit) typechecks clean — asserts the spec "no termination claim is made or enforced". Form-A grammar verified verbatim against the shipped `loop_sum_to.ail`. Full suite 616/0; tail-app non-regression green (9 `tail`-named tests ok incl. the iter-1 verify_tail_positions guards). ## Boss design calls (mirrored from the plan header at iter close) 1. **`RecurTypeMismatch` is an Assign-style structural pre-check, NOT a `unify`-propagate.** `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})`. A `unify`-propagate would surface the generic `type-mismatch` code and fail the spec acceptance ("dedicated `recur-type-mismatch` fires point-exactly"). Rationale semantic (one in-repo mechanism for "declared-vs-actual at a binding site with its own point-exact code", consistent with `AssignTypeMismatch`), not effort. Implemented verbatim; the `test_recur_type_mismatch` fixture fires exactly `["recur-type-mismatch"]`. 2. **`loop_stack` element type is `Vec` (ordered binder types), NOT `IndexMap`.** `recur` rebinds binders *positionally*, so the frame models the ordered binder types for arity (`.len()`) + per-position type checks. Binder *names* enter the ordinary `locals: &mut IndexMap` exactly as `Term::Let` binds its name (save/restore in reverse on loop exit). 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. Implemented verbatim. 3. **Diagnostic-code precedence is by pass ordering, no explicit logic.** `RecurOutsideLoop`/`RecurArityMismatch`/`RecurTypeMismatch` are raised in `synth` (runs at the `check_fn` synth call); `RecurNotInTailPosition` is raised in `verify_loop_body`, invoked *after* `verify_tail_positions(&f.body, true)?;`. A `recur` outside any loop therefore fires `RecurOutsideLoop` (synth, first), not `RecurNotInTailPosition`. No precedence logic added; the pass sequence IS the mechanism. `verify_loop_body` is entered only on synth success, so every `recur` reached there is already inside a loop with matching arity/types — the pass adds only the tail rule. `verify_tail_positions` is byte-frozen (0 deletions); `verify_loop_body` is a new sibling, never a repurpose. ## Concerns - DONE_WITH_CONCERNS (iter loop-recur.2.2): **plan ordering defect — `check_fn` threading must be in Task 2, not Task 4.** The plan's Task 2 Step 3 bullet says "check_fn :1970: handled in Task 4 Step 4 (it declares its own fresh loop_stack)", but Task 2 Step 4's gate is `cargo build -p ailang-check` reaching `Finished` with 0 errors. That gate is *unsatisfiable* while `check_fn` remains an unthreaded `synth` caller (hard `error[E0061]`). Resolution: `check_fn`'s `loop_stack` declaration + synth-call threading (verbatim the plan's Task 4 Step 3 block + Step 4 first half) were pulled into Task 2 where the compile gate forces them; only the `verify_loop_body` *invocation* (Task 4 Step 4 second half) remained for Task 4. This is the unique resolution satisfying both Task 2 Step 4 AND preserving all plan code verbatim — the "fix to compile while preserving evident intent + Boss calls" repair the carrier explicitly authorises. Correctness: the declaration code is byte-identical to the plan's Task 4 Step 3 block; no semantic change, only sequencing. Recurring planner-gap class (a compile-gate task whose gate depends on a caller the plan defers past the gate) — candidate for a planner Step-5 self-review check. - DONE_WITH_CONCERNS (iter loop-recur.2.2): **recon under-counted cross-module `synth` callers** — `builtins.rs` ×2 (test helpers), `lift.rs:746` (letrec-capture re-entry), `mono.rs:720` & `mono.rs:1361` (mono re-synth) were not in the plan's site inventory (`:3161…:3717` + the 8 test sites). Exactly the mut.2-class recon-undercount the iter-1 journal flagged (Boss-call-2-class "recon under-scoped it"). Resolved by mirroring the established mut.2 fresh-stack pattern at each (declare a fresh empty `loop_stack` alongside the existing fresh `mut_scope_stack`, pass `&mut loop_stack` immediately after `&mut mut_scope_stack`). Observation, not a correctness risk — the compile-driven sweep IS the plan's designated exhaustive oracle and surfaced every site; the plan's literal site list is advisory, the compiler is authoritative (as the plan itself states). ## Known debt - No additional `ail run`/binary-stdout E2E fixture written (Phase 3). iter-2 ships typecheck semantics only; the `lower_term` `CodegenError::Internal` stub stays by design (real loop lowering + the positive sum_to-runs-to-a-value / deep-`n` E2E is explicitly iter-3 scope). An `ail run` this iter would only exercise the deliberately-transient codegen stub (a negative-value test of a known-temporary error) — same justified Phase-3 reasoning as iter-1. The iter-2 invariants worth protecting (four codes point-exact, positive + infinite typecheck clean, carve-out/tail-app non-regression) are fully pinned by the tests added in Tasks 1/3/4/5/6 + the ct1 F2 sibling. ## Files touched - Check core: `crates/ailang-check/src/lib.rs` (4 variants + code/ctx, `synth` signature + threading, real Loop/Recur arms, new `verify_loop_body`, `check_fn` + `check_const` wiring), `crates/ailang-check/src/lift.rs`, `crates/ailang-check/src/mono.rs`, `crates/ailang-check/src/builtins.rs` (cross-module synth-caller threading) - Tests/fixtures: `crates/ailang-check/tests/loop_recur_typecheck_pin.rs` (new — 7 tests), `crates/ail/tests/ct1_check_cli.rs` (F2 sibling), `crates/ailang-core/tests/carve_out_inventory.rs` (13→17 + header) - New fixtures: `examples/test_recur_outside_loop.ail.json`, `examples/test_recur_arity_mismatch.ail.json`, `examples/test_recur_type_mismatch.ail.json`, `examples/test_recur_not_in_tail_position.ail.json`, `examples/loop_forever.ail` - Reused (no new file): `examples/loop_sum_to.ail` (iter-1 round-trip fixture, now also the positive `ail check` evidence) ## Stats bench/orchestrator-stats/2026-05-17-iter-loop-recur.2.json