AILang/docs/plans/0071-iter-it.1.md

it.1 — loop/recur additive — Implementation Plan

Parent spec: docs/specs/0031-iteration-discipline.md

For agentic workers: REQUIRED SUB-SKILL: use skills/implement to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Add Term::Loop / Term::Recur / LoopBinder as first-class additive AST nodes — parse, print, prose, round-trip, serde, schema-lockstep, typecheck (binder typing + recur unification + recur-tail-position), and codegen (loop-header block with one phi per binder; recur = back-edge br) — without removing or modifying anything that exists (tail-app/tail-do and the seven existing block_terminated sites stay exactly as they are).

Architecture: Mirror the proven mut.1→mut.2→mut.3 shape. Task 1 lands the variants + every match Term walker arm (structural arms real; the typecheck/codegen dispatch arms are Internal stubs) + the serde/schema lockstep quintet, so cargo test --workspace is green with loop/recur structurally present end-to-end but semantically stubbed. Tasks 2–8 then layer surface parse, print, prose, real typecheck, real codegen, and the test corpus, each green at its own gate. recur↔loop arity/type unification lives in synth via a loop_stack: &mut Vec<Vec<Type>> threaded exactly as mut.2 threaded mut_scope_stack; RecurNotInTailPosition is the only recur check in verify_tail_positions.

Tech Stack: ailang-core (ast/desugar/workspace/serde), ailang-check (lib/lift/mono/linearity/uniqueness/reuse_shape/ pre_desugar_validation), ailang-codegen (lib/escape/lambda), ailang-surface (parse/print), ailang-prose, ail (CLI dep walker + rewrite_term), the schema/spec-drift + carve-out test crates.

---

Design decisions (Boss-resolved; not implementer judgement calls)

• DD-1 — recur context placement. Arity/type unification of a Term::Recur's args against its lexically-enclosing Term::Loop binders lives in synth, threaded via a new loop_stack: &mut Vec<Vec<Type>> parameter added to synth immediately after the existing mut_scope_stack parameter, and propagated through every synth call site exactly as mut.2 propagated mut_scope_stack (lib.rs recursive sites + mono.rs
  • lift.rs + builtins.rs test helpers + the mq.3 in-test helper at lib.rs:6663). Term::Loop pushes its binder type-vector (innermost = last); Term::Recur reads the innermost frame: empty stack ⇒ RecurOutsideLoop; length mismatch ⇒ RecurArityMismatch; per-position unify failure ⇒ RecurTypeMismatch. The tail-position rule for recur is the only recur concern handled in verify_tail_positions; its public signature pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> is unchanged (it.3 reworks it) — loop-tail context is tracked internally as the walk descends (a Term::Loop arm recurses its body in a "recur-legal, recur-must-be-tail" context; a Term::Recur reached outside that tail context ⇒ RecurNotInTailPosition).
• DD-2 — LoopBinder derives. Exactly #[derive(Debug, Clone, Serialize, Deserialize)], mirroring MutVar (ast.rs:564); the type field carries #[serde(rename = "type")]. No PartialEq/Eq (codegen phi emission maps binder name → SSA; it never compares LoopBinder values).
• DD-3 — stub-then-fill sequencing. Task 1 makes the workspace compile and cargo test --workspace pass with the typecheck and codegen dispatch arms returning CheckError::Internal / CodegenError::Internal (same boundary device mut.1 used). Real typecheck lands in Task 6; real codegen in Task 7. No task between 1 and 7 leaves the workspace non-compiling.

---

Files this plan creates or modifies

Create:

• Test: examples/loop_smoke.ail — positive round-trip + parse/print fixture (single counted loop)
• Test: examples/loop_nested_in_lambda.ail — positive: a loop inside a lambda body + a nested loop (mut.3 lambda-boundary analogue)
• Test: examples/loop_counter.ail — e2e: accumulator counter, runs and prints 55
• Test: examples/test_recur_outside_loop.ail.json — negative: recur with no enclosing loop
• Test: examples/test_recur_arity_mismatch.ail.json — negative: recur arg count ≠ binder count
• Test: examples/test_recur_type_mismatch.ail.json — negative: recur arg type ≠ binder type
• Test: examples/test_recur_not_in_tail_position.ail.json — negative: recur not in loop tail position
• Test: crates/ailang-check/tests/loop_recur_pin.rs — driver: typechecks the four negatives + the positive smoke

Modify (line ranges from recon a7224502d6da018ec):

