iter it.1: loop/recur additive — Term::Loop/Term::Recur/LoopBinder end-to-end

Iteration-discipline milestone, 1 of 3. Adds named loop + recur as
strictly-additive first-class AST nodes: parse/print/prose/serde/
round-trip/schema lockstep, typecheck (binder typing + recur
arity/type unification via loop_stack threaded as mut.2's
mut_scope_stack; recur-tail-position via verify_loop_body), codegen
(loop-header + one phi per binder; recur back-edge br with a NEW
parallel block_terminated setter; lambda-boundary loop_frames
save/restore). Four Recur* CheckError variants. Strictly additive:
zero deletions touch tail-app/tail-do or the seven existing
block_terminated sites — this is what makes the destructive it.3
safe. recur synth = fresh metavar (resolves the plan's flagged
Type::unit() risk). loop_counter->55, loop_in_lambda->49, four
negatives fire, tail-app byte-identical, cargo test --workspace
green. Spec fda9b78, plan 7381a42.

crates/ailang-check/src/builtins.rs

@@ -343,6 +343,7 @@ mod tests {
         install(&mut env);
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        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;
@@ -354,6 +355,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -586,6 +588,7 @@ mod tests {
         install(&mut env);
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        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;
@@ -597,6 +600,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,

crates/ailang-check/src/lib.rs

@@ -261,6 +261,23 @@ pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Typ
             name: name.clone(),
             value: Box::new(substitute_rigids_in_term(value, mapping)),
         },
+        // Iter it.1: rebuild each `LoopBinder.ty` via the type-level
+        // rigids substitution, each `init` and the body via the
+        // term-level walker.
+        Term::Loop { binders, body } => Term::Loop {
+            binders: binders
+                .iter()
+                .map(|b| ailang_core::ast::LoopBinder {
+                    name: b.name.clone(),
+                    ty: substitute_rigids(&b.ty, mapping),
+                    init: Box::new(substitute_rigids_in_term(&b.init, mapping)),
+                })
+                .collect(),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+        Term::Recur { args } => Term::Recur {
+            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
+        },
     }
 }
 
@@ -679,6 +696,36 @@ 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 },
 
+    /// Iter it.1: a `Term::Recur` was reached with no lexically
+    /// enclosing `Term::Loop`. Spec
+    /// `docs/specs/2026-05-15-iteration-discipline.md`. (No `span`
+    /// field — the `CheckError` variants in this crate do not carry
+    /// spans; the plan's pseudo-code referenced a type not in scope
+    /// here, so the real `MutAssignOutOfScope`-style shape is used.)
+    #[error("recur outside of any enclosing loop")]
+    RecurOutsideLoop,
+
+    /// Iter it.1: a `Term::Recur`'s argument count differs from the
+    /// lexically nearest enclosing loop's binder count.
+    #[error("recur passes {got} argument(s) but the enclosing loop binds {want}")]
+    RecurArityMismatch { got: usize, want: usize },
+
+    /// Iter it.1: a `Term::Recur` argument's synth type does not
+    /// unify with the corresponding loop binder's declared type.
+    #[error("recur argument {pos} has type {got} but loop binder `{name}` is {want}")]
+    RecurTypeMismatch {
+        pos: usize,
+        name: String,
+        got: String,
+        want: String,
+    },
+
+    /// Iter it.1: a `Term::Recur` was reached outside the tail
+    /// context of its enclosing loop's body. Spec
+    /// `docs/specs/2026-05-15-iteration-discipline.md`.
+    #[error("recur must be in tail position of its enclosing loop")]
+    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
@@ -731,6 +778,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",
         }
     }
