AILang/docs/journals/2026-05-17-iter-loop-recur.2.md

# 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<Vec<Type>>` 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<Vec<Type>>` 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<Type>` (ordered binder
   types), NOT `IndexMap<String,Type>`.** `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<String,Type>` 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