iter loop-recur.2: typecheck semantics — binder typing, recur checks, verify_loop_body

Second of three iterations of the standalone loop/recur milestone
(plan 5ac57fe). Replaces the iter-1 synth CheckError::Internal stub
for Term::Loop/Term::Recur with real binder typing + positional
recur arity/type checking via a new loop_stack: &mut Vec<Vec<Type>>
frame threaded as mut.2's mut_scope_stack, a new private
verify_loop_body tail-position pass (sibling of the byte-frozen
verify_tail_positions — 0 deletions there), and the four Recur*
diagnostics firing point-exactly on four negative fixtures. The
iter-1 loop_sum_to.ail fixture now also typechecks clean; an
infinite loop typechecks (no termination claim). NO codegen (the
iter-1 lower_term stub stays — iter 3); NO Diverge/guardedness
(spec boundary).

Three Boss design calls implemented verbatim and journalled:
RecurTypeMismatch is an Assign-style structural pre-check (not a
unify-propagate); loop_stack is positional Vec<Type> (binder names
via ordinary locals); diagnostic-code precedence is by pass
ordering (no explicit logic).

Two DONE_WITH_CONCERNS, both journalled: a plan-ordering defect
(Task 2's compile gate forced the check_fn threading the plan
deferred to Task 4 — resolved byte-identically, only resequenced)
and the recurring mut.2-class recon-undercount of cross-module
synth callers (resolved via the plan's compile-sweep oracle).

Boss systemic fix folded in: planner SKILL.md Step-5 gains item 7
(compile-gate vs. deferred-caller ordering) so the plan-ordering
defect class is scrubbed at plan time. cargo test --workspace
608 -> 616 / 0 red (Boss-reran independently).

crates/ail/tests/ct1_check_cli.rs

@@ -251,6 +251,42 @@ fn check_human_mode_renders_mut_diagnostic_code_exactly_once() {
     }
 }
 
+/// 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}"
+        );
+    }
+}
+
 /// Property: `ail check --json` on a `.ail` (Form A) source file with
 /// a syntax error returns a structured `surface-parse-error`
 /// diagnostic (non-empty diagnostics array, exit code != 0), rather

crates/ailang-check/src/builtins.rs