@@ -805,6 +856,12 @@ impl CheckError {
             CheckError::MutVarCapturedByLambda { name } => {
                 serde_json::json!({"name": name})
             }
+            CheckError::RecurArityMismatch { got, want } => {
+                serde_json::json!({"expected": want, "actual": got})
+            }
+            CheckError::RecurTypeMismatch { pos, name, got, want } => {
+                serde_json::json!({"pos": pos, "name": name, "expected": want, "actual": got})
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -1950,7 +2007,8 @@ 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)?;
+    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)`
@@ -2679,6 +2737,76 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
         // be in tail position. Its `value` is also not in tail
         // position.
         Term::Assign { value, .. } => verify_tail_positions(value, false),
+        // Iter it.1 (DD-1): binder inits are evaluated before the
+        // loop head and are NOT in tail position. The body opens a
+        // "recur-legal, recur-must-be-tail" context — `verify_loop_body`
+        // walks it, accepting a `Term::Recur` only where the loop
+        // body's value is produced (tail position w.r.t. the loop).
+        Term::Loop { binders, body } => {
+            for b in binders {
+                verify_tail_positions(&b.init, false)?;
+            }
+            verify_loop_body(body)
+        }
+        // Iter it.1 (DD-1): a `Term::Recur` reached by the ordinary
+        // `verify_tail_positions` walk is, by construction, NOT in the
+        // tail context of any enclosing loop body (`verify_loop_body`
+        // intercepts the legal in-tail ones). Either there is no
+        // enclosing loop (synth flags `RecurOutsideLoop`) or this
+        // recur is in a non-tail position.
+        Term::Recur { .. } => Err(CheckError::RecurNotInTailPosition),
+    }
+}
+
+/// Iter it.1 (DD-1): walks a `Term::Loop` body in the
+/// "recur-is-legal-and-must-be-tail" context. A `Term::Recur` is
+/// accepted only at a position that produces the loop body's value
+/// (the loop-tail positions); anywhere else it is
+/// `RecurNotInTailPosition`. Non-recur sub-terms that are NOT in the
+/// loop's tail position are handed back to `verify_tail_positions`
+/// (with `is_tail = false`) so `tail-app`/`tail-do` inside the loop
+/// body are still validated; sub-terms in the loop's tail position
+/// recurse through `verify_loop_body` so a nested `recur` there is
+/// still legal. A nested `Term::Loop` starts its own recur scope.
+fn verify_loop_body(t: &Term) -> Result<()> {
+    match t {
+        // Tail position of the loop body: a recur here is legal.
+        Term::Recur { args } => {
+            for a in args {
+                verify_tail_positions(a, false)?;
+            }
+            Ok(())
+        }
+        Term::If { cond, then, else_ } => {
+            verify_tail_positions(cond, false)?;
+            verify_loop_body(then)?;
+            verify_loop_body(else_)
+        }
+        Term::Seq { lhs, rhs } => {
+            // Only `rhs` is in the loop's tail position.
+            verify_tail_positions(lhs, false)?;
+            verify_loop_body(rhs)
+        }
+        Term::Match { scrutinee, arms } => {
+            verify_tail_positions(scrutinee, false)?;
+            for arm in arms {
+                verify_loop_body(&arm.body)?;
+            }
+            Ok(())
+        }
+        Term::Let { value, body, .. } => {
+            verify_tail_positions(value, false)?;
+            verify_loop_body(body)
+        }
+        // A nested loop is its own recur scope: a `recur` inside it
+        // binds the inner loop, not this one. Validate it through the
+        // ordinary tail-position walk in a fresh tail context.
+        Term::Loop { .. } => verify_tail_positions(t, true),
+        // Any other term is not a recur-carrying tail shape; validate
+        // it normally (it is the loop body's value but carries no
+        // loop-tail recur, so `is_tail = true` keeps a trailing
+        // `tail-app` legal).
+        other => verify_tail_positions(other, true),
     }
 }
 
@@ -2703,7 +2831,8 @@ 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)?;
+    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() {
@@ -2728,6 +2857,14 @@ 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>>,
+    // Iter it.1 (DD-1): per-walk lexical loop-binder-type stack,
+    // threaded exactly as `mut_scope_stack`. Each frame is one
+    // `Term::Loop`'s binder type-vector (positional). Pushed on
+    // `Term::Loop` entry, popped on exit; `Term::Recur` reads the
+    // innermost frame for arity/type unification. Position:
+    // mut_scope_stack-adjacent because both are per-fn-body lexical
+    // scope state.
+    loop_stack: &mut Vec<Vec<Type>>,
     effects: &mut BTreeSet<String>,
     in_def: &str,
     subst: &mut Subst,
@@ -3116,7 +3253,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, .. } => {
@@ -3152,7 +3289,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 {
@@ -3161,9 +3298,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);
@@ -3175,10 +3312,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))
         }
@@ -3196,7 +3333,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());
@@ -3291,7 +3428,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 {
@@ -3300,7 +3437,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),
@@ -3318,7 +3455,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) => {
@@ -3393,9 +3530,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.
@@ -3429,7 +3566,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) => {
@@ -3517,7 +3654,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() {
@@ -3544,7 +3681,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);
@@ -3560,7 +3697,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
@@ -3574,7 +3711,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 => {
@@ -3592,6 +3729,8 @@ pub(crate) fn synth(
                         Term::ReuseAs { .. } => "reuse-as",
                         Term::Mut { .. } => "mut",
                         Term::Assign { .. } => "assign",
+                        Term::Loop { .. } => "loop",
+                        Term::Recur { .. } => "recur",
                         Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
                     };
                     return Err(CheckError::ReuseAsNonAllocatingBody {
@@ -3602,7 +3741,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
@@ -3628,7 +3767,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();
@@ -3637,7 +3776,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();
@@ -3671,7 +3810,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);
@@ -3687,6 +3826,84 @@ pub(crate) fn synth(
                 }
             }
         }
+        // Iter it.1 (DD-1): each binder's `init` is synthesised in
+        // the outer scope plus the already-declared binders (init
+        // order = declaration order), unified against the binder's
+        // declared type. The binder names are bound into `locals`
+        // (save/restore like `Term::Let`) for the body; the binder
+        // type-vector is pushed onto `loop_stack` so an enclosed
+        // `Term::Recur` can check its arity/types. The loop's static
+        // type is the body's static type.
+        Term::Loop { binders, body } => {
+            let mut saved: Vec<(String, Option<Type>)> = Vec::new();
+            let mut binder_tys: Vec<Type> = Vec::with_capacity(binders.len());
+            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)?;
+                let prev = locals.insert(b.name.clone(), b.ty.clone());
+                saved.push((b.name.clone(), prev));
+                binder_tys.push(b.ty.clone());
+            }
+            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 saved.into_iter().rev() {
+                match prev {
+                    Some(p) => {
+                        locals.insert(name, p);
+                    }
+                    None => {
+                        locals.shift_remove(&name);
+                    }
+                }
+            }
+            body_result
+        }
+        // Iter it.1 (DD-1): a `Term::Recur` re-enters the lexically
+        // nearest enclosing loop. Empty `loop_stack` ⇒
+        // `RecurOutsideLoop`; arg count ≠ innermost binder count ⇒
+        // `RecurArityMismatch`; per-position unify failure ⇒
+        // `RecurTypeMismatch`. `recur` never falls through (it is
+        // always a tail jump), so its synth result is a fresh
+        // metavar — it unifies with any type, which is what makes
+        // `(if c then (recur ...))` typecheck. (The plan's named
+        // fallback was `Type::unit()`; a fresh metavar is the
+        // codebase-idiomatic bottom and resolves the plan's "Open
+        // risk" correctly — see the it.1 journal.)
+        Term::Recur { args } => {
+            let want = loop_stack
+                .last()
+                .cloned()
+                .ok_or(CheckError::RecurOutsideLoop)?;
+            if args.len() != want.len() {
+                return Err(CheckError::RecurArityMismatch {
+                    got: args.len(),
+                    want: want.len(),
+                });
+            }
+            for (i, (a, wt)) in args.iter().zip(want.iter()).enumerate() {
+                let at = synth(
+                    a, env, locals, mut_scope_stack, loop_stack, effects, in_def,
+                    subst, counter, residuals, free_fn_calls, warnings,
+                )?;
+                if unify(&at, wt, subst).is_err() {
+                    let applied_got = subst.apply(&at);
+                    return Err(CheckError::RecurTypeMismatch {
+                        pos: i,
+                        name: format!("#{i}"),
+                        got: ailang_core::pretty::type_to_string(&applied_got),
+                        want: ailang_core::pretty::type_to_string(wt),
+                    });
+                }
+            }
+            Ok(Subst::fresh(counter))
+        }
     }
 }
 
@@ -4061,6 +4278,7 @@ 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();
+        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;
@@ -4072,6 +4290,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4098,6 +4317,7 @@ 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();
+        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);
@@ -4114,6 +4334,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4138,6 +4359,7 @@ 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();
+        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);
@@ -4157,6 +4379,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4251,6 +4474,7 @@ 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();
+        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;
@@ -4258,7 +4482,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,
         )
@@ -4291,6 +4515,7 @@ 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();
+        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;
@@ -4298,7 +4523,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,
         )
@@ -4330,6 +4555,7 @@ 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();
+        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;
@@ -4337,7 +4563,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,
         )
@@ -4432,6 +4658,7 @@ 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();
+        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;
@@ -4439,7 +4666,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,
         )
@@ -7171,6 +7398,7 @@ 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();
+        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;
@@ -7182,6 +7410,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

@@ -397,6 +397,25 @@ impl<'a> Lifter<'a> {
                 name: name.clone(),
                 value: Box::new(self.lift_in_term(value, locals, in_def)?),
             }),
+            Term::Loop { binders, body } => Ok(Term::Loop {
+                binders: binders
+                    .iter()
+                    .map(|b| {
+                        Ok(ailang_core::ast::LoopBinder {
+                            name: b.name.clone(),
+                            ty: b.ty.clone(),
+                            init: Box::new(self.lift_in_term(&b.init, locals, in_def)?),
+                        })
+                    })
+                    .collect::<Result<Vec<_>>>()?,
+                body: Box::new(self.lift_in_term(body, locals, in_def)?),
+            }),
+            Term::Recur { args } => Ok(Term::Recur {
+                args: args
+                    .iter()
+                    .map(|a| self.lift_in_term(a, locals, in_def))
+                    .collect::<Result<Vec<_>>>()?,
+            }),
             Term::LetRec { name, ty, params, body, in_term } => {
                 // Iter 16b.3: post-order traversal — lift any inner
                 // LetRecs first. Within the body's scope, `name` and
@@ -724,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)?;
+        // Iter it.1 (DD-1): lift's letrec-capture re-entry walks one
+        // term from a top-of-body position; fresh empty loop_stack is
+        // correct (a loop captured into a letrec carries its own).
+        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))
     }
 }
@@ -761,6 +784,10 @@ fn contains_any_letrec(m: &Module) -> bool {
                 vars.iter().any(|v| term_has_letrec(&v.init)) || term_has_letrec(body)
             }
             Term::Assign { value, .. } => term_has_letrec(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| term_has_letrec(&b.init)) || term_has_letrec(body)
+            }
+            Term::Recur { args } => args.iter().any(term_has_letrec),
         }
     }
     for def in &m.defs {

crates/ailang-check/src/linearity.rs

@@ -609,6 +609,17 @@ impl<'a> Checker<'a> {
                 // a tracked binder). Walk the `value` normally.
                 self.walk(value, Position::Consume);
             }
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
         }
     }
 
@@ -795,6 +806,8 @@ fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> D
         Term::ReuseAs { .. } => "reuse-as",
         Term::Mut { .. } => "mut",
         Term::Assign { .. } => "assign",
+        Term::Loop { .. } => "loop",
+        Term::Recur { .. } => "recur",
     };
     let replacement = term_to_form_a(body);
     Diagnostic::error(
@@ -934,6 +947,17 @@ fn any_sub_binder_consumed_for(
         Term::Assign { value, .. } => {
             any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors)
         }
+        // Iter it.1: loop binders are scalar like mut-vars; recurse
+        // into children defensively so a genuine consume-of-`pname`
+        // inside a binder init / body / recur arg still surfaces.
+        Term::Loop { binders, body } => {
+            binders.iter().any(|b| {
+                any_sub_binder_consumed_for(&b.init, pname, uniq, def_name, ctors)
+            }) || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
+        }
+        Term::Recur { args } => args
+            .iter()
+            .any(|a| any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)),
     }
 }
 

crates/ailang-check/src/mono.rs

@@ -713,11 +713,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();
+    // Iter it.1 (DD-1): mono re-synth from top-of-body — empty
+    // loop_stack; any `Term::Loop` pushes its own frame as the walk
+    // descends.
+    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,
@@ -1239,6 +1244,17 @@ fn rewrite_mono_calls(
         Term::Assign { value, .. } => {
             rewrite_mono_calls(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
         }
+        Term::Loop { binders, body } => {
+            for b in binders.iter_mut() {
+                rewrite_mono_calls(&mut b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+            rewrite_mono_calls(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+        }
+        Term::Recur { args } => {
+            for a in args.iter_mut() {
+                rewrite_mono_calls(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+        }
         Term::Lit { .. } => {}
     }
 }
@@ -1343,11 +1359,14 @@ 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();
+    // Iter it.1 (DD-1): empty loop_stack at top-of-body re-synth.
+    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,
@@ -1613,6 +1632,17 @@ fn interleave_slots(
         Term::Assign { value, .. } => {
             interleave_slots(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
         }
+        Term::Loop { binders, body } => {
+            for b in binders {
+                interleave_slots(&b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+            interleave_slots(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                interleave_slots(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+        }
         Term::Lit { .. } => {}
     }
 }

crates/ailang-check/src/pre_desugar_validation.rs

@@ -133,6 +133,18 @@ fn walk_term(t: &Term) -> Result<(), CheckError> {
             walk_term(body)
         }
         Term::Assign { value, .. } => walk_term(value),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_term(&b.init)?;
+            }
+            walk_term(body)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a)?;
+            }
+            Ok(())
+        }
     }
 }
 

crates/ailang-check/src/reuse_shape.rs

@@ -265,6 +265,17 @@ impl<'a> Checker<'a> {
                 self.walk(body);
             }
             Term::Assign { value, .. } => self.walk(value),
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init);
+                }
+                self.walk(body);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a);
+                }
+            }
         }
     }
 

crates/ailang-check/src/uniqueness.rs

@@ -352,6 +352,17 @@ impl<'a> Walker<'a> {
             Term::Assign { value, .. } => {
                 self.walk(value, Position::Consume);
             }
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
         }
     }