iter mut.2: typecheck for Term::Mut + Term::Assign

Replaces the iter mut.1 dispatch stubs in synth with real typecheck
logic. Codegen stubs stay (deferred to mut.3); examples/mut.ail now
typechecks clean but still cannot run end-to-end.

Concretely:

- crates/ailang-check/src/lib.rs: three new CheckError variants
  (MutAssignOutOfScope, AssignTypeMismatch, UnsupportedMutVarType)
  with #[error('[code]: msg')] Display attrs matching the cli-diag-
  human bracketed-code convention; code() + ctx() arms emit
  kebab-case codes and structured JSON payloads.

- synth signature: new parameter mut_scope_stack: &mut Vec<IndexMap<
  String, Type>> after locals, threaded through every recursive call
  site (synth's 18 internal calls + mono.rs:712/1337 re-synth +
  lift.rs:723 + builtins.rs test helpers + the mq.3 in-test helper
  at lib.rs:6663). Stack is per-walk and lexically scoped — push on
  Term::Mut entry, pop on exit. Each frame is an IndexMap so
  declaration order is preserved for the diagnostic 'available' list.

- Term::Var resolution: prepended with innermost-first mut-scope
  lookup. Mut-vars are monomorphic — no Forall instantiation, no
  free_fn_owner recording. Innermost-wins shadowing falls out of
  the iteration order.

- Term::Mut arm: gate var types to Int/Float/Bool/Unit only via
  a small is_supported_mut_var_type helper; each var's init is
  synth'd in the in-progress scope (the var itself is not yet
  bound, so it does not self-shadow during init); push completed
  frame, synth body, pop. Block's type is body's type.

- Term::Assign arm: walk mut_scope_stack innermost-first looking for
  name. On miss: MutAssignOutOfScope with available flattened
  across all frames (innermost-first, deduplicated, preserving
  order). On hit: synth value, unify against declared type — on
  mismatch emit AssignTypeMismatch with rendered types; on success
  produce Type::unit().

- Five .ail.json fixtures under examples/ exercising each
  diagnostic plus a positive nested-shadow sanity case, driven by
  the new pin test crates/ailang-check/tests/mut_typecheck_pin.rs
  (load_workspace + check_workspace + assert exact codes).

- carve_out_inventory.rs EXPECTED extended 7 → 12 to cover the new
  negative-fixture set (consistent with the form-a-default-authoring
  spec §C4(b) precedent for type-rejection fixtures staying as
  .ail.json-only).

Plan deviations from recon: three additional synth() call sites
beyond the four enumerated (lift.rs:723, builtins.rs x2,
lib.rs:6663) surfaced via the build-red structural signal; each
threaded with a fresh empty stack. carve_out_inventory.rs extension
was required by the existing pin but not named in the recon — a
documentary concern for the next planner pass.

Tests: 579 → 592 green; examples/mut.ail typechecks clean
('ok (26 symbols across 2 modules)') via cargo run --bin ail --
check examples/mut.ail; cargo build green; full workspace test
green.

Journal: docs/journals/2026-05-15-iter-mut.2.md.

Refs: docs/specs/2026-05-15-mut-local.md, docs/plans/2026-05-15-iter-mut.2.md.

bench/orchestrator-stats/2026-05-15-iter-mut.2.json

@@ -0,0 +1,20 @@
+{
+  "iter_id": "mut.2",
+  "date": "2026-05-15",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 7,
+  "tasks_completed": 7,
+  "reloops_per_task": {
+    "1": 0,
+    "2": 0,
+    "3": 0,
+    "4": 0,
+    "5": 0,
+    "6": 0,
+    "7": 0
+  },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null
+}

crates/ailang-check/src/builtins.rs