@@ -349,11 +349,15 @@ mod tests {
         let mut residuals = Vec::new();
         let mut free_fn_calls = Vec::new();
         let mut warnings: Vec<crate::diagnostic::Diagnostic> = Vec::new();
+        // loop-recur iter 2: test helper synths one term from top-of-
+        // body — fresh empty loop-stack (mirrors mut_scope_stack).
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let ty = crate::synth(
             t,
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -592,11 +596,15 @@ mod tests {
         let mut residuals = Vec::new();
         let mut free_fn_calls = Vec::new();
         let mut warnings: Vec<crate::diagnostic::Diagnostic> = Vec::new();
+        // loop-recur iter 2: test helper synths one term from top-of-
+        // body — fresh empty loop-stack (mirrors mut_scope_stack).
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let err = crate::synth(
             &term,
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,

crates/ailang-check/src/lib.rs

@@ -696,6 +696,32 @@ pub enum CheckError {
     #[error("mut-var `{name}` cannot be captured by a lambda — mut-vars are alloca-resident and do not escape their enclosing mut block. Either move the lambda outside the mut block, or restructure to pass `{name}` as a lambda parameter (deferring escape to a future milestone with ref-types and the !Mut effect).")]
     MutVarCapturedByLambda { name: String },
 
+    /// 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,
+
     /// Iter 22b.3: an internal invariant in the typechecker / mono pass
     /// was violated — surfaced as an error so callers can propagate
     /// rather than abort, but in well-formed inputs (typecheck has
@@ -748,6 +774,10 @@ impl CheckError {
             CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch",
             CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type",
             CheckError::MutVarCapturedByLambda { .. } => "mut-var-captured-by-lambda",
+            CheckError::RecurOutsideLoop => "recur-outside-loop",
+            CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
+            CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
+            CheckError::RecurNotInTailPosition => "recur-not-in-tail-position",
             CheckError::Internal(_) => "internal",
         }
     }
@@ -822,6 +852,12 @@ impl CheckError {
             CheckError::MutVarCapturedByLambda { name } => {
                 serde_json::json!({"name": name})
             }
+            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})
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -1967,7 +2003,11 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     // pushed/popped by `Term::Mut` arms during the walk; discarded after
     // the body type-checks.
     let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
-    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)?;
+    // 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();
+    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)?;
     unify(&ret_ty, &body_ty, &mut subst)?;
     // mq.3: surface synth-time warnings into the caller-supplied
     // accumulator. The warnings already carry `def: Some(f.name)`
@@ -1979,6 +2019,12 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     // call doesn't drown out the underlying type error.
     verify_tail_positions(&f.body, true)?;
 
+    // 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)?;
+
     let declared: BTreeSet<String> = declared_effs.into_iter().collect();
     for e in &effects {
         if !declared.contains(e) {
@@ -2724,6 +2770,106 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
     }
 }
 
+/// 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),
+    }
+}
+
 fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> {
     // Const types are never polymorphic — a Forall here is rejected
     // outright. Any other type passes through to `synth` as before.
@@ -2745,7 +2891,10 @@ fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> R
     // at this entry point — `Term::Mut` may appear inside a const body
     // and push frames as the walk descends).
     let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
-    let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
+    // loop-recur iter 2: a const value has no enclosing loop; any
+    // `recur` in a const body correctly fires `RecurOutsideLoop`.
+    let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+    let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
     out_warnings.extend(warnings);
     unify(&c.ty, &v, &mut subst)?;
     if !effects.is_empty() {
@@ -2770,6 +2919,15 @@ pub(crate) fn synth(
     // name through it. Position: locals-adjacent because both are
     // per-fn-body lexical scope state.
     mut_scope_stack: &mut Vec<IndexMap<String, Type>>,
+    // 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>>,
     effects: &mut BTreeSet<String>,
     in_def: &str,
     subst: &mut Subst,
@@ -3158,7 +3316,7 @@ pub(crate) fn synth(
             Ok(maybe_instantiate(raw, counter))
         }
         Term::App { callee, args, .. } => {
-            let cty = synth(callee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let cty = synth(callee, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             let cty = subst.apply(&cty);
             let (params, ret, fx) = match &cty {
                 Type::Fn { params, ret, effects: fx, .. } => {
@@ -3194,7 +3352,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(params.iter()) {
-                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(exp, &actual, subst)?;
             }
             for e in fx {
@@ -3203,9 +3361,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&ret))
         }
         Term::Let { name, value, body } => {
-            let v = synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let v = synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             let prev = locals.insert(name.clone(), v);
-            let r = synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let r = synth(body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             match prev {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -3217,10 +3375,10 @@ pub(crate) fn synth(
             Ok(r)
         }
         Term::If { cond, then, else_ } => {
-            let c = synth(cond, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let c = synth(cond, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&Type::bool_(), &c, subst)?;
-            let t1 = synth(then, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
-            let t2 = synth(else_, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let t1 = synth(then, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let t2 = synth(else_, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&t1, &t2, subst)?;
             Ok(subst.apply(&t1))
         }
@@ -3238,7 +3396,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(sig.params.iter()) {
-                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(exp, &actual, subst)?;
             }
             effects.insert(sig.effect.clone());
@@ -3333,7 +3491,7 @@ pub(crate) fn synth(
             }
             for (a, exp) in args.iter().zip(qualified_fields.iter()) {
                 let exp_inst = substitute_rigids(exp, &mapping);
-                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(&exp_inst, &actual, subst)?;
             }
             Ok(Type::Con {
@@ -3342,7 +3500,7 @@ pub(crate) fn synth(
             })
         }
         Term::Match { scrutinee, arms } => {
-            let s_ty = synth(scrutinee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let s_ty = synth(scrutinee, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             if arms.is_empty() {
                 return Err(CheckError::NonExhaustive {
                     ty: ailang_core::pretty::type_to_string(&s_ty),
@@ -3360,7 +3518,7 @@ pub(crate) fn synth(
                     let prev = locals.insert(n.clone(), t.clone());
                     pushed.push((n.clone(), prev));
                 }
-                let body_ty = synth(&arm.body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let body_ty = synth(&arm.body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 for (n, prev) in pushed.into_iter().rev() {
                     match prev {
                         Some(p) => {
@@ -3435,9 +3593,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
         }
         Term::Seq { lhs, rhs } => {
-            let lty = synth(lhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let lty = synth(lhs, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&Type::unit(), &lty, subst)?;
-            synth(rhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(rhs, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
         Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
             // Iter mut.4-tidy: reject lambda-captures-of-mut-var.
@@ -3471,7 +3629,7 @@ pub(crate) fn synth(
                 pushed.push((n.clone(), prev));
             }
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let body_ty = synth(body, env, locals, mut_scope_stack, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
             for (n, prev) in pushed.into_iter().rev() {
                 match prev {
                     Some(p) => {
@@ -3559,7 +3717,7 @@ pub(crate) fn synth(
             // subset rule against `declared_effs` — exactly like
             // `Term::Lam`.
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let body_ty = synth(body, env, locals, mut_scope_stack, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
 
             // Restore body-scope locals (params + name).
             for (n, prev) in pushed.into_iter().rev() {
@@ -3586,7 +3744,7 @@ pub(crate) fn synth(
             // scope (params are not visible here; only the recursive
             // binding is).
             let prev_in = locals.insert(name.clone(), ty.clone());
-            let in_ty = synth(in_term, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let in_ty = synth(in_term, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
             match prev_in {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -3602,7 +3760,7 @@ pub(crate) fn synth(
             // No constraint generated, no environment change. The
             // wrapper records author intent for the future RC inc/dec
             // emission pass (18c.3); typing is pure passthrough.
-            synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
         Term::ReuseAs { source, body } => {
             // Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to
@@ -3616,7 +3774,7 @@ pub(crate) fn synth(
             // shape-compatibility check (18d.2 will add a
             // `reuse-as-shape-mismatch` diagnostic when codegen has
             // the actual size info).
-            let _ = synth(source, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let _ = synth(source, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             match body.as_ref() {
                 Term::Ctor { .. } | Term::Lam { .. } => {}
                 other => {
@@ -3646,7 +3804,7 @@ pub(crate) fn synth(
             }
             // Body's type is the result type of the whole reuse-as
             // expression.
-            synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
         // Iter mut.2: a mut block opens a fresh lexical scope for its
         // mut-vars. Each var's `init` is synthed in the outer scope
@@ -3672,7 +3830,7 @@ pub(crate) fn synth(
                 // the `mut_scope_stack` truthful at all times.
                 mut_scope_stack.push(frame.clone());
                 let init_ty = synth(
-                    &v.init, env, locals, mut_scope_stack, effects, in_def,
+                    &v.init, env, locals, mut_scope_stack, loop_stack, effects, in_def,
                     subst, counter, residuals, free_fn_calls, warnings,
                 )?;
                 mut_scope_stack.pop();
@@ -3681,7 +3839,7 @@ pub(crate) fn synth(
             }
             mut_scope_stack.push(frame);
             let body_result = synth(
-                body, env, locals, mut_scope_stack, effects, in_def,
+                body, env, locals, mut_scope_stack, loop_stack, effects, in_def,
                 subst, counter, residuals, free_fn_calls, warnings,
             );
             mut_scope_stack.pop();
@@ -3715,7 +3873,7 @@ pub(crate) fn synth(
                 }
                 Some(declared_ty) => {
                     let value_ty = synth(
-                        value, env, locals, mut_scope_stack, effects, in_def,
+                        value, env, locals, mut_scope_stack, loop_stack, effects, in_def,
                         subst, counter, residuals, free_fn_calls, warnings,
                     )?;
                     let applied_declared = subst.apply(&declared_ty);
@@ -3731,15 +3889,83 @@ pub(crate) fn synth(
                 }
             }
         }
-        // loop-recur iter 1: typecheck semantics (binder typing,
-        // recur arity/type unification, verify_loop_body
-        // tail-position, the four Recur* CheckError variants) land
-        // in loop-recur iter 2. This iter stubs the dispatch so the
-        // workspace compiles and round-trips; no loop/recur fixture
-        // is typechecked in iter 1. Mirrors mut.1's synth stub.
-        Term::Loop { .. } | Term::Recur { .. } => Err(CheckError::Internal(
-            "Term::Loop/Term::Recur typecheck lands in loop-recur iter 2".into(),
-        )),
+        // 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))
+        }
     }
 }
 
@@ -4114,6 +4340,9 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4125,6 +4354,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4151,6 +4381,9 @@ mod tests {
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         locals.insert("x".into(), Type::int()); // outer let-style binding
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut frame: IndexMap<String, Type> = IndexMap::new();
         frame.insert("x".into(), Type::float()); // inner mut-var
         mut_scope_stack.push(frame);
@@ -4167,6 +4400,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4191,6 +4425,9 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut outer: IndexMap<String, Type> = IndexMap::new();
         outer.insert("x".into(), Type::int());
         mut_scope_stack.push(outer);
@@ -4210,6 +4447,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4304,6 +4542,9 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4311,7 +4552,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -4344,6 +4585,9 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4351,7 +4595,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -4383,6 +4627,9 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4390,7 +4637,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -4437,6 +4684,32 @@ mod tests {
         let _ = e.ctx();
     }
 
+    /// loop-recur iter 2: the four `Recur*` `CheckError` variants carry
+    /// the exact stable kebab codes the spec acceptance mandates
+    /// (`recur-outside-loop` / `recur-arity-mismatch` /
+    /// `recur-type-mismatch` / `recur-not-in-tail-position`).
+    #[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"
+        );
+    }
+
     /// Iter mut.4-tidy (Task 2): regression guard — a lambda built
     /// without any enclosing mut-scope stack typechecks unchanged.
     /// Property protected: the new free-var scan in `Term::Lam`'s synth
@@ -4485,6 +4758,9 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4492,7 +4768,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -7224,6 +7500,9 @@ mod tests {
         let term = Term::Var { name: "show".into() };
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        // loop-recur iter 2: loop-free unit-test call site — fresh
+        // empty loop-stack, mirroring the mut-scope above.
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -7235,6 +7514,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "test_call_site",
             &mut subst,

crates/ailang-check/src/lift.rs

@@ -743,7 +743,11 @@ impl<'a> Lifter<'a> {
         // term at a time, beginning from a top-of-body position; fresh
         // empty mut-scope stack is correct.
         let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
-        let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
+        // loop-recur iter 2: lift's letrec-capture synth re-entry walks
+        // one term at a time from a top-of-body position; fresh empty
+        // loop-stack is correct (any `Term::Loop` pushes its own frame).
+        let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
+        let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
         Ok(subst.apply(&ty))
     }
 }

crates/ailang-check/src/mono.rs

@@ -717,11 +717,16 @@ pub fn collect_mono_targets(
     // mut-scope, since any `Term::Mut` will push its own frame as the
     // walk descends.
     let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
+    // loop-recur iter 2: mono re-synth begins from top-of-body —
+    // empty loop-stack (any `Term::Loop` pushes its own frame as the
+    // walk descends), mirroring the fresh mut-scope above.
+    let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
     crate::synth(
         &f.body,
         &env,
         &mut locals,
         &mut mut_scope_stack,
+        &mut loop_stack,
         &mut effects,
         &f.name,
         &mut subst,
@@ -1358,11 +1363,16 @@ pub(crate) fn collect_residuals_ordered(
     // mut-scope, since any `Term::Mut` will push its own frame as the
     // walk descends.
     let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
+    // loop-recur iter 2: mono re-synth begins from top-of-body —
+    // empty loop-stack (any `Term::Loop` pushes its own frame as the
+    // walk descends), mirroring the fresh mut-scope above.
+    let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
     crate::synth(
         &f.body,
         &env,
         &mut locals,
         &mut mut_scope_stack,
+        &mut loop_stack,
         &mut effects,
         &f.name,
         &mut subst,

crates/ailang-check/tests/loop_recur_typecheck_pin.rs

@@ -0,0 +1,68 @@
+//! 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, not the
+//! surface form.
+
+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("CARGO_MANIFEST_DIR has a parent (crates/ailang-check)")
+        .parent().expect("CARGO_MANIFEST_DIR has a grandparent (crates/)")
+        .join("examples")
+}
+
+/// Load the named fixture under `examples/`, run check_workspace, and
+/// return the diagnostic code list (one entry per Diagnostic).
+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:?}");
+}
+
+#[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()]);
+}
+
+#[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()]);
+}
+
+#[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:?}");
+}

crates/ailang-core/tests/carve_out_inventory.rs

@@ -3,7 +3,7 @@
 //! under `examples/*.ail.json` after milestone close. The list is
 //! hardcoded; any change is a deliberate, brainstorm-level decision.
 //!
-//! Twelve carve-outs post iter mut.2 (2026-05-15):
+//! Seventeen carve-outs post iter loop-recur.2 (2026-05-17):
 //! - §C4 (a) subject-matter: 7 fixtures from form-a.1 milestone
 //!   close (canonical-form rejection / unbound / class-def rejection).
 //! - Iter mut.2: 5 negative typecheck fixtures for the new mut /
@@ -17,6 +17,12 @@
 //!   prelude-decouple; the prelude is now embedded as `prelude.ail`
 //!   in `ailang-surface` and parsed at compile time via
 //!   `ailang_surface::parse_prelude`.
+//! - 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.
 
 use std::collections::BTreeSet;
 
@@ -37,6 +43,11 @@ const EXPECTED: &[&str] = &[
     "test_mut_var_unsupported_type.ail.json",
     // Iter mut.4-tidy — lambda-capture-of-mut-var rejection
     "test_mut_var_captured_by_lambda.ail.json",
+    // 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",
 ];
 
 fn examples_dir() -> std::path::PathBuf {