From 1566ce0b294867b240015388b2d5cc01ff7f3410 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 17 May 2026 23:33:43 +0200 Subject: [PATCH] =?UTF-8?q?iter=20loop-recur.2:=20typecheck=20semantics=20?= =?UTF-8?q?=E2=80=94=20binder=20typing,=20recur=20checks,=20verify=5Floop?= =?UTF-8?q?=5Fbody?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> 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 (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). --- .../2026-05-17-iter-loop-recur.2.json | 13 + crates/ail/tests/ct1_check_cli.rs | 36 ++ crates/ailang-check/src/builtins.rs | 8 + crates/ailang-check/src/lib.rs | 354 ++++++++++++++++-- crates/ailang-check/src/lift.rs | 6 +- crates/ailang-check/src/mono.rs | 10 + .../tests/loop_recur_typecheck_pin.rs | 68 ++++ .../ailang-core/tests/carve_out_inventory.rs | 13 +- docs/journals/2026-05-17-iter-loop-recur.2.md | 185 +++++++++ docs/journals/INDEX.md | 1 + examples/loop_forever.ail | 7 + examples/test_recur_arity_mismatch.ail.json | 22 ++ .../test_recur_not_in_tail_position.ail.json | 33 ++ examples/test_recur_outside_loop.ail.json | 15 + examples/test_recur_type_mismatch.ail.json | 21 ++ skills/planner/SKILL.md | 18 + 16 files changed, 771 insertions(+), 39 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-17-iter-loop-recur.2.json create mode 100644 crates/ailang-check/tests/loop_recur_typecheck_pin.rs create mode 100644 docs/journals/2026-05-17-iter-loop-recur.2.md create mode 100644 examples/loop_forever.ail create mode 100644 examples/test_recur_arity_mismatch.ail.json create mode 100644 examples/test_recur_not_in_tail_position.ail.json create mode 100644 examples/test_recur_outside_loop.ail.json create mode 100644 examples/test_recur_type_mismatch.ail.json diff --git a/bench/orchestrator-stats/2026-05-17-iter-loop-recur.2.json b/bench/orchestrator-stats/2026-05-17-iter-loop-recur.2.json new file mode 100644 index 0000000..db4f81c --- /dev/null +++ b/bench/orchestrator-stats/2026-05-17-iter-loop-recur.2.json @@ -0,0 +1,13 @@ +{ + "iter_id": "loop-recur.2", + "date": "2026-05-17", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 6, + "tasks_completed": 6, + "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 0, "6": 0 }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null, + "notes": "Two DONE_WITH_CONCERNS on Task 2: (1) plan-ordering defect — check_fn loop_stack declaration+threading had to move from Task 4 into Task 2 because Task 2 Step 4's cargo-build 0-errors gate is unsatisfiable while check_fn is an unthreaded synth caller; resolved by executing the plan's Task-4 Step-3 block verbatim at the gate-forced point, only the verify_loop_body invocation stayed in Task 4. (2) recon under-counted cross-module synth callers (builtins.rs x2, lift.rs, mono.rs x2) — mut.2-class recon-undercount, resolved by mirroring the mut.2 fresh-stack pattern; the compile-driven sweep was the plan's designated exhaustive oracle. Zero review re-loops; all three Boss design calls implemented verbatim. cargo test --workspace 608 -> 616." +} diff --git a/crates/ail/tests/ct1_check_cli.rs b/crates/ail/tests/ct1_check_cli.rs index d0eaf3c..62d89bb 100644 --- a/crates/ail/tests/ct1_check_cli.rs +++ b/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 `[]` 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 diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs index fbd7b1b..6b5df35 100644 --- a/crates/ailang-check/src/builtins.rs +++ b/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 = 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::new(); let ty = crate::synth( t, &env, &mut locals, &mut mut_scope_stack, + &mut loop_stack, &mut effects, "", &mut subst, @@ -592,11 +596,15 @@ mod tests { let mut residuals = Vec::new(); let mut free_fn_calls = Vec::new(); let mut warnings: Vec = 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::new(); let err = crate::synth( &term, &env, &mut locals, &mut mut_scope_stack, + &mut loop_stack, &mut effects, "", &mut subst, diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 885da3f..b177b8c 100644 --- a/crates/ailang-check/src/lib.rs +++ b/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) -> Result< // pushed/popped by `Term::Mut` arms during the walk; discarded after // the body type-checks. let mut mut_scope_stack: Vec> = 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::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) -> 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 = 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) -> 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) -> 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> = 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::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>, + // 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` 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>, effects: &mut BTreeSet, 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(), <y, 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 = 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 = 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 = Vec::new(); + let mut restore: Vec<(String, Option)> = 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 = IndexMap::new(); let mut mut_scope_stack: Vec> = 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::new(); let mut effects: BTreeSet = 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, "", &mut subst, @@ -4151,6 +4381,9 @@ mod tests { let mut locals: IndexMap = IndexMap::new(); locals.insert("x".into(), Type::int()); // outer let-style binding let mut mut_scope_stack: Vec> = 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::new(); let mut frame: IndexMap = 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, "", &mut subst, @@ -4191,6 +4425,9 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = 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::new(); let mut outer: IndexMap = 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, "", &mut subst, @@ -4304,6 +4542,9 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = 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::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -4311,7 +4552,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = 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, "", &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 = IndexMap::new(); let mut mut_scope_stack: Vec> = 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::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -4351,7 +4595,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = 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, "", &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 = IndexMap::new(); let mut mut_scope_stack: Vec> = 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::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -4390,7 +4637,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = 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, "", &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 = IndexMap::new(); let mut mut_scope_stack: Vec> = 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::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -4492,7 +4768,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = 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, "", &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 = IndexMap::new(); let mut mut_scope_stack: Vec> = 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::new(); let mut effects: BTreeSet = 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, diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs index 783ca6d..d2dbba3 100644 --- a/crates/ailang-check/src/lift.rs +++ b/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> = 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::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)) } } diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs index e283dd0..7092055 100644 --- a/crates/ailang-check/src/mono.rs +++ b/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> = 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::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> = 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::new(); crate::synth( &f.body, &env, &mut locals, &mut mut_scope_stack, + &mut loop_stack, &mut effects, &f.name, &mut subst, diff --git a/crates/ailang-check/tests/loop_recur_typecheck_pin.rs b/crates/ailang-check/tests/loop_recur_typecheck_pin.rs new file mode 100644 index 0000000..060806e --- /dev/null +++ b/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 { + 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:?}"); +} diff --git a/crates/ailang-core/tests/carve_out_inventory.rs b/crates/ailang-core/tests/carve_out_inventory.rs index e36c78f..29de783 100644 --- a/crates/ailang-core/tests/carve_out_inventory.rs +++ b/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 { diff --git a/docs/journals/2026-05-17-iter-loop-recur.2.md b/docs/journals/2026-05-17-iter-loop-recur.2.md new file mode 100644 index 0000000..0dd1f77 --- /dev/null +++ b/docs/journals/2026-05-17-iter-loop-recur.2.md @@ -0,0 +1,185 @@ +# iter loop-recur.2 — Typecheck Semantics (Component 4) + +**Date:** 2026-05-17 +**Started from:** 5ac57fe8dec2d83ba135dd5ff6dd9caa1165c700 +**Status:** DONE +**Tasks completed:** 6 of 6 + +## Summary + +The iter-1 `synth` `CheckError::Internal` stub for `Term::Loop` / +`Term::Recur` is replaced with real typecheck semantics: binder +typing (each init synthed in outer scope + already-declared binder +names of THIS loop; loop's static type = body type), positional +`recur` arity + per-arg type checking via a new `loop_stack: &mut +Vec>` frame threaded exactly as mut.2's `mut_scope_stack`, +the four `Recur*` `CheckError` variants (bracket-`[code]`-free +Display per F2) + `code()` + two `ctx()` arms, and a NEW private +`verify_loop_body` tail-position pass (a *sibling* of the +spec-frozen `verify_tail_positions`, run after `synth` in `check_fn` +so synth-raised codes take precedence by pass ordering). Four +negative `.ail.json` fixtures fire their codes point-exactly +(`assert_eq!`, non-vacuous); the iter-1 `loop_sum_to.ail` +round-trip fixture now ALSO typechecks clean; an infinite `loop` +typechecks (no termination claim). NO codegen this iter (the iter-1 +`lower_term` `CodegenError::Internal` stub stays — iter 3); NO +`Diverge`/`verify_structural_recursion`/guardedness (spec deliberate +boundary). `verify_tail_positions` is byte-frozen (0 deletions). +`cargo test --workspace` 616 green / 0 red (iter-1 baseline 608). + +## Per-task notes + +- iter loop-recur.2.1: the four `Recur*` `CheckError` variants + (`RecurOutsideLoop`, `RecurArityMismatch{expected,got}`, + `RecurTypeMismatch{position,expected,got}`, + `RecurNotInTailPosition`) + 4 `code()` arms + 2 `ctx()` arms + (Arity/Type only; OutsideLoop/NotInTailPosition use the `{}` + catch-all). RED-first via `recur_checkerror_codes_are_exact` + (observed 4× E0599); GREEN exact. Bracket-`[code]`-free Display. +- iter loop-recur.2.2: `synth` signature gains + `loop_stack: &mut Vec>` after `mut_scope_stack`; + threaded at every recursive call site (17 single-line canonical + + 3 multi-line `Term::Mut`-init/body & `Term::Assign`-value + 2 + letrec-capture `&mut body_effects`-shape) + `check_const` (fresh + empty stack) + cross-module callers + test-module callers. The + compile-driven sweep (`cargo build`/`cargo test --no-run`) was the + exhaustive caller oracle as the plan specifies; iterated to 0 + errors. Stub intact, lib suite green. +- iter loop-recur.2.3: iter-1 `Internal` stub replaced with the two + real `Term::Loop`/`Term::Recur` arms. Binder-name save/restore + mirrors `Term::Let` (`lib.rs:3205-3218`) verbatim; per-arg type + check mirrors `Term::Assign` (`lib.rs:3716-3730`) verbatim per + Boss call 1; `recur`'s own type = `Subst::fresh(counter)`. + RED `loop_sum_to_typechecks_clean` observed `["internal"]`; + GREEN zero diagnostics. +- iter loop-recur.2.4: new private `verify_loop_body(t, in_loop_tail)` + immediately after `verify_tail_positions`'s closing brace — + exhaustive no-`_` match over all 16 `Term` variants (verified + equal to `verify_tail_positions`' variant set). Invoked from + `check_fn` after `verify_tail_positions(&f.body, true)?;`. RED + `recur_not_in_tail_position` observed `left: []`; GREEN + `["recur-not-in-tail-position"]`, positive still clean. +- iter loop-recur.2.5: 3 remaining negative fixtures + (`test_recur_outside_loop` / `_arity_mismatch` / `_type_mismatch`) + + 3 pins (all 5 green) + `carve_out_inventory` 13→17 with header + refresh (`Twelve…mut.2` → `Seventeen…loop-recur.2`, pre-existing + Twelve-vs-13 mut.4-tidy drift corrected in passing) + ct1 F2 + sibling `check_human_mode_renders_recur_diagnostic_code_exactly_once`. +- iter loop-recur.2.6: `examples/loop_forever.ail` (loop whose only + path is `recur`, no exit) typechecks clean — asserts the spec + "no termination claim is made or enforced". Form-A grammar + verified verbatim against the shipped `loop_sum_to.ail`. Full + suite 616/0; tail-app non-regression green (9 `tail`-named tests + ok incl. the iter-1 verify_tail_positions guards). + +## Boss design calls (mirrored from the plan header at iter close) + +1. **`RecurTypeMismatch` is an Assign-style structural pre-check, + NOT a `unify`-propagate.** `Term::Recur` per-arg checking mirrors + the `Term::Assign` arm (`lib.rs:3716-3730`) verbatim in + mechanism: synth the arg, `subst.apply` both the arg type and the + binder type, structural `!=`, on mismatch + `Err(RecurTypeMismatch{position,expected,got})`. A + `unify`-propagate would surface the generic `type-mismatch` code + and fail the spec acceptance ("dedicated `recur-type-mismatch` + fires point-exactly"). Rationale semantic (one in-repo mechanism + for "declared-vs-actual at a binding site with its own + point-exact code", consistent with `AssignTypeMismatch`), not + effort. Implemented verbatim; the `test_recur_type_mismatch` + fixture fires exactly `["recur-type-mismatch"]`. +2. **`loop_stack` element type is `Vec` (ordered binder + types), NOT `IndexMap`.** `recur` rebinds binders + *positionally*, so the frame models the ordered binder types for + arity (`.len()`) + per-position type checks. Binder *names* enter + the ordinary `locals: &mut IndexMap` exactly as + `Term::Let` binds its name (save/restore in reverse on loop + exit). The spec phrase "threaded exactly as mut.2's + `mut_scope_stack`" governs the *threading discipline* + (a `&mut Vec<…>` pushed/popped around the body, passed through + every recursive `synth`), not the element type. Semantic, not + effort. Implemented verbatim. +3. **Diagnostic-code precedence is by pass ordering, no explicit + logic.** `RecurOutsideLoop`/`RecurArityMismatch`/`RecurTypeMismatch` + are raised in `synth` (runs at the `check_fn` synth call); + `RecurNotInTailPosition` is raised in `verify_loop_body`, invoked + *after* `verify_tail_positions(&f.body, true)?;`. A `recur` + outside any loop therefore fires `RecurOutsideLoop` (synth, + first), not `RecurNotInTailPosition`. No precedence logic added; + the pass sequence IS the mechanism. `verify_loop_body` is entered + only on synth success, so every `recur` reached there is already + inside a loop with matching arity/types — the pass adds only the + tail rule. `verify_tail_positions` is byte-frozen (0 deletions); + `verify_loop_body` is a new sibling, never a repurpose. + +## Concerns + +- DONE_WITH_CONCERNS (iter loop-recur.2.2): **plan ordering defect — + `check_fn` threading must be in Task 2, not Task 4.** The plan's + Task 2 Step 3 bullet says "check_fn :1970: handled in Task 4 Step + 4 (it declares its own fresh loop_stack)", but Task 2 Step 4's + gate is `cargo build -p ailang-check` reaching `Finished` with 0 + errors. That gate is *unsatisfiable* while `check_fn` remains an + unthreaded `synth` caller (hard `error[E0061]`). Resolution: + `check_fn`'s `loop_stack` declaration + synth-call threading + (verbatim the plan's Task 4 Step 3 block + Step 4 first half) were + pulled into Task 2 where the compile gate forces them; only the + `verify_loop_body` *invocation* (Task 4 Step 4 second half) + remained for Task 4. This is the unique resolution satisfying both + Task 2 Step 4 AND preserving all plan code verbatim — the "fix to + compile while preserving evident intent + Boss calls" repair the + carrier explicitly authorises. Correctness: the declaration code + is byte-identical to the plan's Task 4 Step 3 block; no semantic + change, only sequencing. Recurring planner-gap class (a + compile-gate task whose gate depends on a caller the plan defers + past the gate) — candidate for a planner Step-5 self-review check. +- DONE_WITH_CONCERNS (iter loop-recur.2.2): **recon under-counted + cross-module `synth` callers** — `builtins.rs` ×2 (test helpers), + `lift.rs:746` (letrec-capture re-entry), `mono.rs:720` & + `mono.rs:1361` (mono re-synth) were not in the plan's site + inventory (`:3161…:3717` + the 8 test sites). Exactly the + mut.2-class recon-undercount the iter-1 journal flagged + (Boss-call-2-class "recon under-scoped it"). Resolved by mirroring + the established mut.2 fresh-stack pattern at each (declare a fresh + empty `loop_stack` alongside the existing fresh `mut_scope_stack`, + pass `&mut loop_stack` immediately after `&mut mut_scope_stack`). + Observation, not a correctness risk — the compile-driven sweep IS + the plan's designated exhaustive oracle and surfaced every site; + the plan's literal site list is advisory, the compiler is + authoritative (as the plan itself states). + +## Known debt + +- No additional `ail run`/binary-stdout E2E fixture written (Phase + 3). iter-2 ships typecheck semantics only; the `lower_term` + `CodegenError::Internal` stub stays by design (real loop lowering + + the positive sum_to-runs-to-a-value / deep-`n` E2E is explicitly + iter-3 scope). An `ail run` this iter would only exercise the + deliberately-transient codegen stub (a negative-value test of a + known-temporary error) — same justified Phase-3 reasoning as + iter-1. The iter-2 invariants worth protecting (four codes + point-exact, positive + infinite typecheck clean, + carve-out/tail-app non-regression) are fully pinned by the tests + added in Tasks 1/3/4/5/6 + the ct1 F2 sibling. + +## Files touched + +- Check core: `crates/ailang-check/src/lib.rs` (4 variants + + code/ctx, `synth` signature + threading, real Loop/Recur arms, + new `verify_loop_body`, `check_fn` + `check_const` wiring), + `crates/ailang-check/src/lift.rs`, `crates/ailang-check/src/mono.rs`, + `crates/ailang-check/src/builtins.rs` (cross-module synth-caller + threading) +- Tests/fixtures: `crates/ailang-check/tests/loop_recur_typecheck_pin.rs` + (new — 7 tests), `crates/ail/tests/ct1_check_cli.rs` (F2 sibling), + `crates/ailang-core/tests/carve_out_inventory.rs` (13→17 + header) +- New fixtures: `examples/test_recur_outside_loop.ail.json`, + `examples/test_recur_arity_mismatch.ail.json`, + `examples/test_recur_type_mismatch.ail.json`, + `examples/test_recur_not_in_tail_position.ail.json`, + `examples/loop_forever.ail` +- Reused (no new file): `examples/loop_sum_to.ail` (iter-1 + round-trip fixture, now also the positive `ail check` evidence) + +## Stats + +bench/orchestrator-stats/2026-05-17-iter-loop-recur.2.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index be725ee..a08fd81 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -82,3 +82,4 @@ - 2026-05-16 — audit iteration-discipline-revert (milestone close, clean): architect confirmed the revert byte-pristine (18 src + 5 test files byte-identical to `1ff7e81`, zero residual it.1/it.2 production surface, DESIGN.md coherent, roadmap/spec hygiene correct); one `[medium]` drift — a dangling `loop`/`recur` cross-reference into the reverted milestone inside the *live* Stateful-islands roadmap scope bullet — fixed inline (Boss doc-hygiene; reworded to keep the real "no `while`; repetition stays recursion" scope guard, drop the reverted-milestone reference). Bench: `compile_check.py`/`cross_lang.py` exit 0; `check.py` exit 1 on the single metric `bench_list_sum.bump_s` +12.71%. Bencher localisation: HEAD and `1ff7e81` bump binaries `cmp`-identical, interleaved 3×60-run measurement shows head−oracle delta ~0 (±1.5% stdev) with *both* ~+11% over the 2026-05-09 baseline → environmental/hardware drift, NOT a revert regression (third independent proof codegen == `1ff7e81`). Resolution: carry-on, baseline NOT ratified (Iron Law — nothing intentionally moved the metric; byte-identical codegen must not move the baseline; the spec's PRISTINE mandate is satisfied because pristine = "no regression introduced", proven). Pre-existing `*.bump_s` baseline-vs-hardware staleness (the `1ff7e81` oracle trips the same +11%) filed forward as a separate P2 `[todo]` (bench-harness recalibration, no language change), not mis-attributed to the revert. Fieldtest skipped (revert restores the already-field-tested pre-`9973546` surface; Task-11 164-fixture byte-equivalence is the stronger proof). Milestone closed clean → 2026-05-16-audit-iteration-discipline-revert.md - 2026-05-16 — iter effect-doc-honesty: standalone documentation-honesty tidy (split out from the retired effect-op-arg-modes bundle — user rejected bundling a real DESIGN.md fix with speculative build-ahead infra). Corrected three false effect-system claims the recon surfaced: DESIGN.md Decision 3 "row-polymorphic (`![IO | r]`)" (no `EffectRow`/row var exists — effect sets are flat closed sets unified by set-equality) + "`IO` and `Diverge` … are wired up" (`Diverge` is 100% vapour: zero code in any crate) → reconciled to IO-only/Diverge-reserved-unimplemented (modelled on Decision 4's reserved-refinements precedent); DESIGN.md §"What is not supported" "IO and Diverge ops" bullet; `ast.rs` `Term::Do` doc-comment "resolved against the effect-handler table at link time" → the real mechanism (typecheck `Env::effect_ops` lookup + `lower_effect_op` literal codegen match, no handler table). Satellite lockstep: `form_a.md:226` + rule-3, `main.rs:289` merge-prose CONTRACT example. Guarded by a new 4-test doc-presence pin `crates/ailang-core/tests/effect_doc_honesty_pin.rs` (fiction-absent + corrected-anchor-present, single-line substrings — wrap-robust). No language/checker/codegen change; `ail check`/`run` byte-unchanged by construction. `cargo test --workspace` 600 → 604; drift/coverage trio (`design_schema_drift`/`spec_drift`/`schema_coverage`) green, empirically confirming none scans the effect-prose region. One concern: the plan's Task-2 replacement body soft-wrapped a phrase the single-line pin asserts; orchestrator resolved correctly (exact wording + exact pin preserved, wrap column moved) — recurring-class planner gap, fixed forward by a Step-5 self-review tightening → 2026-05-16-iter-effect-doc-honesty.md - 2026-05-17 — iter loop-recur.1: standalone-`loop`/`recur` milestone (1 of 3) — the strictly-additive AST-node foundation. `Term::Loop { binders: Vec, body }` / `Term::Recur { args }` / `struct LoopBinder` (mirrors `MutVar`'s `(name,type,init)` triple; `binders` no `skip_serializing_if`) added end-to-end across all six crates' no-`_`-wildcard exhaustive `Term` matches (~30 sites incl. one recon-undercount integration-test pin): Form-A `parse_loop`/`parse_recur` (binder/body boundary disambiguated by an `is_term_head_kw` guard — the plan's flagged sole parser judgement) + print + `form_a.md` grammar/notes + prose render/free-var/subst lockstep + canonical-JSON serde/round-trip + DESIGN.md §Data-model `"t":"loop"`/`"t":"recur"` blocks + design_schema_drift/spec_drift/schema_coverage anchors + a new `loop_recur` hash pin (additivity proven: iter13a + new pin both green, pre-existing canonical-JSON bytes byte-stable) + `examples/loop_sum_to.ail` round-trip fixture. NO typecheck semantics + NO real codegen by design: the two semantic dispatch points stubbed `synth`→`CheckError::Internal` / `lower_term`→`CodegenError::Internal` exactly as mut.1; pure analysis walkers (escape/lambda/`synth_with_extras`) get real structural pass-through. Two binding Boss design calls (mirrored into the journal): (1) `verify_tail_positions` "byte-unchanged" = tail-app *role* unchanged not source-frozen — it is an exhaustive no-wildcard match so two additive descent-only arms are mandatory; acceptance evidence is the tail-app non-regression test (all `tail`-filtered tests byte-identical), mut.1 set the precedent; (2) codegen IS iter-1 scope as stubs/pass-throughs (no real loop-header/phi/back-edge — that is iter 3). Three plan-pseudo-vs-reality substitutions, all intent-preserving, recurring `feedback_specs_need_concrete_code`/`feedback_plan_pseudo_vs_reality` class: serde `Type::Con` literal `{"t":"con",…,"args":[]}`→real `{"k":"con","name":"Int"}`; bare `Int`→`(con Int)` in binder triples (bare `Int` parses as `Type::Var`); `ailang_core::ast::LoopBinder`→unqualified inside ailang-core. Boss forward-fix folded in: Concern 2 surfaced that the committed specs themselves (`2026-05-17-loop-recur.md` headline + `bad_recur`, `2026-05-17-llm-surface-discipline.md` §5) wrote bare `Int` — corrected all three snippets to `(con Int)` (doc-honesty, same class as the mono.rs header; no design/schema/assumption change, no re-brainstorm). `cargo test --workspace` 600→608 / 0 red (Boss-reran independently). Component 4 (typecheck) = iter 2; Component 5 (codegen) + positive/deep-`n` E2E = iter 3 → 2026-05-17-iter-loop-recur.1.md +- 2026-05-17 — iter loop-recur.2: standalone-`loop`/`recur` milestone (2 of 3) — Component 4 typecheck semantics. The iter-1 `synth` `CheckError::Internal` stub for `Term::Loop`/`Term::Recur` is replaced with real binder typing (each init synthed in outer scope + already-declared binder names of THIS loop via ordinary `locals` save/restore mirroring `Term::Let` verbatim; loop's static type = body type) + positional `recur` arity/per-arg-type checking via a new `loop_stack: &mut Vec>` frame threaded exactly as mut.2's `mut_scope_stack` (every recursive + cross-module + test synth caller, compile-swept). New private `verify_loop_body(t,in_loop_tail)` pass — a SIBLING of the byte-frozen `verify_tail_positions` (0 deletions, tail-app role untouched), invoked in `check_fn` after it so synth-raised codes take precedence by pass ordering. Four `Recur*` `CheckError` variants (`RecurOutsideLoop`, `RecurArityMismatch{expected,got}`, `RecurTypeMismatch{position,expected,got}`, `RecurNotInTailPosition`) + `code()` + 2 `ctx()` arms, bracket-`[code]`-free Display (F2); four negative `.ail.json` fixtures fire their codes point-exactly (`assert_eq!`, non-vacuous) via a new `loop_recur_typecheck_pin.rs` (7 tests) + a ct1 F2 human-mode sibling; `carve_out_inventory` 13→17 with the pre-existing mut.4-tidy "Twelve"-vs-13 stale-header drift corrected in passing. iter-1's `loop_sum_to.ail` round-trip fixture now ALSO typechecks clean (one fixture, two properties — no near-duplicate); `loop_forever.ail` (loop whose only path is `recur`) typechecks clean, asserting the spec "no termination claim is made or enforced". Three binding Boss design calls (mirrored into the journal): (1) `RecurTypeMismatch` is an Assign-style `subst.apply`-both-then-structural-`!=` pre-check, NOT a `unify`-propagate (a propagate would surface generic `type-mismatch` and fail the point-exact-code acceptance); (2) `loop_stack` element type is positional `Vec` NOT name-keyed `IndexMap` (recur rebinds by position; binder names live in `locals`); (3) diagnostic-code precedence is by pass ordering (synth before verify_loop_body), no explicit logic. NO codegen (iter-1 `lower_term` `CodegenError::Internal` stub stays — iter 3); NO `Diverge`/`verify_structural_recursion`/guardedness (spec deliberate boundary). Two DONE_WITH_CONCERNS, both Task 2, both journalled: (a) a plan-ordering defect — Task 2's `cargo build` 0-errors gate is unsatisfiable while `check_fn` (deferred by the plan to Task 4) is an unthreaded caller; orchestrator pulled the byte-identical declaration+threading forward to Task 2, left only the `verify_loop_body` invocation in Task 4 (no semantic change, only sequencing); (b) recon-undercount of cross-module synth callers (`builtins.rs`×2, `lift.rs:746`, `mono.rs:720`/`:1361`), the recurring mut.2-class, resolved via the plan's own designated compile-sweep oracle. Boss systemic fix folded into this commit: planner SKILL.md Step-5 self-review gains item 7 (compile-gate vs. deferred-caller ordering) so the Concern-(a) class is scrubbed at plan time, not discovered at execution. `cargo test --workspace` 608→616 / 0 red (Boss-reran independently); `verify_tail_positions`/tail-app byte-frozen confirmed by diff-hunk inspection. Component 5 (codegen loop-header/phi/back-edge) + the positive RUN-to-value / deep-`n` E2E = iteration 3 → 2026-05-17-iter-loop-recur.2.md diff --git a/examples/loop_forever.ail b/examples/loop_forever.ail new file mode 100644 index 0000000..ebb1eb9 --- /dev/null +++ b/examples/loop_forever.ail @@ -0,0 +1,7 @@ +(module loop_forever + (fn spin + (type (fn-type (params (con Int)) (ret (con Int)))) + (params n) + (body + (loop (i (con Int) 0) + (recur (app + i 1)))))) diff --git a/examples/test_recur_arity_mismatch.ail.json b/examples/test_recur_arity_mismatch.ail.json new file mode 100644 index 0000000..220c1d8 --- /dev/null +++ b/examples/test_recur_arity_mismatch.ail.json @@ -0,0 +1,22 @@ +{ + "schema": "ailang/v0", + "name": "test_recur_arity_mismatch", + "imports": [], + "defs": [ + { + "kind": "fn", + "name": "bad_arity", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] }, + "params": [], + "doc": "loop-recur iter 2: 2 binders, recur passes 1 arg -> recur-arity-mismatch.", + "body": { + "t": "loop", + "binders": [ + { "name": "a", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }, + { "name": "b", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 1 } } } + ], + "body": { "t": "recur", "args": [ { "t": "var", "name": "a" } ] } + } + } + ] +} diff --git a/examples/test_recur_not_in_tail_position.ail.json b/examples/test_recur_not_in_tail_position.ail.json new file mode 100644 index 0000000..9221132 --- /dev/null +++ b/examples/test_recur_not_in_tail_position.ail.json @@ -0,0 +1,33 @@ +{ + "schema": "ailang/v0", + "name": "test_recur_not_in_tail_position", + "imports": [], + "defs": [ + { + "kind": "fn", + "name": "bad_recur", + "type": { + "k": "fn", + "params": [ { "k": "con", "name": "Int" } ], + "ret": { "k": "con", "name": "Int" }, + "effects": [] + }, + "params": [ "n" ], + "doc": "loop-recur iter 2: recur as an argument to + is NOT in tail position -> recur-not-in-tail-position.", + "body": { + "t": "loop", + "binders": [ + { "name": "i", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } } + ], + "body": { + "t": "app", + "fn": { "t": "var", "name": "+" }, + "args": [ + { "t": "lit", "lit": { "kind": "int", "value": 1 } }, + { "t": "recur", "args": [ { "t": "app", "fn": { "t": "var", "name": "+" }, "args": [ { "t": "var", "name": "i" }, { "t": "lit", "lit": { "kind": "int", "value": 1 } } ] } ] } + ] + } + } + } + ] +} diff --git a/examples/test_recur_outside_loop.ail.json b/examples/test_recur_outside_loop.ail.json new file mode 100644 index 0000000..ef19edb --- /dev/null +++ b/examples/test_recur_outside_loop.ail.json @@ -0,0 +1,15 @@ +{ + "schema": "ailang/v0", + "name": "test_recur_outside_loop", + "imports": [], + "defs": [ + { + "kind": "fn", + "name": "main", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] }, + "params": [], + "doc": "loop-recur iter 2: recur with no enclosing loop -> recur-outside-loop.", + "body": { "t": "recur", "args": [ { "t": "lit", "lit": { "kind": "int", "value": 1 } } ] } + } + ] +} diff --git a/examples/test_recur_type_mismatch.ail.json b/examples/test_recur_type_mismatch.ail.json new file mode 100644 index 0000000..a073bb4 --- /dev/null +++ b/examples/test_recur_type_mismatch.ail.json @@ -0,0 +1,21 @@ +{ + "schema": "ailang/v0", + "name": "test_recur_type_mismatch", + "imports": [], + "defs": [ + { + "kind": "fn", + "name": "bad_type", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Int" }, "effects": [] }, + "params": [], + "doc": "loop-recur iter 2: binder is Int, recur arg is Bool -> recur-type-mismatch.", + "body": { + "t": "loop", + "binders": [ + { "name": "i", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } } + ], + "body": { "t": "recur", "args": [ { "t": "lit", "lit": { "kind": "bool", "value": true } } ] } + } + } + ] +} diff --git a/skills/planner/SKILL.md b/skills/planner/SKILL.md index 32d47bd..24ef2d9 100644 --- a/skills/planner/SKILL.md +++ b/skills/planner/SKILL.md @@ -190,6 +190,24 @@ Before handing the plan off, run this checklist inline: line-wrap family (iter-revert Concern 2; iter effect-doc-honesty Task 2) — scrub it here, every plan that pairs a presence-pin with a verbatim text edit. +7. **Compile-gate vs. deferred-caller ordering:** when a task + changes a function signature (or any change that makes the + *whole crate* fail to compile until N call sites are updated) + AND that task ends with a `cargo build`/`cargo test` "0 errors" + gate, every caller the signature change touches MUST be threaded + *inside that same task* — not deferred to a later task. A + "0-errors" gate is unsatisfiable while any caller is still + unthreaded (hard `error[E0061]`), so a plan that defers a caller + (e.g. "the `check_fn` call site is handled in Task 4") past an + earlier task's compile gate is internally contradictory: the + executor is forced to pull the deferred code forward to satisfy + the gate, silently resequencing the plan. Either fold all + caller-threading into the signature-change task, or make the + gate a *partial* build of just the changed module with the + crate-wide build deferred to the task that finishes threading. + This is the recurring "compile-gate depends on a caller the plan + defers past the gate" family (iter loop-recur.2 Concern 1) — + scrub it here, every plan with a signature-change task. Fix issues inline.