• crates/ailang-core/src/ast.rs:513–540 (variant block), :554–581 (MutVar→LoopBinder template), :894–949 (serde round-trip mod tests)
• crates/ailang-core/tests/design_schema_drift.rs:140–175
• crates/ailang-core/tests/schema_coverage.rs (VariantTag + EXPECTED_VARIANTS + visit_term)
• crates/ailang-core/tests/spec_drift.rs (2 exemplars + 2 arms)
• docs/DESIGN.md:2394–2412 (§"Data model" jsonc, must stay inside ## Data model…## Pipeline)
• crates/ailang-core/src/desugar.rs — 9 sites: :349,:559,:1214,:1381,:1551,:1629,:1686,:1716,:2837
• crates/ailang-core/src/workspace.rs:1254,:1388
• crates/ailang-check/src/lib.rs — :249 (type-rebuilder), :2590 (verify_tail_positions), :2613/:3593/Term::Mut@3614 (synth), CheckError enum :660–680 + code() :732 + ctx()/Display :802, synth call sites for loop_stack
• crates/ailang-check/src/lift.rs:383,:760; mono.rs:1233,:1607; linearity.rs:601,:796,:929; uniqueness.rs:346; reuse_shape.rs:261; pre_desugar_validation.rs:129
• crates/ailang-codegen/src/lib.rs:1325 (lower_term), :564/:3094 (synth_with_extras); escape.rs:197,:389,:506; lambda.rs:478,:119–154/:248–260
• crates/ailang-prose/src/lib.rs:909,:1109,:1251
• crates/ail/src/main.rs:1520,:2754
• crates/ail/tests/codegen_import_map_fallback_pin.rs:62 (test-side exhaustive Term match — mut.1's plan missed this; do not miss again)
• crates/ailang-surface/src/parse.rs:42–43,:69–72,:1212–1214,:1582–1643,:2504–2551
• crates/ailang-surface/src/print.rs:551–597
• crates/ailang-core/specs/form_a.md:283–286,:304–324
• crates/ailang-core/tests/carve_out_inventory.rs:23–40 (EXPECTED 13 → 17)

---

Task 1: AST variants + every walker arm + serde/schema lockstep (stub-then-fill base)

Files: crates/ailang-core/src/ast.rs, crates/ailang-core/tests/design_schema_drift.rs, crates/ailang-core/tests/schema_coverage.rs, crates/ailang-core/tests/spec_drift.rs, docs/DESIGN.md, all walker files listed above, crates/ailang-check/src/lib.rs (stub arms only), crates/ailang-codegen/src/lib.rs (stub arms only).

• Step 1.1: Add the AST variants and LoopBinder.

In crates/ailang-core/src/ast.rs, inside pub enum Term adjacent to the Term::Mut/Term::Assign block (:513–540), add:

    /// Named loop head. The only repetition form besides structural
    /// recursion. Iter it.1. `recur` re-enters the lexically
    /// nearest enclosing `Loop`, rebinding `binders` positionally.
    Loop {
        binders: Vec<LoopBinder>,
        body: Box<Term>,
    },
    /// Backward jump to the lexically nearest enclosing `Loop`.
    /// Must be in tail position of that loop's body. Iter it.1.
    Recur {
        #[serde(default)]
        args: Vec<Term>,
    },

Immediately after the MutVar struct (:554–581), add:

/// One named, typed, initialised binder of a `Term::Loop`.
/// Mirrors `MutVar` exactly (DD-2): no `PartialEq` — codegen maps
/// the binder name to an SSA value, never compares binders.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct LoopBinder {
    pub name: String,
    #[serde(rename = "type")]
    pub ty: Type,
    pub init: Box<Term>,
}

• Step 1.2: Run the build to enumerate every non-exhaustive match Term.

Run: cargo build --workspace 2>&1 | grep -E "pattern .* not covered|crates/" | head -60 Expected: a list of E0004 non-exhaustive-match errors at exactly the walker sites enumerated in "Files this plan creates or modifies". Use this list to drive Steps 1.3–1.5 (it must match the recon site list; any extra site is a new arm to add with the same rule).

• Step 1.3: Add structural pass-through arms.

At each site below, insert the arm immediately after the adjacent Term::Assign arm, mirroring the recursion shape of the local Term::Mut arm (recurse into children, rebuild the same variant; visitors return the visitor's unit/bool fold; rebuilders return Term::Loop/Term::Recur reconstructed). The exact arm for a rebuilder (returns Term):

Term::Loop { binders, body } => Term::Loop {
    binders: binders.iter().map(|b| LoopBinder {
        name: b.name.clone(),
        ty: b.ty.clone(),
        init: Box::new(rebuild(&b.init)),
    }).collect(),
    body: Box::new(rebuild(body)),
},
Term::Recur { args } => Term::Recur {
    args: args.iter().map(|a| rebuild(a)).collect(),
},

(Replace rebuild with the local recursive call name at the site.) The exact arm for a visitor (returns () / bool / accumulates):

Term::Loop { binders, body } => {
    for b in binders { visit(&b.init); }
    visit(body);
}
Term::Recur { args } => { for a in args { visit(a); } }

Structural-pass-through sites (visitor or plain rebuild, no binding semantics): desugar.rs:349, :559, :1214, :1381, :1551, :1686, :1716, :2837; workspace.rs:1388; lift.rs:760; mono.rs:1233, :1607; uniqueness.rs:346; reuse_shape.rs:261; pre_desugar_validation.rs:129; main.rs:1520; codegen_import_map_fallback_pin.rs:62; crates/ailang-check/src/lib.rs:249 (type-rebuilder — rebuild each LoopBinder.ty via the local type-rebuild fn); lift.rs:383 (rebuilder).

• Step 1.4: Add the binding-aware / type-embedding arms (substantive).

These arms are NOT pass-through — a Term::Loop binds its binder names and embeds the binder types:

crates/ailang-core/src/desugar.rs:1629 — free_vars_in_term (load-bearing: feeds MutVarCapturedByLambda). Loop binder names are bound; recur args are uses:

Term::Loop { binders, body } => {
    let mut inner = free_vars_in_term(body);
    for b in binders {
        out.extend(free_vars_in_term(&b.init));
        inner.remove(&b.name);
    }
    out.extend(inner);
}
Term::Recur { args } => {
    for a in args { out.extend(free_vars_in_term(a)); }
}

(Adapt to the site's exact accumulator/return convention — match the local Term::Mut arm's free/bound treatment of MutVar.name.)

crates/ailang-codegen/src/lambda.rs:478 — collect_captures (loop-inside-lambda soundness). Loop binder names are NOT captures inside the loop body; recur args ARE uses. Mirror the Term::Mut-binds-var-names treatment at lambda.rs:482.

crates/ailang-prose/src/lib.rs:1109 — count_free_var: loop binders bind (subtract), recur args count as uses. Mirror the Term::Mut arm at :1113.

crates/ailang-core/src/workspace.rs:1254 — walk_term_embedded_types: each LoopBinder.ty is an embedded type, walked exactly as MutVar.ty at :1254–1260; recur has no embedded type.

crates/ail/src/main.rs:2754 — rewrite_term: rewrite each LoopBinder.ty (mirror the MutVar.ty rewrite at :2754); recur args structural.

crates/ailang-check/src/linearity.rs:601,:929 — binder inits consume, body uses; recur args consume. Mirror the local Term::Mut/MutVar.init linearity treatment. crates/ailang-codegen/src/escape.rs:197,:389,:506 — binder inits + body escape-walk; recur args escape-walk. Mirror the local Term::Mut escape arm.

• Step 1.5: Add the variant-name string emitters.

At crates/ailang-check/src/lib.rs:3593 (the Term::Mut => "mut" sub-match), crates/ailang-check/src/linearity.rs:796, and any other Term::Mut => "mut"/Term::Assign => "assign" string mapping the build flags, add Term::Loop { .. } => "loop" and Term::Recur { .. } => "recur".

• Step 1.6: Add the typecheck + codegen DISPATCH STUBS (DD-3).

crates/ailang-check/src/lib.rs synth (match t at :2613, adjacent to Term::Mut arm :3614):

Term::Loop { .. } | Term::Recur { .. } => Err(CheckError::Internal {
    msg: "Term::Loop/Recur typecheck lands in it.1 Task 6".into(),
}),

crates/ailang-codegen/src/lib.rs lower_term (match t at :1326, adjacent to Term::Mut arm :1762):

Term::Loop { .. } | Term::Recur { .. } => Err(CodegenError::Internal(
    "Term::Loop/Recur codegen lands in it.1 Task 7".into(),
)),

crates/ailang-codegen/src/lib.rs synth_with_extras (match t at :564, adjacent to Term::Mut arm :3094):

Term::Loop { binders: _, body } => self.synth_with_extras(body, extras),
Term::Recur { .. } => Ok(Type::unit()),

(Use the exact CheckError::Internal / CodegenError::Internal constructor shapes the recon-named adjacent arms use — copy the Term::Mut mut.1-era stub form verbatim, only changing the message.)

• Step 1.7: Serde round-trip unit tests.

In crates/ailang-core/src/ast.rs #[cfg(test)] mod tests (:894–949), beside the existing Term::Mut/Assign tests, add:

#[test]
fn term_loop_round_trips_through_json() {
    let t = Term::Loop {
        binders: vec![LoopBinder {
            name: "i".into(),
            ty: Type::con("Int"),
            init: Box::new(Term::Lit(Lit::Int(0))),
        }],
        body: Box::new(Term::Recur {
            args: vec![Term::Var { name: "i".into() }],
        }),
    };
    let j = serde_json::to_string(&t).unwrap();
    assert!(j.contains(r#""t":"loop""#));
    assert!(j.contains(r#""type":"#)); // LoopBinder.ty serde rename
    let back: Term = serde_json::from_str(&j).unwrap();
    assert_eq!(serde_json::to_string(&back).unwrap(), j);
}

#[test]
fn term_recur_empty_args_round_trips() {
    let t = Term::Recur { args: vec![] };
    let j = serde_json::to_string(&t).unwrap();
    let back: Term = serde_json::from_str(&j).unwrap();
    assert_eq!(serde_json::to_string(&back).unwrap(), j);
}

(Match the exact Type::con / Lit / Term::Var constructors the neighbouring term_assign_round_trips_through_json test uses; if a constructor name differs, copy the neighbour's verbatim.)

• Step 1.8: Schema-drift exemplars + variant→tag arms.

crates/ailang-core/tests/design_schema_drift.rs: in the exemplar tuple list (:140–153), after the assign exemplar, add tuples for Term::Loop (a minimal Loop{binders:vec![],body:Box::new(unit)}, tag "loop") and Term::Recur (Recur{args:vec![]}, tag "recur"), mirroring the mut/assign tuple shape. In the exhaustive variant→tag match (:160–175), after Term::Assign => "assign" (:174), add Term::Loop { .. } => "loop", Term::Recur { .. } => "recur".

• Step 1.9: DESIGN.md §"Data model" jsonc entries (in-range).

In docs/DESIGN.md, between the { "t": "assign", … } entry (:2410–2412) and the next entry — guaranteed to stay inside the ## Data model (:2249) … ## Pipeline (:2490) slice the drift test scans — add:

{ "t": "loop", "binders": [{ "name": "<id>", "type": <Type>, "init": <Term> }], "body": <Term> }
// Named loop. recur re-enters the nearest enclosing loop. Iter it.1.
{ "t": "recur", "args": [<Term>] }
// Backward jump; tail-position-only; binds the enclosing loop. Iter it.1.

Also add a one-line status note paragraph mirroring the mut.3 status note at :2419–2426: "loop/recur are additive as of it.1; structural-recursion restriction and the Diverge effect land in it.2; tail-app/tail-do are retired in it.3."

• Step 1.10: schema_coverage + spec_drift lockstep.

crates/ailang-core/tests/schema_coverage.rs: add VariantTag::TermLoop, VariantTag::TermRecur; extend EXPECTED_VARIANTS; add the two visit_term arms (structural recurse, same shape as the TermMut/TermAssign arms mut.1 added). crates/ailang-core/tests/spec_drift.rs: add the 2 exemplars + 2 match arms analogous to mut.1's mut/assign additions.

• Step 1.11: Build + full test gate.

Run: cargo build --workspace Expected: clean (0 errors).

Run: cargo test --workspace 2>&1 | tail -5 Expected: all green. Test count rises by the new serde tests (+2) and the schema/spec-drift additions. No test regresses. schema_coverage passes only after a corpus fixture observes loop/recur — if it fails "variant never observed", that is expected to remain RED until Task 3 lands examples/loop_smoke.ail; record the failing test name and proceed (Task 3 closes it). Every OTHER test must be green here.

---

Task 2: Form-A parse (parse_loop / parse_recur)

Files: crates/ailang-surface/src/parse.rs, crates/ailang-core/specs/form_a.md.

• Step 2.1: RED — parser pin tests.

In crates/ailang-surface/src/parse.rs test module (beside the (mut …) pins at :2504–2551):

#[test]
fn parses_loop_with_one_binder_and_recur_body() {
    let src = "(loop ((var i Int 0)) (recur i))";
    let t = parse_term_str(src).expect("loop parses");
    match t {
        Term::Loop { binders, body } => {
            assert_eq!(binders.len(), 1);
            assert_eq!(binders[0].name, "i");
            assert!(matches!(*body, Term::Recur { .. }));
        }
        other => panic!("expected Term::Loop, got {other:?}"),
    }
}

#[test]
fn parses_recur_zero_args() {
    let t = parse_term_str("(recur)").expect("recur parses");
    assert!(matches!(t, Term::Recur { args } if args.is_empty()));
}

(Use the exact test-harness entry the neighbouring (mut …) pin uses — copy its parse_term_str/equivalent helper name verbatim.)

• Step 2.2: Run RED.

Run: cargo test --workspace -p ailang-surface parses_loop_with_one_binder_and_recur_body parses_recur_zero_args Expected: FAIL — loop/recur fall through the head dispatch to the "unknown head" / generic-app error.

• Step 2.3: Dispatch + parse_loop + parse_recur.

In parse.rs, in the head-keyword dispatch match (:1212–1214, after the "assign" arm), add:

"loop" => self.parse_loop(items)?,
"recur" => self.parse_recur(items)?,

Add the keyword strings to the head-keyword list used for the "unknown head" error message (same list mut/assign are in, recon :1212–1214 region). Then, modelled on parse_mut (:1582–1625) and parse_assign (:1633–1643):

fn parse_loop(&mut self, items: &[Sexp]) -> Result<Term, ParseError> {
    // items[0] == "loop". items[1] == binder list ((var n T init)...).
    // items[2..] == body terms, right-folded into Term::Seq (mirror
    // parse_mut's body fold at parse.rs:1600-1620 exactly).
    let binder_list = items.get(1).ok_or_else(|| self.err("loop: missing binder list"))?;
    let binders = self.parse_loop_binders(binder_list)?;
    let body = self.parse_body_seq(&items[2..])?; // same helper parse_mut uses
    Ok(Term::Loop { binders, body: Box::new(body) })
}

fn parse_loop_binders(&mut self, list: &Sexp) -> Result<Vec<LoopBinder>, ParseError> {
    // Each entry: (var <name> <Type> <init>) — IDENTICAL shape to
    // the MutVar pull in parse_mut at parse.rs:1588-1597. Reuse that
    // parsing inline, constructing LoopBinder instead of MutVar.
    // ... (copy parse_mut's per-(var ...) decode verbatim, swap the
    //      constructed struct from MutVar to LoopBinder)
}

fn parse_recur(&mut self, items: &[Sexp]) -> Result<Term, ParseError> {
    let args = items[1..].iter().map(|s| self.parse_term(s)).collect::<Result<_,_>>()?;
    Ok(Term::Recur { args })
}

(The parse_body_seq / per-(var …) decode helpers MUST be the exact ones parse_mut calls — recon parse.rs:1582–1625; do not introduce a new body-folding helper.)

• Step 2.4: EBNF doc + form_a.md.

In parse.rs module-doc EBNF: :42–43 add | loop-term | recur-term to the term production; :69–72 add productions:

   loop-term   ::= "(" "loop" "(" loop-binder* ")" term+ ")"
   loop-binder ::= "(" "var" IDENT type term ")"
   recur-term  ::= "(" "recur" term* ")"

In crates/ailang-core/specs/form_a.md: :283–286 add loop / recur to the §Terms production list; :304–324 add a prose block mirroring the mut/var/assign block: loop introduces named binders; recur re-enters the lexically nearest enclosing loop, must be in tail position, arity/type must match the binders; diagnostics recur-outside-loop, recur-arity-mismatch, recur-type-mismatch, recur-not-in-tail-position.

• Step 2.5: Run GREEN.

Run: cargo test --workspace -p ailang-surface parses_loop_with_one_binder_and_recur_body parses_recur_zero_args Expected: PASS.

---

Task 3: Form-A print + positive round-trip fixture

Files: crates/ailang-surface/src/print.rs, examples/loop_smoke.ail, examples/loop_nested_in_lambda.ail.

• Step 3.1: Print arms.

In print.rs, after the Term::Assign arm (:586–596, before the match close :597), add — mirroring the Term::Mut Seq-spine walk at :551–585:

Term::Loop { binders, body } => {
    write!(w, "(loop (")?;
    for (k, b) in binders.iter().enumerate() {
        if k > 0 { write!(w, " ")?; }
        write!(w, "(var {} ", b.name)?;
        write_type(w, &b.ty)?;
        write!(w, " ")?;
        write_term(w, &b.init)?;
        write!(w, ")")?;
    }
    write!(w, ") ")?;
    // body is a Term::Seq right-spine when multi-term; walk it the
    // SAME way the Term::Mut arm walks its body spine (print.rs:551-585)
    write_seq_spine(w, body)?;
    write!(w, ")")
}
Term::Recur { args } => {
    write!(w, "(recur")?;
    for a in args { write!(w, " ")?; write_term(w, a)?; }
    write!(w, ")")
}

(write_type / write_term / the seq-spine helper MUST be the exact identifiers the Term::Mut arm uses at :551–585.)

• Step 3.2: Positive fixtures.

examples/loop_smoke.ail:

(module loop_smoke
  (fn count_to : Int -> Int (n)
    (loop ((var i Int 0))
      (if (app eq i n) i (recur (app add i 1))))))

examples/loop_nested_in_lambda.ail — a loop inside a lambda body plus a nested loop (mut.3 lambda-boundary analogue):

(module loop_nested_in_lambda
  (fn make_adder : Int -> (Int -> Int) (base)
    (lam (x : Int)
      (loop ((var acc Int base) (var k Int 0))
        (if (app eq k x) acc (recur (app add acc 1) (app add k 1)))))))

(Use the exact head-keyword/prelude call spellings the existing examples/mut_counter.ail fixture uses for if/eq/add/lam — read that file and match its surface forms verbatim so the fixture parses against the real prelude. If a prelude function name differs, copy mut_counter.ail's spelling.)

• Step 3.3: Round-trip + schema-coverage GREEN.

Run: cargo test --workspace -p ailang-surface parse_then_print_then_parse_is_idempotent_on_every_ail_fixture parse_is_deterministic_over_every_ail_fixture Expected: PASS (the new examples/loop_*.ail are auto-discovered; parse→print→parse is byte-idempotent).

Run: cargo test --workspace -p ailang-core schema_coverage Expected: PASS — loop/recur are now observed in the corpus, closing the Task 1.11 deferred RED.

---

Task 4: Prose projection lockstep

Files: crates/ailang-prose/src/lib.rs.

• Step 4.1: RED — prose round-trip pin.

Add beside the existing prose snapshot tests a test that renders examples/loop_smoke.ail's parsed AST to prose and back, asserting AST equality (mirror the nearest existing prose round-trip test's harness verbatim).

Run: cargo test --workspace -p ailang-prose <new test name> Expected: FAIL (the :909 render walker hits the stub/todo arm or mis-renders).

• Step 4.2: Render + free-var + subst arms.

crates/ailang-prose/src/lib.rs:909 — real render arms for Term::Loop (binder list + body) / Term::Recur (args), mirroring the Term::Mut/Assign render at :909–933. :1109 — count_free_var: loop binders bind (done in Task 1.4 if this file built; confirm the arm is the binding-aware one, not pass-through). :1251 — subst_var_with_term rebuilder: reconstruct Term::Loop rebuilding each LoopBinder (mirror the MutVar reconstruction at :1253–1276), Term::Recur rebuilding args.

• Step 4.3: GREEN.

Run: cargo test --workspace -p ailang-prose Expected: PASS (all prose tests, including the new round-trip pin).

---

Task 5: Real typecheck — binder typing, recur unification, loop_stack (DD-1)

Files: crates/ailang-check/src/lib.rs, all synth call sites that thread mut_scope_stack.

• Step 5.1: RED — positive typecheck + four negatives.

Create the four negative .ail.json fixtures and the positive check via crates/ailang-check/tests/loop_recur_pin.rs:

// recur_outside_loop.ail.json: (recur 1) at fn-body top level
// recur_arity_mismatch.ail.json: (loop ((var i Int 0)) (recur 1 2))
// recur_type_mismatch.ail.json: (loop ((var i Int 0)) (recur true))
// recur_not_in_tail_position.ail.json:
//   (loop ((var i Int 0)) (do (recur i) 0))   // recur not in tail pos
#[test]
fn loop_smoke_typechecks_clean() {
    assert!(check_ok("examples/loop_smoke.ail"));
}
#[test]
fn recur_outside_loop_is_rejected() {
    assert_eq!(check_err_code("examples/test_recur_outside_loop.ail.json"),
               "recur-outside-loop");
}
// ...arity-mismatch -> "recur-arity-mismatch",
//    type-mismatch  -> "recur-type-mismatch",
//    not-in-tail-pos -> "recur-not-in-tail-position"

(Use the exact fixture-loading + code-extraction helpers crates/ailang-check/tests/mut_typecheck_pin.rs uses — copy that driver's helpers verbatim.)

Run: cargo test --workspace -p ailang-check --test loop_recur_pin Expected: FAIL — loop_smoke errors with the Task 1.6 stub Internal("…typecheck lands in it.1 Task 6"); the four negatives also hit the stub (wrong code).

• Step 5.2: Add the four CheckError variants.

In crates/ailang-check/src/lib.rs CheckError enum, beside MutVarCapturedByLambda (:680), add (Display body without an embedded [code] prefix — the CLI formatter prepends it; 2026-05-15 F2 convention):

#[error("recur outside of any enclosing loop")]
RecurOutsideLoop { span: Option<Span> },
#[error("recur passes {got} argument(s) but the enclosing loop binds {want}")]
RecurArityMismatch { got: usize, want: usize, span: Option<Span> },
#[error("recur argument {pos} has type {got} but loop binder `{name}` is {want}")]
RecurTypeMismatch { pos: usize, name: String, got: String, want: String, span: Option<Span> },
#[error("recur must be in tail position of its enclosing loop")]
RecurNotInTailPosition { span: Option<Span> },

Add the matching code() arms beside :732 ("recur-outside-loop", "recur-arity-mismatch", "recur-type-mismatch", "recur-not-in-tail-position") and ctx() arms beside :802 (mirror the MutAssignOutOfScope ctx shape). Add the four code strings to the diagnostic-doc list in crates/ailang-check/src/diagnostic.rs (same list the mut codes were added to).

• Step 5.3: Thread loop_stack through synth (DD-1).

Change synth's signature to add, immediately after the mut_scope_stack: &mut Vec<IndexMap<String, Type>> parameter:

loop_stack: &mut Vec<Vec<Type>>,

Propagate it through every recursive synth call and every external call site exactly where mut_scope_stack is already passed: all lib.rs recursive sites, mono.rs:712/:1337, lift.rs:723, the builtins.rs test helpers, and the mq.3 in-test helper at lib.rs:6663. (Grep mut_scope_stack to get the exact site set; loop_stack goes through the identical set — this is the mut.2 dev-dep-cycle-aware pattern; integration tests call across the edge, in-source #[cfg(test)] cannot.)

• Step 5.4: Real Term::Loop / Term::Recur typing arms.

Replace the Task 1.6 stub arm in synth (:3614 region) with:

Term::Loop { binders, body } => {
    let mut binder_tys = Vec::with_capacity(binders.len());
    let mut frame = IndexMap::new();
    for b in binders {
        let init_ty = self.synth(&b.init, env, locals, mut_scope_stack, loop_stack, /*…existing args…*/)?;
        self.unify(&init_ty, &b.ty).map_err(|_| CheckError::AssignTypeMismatch { /* reuse shape: init vs declared */ })?;
        frame.insert(b.name.clone(), b.ty.clone());
        binder_tys.push(b.ty.clone());
    }
    loop_stack.push(binder_tys);
    locals.push(frame); // same frame mechanism Term::Mut uses
    let body_ty = self.synth(body, env, locals, mut_scope_stack, loop_stack, /*…*/)?;
    locals.pop();
    loop_stack.pop();
    Ok(body_ty)
}
Term::Recur { args } => {
    let want = loop_stack.last().cloned()
        .ok_or(CheckError::RecurOutsideLoop { span: None })?;
    if args.len() != want.len() {
        return Err(CheckError::RecurArityMismatch {
            got: args.len(), want: want.len(), span: None });
    }
    for (i, (a, wt)) in args.iter().zip(want.iter()).enumerate() {
        let at = self.synth(a, env, locals, mut_scope_stack, loop_stack, /*…*/)?;
        if self.unify(&at, wt).is_err() {
            return Err(CheckError::RecurTypeMismatch {
                pos: i, name: format!("#{i}"),
                got: type_display(&at), want: type_display(wt), span: None });
        }
    }
    Ok(Type::never()) // recur does not fall through; bottom unifies anywhere
}

(Match the EXACT self.synth(...) argument list of the neighbouring Term::Mut arm — copy its call shape, only adding loop_stack. Use the project's existing bottom/never type constructor; if none exists, return the innermost loop's body type sentinel the way the Term::Mut arm returns its body type — pick Type::unit() only if the codebase has no bottom; record which in the journal. Use the real unify / type_display identifiers from the neighbouring arms.)

• Step 5.5: verify_tail_positions recur-tail arms (DD-1).

In crates/ailang-check/src/lib.rs:2590 verify_tail_positions (signature unchanged), add arms — modelled on the existing Term::Mut arm at :2672–2677:

Term::Loop { binders, body } => {
    for b in binders { verify_tail_positions(&b.init, false)?; }
    // recur is legal and must be tail INSIDE this body:
    verify_loop_body(body)?; // new private helper, below
}
Term::Recur { .. } => {
    // Reached here only OUTSIDE a loop body's tail context
    // (verify_loop_body intercepts the in-tail ones). Either no
    // enclosing loop (synth already flags RecurOutsideLoop) or
    // non-tail position:
    return Err(CheckError::RecurNotInTailPosition { span: None });
}

Add the private helper next to verify_tail_positions:

fn verify_loop_body(t: &Term) -> Result<(), CheckError> {
    match t {
        Term::Recur { .. } => Ok(()), // tail position: OK
        Term::If { cond, then, els } => {
            verify_tail_positions(cond, false)?;
            verify_loop_body(then)?; verify_loop_body(els)
        }
        Term::Seq(items) => {
            // only the last item is in tail position
            for it in &items[..items.len().saturating_sub(1)] {
                verify_tail_positions(it, false)?;
            }
            if let Some(last) = items.last() { verify_loop_body(last)?; }
            Ok(())
        }
        Term::Match { scrutinee, arms } => {
            verify_tail_positions(scrutinee, false)?;
            for a in arms { verify_loop_body(&a.body)?; }
            Ok(())
        }
        Term::Let { value, body, .. } => {
            verify_tail_positions(value, false)?;
            verify_loop_body(body)
        }
        Term::Loop { .. } => verify_tail_positions(t, true), // inner loop: its own recur scope
        other => verify_tail_positions(other, true),
    }
}

(Mirror the EXACT child-arm names the existing verify_tail_positions Term::If/Term::Seq/Term::Match/Term::Let arms use at :2590–2682 — copy their destructuring shapes verbatim; the only new behaviour is "a Recur in tail context is OK, anywhere else is RecurNotInTailPosition".)

• Step 5.6: GREEN.

Run: cargo test --workspace -p ailang-check --test loop_recur_pin Expected: PASS — loop_smoke typechecks; the four negatives each return their exact code.

Run: cargo test --workspace 2>&1 | tail -3 Expected: all green (the loop_stack threading touched many call sites; no regression).

---

Task 6: Carve-out inventory + check the corpus still classifies

Files: crates/ailang-core/tests/carve_out_inventory.rs.

• Step 6.1: Extend EXPECTED.

In carve_out_inventory.rs:23–40 const EXPECTED, add the four new negative fixtures (test_recur_outside_loop.ail.json, test_recur_arity_mismatch.ail.json, test_recur_type_mismatch.ail.json, test_recur_not_in_tail_position.ail.json), count 13 → 17, preserving alphabetical order if the const is sorted.

• Step 6.2: GREEN.

Run: cargo test --workspace -p ailang-core carve_out_inventory Expected: PASS (inventory matches the .ail.json-only set).

---

Task 7: Real codegen — loop-header + phi, recur back-edge, lambda boundary

Files: crates/ailang-codegen/src/lib.rs, crates/ailang-codegen/src/lambda.rs, examples/loop_counter.ail.

• Step 7.1: RED — e2e fixture.

examples/loop_counter.ail (sum 1..10 via an accumulator loop; equivalent tail-rec helper prints 55):

(module loop_counter
  (fn main : () -> () !IO ()
    (app print
      (loop ((var acc Int 0) (var i Int 1))
        (if (app gt i 10)
            acc
            (recur (app add acc i) (app add i 1)))))))

(Match examples/mut_counter.ail's exact print/gt/add spellings + module/fn header form verbatim — read it first.)

Add an e2e assertion (mirror the mut_counter e2e in crates/ail/tests/e2e.rs):

#[test]
fn loop_counter_runs_and_prints_55() {
    assert_eq!(run_example("examples/loop_counter.ail").trim(), "55");
}

Run: cargo test --workspace -p ail --test e2e loop_counter_runs_and_prints_55 Expected: FAIL — codegen hits the Task 1.6 stub CodegenError::Internal("…codegen lands in it.1 Task 7").

• Step 7.2: Term::Loop lowering — header block + phi.

Replace the Task 1.6 lower_term stub (:1326 match, Term::Mut neighbour :1762) with:

Term::Loop { binders, body } => {
    // 1. lower each binder init in the CURRENT block
    let mut init_ssa = Vec::with_capacity(binders.len());
    for b in binders {
        let (v, ty) = self.lower_term(&b.init, /*…existing args…*/)?;
        init_ssa.push((b.name.clone(), b.ty.clone(), v, ty));
    }
    let pred = self.current_block_label();
    let header = self.fresh_label("loop.header");
    self.emit(&format!("  br label %{header}\n"));
    self.start_block(&header);
    // 2. one phi per binder; record the SSA name so Term::Var
    //    inside the body resolves to the phi, and Term::Recur
    //    knows the back-edge incoming list. Reuse the
    //    mut_var_allocas-style name->ssa map (a parallel
    //    loop_binder_phis: Vec<(String, phi_ssa, llvm_ty)> on a
    //    per-loop save stack mirroring mut.3's save/restore).
    let mut phis = Vec::new();
    for (name, decl_ty, iv, _) in &init_ssa {
        let p = self.fresh_ssa();
        let lty = self.llvm_ty(decl_ty);
        // back-edge incomings are patched after the body is lowered
        self.emit(&format!("  {p} = phi {lty} [ {iv}, %{pred} ] ; +recur edges\n"));
        phis.push((name.clone(), p, lty, decl_ty.clone()));
    }
    self.push_loop_frame(header.clone(), phis.clone()); // name->phi + header label
    let (body_v, body_ty) = self.lower_term(body, /*…*/)?;
    let recur_edges = self.pop_loop_frame(); // Vec<(pred_label, Vec<arg_ssa>)>
    // 3. patch each phi's incoming list with the collected recur edges
    self.patch_loop_phis(&header, &phis, &recur_edges);
    // 4. the loop's value is the body value on the non-recur exit
    Ok((body_v, body_ty))
}
Term::Recur { args } => {
    let frame = self.current_loop_frame()
        .expect("Term::Recur without loop frame — typecheck guarantees this");
    let mut arg_ssa = Vec::with_capacity(args.len());
    for a in args {
        let (v, _) = self.lower_term(a, /*…*/)?;
        arg_ssa.push(v);
    }
    let from = self.current_block_label();
    self.record_recur_edge(from.clone(), arg_ssa);   // for phi patching
    self.emit(&format!("  br label %{}\n", frame.header));
    self.block_terminated = true;                    // NEW seam (additive)
    Ok((self.unit_ssa(), Type::unit()))
}

Add the minimal helper surface used above next to the mut_var_allocas/pending_entry_allocas fields (:725–737), mirroring their lifecycle: loop_frames: Vec<LoopFrame> where LoopFrame { header: String, phis: Vec<(String,String,String,Type)>, recur_edges: Vec<(String, Vec<String>)> }; push_loop_frame / pop_loop_frame / current_loop_frame / record_recur_edge / patch_loop_phis / current_block_label / start_block / fresh_label. Where an equivalent already exists (e.g. a fresh-label or current-block helper), REUSE it — grep before adding. Term::Var resolution must consult the innermost loop_frames phi map before the mut_var_allocas load path (a binder name shadows like a mut var), exactly as mut.3 prepended the mut-var lookup in the Term::Var arm.

Do not modify any of the seven existing block_terminated = true sites (:1377,:1601,:2271,:2352,:2493, :2565,:2657) or the tail-driven emit_call/emit_indirect_call/ lower_effect_op paths — recur's block_terminated = true is a new parallel setter (spec it.1 additive constraint).

• Step 7.3: Lambda boundary (loop-inside-lambda).

In crates/ailang-codegen/src/lambda.rs, the save/restore block (:119–154 save, :248–260 restore) that already saves block_terminated/mut_var_allocas/pending_entry_allocas/ entry_block_end_marker across the closure boundary: add loop_frames to the saved+reset+restored set so a loop inside a lambda body scopes its header/phis to the closure's own entry, not the outer fn's (exact mut.3 analogue — mirror the lines that handle mut_var_allocas at :144/:252).

• Step 7.4: GREEN.

Run: cargo test --workspace -p ail --test e2e loop_counter_runs_and_prints_55 Expected: PASS (prints 55).

Run: ail run examples/loop_nested_in_lambda.ail (build first if needed) — Expected: builds and runs without codegen error (loop-inside-lambda lowers to the closure's own header).

• Step 7.5: Full workspace gate.

Run: cargo test --workspace 2>&1 | tail -3 Expected: all green. tail-app fixtures still build+run unchanged (no existing codegen path was modified).

---

Task 8: tail-app coexistence proof + IR snapshots

Files: IR snapshot fixtures if any new unconditional declare line was added (none expected — loop adds no extern); the existing tail-app corpus.

• Step 8.1: Prove tail-app is untouched.

Run: ail run examples/bench_compute_intsum.ail and ail run examples/list_map_poly.ail Expected: byte-identical stdout to pre-it.1 (these are tail-app fixtures; it.1 must not perturb them).

• Step 8.2: IR snapshot check.

Run: cargo test --workspace 2>&1 | grep -iE "snapshot|\.ll" | tail Expected: no IR-snapshot test regressed. If one did, it means an unconditional IR-header line changed — investigate; loop codegen should add none (no new extern). Do NOT blanket-regen snapshots; the expectation is zero snapshot drift in it.1.

• Step 8.3: Acceptance gate (spec it.1 acceptance criteria).

Run: cargo test --workspace 2>&1 | tail -3 Expected: all green.

Verify each spec it.1 acceptance bullet:

• examples/loop_counter.ail builds + prints 55 ✓ (Task 7.4)
• loop/recur round-trips, JSON-AST hashable ✓ (Tasks 1.7, 3.3)
• all five Recur* diagnostics fire on negatives — note: only four Recur* variants exist in it.1 (RecurOutsideLoop/RecurArityMismatch/RecurTypeMismatch/ RecurNotInTailPosition); the spec's "five" counts NonStructuralRecursion, which is it.2, not it.1. The it.1 gate is the four Recur* (Task 5.6) ✓
• tail-app still works unchanged ✓ (Task 8.1)
• cargo test --workspace green ✓

---

Self-review (planner Step 5)

1. Spec coverage. Spec §Components it.1 bullets → tasks: AST+serde → T1.1/1.7; schema-drift+DESIGN+coverage → T1.8–1.10; Form-A parse → T2; print → T3.1; round-trip fixture → T3.2/3.3; prose → T4; check (binder typing + recur unify + tail-pos) + 4 diagnostics → T5; codegen loop-header/phi + recur + escape + lambda → T7; e2e loop_counter → T7.1/7.4; ~25 walker arms → T1.3– 1.5; carve-out → T6. All it.1 spec sections covered. it.2/it.3 explicitly excluded (Task 8.3 calls out the spec's "five diagnostics" wording counting an it.2 variant — resolved as "four in it.1", not a placeholder).
2. Placeholder scan. No "TBD/TODO/implement later/similar to Task N/add appropriate error handling". The structural-arm template + enumerated site list is literal code + literal locations, not a placeholder. The "copy the neighbouring Term::Mut arm verbatim, swapping the constructed struct" instructions are exact transformations of named, line-located existing code — executable without judgement.
3. Type/name consistency. Term::Loop/Term::Recur/ LoopBinder, loop_stack: &mut Vec<Vec<Type>>, the four codes recur-outside-loop/recur-arity-mismatch/recur-type-mismatch/ recur-not-in-tail-position, examples/loop_smoke.ail/ loop_counter.ail/loop_nested_in_lambda.ail, loop_recur_pin.rs — used consistently across all tasks.
4. Step granularity. Each step is one action (add arms at enumerated sites / run one command / write one code block) in the 2–5-minute band. The largest, T1.3–1.5, is bounded by the recon site list and a fixed per-site template.
5. No commit steps. None present. Work stays in the working tree; the Boss commits the whole it.1 diff at iter end.

Open risk recorded for the implementer (not a placeholder — a named fallback with a decision rule): if the codebase has no bottom/never Type constructor for Term::Recur's synth result (Step 5.4), use Type::unit() and record the substitution in the per-iter journal; recur is always in tail position so its "value" is never consumed, making the choice observationally inert.