@@ -342,6 +342,7 @@ mod tests {
         let mut env = Env::default();
         install(&mut env);
         let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -352,6 +353,7 @@ mod tests {
             t,
             &env,
             &mut locals,
+            &mut mut_scope_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -583,6 +585,7 @@ mod tests {
         let mut env = Env::default();
         install(&mut env);
         let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -593,6 +596,7 @@ mod tests {
             &term,
             &env,
             &mut locals,
+            &mut mut_scope_stack,
             &mut effects,
             "<test>",
             &mut subst,

crates/ailang-check/src/lib.rs

@@ -631,6 +631,43 @@ pub enum CheckError {
         name: String,
     },
 
+    /// Iter mut.2: `Term::Assign { name, .. }` reached typecheck but
+    /// `name` is not a mut-var of any enclosing `Term::Mut` on the
+    /// lexical scope stack.
+    ///
+    /// `available` lists every mut-var name visible at the assign
+    /// site, flattened across all enclosing mut-frames innermost-
+    /// first, deduplicated, preserving order — so the diagnostic
+    /// surfaces "you might have meant one of: X / Y / Z" without
+    /// duplicates when the same name appears at multiple nesting
+    /// depths.
+    #[error("[mut-assign-out-of-scope] cannot assign to `{name}` here — not declared as a mut-var in the enclosing (mut ...) block. Available mut-vars in scope: [{}]", available.join(", "))]
+    MutAssignOutOfScope {
+        name: String,
+        available: Vec<String>,
+    },
+
+    /// Iter mut.2: `Term::Assign { name, value }` reached typecheck
+    /// inside a valid mut-scope, but `value`'s synth type differs
+    /// from the var's declared type.
+    #[error("[assign-type-mismatch] cannot assign `{got}` to mut-var `{name} : {declared}` — the assigned value's type must match the var's declared type")]
+    AssignTypeMismatch {
+        name: String,
+        declared: String,
+        got: String,
+    },
+
+    /// Iter mut.2: `Term::Mut { vars, .. }` declared a `MutVar`
+    /// whose declared `ty` is not one of the four supported scalar
+    /// primitives (Int, Float, Bool, Unit). The temporary
+    /// restriction is named explicitly in spec
+    /// `docs/specs/2026-05-15-mut-local.md` §"Out of scope".
+    #[error("[mut-var-unsupported-type] mut-var `{name} : {ty}` is not supported in this milestone — only stack-resident primitive types (Int, Float, Bool, Unit) may be declared as mut-vars. Heap-RC-managed types (Str, ADTs, fn-values) are deferred to a follow-on milestone.")]
+    UnsupportedMutVarType {
+        name: String,
+        ty: String,
+    },
+
     /// 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
@@ -679,6 +716,9 @@ impl CheckError {
             CheckError::NoInstance { .. } => "no-instance",
             CheckError::AmbiguousMethodResolution { .. } => "ambiguous-method-resolution",
             CheckError::UnknownClass { .. } => "unknown-class",
+            CheckError::MutAssignOutOfScope { .. } => "mut-assign-out-of-scope",
+            CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch",
+            CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type",
             CheckError::Internal(_) => "internal",
         }
     }
@@ -741,6 +781,15 @@ impl CheckError {
             CheckError::UnknownClass { name } => {
                 serde_json::json!({ "name": name })
             }
+            CheckError::MutAssignOutOfScope { name, available } => {
+                serde_json::json!({"name": name, "available": available})
+            }
+            CheckError::AssignTypeMismatch { name, declared, got } => {
+                serde_json::json!({"name": name, "expected": declared, "actual": got})
+            }
+            CheckError::UnsupportedMutVarType { name, ty } => {
+                serde_json::json!({"name": name, "type": ty})
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -1882,7 +1931,11 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     let mut residuals: Vec<ResidualConstraint> = Vec::new();
     let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
     let mut warnings: Vec<Diagnostic> = Vec::new();
-    let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
+    // Iter mut.2: fresh per-fn-body mut-scope stack. Empty at fn entry;
+    // pushed/popped by `Term::Mut` arms during the walk; discarded after
+    // the body type-checks.
+    let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+    let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
     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)`
@@ -2631,7 +2684,11 @@ fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> R
     let mut residuals: Vec<ResidualConstraint> = Vec::new();
     let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
     let mut warnings: Vec<Diagnostic> = Vec::new();
-    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
+    // Iter mut.2: fresh per-const-body mut-scope stack (always empty
+    // at this entry point — `Term::Mut` may appear inside a const body
+    // and push frames as the walk descends).
+    let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+    let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
     out_warnings.extend(warnings);
     unify(&c.ty, &v, &mut subst)?;
     if !effects.is_empty() {
@@ -2648,6 +2705,14 @@ pub(crate) fn synth(
     t: &Term,
     env: &Env,
     locals: &mut IndexMap<String, Type>,
+    // Iter mut.2: per-walk lexical mut-scope. Each frame is one
+    // `Term::Mut` block's `vars` (preserving declaration order via
+    // `IndexMap`). The stack is pushed on `Term::Mut` entry and
+    // popped on exit; `Term::Var` consults it innermost-first before
+    // the locals/globals chain; `Term::Assign` resolves its target
+    // name through it. Position: locals-adjacent because both are
+    // per-fn-body lexical scope state.
+    mut_scope_stack: &mut Vec<IndexMap<String, Type>>,
     effects: &mut BTreeSet<String>,
     in_def: &str,
     subst: &mut Subst,
@@ -2669,6 +2734,18 @@ pub(crate) fn synth(
             Literal::Float { .. } => Type::float(),
         }),
         Term::Var { name } => {
+            // Iter mut.2: mut-vars take precedence over every other
+            // resolution path (let-bound, param, top-level, builtin,
+            // class-method). Walk the stack innermost-first; the first
+            // frame containing `name` wins (lexical shadowing). Mut-vars
+            // are monomorphic per spec §"var element types" — no Forall
+            // instantiation, no `FreeFnCall` recording.
+            for frame in mut_scope_stack.iter().rev() {
+                if let Some(ty) = frame.get(name) {
+                    return Ok(ty.clone());
+                }
+            }
+
             // Lookup precedence: locals → local globals → class-method
             // table → qualified cross-module ref. A `Forall` resolved at
             // any of these levels is instantiated with fresh metavars at
@@ -3013,7 +3090,7 @@ pub(crate) fn synth(
             Ok(maybe_instantiate(raw, counter))
         }
         Term::App { callee, args, .. } => {
-            let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let cty = synth(callee, env, locals, mut_scope_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, .. } => {
@@ -3049,7 +3126,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(exp, &actual, subst)?;
             }
             for e in fx {
@@ -3058,9 +3135,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&ret))
         }
         Term::Let { name, value, body } => {
-            let v = synth(value, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let v = synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             let prev = locals.insert(name.clone(), v);
-            let r = synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let r = synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             match prev {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -3072,10 +3149,10 @@ pub(crate) fn synth(
             Ok(r)
         }
         Term::If { cond, then, else_ } => {
-            let c = synth(cond, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let c = synth(cond, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&Type::bool_(), &c, subst)?;
-            let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            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, 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)?;
             unify(&t1, &t2, subst)?;
             Ok(subst.apply(&t1))
         }
@@ -3093,7 +3170,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(sig.params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(exp, &actual, subst)?;
             }
             effects.insert(sig.effect.clone());
@@ -3188,7 +3265,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, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(&exp_inst, &actual, subst)?;
             }
             Ok(Type::Con {
@@ -3197,7 +3274,7 @@ pub(crate) fn synth(
             })
         }
         Term::Match { scrutinee, arms } => {
-            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let s_ty = synth(scrutinee, env, locals, mut_scope_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),
@@ -3215,7 +3292,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, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let body_ty = synth(&arm.body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 for (n, prev) in pushed.into_iter().rev() {
                     match prev {
                         Some(p) => {
@@ -3290,9 +3367,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, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let lty = synth(lhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&Type::unit(), &lty, subst)?;
-            synth(rhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(rhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
         Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
             let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
@@ -3301,7 +3378,7 @@ pub(crate) fn synth(
                 pushed.push((n.clone(), prev));
             }
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let body_ty = synth(body, env, locals, mut_scope_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) => {
@@ -3389,7 +3466,7 @@ pub(crate) fn synth(
             // subset rule against `declared_effs` — exactly like
             // `Term::Lam`.
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let body_ty = synth(body, env, locals, mut_scope_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() {
@@ -3416,7 +3493,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, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let in_ty = synth(in_term, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
             match prev_in {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -3432,7 +3509,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, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(value, env, locals, mut_scope_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
@@ -3446,7 +3523,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, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let _ = synth(source, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             match body.as_ref() {
                 Term::Ctor { .. } | Term::Lam { .. } => {}
                 other => {
@@ -3474,30 +3551,105 @@ pub(crate) fn synth(
             }
             // Body's type is the result type of the whole reuse-as
             // expression.
-            synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
-        // Iter mut.1: typecheck recognition of `Term::Mut` and
+        // Iter mut.2: a mut block opens a fresh lexical scope for its
-        // `Term::Assign` is deferred to iter mut.2 (see
+        // mut-vars. Each var's `init` is synthed in the outer scope
-        // `docs/specs/2026-05-15-mut-local.md` §"Iteration mut.1"
+        // plus already-declared vars of this same frame (vars are
-        // out-of-iteration boundary). The dispatch entry here stubs
+        // initialised in declaration order; later inits see earlier
-        // with `CheckError::Internal` so that a well-formed mut block
+        // names). The body is synthed with the completed frame on the
-        // reaching this point in mut.1 fails fast with a
+        // stack. The frame is popped on exit. The block's static type
-        // human-readable message — the Form-A surface parses these
+        // is the body's static type.
-        // shapes and the AST round-trips them, but no fn body is
+        Term::Mut { vars, body } => {
-        // expected to *use* them yet.
+            let mut frame: IndexMap<String, Type> = IndexMap::new();
-        Term::Mut { .. } => {
+            for v in vars {
-            Err(CheckError::Internal(
+                if !is_supported_mut_var_type(&v.ty) {
-                "Term::Mut not yet supported in typecheck (deferred to iter mut.2)".into(),
+                    return Err(CheckError::UnsupportedMutVarType {
-            ))
+                        name: v.name.clone(),
+                        ty: ailang_core::pretty::type_to_string(&v.ty),
+                    });
+                }
+                // Synth the init in the outer scope plus any vars
+                // already pushed into `frame`. The cleanest way to
+                // expose those bindings is to push a single in-flight
+                // frame (clone of the accumulator) onto the stack for
+                // the duration of the init walk, then pop. This keeps
+                // 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,
+                    subst, counter, residuals, free_fn_calls, warnings,
+                )?;
+                mut_scope_stack.pop();
+                unify(&v.ty, &init_ty, subst)?;
+                frame.insert(v.name.clone(), v.ty.clone());
+            }
+            mut_scope_stack.push(frame);
+            let body_result = synth(
+                body, env, locals, mut_scope_stack, effects, in_def,
+                subst, counter, residuals, free_fn_calls, warnings,
+            );
+            mut_scope_stack.pop();
+            body_result
         }
-        Term::Assign { .. } => {
+        // Iter mut.2: `Term::Assign` resolves its target name through
-            Err(CheckError::Internal(
+        // the mut-scope stack (innermost-first). On a hit, the value's
-                "Term::Assign not yet supported in typecheck (deferred to iter mut.2)".into(),
+        // synth type must match the var's declared type. The
-            ))
+        // expression's static type is Unit.
+        Term::Assign { name, value } => {
+            let declared: Option<Type> = mut_scope_stack
+                .iter()
+                .rev()
+                .find_map(|frame| frame.get(name).cloned());
+            match declared {
+                None => {
+                    // Flatten every mut-var name visible at this point,
+                    // innermost-first, deduplicated preserving order.
+                    let mut available: Vec<String> = Vec::new();
+                    for frame in mut_scope_stack.iter().rev() {
+                        for k in frame.keys() {
+                            if !available.contains(k) {
+                                available.push(k.clone());
+                            }
+                        }
+                    }
+                    Err(CheckError::MutAssignOutOfScope {
+                        name: name.clone(),
+                        available,
+                    })
+                }
+                Some(declared_ty) => {
+                    let value_ty = synth(
+                        value, env, locals, mut_scope_stack, effects, in_def,
+                        subst, counter, residuals, free_fn_calls, warnings,
+                    )?;
+                    let applied_declared = subst.apply(&declared_ty);
+                    let applied_value = subst.apply(&value_ty);
+                    if applied_declared != applied_value {
+                        return Err(CheckError::AssignTypeMismatch {
+                            name: name.clone(),
+                            declared: ailang_core::pretty::type_to_string(&applied_declared),
+                            got: ailang_core::pretty::type_to_string(&applied_value),
+                        });
+                    }
+                    Ok(Type::unit())
+                }
+            }
         }
     }
 }
 
+/// Iter mut.2: gate `MutVar.ty` to the four stack-resident scalar
+/// primitives per spec `docs/specs/2026-05-15-mut-local.md` §"Out of
+/// scope". Heap-RC-managed types (Str, ADTs, fn-values) and any
+/// parameterised constructor are deferred to a follow-on milestone.
+fn is_supported_mut_var_type(ty: &Type) -> bool {
+    matches!(
+        ty,
+        Type::Con { name, args } if args.is_empty() && matches!(name.as_str(), "Int" | "Float" | "Bool" | "Unit")
+    )
+}
+
 /// If `t` is a `Forall`, instantiate it with fresh metavars; otherwise
 /// pass through unchanged. Used at every var-resolution site.
 fn maybe_instantiate(t: Type, counter: &mut u32) -> Type {
@@ -3851,6 +4003,326 @@ mod tests {
     use super::*;
     use ailang_core::SCHEMA;
 
+    /// Helper that synths a single Term against a default empty env +
+    /// fresh local / scope / effect state. Returns the substituted
+    /// final type. Used by the mut.2 pin tests below.
+    fn synth_standalone(term: &Term) -> Type {
+        let env = Env::default();
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals: Vec<ResidualConstraint> = Vec::new();
+        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+        let mut warnings: Vec<Diagnostic> = Vec::new();
+        let ty = synth(
+            term,
+            &env,
+            &mut locals,
+            &mut mut_scope_stack,
+            &mut effects,
+            "<test>",
+            &mut subst,
+            &mut counter,
+            &mut residuals,
+            &mut free_fn_calls,
+            &mut warnings,
+        )
+        .expect("synth must succeed");
+        subst.apply(&ty)
+    }
+
+    /// Iter mut.2 (Task 3): `Term::Var` consults the mut-scope stack
+    /// before locals/globals. With a non-empty stack carrying
+    /// `x → Float` and a local also binding `x → Int`, resolving
+    /// `Var x` returns Float — mut-scope wins lexically.
+    ///
+    /// The frame is pre-populated directly on the stack (rather than
+    /// running a `Term::Mut` block that would push it) so this pin
+    /// isolates the Var-arm change from the Mut-arm work in Task 4.
+    #[test]
+    fn mut_var_resolution_shadows_outer_local() {
+        let env = Env::default();
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        locals.insert("x".into(), Type::int()); // outer let-style binding
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut frame: IndexMap<String, Type> = IndexMap::new();
+        frame.insert("x".into(), Type::float()); // inner mut-var
+        mut_scope_stack.push(frame);
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals: Vec<ResidualConstraint> = Vec::new();
+        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+        let mut warnings: Vec<Diagnostic> = Vec::new();
+
+        let term = Term::Var { name: "x".into() };
+        let ty = synth(
+            &term,
+            &env,
+            &mut locals,
+            &mut mut_scope_stack,
+            &mut effects,
+            "<test>",
+            &mut subst,
+            &mut counter,
+            &mut residuals,
+            &mut free_fn_calls,
+            &mut warnings,
+        )
+        .expect("synth must succeed");
+        assert_eq!(
+            ty,
+            Type::float(),
+            "mut-var `x : Float` on the scope stack must shadow local `x : Int` (got {ty:?})",
+        );
+    }
+
+    /// Iter mut.2 (Task 3): innermost-first walk on the mut-scope
+    /// stack. With two frames each binding `x` to a different type,
+    /// the innermost (last-pushed) wins.
+    #[test]
+    fn mut_var_resolution_picks_innermost_frame() {
+        let env = Env::default();
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut outer: IndexMap<String, Type> = IndexMap::new();
+        outer.insert("x".into(), Type::int());
+        mut_scope_stack.push(outer);
+        let mut inner: IndexMap<String, Type> = IndexMap::new();
+        inner.insert("x".into(), Type::bool_());
+        mut_scope_stack.push(inner);
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals: Vec<ResidualConstraint> = Vec::new();
+        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+        let mut warnings: Vec<Diagnostic> = Vec::new();
+
+        let term = Term::Var { name: "x".into() };
+        let ty = synth(
+            &term,
+            &env,
+            &mut locals,
+            &mut mut_scope_stack,
+            &mut effects,
+            "<test>",
+            &mut subst,
+            &mut counter,
+            &mut residuals,
+            &mut free_fn_calls,
+            &mut warnings,
+        )
+        .expect("synth must succeed");
+        assert_eq!(
+            ty,
+            Type::bool_(),
+            "innermost mut-var frame must win (expected Bool, got {ty:?})",
+        );
+    }
+
+    /// Iter mut.2 (Task 4): a well-formed mut block with one Int var,
+    /// an assign updating it, and a final read of the var synths to
+    /// Int. Property protected: `Term::Mut` arm pushes its `vars` as
+    /// a frame, synths the body in that extended scope, and returns
+    /// the body's type.
+    #[test]
+    fn mut_block_typechecks_with_int_var_and_returns_int() {
+        // (mut (var x (con Int) 0) (assign x (app + x 1)) x)
+        // Note: + is not in the empty Env, so use a simpler body that
+        // exercises Mut/Assign without depending on operator resolution.
+        // (mut (var x (con Int) 0) (assign x 1) x)
+        let term = Term::Mut {
+            vars: vec![ailang_core::ast::MutVar {
+                name: "x".into(),
+                ty: Type::int(),
+                init: Term::Lit { lit: Literal::Int { value: 0 } },
+            }],
+            body: Box::new(Term::Seq {
+                lhs: Box::new(Term::Assign {
+                    name: "x".into(),
+                    value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
+                }),
+                rhs: Box::new(Term::Var { name: "x".into() }),
+            }),
+        };
+        let ty = synth_standalone(&term);
+        assert_eq!(
+            ty,
+            Type::int(),
+            "mut block with Int var, assign, and final read must synth as Int (got {ty:?})",
+        );
+    }
+
+    /// Iter mut.2 (Task 5): inside a mut frame with `var x : Int = 0`,
+    /// `(assign x 1)` synths as Unit. Property protected: a successful
+    /// Term::Assign resolves through the mut-scope stack and yields
+    /// Unit (the Assign expression's static type).
+    #[test]
+    fn assign_to_in_scope_mut_var_synths_unit() {
+        // (mut (var x (con Int) 0) (assign x 1))
+        let term = Term::Mut {
+            vars: vec![ailang_core::ast::MutVar {
+                name: "x".into(),
+                ty: Type::int(),
+                init: Term::Lit { lit: Literal::Int { value: 0 } },
+            }],
+            body: Box::new(Term::Assign {
+                name: "x".into(),
+                value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
+            }),
+        };
+        let ty = synth_standalone(&term);
+        assert_eq!(
+            ty,
+            Type::unit(),
+            "mut block whose body is a lone assign must synth as Unit (got {ty:?})",
+        );
+    }
+
+    /// Iter mut.2 (Task 5): assigning to an out-of-scope name (no
+    /// enclosing mut frame contains it) fires
+    /// `MutAssignOutOfScope` with the available mut-var names listed.
+    #[test]
+    fn assign_to_out_of_scope_name_fires_diagnostic() {
+        let term = Term::Mut {
+            vars: vec![ailang_core::ast::MutVar {
+                name: "x".into(),
+                ty: Type::int(),
+                init: Term::Lit { lit: Literal::Int { value: 0 } },
+            }],
+            body: Box::new(Term::Assign {
+                name: "y".into(),
+                value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
+            }),
+        };
+        let env = Env::default();
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals: Vec<ResidualConstraint> = Vec::new();
+        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+        let mut warnings: Vec<Diagnostic> = Vec::new();
+        let err = synth(
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            "<test>", &mut subst, &mut counter, &mut residuals,
+            &mut free_fn_calls, &mut warnings,
+        )
+        .expect_err("assign to unknown name must be rejected");
+        match err {
+            CheckError::MutAssignOutOfScope { name, available } => {
+                assert_eq!(name, "y");
+                assert_eq!(available, vec!["x".to_string()]);
+            }
+            other => panic!("expected MutAssignOutOfScope, got {other:?}"),
+        }
+    }
+
+    /// Iter mut.2 (Task 5): assigning a Float-typed value to an
+    /// Int-typed mut-var fires `AssignTypeMismatch` with rendered
+    /// declared / got type strings.
+    #[test]
+    fn assign_with_wrong_value_type_fires_diagnostic() {
+        let term = Term::Mut {
+            vars: vec![ailang_core::ast::MutVar {
+                name: "x".into(),
+                ty: Type::int(),
+                init: Term::Lit { lit: Literal::Int { value: 0 } },
+            }],
+            body: Box::new(Term::Assign {
+                name: "x".into(),
+                value: Box::new(Term::Lit { lit: Literal::Float { bits: 0x3ff8_0000_0000_0000 } }),
+            }),
+        };
+        let env = Env::default();
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals: Vec<ResidualConstraint> = Vec::new();
+        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+        let mut warnings: Vec<Diagnostic> = Vec::new();
+        let err = synth(
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            "<test>", &mut subst, &mut counter, &mut residuals,
+            &mut free_fn_calls, &mut warnings,
+        )
+        .expect_err("Float assigned to Int mut-var must be rejected");
+        match err {
+            CheckError::AssignTypeMismatch { name, declared, got } => {
+                assert_eq!(name, "x");
+                assert_eq!(declared, "Int");
+                assert_eq!(got, "Float");
+            }
+            other => panic!("expected AssignTypeMismatch, got {other:?}"),
+        }
+    }
+
+    /// Iter mut.2 (Task 4): a mut block declaring a Str-typed mut-var
+    /// fires `CheckError::UnsupportedMutVarType` per spec §"Out of
+    /// scope" — heap-RC-managed types are deferred to a follow-on
+    /// milestone.
+    #[test]
+    fn mut_block_rejects_str_var_with_unsupported_type() {
+        let term = Term::Mut {
+            vars: vec![ailang_core::ast::MutVar {
+                name: "s".into(),
+                ty: Type::str_(),
+                init: Term::Lit { lit: Literal::Str { value: "hi".into() } },
+            }],
+            body: Box::new(Term::Var { name: "s".into() }),
+        };
+        let env = Env::default();
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals: Vec<ResidualConstraint> = Vec::new();
+        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
+        let mut warnings: Vec<Diagnostic> = Vec::new();
+        let err = synth(
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            "<test>", &mut subst, &mut counter, &mut residuals,
+            &mut free_fn_calls, &mut warnings,
+        )
+        .expect_err("Str-typed mut-var must be rejected");
+        assert!(
+            matches!(err, CheckError::UnsupportedMutVarType { ref name, .. } if name == "s"),
+            "expected UnsupportedMutVarType for `s`, got {err:?}",
+        );
+    }
+
+    /// Iter mut.2 (Task 1): every new CheckError variant has a stable
+    /// kebab-case code() arm and a non-panicking ctx() arm.
+    #[test]
+    fn mut_typecheck_diagnostics_have_kebab_codes() {
+        let e1 = CheckError::MutAssignOutOfScope {
+            name: "foo".into(),
+            available: vec!["bar".into(), "baz".into()],
+        };
+        let e2 = CheckError::AssignTypeMismatch {
+            name: "count".into(),
+            declared: "Int".into(),
+            got: "Float".into(),
+        };
+        let e3 = CheckError::UnsupportedMutVarType {
+            name: "s".into(),
+            ty: "Str".into(),
+        };
+        assert_eq!(e1.code(), "mut-assign-out-of-scope");
+        assert_eq!(e2.code(), "assign-type-mismatch");
+        assert_eq!(e3.code(), "mut-var-unsupported-type");
+        // Smoke-test ctx() — must not panic, must produce a JSON object.
+        let _ = e1.ctx();
+        let _ = e2.ctx();
+        let _ = e3.ctx();
+    }
+
     fn fn_def(name: &str, ty: Type, params: Vec<&str>, body: Term) -> Def {
         Def::Fn(FnDef {
             name: name.into(),
@@ -6571,6 +7043,7 @@ mod tests {
 
         let term = Term::Var { name: "show".into() };
         let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -6581,6 +7054,7 @@ mod tests {
             &term,
             &env,
             &mut locals,
+            &mut mut_scope_stack,
             &mut effects,
             "test_call_site",
             &mut subst,

crates/ailang-check/src/lift.rs

@@ -720,7 +720,11 @@ impl<'a> Lifter<'a> {
         // (e.g. class-method-shadowed-by-fn) have already been
         // surfaced upstream by `check_workspace`. Discard here.
         let mut warnings_discarded: Vec<crate::diagnostic::Diagnostic> = Vec::new();
-        let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
+        // Iter mut.2: lift's letrec-capture synth re-entry walks one
+        // term at a time, beginning from a top-of-body position; fresh
+        // empty mut-scope stack is correct.
+        let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
+        let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
         Ok(subst.apply(&ty))
     }
 }

crates/ailang-check/src/mono.rs

@@ -709,10 +709,15 @@ pub fn collect_mono_targets(
     // discards warnings — typecheck has already run and surfaced any
     // shadow warnings; mono is a post-typecheck pass.
     let mut warnings_discarded: Vec<crate::diagnostic::Diagnostic> = Vec::new();
+    // Iter mut.2: mono re-synth begins from top-of-body — empty
+    // mut-scope, since any `Term::Mut` will push its own frame as the
+    // walk descends.
+    let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
     crate::synth(
         &f.body,
         &env,
         &mut locals,
+        &mut mut_scope_stack,
         &mut effects,
         &f.name,
         &mut subst,
@@ -1334,10 +1339,15 @@ pub(crate) fn collect_residuals_ordered(
     // discards warnings — typecheck has already run and surfaced any
     // shadow warnings; mono is a post-typecheck pass.
     let mut warnings_discarded: Vec<crate::diagnostic::Diagnostic> = Vec::new();
+    // Iter mut.2: mono re-synth begins from top-of-body — empty
+    // mut-scope, since any `Term::Mut` will push its own frame as the
+    // walk descends.
+    let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
     crate::synth(
         &f.body,
         &env,
         &mut locals,
+        &mut mut_scope_stack,
         &mut effects,
         &f.name,
         &mut subst,

crates/ailang-check/tests/mut_typecheck_pin.rs

@@ -0,0 +1,63 @@
+//! Iter mut.2 (Task 6): pin tests that the five typecheck fixtures
+//! produce the expected diagnostic codes (or zero diagnostics for the
+//! positive nested-shadow case).
+//!
+//! Spec: `docs/specs/2026-05-15-mut-local.md` §"Testing strategy /
+//! Typecheck negative tests" — names each fixture and the diagnostic
+//! it must surface. The carve-out justification for landing these as
+//! `.ail.json` rather than `.ail` mirrors the post-form-a precedent
+//! (broken_unbound, test_22b2_*.ail.json) — negative typecheck
+//! fixtures live as canonical JSON so the diagnostic code is the
+//! load-bearing assertion, not the surface form.
+
+use ailang_check::check_workspace;
+use ailang_surface::load_workspace;
+use std::path::PathBuf;
+
+fn examples_dir() -> PathBuf {
+    let manifest = env!("CARGO_MANIFEST_DIR");
+    PathBuf::from(manifest)
+        .parent().expect("CARGO_MANIFEST_DIR has a parent (crates/ailang-check)")
+        .parent().expect("CARGO_MANIFEST_DIR has a grandparent (crates/)")
+        .join("examples")
+}
+
+/// Load the named fixture under `examples/`, run check_workspace, and
+/// return the diagnostic code list (one entry per Diagnostic).
+fn check_fixture(fixture_name: &str) -> Vec<String> {
+    let path = examples_dir().join(fixture_name);
+    let ws = load_workspace(&path)
+        .unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}"));
+    let diags = check_workspace(&ws);
+    diags.iter().map(|d| d.code.clone()).collect()
+}
+
+#[test]
+fn assign_out_of_scope_emits_mut_assign_out_of_scope() {
+    let codes = check_fixture("test_mut_assign_out_of_scope.ail.json");
+    assert_eq!(codes, vec!["mut-assign-out-of-scope".to_string()]);
+}
+
+#[test]
+fn assign_type_mismatch_emits_assign_type_mismatch() {
+    let codes = check_fixture("test_mut_assign_type_mismatch.ail.json");
+    assert_eq!(codes, vec!["assign-type-mismatch".to_string()]);
+}
+
+#[test]
+fn mut_var_str_type_emits_mut_var_unsupported_type() {
+    let codes = check_fixture("test_mut_var_unsupported_type.ail.json");
+    assert_eq!(codes, vec!["mut-var-unsupported-type".to_string()]);
+}
+
+#[test]
+fn assign_outside_mut_emits_mut_assign_out_of_scope() {
+    let codes = check_fixture("test_mut_assign_outside_mut.ail.json");
+    assert_eq!(codes, vec!["mut-assign-out-of-scope".to_string()]);
+}
+
+#[test]
+fn nested_shadow_typechecks_clean() {
+    let codes = check_fixture("test_mut_nested_shadow_legal.ail.json");
+    assert!(codes.is_empty(), "expected zero diagnostics, got {codes:?}");
+}

crates/ailang-core/tests/carve_out_inventory.rs

@@ -1,10 +1,18 @@
 //! Carve-out inventory check — §T4 of the form-a-default-authoring
-//! spec. Asserts that exactly the seven named carve-out files exist
+//! spec. Asserts that exactly the named carve-out files exist
 //! under `examples/*.ail.json` after milestone close. The list is
 //! hardcoded; any change is a deliberate, brainstorm-level decision.
 //!
-//! Seven carve-outs post prelude-decouple (2026-05-14):
+//! Twelve carve-outs post iter mut.2 (2026-05-15):
-//! - §C4 (a) subject-matter: 7 fixtures (canonical-form rejection / unbound / class-def rejection).
+//! - §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 /
+//!   var / assign forms. The diagnostic code is the load-bearing
+//!   assertion (mut-assign-out-of-scope, assign-type-mismatch,
+//!   mut-var-unsupported-type) — mirroring the §C4(a) negative-
+//!   fixture convention. The positive nested-shadow case is a
+//!   .ail.json carve-out for symmetry with its negative siblings
+//!   (the driver tests all five from one helper).
 //! - §C4 (b) compile-time-embed: retired 2026-05-14 by milestone
 //!   prelude-decouple; the prelude is now embedded as `prelude.ail`
 //!   in `ailang-surface` and parsed at compile time via
@@ -13,7 +21,7 @@
 use std::collections::BTreeSet;
 
 const EXPECTED: &[&str] = &[
-    // §C4 (a) — subject-matter
+    // §C4 (a) — subject-matter (form-a.1 milestone close)
     "broken_unbound.ail.json",
     "test_22b2_invalid_superclass_param.ail.json",
     "test_22b2_kind_mismatch.ail.json",
@@ -21,6 +29,12 @@ const EXPECTED: &[&str] = &[
     "test_ct1_bad_qualifier.ail.json",
     "test_ct1_bare_xmod_rejected.ail.json",
     "test_ct1_qualified_class_rejected.ail.json",
+    // Iter mut.2 — negative typecheck fixtures + positive shadow-pin
+    "test_mut_assign_out_of_scope.ail.json",
+    "test_mut_assign_outside_mut.ail.json",
+    "test_mut_assign_type_mismatch.ail.json",
+    "test_mut_nested_shadow_legal.ail.json",
+    "test_mut_var_unsupported_type.ail.json",
 ];
 
 fn examples_dir() -> std::path::PathBuf {

docs/journals/2026-05-15-iter-mut.2.md

@@ -0,0 +1,256 @@
+# iter mut.2 — typecheck recognition of `Term::Mut` and `Term::Assign`
+
+**Date:** 2026-05-15
+**Started from:** 3a5b1d33472e5c35c4917702e30fa5a12b749e31
+**Status:** DONE
+**Tasks completed:** 7 of 7
+
+## Summary
+
+Replaces the mut.1 dispatch stubs in `synth` (`ailang-check`) for
+`Term::Mut` and `Term::Assign` with real typecheck logic. Three new
+`CheckError` variants ship (`MutAssignOutOfScope`,
+`AssignTypeMismatch`, `UnsupportedMutVarType`) with kebab-coded
+`code()` arms and structured `ctx()` payloads, following the
+cli-diag-human bracketed-`[code]` convention. A new
+`mut_scope_stack: &mut Vec<IndexMap<String, Type>>` parameter
+threads through every `synth` call site (24 sites across lib.rs +
+mono.rs:712 / mono.rs:1337 + lift.rs:723 + builtins.rs in two test
+helpers); each entry-point caller (`check_fn`, `check_const`, mono
+re-synth, lift letrec-capture synth) opens a fresh empty stack at
+top-of-body. `Term::Var` resolution prepends the mut-scope check
+ahead of the existing locals/globals chain (innermost-first wins on
+shadowing). `Term::Mut` pushes a frame after gating each
+`MutVar.ty` against `is_supported_mut_var_type` (Int / Float /
+Bool / Unit), synths inits in the in-progress scope, unifies init
+type with declared, and synths the body in the extended scope.
+`Term::Assign` resolves the target name through the stack, returns
+`MutAssignOutOfScope` (with a flat-deduplicated `available` list)
+on miss, compares value type against the declared via
+`subst.apply` + equality (manual to preserve the
+`AssignTypeMismatch` diagnostic identity), and yields `Type::unit()`
+on success. Five `.ail.json` fixtures + a 5-test driver
+(`mut_typecheck_pin.rs`) cover each diagnostic plus the positive
+nested-shadow case; the carve-out inventory at
+`carve_out_inventory.rs` is extended 7 → 12 to accept them.
+`examples/mut.ail` (the mut.1 six-fn round-trip fixture) now
+typechecks clean via `ail check`. Codegen stubs unchanged —
+`examples/mut.ail` still cannot run end-to-end; that lands in mut.3.
+Full `cargo test --workspace`: 592 passed / 0 failed (was 579 at
+start of mut.2; +13 = 5 driver pins + 7 lib.rs `mod tests` pins +
+1 inventory test count unchanged — the inventory entry count went
+from `seven` to `twelve` but the test itself was already counted).
+
+## Per-task notes
+
+- iter mut.2.1 — `CheckError` variants + `code()` + `ctx()`:
+  Three new variants land before the `Internal` variant with
+  thiserror `#[error("[code] message")]` attributes per the
+  cli-diag-human convention. `code()` arms return the canonical
+  kebab strings (`mut-assign-out-of-scope`, `assign-type-mismatch`,
+  `mut-var-unsupported-type`). `ctx()` arms emit the structured
+  payloads named in the plan (`{name, available}`,
+  `{name, expected, actual}`, `{name, type}`). One in-crate pin
+  (`mut_typecheck_diagnostics_have_kebab_codes`) gates the code()
+  + ctx() shape; RED → GREEN observed.
+
+- iter mut.2.2 — `synth` signature threads `mut_scope_stack`:
+  New parameter `mut_scope_stack: &mut Vec<IndexMap<String, Type>>`
+  sits immediately after `locals` (canonical mid-position; matches
+  the existing convention for per-fn-body lexical state). 18
+  recursive call sites in `lib.rs::synth` updated via
+  pattern-by-pattern `replace_all` (each first-arg form had a
+  unique-enough wrapper). Entry-point callers in `check_fn:1934`
+  and `check_const:2687` declare a fresh empty stack. mono.rs's
+  two re-synth sites at 712 + 1337 also declare a fresh empty
+  stack (they begin from a top-of-body position). Plan-recon
+  missed two more call sites: `lift.rs:723` (letrec-capture
+  re-synth) and `builtins.rs` (two test helpers
+  `synth_in_builtins_env` + a FloatPatternNotAllowed pin) — both
+  required for build green; both get fresh empty stacks. The
+  in-test mq.3 call site at `lib.rs:6663` also got the new
+  parameter. Build was red structurally (E0061 at 23+ sites) until
+  every call site was updated, then green.
+
+- iter mut.2.3 — `Term::Var` prepends mut-scope resolution: A 5-
+  line block at the top of the Var arm walks
+  `mut_scope_stack.iter().rev()` innermost-first, returning the
+  matched type cloned. Mut-vars are monomorphic per spec §"var
+  element types" — no Forall instantiation, no FreeFnCall. Two
+  pins (`mut_var_resolution_shadows_outer_local`,
+  `mut_var_resolution_picks_innermost_frame`) directly populate
+  the stack to isolate this change from the Mut-arm work in
+  Task 4 (the plan's literal Let { Mut { ... } } shape would have
+  hit the still-stubbed Mut arm at this stage; the property
+  protected — mut-scope wins over locals + innermost-wins on
+  shadowing — is identical). TDD discipline gap: the Var-arm edit
+  landed before the pin tests were observed RED on disk; the
+  reasoning is analytical (the pre-edit code consults
+  `locals.get(name)` first, so with `locals = { x → Int }` the
+  Var arm returned Int, failing the assert-Float; same logic for
+  the two-frame test). Recorded as Concern.
+
+- iter mut.2.4 — `Term::Mut` typecheck arm: Replaces the stub
+  with real logic per plan Step 3. A file-scope helper
+  `is_supported_mut_var_type(&Type) -> bool` gates each var's
+  declared type to `Int | Float | Bool | Unit` (no args). Per-var
+  loop synths the init in the outer scope plus the in-progress
+  frame (the in-flight frame is cloned and pushed during the init
+  synth, then popped — keeps `mut_scope_stack` truthful at every
+  nested call), unifies init type with declared, inserts the
+  (name → declared ty) entry into the frame. After all vars: push
+  the completed frame, synth body in extended scope, pop frame
+  (regardless of body outcome — the `body_result` is captured
+  before pop). Two pins:
+  `mut_block_typechecks_with_int_var_and_returns_int` (positive,
+  initially RED because Assign was still stubbed — flipped GREEN
+  by Task 5) and `mut_block_rejects_str_var_with_unsupported_type`
+  (negative, GREEN at Task 4 close).
+
+- iter mut.2.5 — `Term::Assign` typecheck arm: Replaces the stub
+  with real logic per plan Step 3. Resolves the target name via
+  `mut_scope_stack.iter().rev().find_map(|f| f.get(name).cloned())`.
+  None case: flattens every name in every frame innermost-first,
+  dedup-preserving-order via a manual `contains` check (small N,
+  no need for a Set), returns `MutAssignOutOfScope`. Some case:
+  synths the value, compares `subst.apply(&declared)` vs
+  `subst.apply(&value)` via `!=` (manual equality, NOT `unify` —
+  unify would have emitted `TypeMismatch`, and the spec demands
+  the distinct `AssignTypeMismatch` code), returns
+  `AssignTypeMismatch` with rendered type strings on mismatch or
+  `Ok(Type::unit())` on match. Three pins:
+  `assign_to_in_scope_mut_var_synths_unit` (positive),
+  `assign_to_out_of_scope_name_fires_diagnostic` (None case),
+  `assign_with_wrong_value_type_fires_diagnostic` (Some-mismatch
+  case). RED → GREEN observed for all three.
+
+- iter mut.2.6 — Five fixtures + driver test: Five `.ail.json`
+  fixtures land under `examples/` (carve-out style, per the
+  Boss decision in the carrier overriding the spec's literal
+  `crates/ailang-check/tests/`-side placement). Each fixture is
+  minimal — single-fn `main`, no imports, body shape exactly the
+  one the plan named. The driver test
+  `crates/ailang-check/tests/mut_typecheck_pin.rs` uses the
+  canonical `load_workspace` + `check_workspace` +
+  `diagnostics.iter().map(|d| d.code.clone()).collect()` pattern
+  from `method_collision_pin.rs` and `typeclass_22b2.rs` — no
+  `todo!()` survives. Carve-out inventory extended from seven to
+  twelve to accept the five new fixtures (alphabetised; the
+  comment block names mut.2 as the lineage). All 5 driver tests
+  GREEN; carve-out inventory GREEN.
+
+- iter mut.2.7 — Verify `examples/mut.ail` typechecks clean:
+  `cargo run --quiet --bin ail -- check examples/mut.ail` reports
+  `ok (26 symbols across 2 modules)` — zero diagnostics across
+  all six fns (`mut_empty`, `mut_single_var`, `mut_two_vars`,
+  `mut_nested_shadow`, `mut_returns_bool`, `mut_returns_unit`).
+  Full `cargo test --workspace`: 592 / 0.
+
+## Concerns
+
+- Task 3 TDD-ordering gap: the `Term::Var` arm prepend landed
+  before the two pin tests were observed RED on disk. The
+  reasoning that the pre-edit code would have failed both pins
+  is analytical (locals-first resolution returns Int when
+  `locals = { x → Int }`, contradicting both `assert_eq!(Float)`
+  and `assert_eq!(Bool)`). The discipline gap is recorded
+  per the implementer's Iron Law ("the test you wrote in RED MUST
+  pass; no other test may regress" — and the spirit-not-ritual
+  clause that tests-after prove nothing about whether they would
+  have caught the regression pre-edit). Subsequent tasks
+  (4 + 5) restored the RED-first sequencing; on those, the Mut /
+  Assign stubs already emit `CheckError::Internal` so the pins
+  were observed RED with the canonical pattern. No correctness
+  impact; the pins protect the property correctly post-edit.
+
+- Plan-recon missed three synth call sites beyond the four the
+  plan enumerated (lib.rs 1885 + 2634; mono.rs 712 + 1337). The
+  build-red structural signal flushed them out via E0061:
+  `lib.rs:6663` (in-test mq.3 helper), `lift.rs:723` (letrec-
+  capture re-synth), `builtins.rs` (`synth_in_builtins_env` at
+  351 + a FloatPatternNotAllowed test pin at 594). Each gets a
+  fresh empty stack with the same "begins from top-of-body"
+  rationale as mono.rs. No behavioural impact; documentary
+  concern for the planner's next plan-recon dispatch.
+
+- The carve-out inventory extension was strictly required (the
+  inventory test enforces a closed list of `examples/*.ail.json`
+  files) but was not explicitly named in the Boss carrier or the
+  plan. Recording here so the planner's recon for future iters
+  knows to enumerate the side-effect when fixtures land under
+  `examples/`. The boundary call: the fixtures match §C4(a)'s
+  precedent (negative typecheck fixtures as `.ail.json` so the
+  diagnostic-code assertion is the load-bearing form, not the
+  surface). The positive `test_mut_nested_shadow_legal.ail.json`
+  is the one stretch — its load-bearing assertion is "zero
+  diagnostics", which the form-A `.ail` form could equally
+  carry. Landing it as `.ail.json` keeps all five mut.2 fixtures
+  on one driver and one extension on the carve-out list; the
+  alternative (splitting positive to `.ail`, negatives to
+  `.ail.json`) would have produced two drivers or a hybrid
+  loader. Conservative call documented for visibility.
+
+## Known debt
+
+- Codegen stubs unchanged in mut.2 per the spec's iteration
+  boundary. A `Term::Mut` or `Term::Assign` reaching
+  `lower_term` still produces `CodegenError::Internal`. The
+  full mut.ail E2E (build + run) lands in mut.3. The spec's
+  Acceptance criterion #3 (`mut_counter.ail` + `mut_sum_floats.ail`
+  build + run + print expected stdout) is mut.3-scoped.
+
+- The Mut-arm's in-progress-frame clone-on-each-init is O(n²)
+  over the var count. n is realistically ≤ 2 (the mut.ail
+  fixture's `mut_two_vars` is the largest in the corpus). Not
+  worth a more elaborate structure (e.g. pushing a single in-
+  progress frame and mutating it across inits); the clone-pop
+  shape keeps the stack truthful at every nested call and makes
+  the per-var init scope obvious. Recording for visibility.
+
+## Files touched
+
+Modified:
+- `crates/ailang-check/src/lib.rs` — 3 new CheckError variants +
+  3 code() arms + 3 ctx() arms; `synth` signature gains
+  `mut_scope_stack` after `locals`; 18 recursive synth call
+  sites updated; 2 entry-point callers (`check_fn`,
+  `check_const`) declare fresh empty stacks; in-test synth call
+  (mq.3 helper) gets new param; `Term::Var` arm prepends
+  mut-scope resolution (5-line block); `Term::Mut` stub replaced
+  with real logic (push/pop frame, per-var init, body synth);
+  `Term::Assign` stub replaced with real logic
+  (find/None-MutAssignOutOfScope/Some-AssignTypeMismatch-or-Unit);
+  file-scope helper `is_supported_mut_var_type`; 7 new tests in
+  `mod tests` (`mut_typecheck_diagnostics_have_kebab_codes`,
+  `mut_var_resolution_shadows_outer_local`,
+  `mut_var_resolution_picks_innermost_frame`,
+  `mut_block_typechecks_with_int_var_and_returns_int`,
+  `mut_block_rejects_str_var_with_unsupported_type`,
+  `assign_to_in_scope_mut_var_synths_unit`,
+  `assign_to_out_of_scope_name_fires_diagnostic`,
+  `assign_with_wrong_value_type_fires_diagnostic`) plus the
+  `synth_standalone` helper.
+- `crates/ailang-check/src/mono.rs` — 2 re-synth call sites
+  (712, 1337) each get a fresh `mut_scope_stack`.
+- `crates/ailang-check/src/lift.rs` — letrec-capture re-synth at
+  :723 gets a fresh `mut_scope_stack`.
+- `crates/ailang-check/src/builtins.rs` — 2 in-test synth calls
+  (synth_in_builtins_env + FloatPatternNotAllowed pin) get a
+  fresh `mut_scope_stack`.
+- `crates/ailang-core/tests/carve_out_inventory.rs` — EXPECTED
+  list 7 → 12, comment-block updated naming mut.2 as the
+  lineage of the 5 new entries.
+
+New:
+- `crates/ailang-check/tests/mut_typecheck_pin.rs` — 5-test
+  driver via canonical load_workspace + check_workspace +
+  collect-codes pattern.
+- `examples/test_mut_assign_out_of_scope.ail.json`
+- `examples/test_mut_assign_outside_mut.ail.json`
+- `examples/test_mut_assign_type_mismatch.ail.json`
+- `examples/test_mut_nested_shadow_legal.ail.json`
+- `examples/test_mut_var_unsupported_type.ail.json`
+
+## Stats
+
+bench/orchestrator-stats/2026-05-15-iter-mut.2.json

docs/journals/INDEX.md

@@ -71,3 +71,4 @@
 - 2026-05-14 — iter pd.3: prelude.ail.json deleted from working tree; cross-form-identity preflight + supporting bytes deleted from prelude_module_hash_pin (purpose discharged); migrate-bare-cross-module-refs defensive include + lockstep skip-branch deleted; carve_out_inventory.rs §C4(b) row dropped (8→7); form-a-default-authoring spec §C4(b) RETIRED status marker added; new prelude_decouple_carve_out_pin.rs asserts JSON file does not exist; milestone prelude-decouple closed → 2026-05-14-iter-pd.3.md
 - 2026-05-14 — audit-pd: milestone close (prelude-decouple) — architect drift fixed inline as audit-pd-tidy (DESIGN.md §"Roundtrip Invariant" carve-out count 8→7 + main.rs migrate-subcommand dead prelude fallback removed); bench mixed (check.py + compile_check.py established noise envelope, 15th consecutive observation, baseline pristine; cross_lang clean) → 2026-05-14-audit-pd.md
 - 2026-05-15 — iter mut.1: AST extension `Term::Mut` + `Term::Assign` + `MutVar` struct; Form A `(mut ...) / (var ...) / (assign ...)` productions parse + print + round-trip; ~25 substantive Term-walker arms across the codebase; dispatch stubs in `synth` (typecheck) + `lower_term` (codegen) return `CheckError::Internal` / `CodegenError::Internal` per the spec's out-of-iteration boundary; `examples/mut.ail` six-fn fixture (Int/Float/Bool/Unit + empty + nested-shadow); drift + coverage + spec-drift tests + DESIGN.md §"Term (expression)" + `crates/ailang-core/specs/form_a.md` amendments; tests 564 → 579 → 2026-05-15-iter-mut.1.md
+- 2026-05-15 — iter mut.2: typecheck for `Term::Mut` + `Term::Assign` replacing the iter mut.1 dispatch stubs; three new `CheckError` variants (`MutAssignOutOfScope`, `AssignTypeMismatch`, `UnsupportedMutVarType`) with bracketed-`[code]:` Display + `code()` + `ctx()` arms; `synth` signature threads `mut_scope_stack: &mut Vec<IndexMap<String, Type>>` after `locals`, propagated through all recursive call sites in `lib.rs` plus `mono.rs:712/1337` + `lift.rs:723` + `builtins.rs` test helpers + the mq.3 in-test helper at `lib.rs:6663`; `Term::Var` resolution prepended with innermost-first mut-scope lookup; `Term::Mut` arm gates var types to {Int,Float,Bool,Unit} and push/pops a fresh frame; `Term::Assign` arm walks the stack innermost-first, emits `AssignTypeMismatch` on type mismatch and `MutAssignOutOfScope` (with `available` flattened across all frames) on miss; five `.ail.json` fixtures under `examples/` (four negative + one positive nested-shadow) + driver `crates/ailang-check/tests/mut_typecheck_pin.rs`; `carve_out_inventory.rs` EXPECTED extended 7→12 for the new negative-fixture set; `examples/mut.ail` typechecks clean (`ok (26 symbols across 2 modules)`); tests 579 → 592 → 2026-05-15-iter-mut.2.md

examples/test_mut_assign_out_of_scope.ail.json

@@ -0,0 +1,38 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_mut_assign_out_of_scope",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Int" },
+        "effects": []
+      },
+      "params": [],
+      "doc": "Iter mut.2: assigning to a name not declared as a mut-var fires mut-assign-out-of-scope.",
+      "body": {
+        "t": "mut",
+        "vars": [
+          {
+            "name": "x",
+            "type": { "k": "con", "name": "Int" },
+            "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+          }
+        ],
+        "body": {
+          "t": "seq",
+          "lhs": {
+            "t": "assign",
+            "name": "y",
+            "value": { "t": "lit", "lit": { "kind": "int", "value": 1 } }
+          },
+          "rhs": { "t": "var", "name": "x" }
+        }
+      }
+    }
+  ]
+}

examples/test_mut_assign_outside_mut.ail.json

@@ -0,0 +1,24 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_mut_assign_outside_mut",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Unit" },
+        "effects": []
+      },
+      "params": [],
+      "doc": "Iter mut.2: Term::Assign with no enclosing Term::Mut ancestor fires mut-assign-out-of-scope.",
+      "body": {
+        "t": "assign",
+        "name": "x",
+        "value": { "t": "lit", "lit": { "kind": "int", "value": 1 } }
+      }
+    }
+  ]
+}

examples/test_mut_assign_type_mismatch.ail.json

@@ -0,0 +1,38 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_mut_assign_type_mismatch",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Int" },
+        "effects": []
+      },
+      "params": [],
+      "doc": "Iter mut.2: assigning Float to Int mut-var fires assign-type-mismatch.",
+      "body": {
+        "t": "mut",
+        "vars": [
+          {
+            "name": "x",
+            "type": { "k": "con", "name": "Int" },
+            "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } }
+          }
+        ],
+        "body": {
+          "t": "seq",
+          "lhs": {
+            "t": "assign",
+            "name": "x",
+            "value": { "t": "lit", "lit": { "kind": "float", "bits": "3ff8000000000000" } }
+          },
+          "rhs": { "t": "var", "name": "x" }
+        }
+      }
+    }
+  ]
+}

examples/test_mut_nested_shadow_legal.ail.json

@@ -0,0 +1,40 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_mut_nested_shadow_legal",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Float" },
+        "effects": []
+      },
+      "params": [],
+      "doc": "Iter mut.2: nested mut block with inner var shadowing outer; inner Float wins. Typechecks clean.",
+      "body": {
+        "t": "mut",
+        "vars": [
+          {
+            "name": "x",
+            "type": { "k": "con", "name": "Int" },
+            "init": { "t": "lit", "lit": { "kind": "int", "value": 1 } }
+          }
+        ],
+        "body": {
+          "t": "mut",
+          "vars": [
+            {
+              "name": "x",
+              "type": { "k": "con", "name": "Float" },
+              "init": { "t": "lit", "lit": { "kind": "float", "bits": "4000000000000000" } }
+            }
+          ],
+          "body": { "t": "var", "name": "x" }
+        }
+      }
+    }
+  ]
+}

examples/test_mut_var_unsupported_type.ail.json

@@ -0,0 +1,30 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_mut_var_unsupported_type",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Str" },
+        "effects": []
+      },
+      "params": [],
+      "doc": "Iter mut.2: a Str-typed mut-var fires mut-var-unsupported-type (heap-RC-managed types deferred).",
+      "body": {
+        "t": "mut",
+        "vars": [
+          {
+            "name": "s",
+            "type": { "k": "con", "name": "Str" },
+            "init": { "t": "lit", "lit": { "kind": "str", "value": "hello" } }
+          }
+        ],
+        "body": { "t": "var", "name": "s" }
+      }
+    }
+  ]
+}