AILang/docs/plans/0068-iter-mut.2.md

# mut.2 — typecheck — Implementation Plan

> **Parent spec:** `docs/specs/0029-mut-local.md`
>
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
> to run this plan. Steps use `- [ ]` checkboxes for tracking.

**Goal:** Replace the iter mut.1 dispatch stubs for `Term::Mut` and
`Term::Assign` in `synth` with real typecheck logic. Add three new
`CheckError` variants (`MutAssignOutOfScope`, `AssignTypeMismatch`,
`UnsupportedMutVarType`) and their `code()` + `ctx()` arms. Introduce
a `mut_scope_stack: &mut Vec<IndexMap<String, Type>>` parameter on
`synth`, thread it through all call sites (recursive inside `lib.rs`
plus the two re-synth sites in `mono.rs`), prepend it to the
`Term::Var` resolution chain. Ship five fixtures under `examples/`
plus one Rust driver under `crates/ailang-check/tests/` to gate the
behaviour. Codegen stays untouched — `examples/mut.ail` still does
not run, but it now typechecks cleanly.

**Architecture:** The natural locality for mut-scope state is a
`synth`-parameter slot (matching the existing `locals` / `effects` /
`subst` / `counter` / `residuals` / `free_fn_calls` / `warnings`
threading pattern), NOT an `Env` field. The stack is per-walk
(reset on every fn body) and lexically scoped (push on
`Term::Mut`-entry, pop on `Term::Mut`-exit); both properties argue
against an `Env` field. Each frame is an `IndexMap<String, Type>` so
declaration order is preserved (relevant for the `available` list in
`MutAssignOutOfScope`). The `Term::Var` resolution order becomes:
mut-scope (innermost-first) → existing chain (locals → params →
top-level defs → builtins → class-methods). Innermost-wins on
shadowing falls out for free.

**Tech Stack:** `ailang-check` only. No `ailang-core`, `ailang-surface`,
`ailang-codegen`, `ailang-prose`, or `ail` changes.

---

**Files this plan creates or modifies:**

- Create: `examples/test_mut_assign_out_of_scope.ail.json` — `assign` to a name not declared as a mut-var of any enclosing `Term::Mut`.
- Create: `examples/test_mut_assign_type_mismatch.ail.json` — `(assign x 1.0)` against `(var x (con Int) 0)`.
- Create: `examples/test_mut_var_unsupported_type.ail.json` — `(var s (con Str) "...")` — the deferred-type case.
- Create: `examples/test_mut_assign_outside_mut.ail.json` — `Term::Assign` directly in a fn body with no `Term::Mut` ancestor.
- Create: `examples/test_mut_nested_shadow_legal.ail.json` — positive: outer `var x : Int` shadowed by inner `var x : Float` in nested mut.
- Create: `crates/ailang-check/tests/mut_typecheck_pin.rs` — driver test loading each fixture and asserting expected diagnostic code (or empty for the positive case).
- Modify: `crates/ailang-check/src/lib.rs:384-746` — add three `CheckError` variants + `code()` arms + `ctx()` arms.
- Modify: `crates/ailang-check/src/lib.rs:2647-2662` — `synth` signature: add `mut_scope_stack: &mut Vec<indexmap::IndexMap<String, Type>>`.
- Modify: `crates/ailang-check/src/lib.rs:1885, 2634` — top-of-walk synth entry points (`check_fn` and `check_const` — find exact names by looking for synth-callers in lib.rs that do NOT recurse from synth itself).
- Modify: `crates/ailang-check/src/lib.rs:2671-2941` — prepend mut-scope resolution to `Term::Var` arm.
- Modify: `crates/ailang-check/src/lib.rs:3488-3497` — replace `Term::Mut` and `Term::Assign` `Internal` stubs with real logic.
- Modify: `crates/ailang-check/src/lib.rs:~19 internal synth() calls` — thread new param through every recursive site.
- Modify: `crates/ailang-check/src/mono.rs:712, 1337` — thread new param through both `crate::synth(...)` call sites.

---

## Task 1 — `CheckError` variants + `code()` + `ctx()`

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:384-746`

- [ ] **Step 1: Write the failing pin test**

Add to `crates/ailang-check/src/lib.rs` `#[cfg(test)] mod tests` block:

```rust
#[test]
fn mut_typecheck_diagnostics_have_kebab_codes() {
    use indexmap::IndexMap;
    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");
    let _ = (e1.ctx(), e2.ctx(), e3.ctx()); // smoke-test ctx() doesn't panic
}
```

- [ ] **Step 2: Run to verify red**

Run: `cargo test --workspace -p ailang-check mut_typecheck_diagnostics_have_kebab_codes`
Expected: FAIL — `CheckError` has no `MutAssignOutOfScope` / `AssignTypeMismatch` / `UnsupportedMutVarType` variants.

- [ ] **Step 3: Add the three variants**

In the `CheckError` enum body (around `crates/ailang-check/src/lib.rs:384-639`),
immediately before the `Internal` variant at line 638, insert:

```rust
    /// 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), so the diagnostic can surface "you might have meant
    /// one of: X / Y / Z".
    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.
    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/0029-mut-local.md` §"Out of scope".
    UnsupportedMutVarType {
        name: String,
        ty: String,
    },
```

- [ ] **Step 4: Add `code()` arms**

In the `impl CheckError { pub fn code(&self) -> &'static str { match self { ... } } }`
block (around line 648), add three new arms before the `Internal` arm:

```rust
            CheckError::MutAssignOutOfScope { .. } => "mut-assign-out-of-scope",
            CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch",
            CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type",
```

- [ ] **Step 5: Add `ctx()` arms**

In the `impl CheckError { pub fn ctx(&self) -> serde_json::Value { match self { ... } } }`
block (around line 688), add three new arms before the `Internal` arm.
Each emits a structured JSON payload consistent with sibling
diagnostics:

```rust
            CheckError::MutAssignOutOfScope { name, available } => json!({
                "name": name,
                "available": available,
            }),
            CheckError::AssignTypeMismatch { name, declared, got } => json!({
                "name": name,
                "expected": declared,
                "actual": got,
            }),
            CheckError::UnsupportedMutVarType { name, ty } => json!({
                "name": name,
                "type": ty,
            }),
```

- [ ] **Step 6: Add `Display`-style message for each variant**

The existing `CheckError` derives `thiserror::Error` and the variants
carry `#[error("...")]` attributes — verify by reading 1-2 existing
variants for the exact attribute shape, then add:

```rust
    #[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> },

    #[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 },

    #[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 },
```

The bracketed-`[code]:` prefix is consistent with the cli-diag-human
iter convention (2026-05-14).

- [ ] **Step 7: Run to verify green**

Run: `cargo test --workspace -p ailang-check mut_typecheck_diagnostics_have_kebab_codes`
Expected: PASS.

Run: `cargo build --workspace 2>&1 | tail -10`
Expected: green (no other consumers of `CheckError` are broken because
adding variants is additive and we have not introduced consumers yet).

---

## Task 2 — `synth` signature: thread `mut_scope_stack`

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:2647-2662` — signature.
- Modify: `crates/ailang-check/src/lib.rs` — ~19 internal recursive call sites.
- Modify: `crates/ailang-check/src/lib.rs:1885, 2634` — entry-point callers.
- Modify: `crates/ailang-check/src/mono.rs:712, 1337` — re-synth call sites.

The new parameter is `mut_scope_stack: &mut Vec<indexmap::IndexMap<String, Type>>`.
Position: immediately after `locals` (canonical mid-position; matches
the existing convention of locals-adjacent scope state).

- [ ] **Step 1: Extend `synth` signature**

In `crates/ailang-check/src/lib.rs:2647`, change:

```rust
pub(crate) fn synth(
    term: &Term,
    locals: &IndexMap<String, Type>,
    // ... existing params ...
) -> Result<(Type, ...), CheckError> {
```

to:

```rust
pub(crate) fn synth(
    term: &Term,
    locals: &IndexMap<String, Type>,
    mut_scope_stack: &mut Vec<indexmap::IndexMap<String, Type>>,
    // ... existing params ...
) -> Result<(Type, ...), CheckError> {
```

(The exact return shape and the other params are whatever the
function already has — preserve them verbatim and only add the new
slot.)

- [ ] **Step 2: Run to verify the parameter is exposed**

Run: `cargo build --workspace -p ailang-check 2>&1 | head -10`
Expected: many `error[E0061]: this function takes N arguments but ...`
errors at every `synth(...)` call site. This is the structural red
signal.

- [ ] **Step 3: Update entry-point callers in `lib.rs`**

Locate the two top-of-walk entry points around lines 1885 and 2634
(grep for `synth(` calls that are NOT inside `pub(crate) fn synth`
itself). Each entry-point caller passes a fresh empty stack:

```rust
let mut mut_scope_stack: Vec<indexmap::IndexMap<String, Type>> = Vec::new();
let result = synth(term, &locals, &mut mut_scope_stack, /* existing args */)?;
```

The stack is dropped at the end of the entry point; it is per-fn-body.

- [ ] **Step 4: Update all recursive `synth(...)` call sites in `lib.rs`**

Per the recon, the recursive call sites are at lines 3016, 3052,
3061, 3063, 3075, 3077, 3078, 3096, 3191, 3200, 3218, 3293, 3295,
3304, 3392, 3419, 3435, 3477 (and possibly some lift / mono call
sites; the build errors enumerate them). Each becomes:

```rust
synth(<term>, locals, mut_scope_stack, /* existing args */)
```

The implementer should grep for `synth(` in `lib.rs` after Step 3 and
update every remaining call site.

- [ ] **Step 5: Update `mono.rs` re-synth call sites**

Two sites: `crates/ailang-check/src/mono.rs:712` and `:1337`. Both
invoke `crate::synth(...)`. Both need:

```rust
let mut mut_scope_stack: Vec<indexmap::IndexMap<String, Type>> = Vec::new();
crate::synth(<term>, locals, &mut mut_scope_stack, /* existing args */)
```

(Each call site gets its own fresh stack — these are re-synth sites
that begin from a top-of-body position, so an empty stack is correct.)

- [ ] **Step 6: Verify build green**

Run: `cargo build --workspace 2>&1 | tail -10`
Expected: green.

Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
Expected: all existing tests still pass (the new parameter is
unconsumed at the existing call sites; behaviour is identical).

---

## Task 3 — `Term::Var` resolution: prepend mut-scope

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:2671-2941` — `Term::Var` arm in `synth`.

- [ ] **Step 1: Locate the `Term::Var` resolution arm**

In `synth`, find the `Term::Var { name } => { ... }` arm. The
existing resolution chain consults `locals` first, then params, then
the top-level def map, then builtins, then class-method dispatch.

- [ ] **Step 2: Prepend mut-scope lookup**

Immediately before the existing `locals.get(name)` lookup, insert:

```rust
// Iter mut.2: mut-vars take precedence over let-bound / param /
// top-level / builtin / class-method resolutions. Innermost-first.
for frame in mut_scope_stack.iter().rev() {
    if let Some(ty) = frame.get(name) {
        // Mut-vars are monomorphic by spec §"var element types" —
        // no Forall instantiation, no free_fn_owner recording.
        return Ok((ty.clone(), /* whatever return-tuple shape is */));
    }
}
```

The exact return-tuple shape must match the existing `Term::Var`
arm's return shape (the function returns more than just `Type`; see
the locals-hit branch for the canonical form, then mirror it).

- [ ] **Step 3: Pin test — mut-var shadows outer let**

Add to `#[cfg(test)] mod tests`:

```rust
#[test]
fn mut_var_resolution_shadows_outer_let() {
    // (let x 1 (mut (var x (con Float) 2.0) x))
    //     -> the inner x is Float, the outer x is Int;
    //     the body's x resolves to the mut-var (Float).
    let term = Term::Let {
        name: "x".into(),
        value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
        body: Box::new(Term::Mut {
            vars: vec![ailang_core::ast::MutVar {
                name: "x".into(),
                ty: Type::float(),
                init: Term::Lit { lit: Literal::Float { bits: "4000000000000000".into() } },
            }],
            body: Box::new(Term::Var { name: "x".into() }),
        }),
    };
    let (ty, _) = synth_in_builtins_env(&term);
    assert_eq!(ty, Type::float(), "inner mut-var x : Float must shadow outer let x : Int");
}
```

(`synth_in_builtins_env` is the existing test helper; use whichever
helper the existing builtins-related tests in lib.rs use to drive
`synth`.)

- [ ] **Step 4: Run to verify pass**

Run: `cargo test --workspace -p ailang-check mut_var_resolution_shadows_outer_let`
Expected: PASS.

---

## Task 4 — `Term::Mut` typecheck arm

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:3488-3492` — replace `Term::Mut` `Internal` stub.

- [ ] **Step 1: Write the failing positive pin**

Add to `#[cfg(test)] mod tests`:

```rust
#[test]
fn mut_block_typechecks_with_int_var_and_returns_int() {
    // (mut (var x (con Int) 0) (assign x (app + x 1)) x)
    //     -> Int.
    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::App {
                    func: Box::new(Term::Var { name: "+".into() }),
                    args: vec![
                        Term::Var { name: "x".into() },
                        Term::Lit { lit: Literal::Int { value: 1 } },
                    ],
                    // ... whatever tail-call flag default the existing tests use
                }),
            }),
            rhs: Box::new(Term::Var { name: "x".into() }),
        }),
    };
    let (ty, _) = synth_in_builtins_env(&term);
    assert_eq!(ty, Type::int(), "mut block returning a mut-var of type Int must synth as Int");
}
```

- [ ] **Step 2: Run to verify red**

Run: `cargo test --workspace -p ailang-check mut_block_typechecks_with_int_var_and_returns_int`
Expected: FAIL with `CheckError::Internal` from the mut.1 stub.

- [ ] **Step 3: Replace the `Term::Mut` stub with real logic**

At `crates/ailang-check/src/lib.rs:3488-3492` (the `Term::Mut` arm
in `synth`), replace:

```rust
Term::Mut { .. } => {
    Err(CheckError::Internal(
        "Term::Mut not yet supported in typecheck (deferred to iter mut.2)".into(),
    ))
}
```

with:

```rust
Term::Mut { vars, body } => {
    // Gate var types: only Int / Float / Bool / Unit allowed in
    // mut.2 per spec §"Out of scope".
    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"))
    }

    // Build a fresh frame.
    let mut frame: indexmap::IndexMap<String, Type> = indexmap::IndexMap::new();
    for v in vars {
        if !is_supported_mut_var_type(&v.ty) {
            return Err(CheckError::UnsupportedMutVarType {
                name: v.name.clone(),
                ty: render_type(&v.ty), // existing helper; or use std::fmt path
            });
        }
        // Synth init in the outer scope (current mut_scope_stack contents
        // are already on the stack; this frame is not yet pushed, so the
        // var's own name does not shadow itself during init).
        let (init_ty, /* ...other return components... */) = synth(
            &v.init,
            locals,
            mut_scope_stack,
            /* existing args */
        )?;
        // Unify init type with declared type.
        unify(&init_ty, &v.ty, /* existing unify args */)?;
        // Bind name → declared type in the current frame.
        frame.insert(v.name.clone(), v.ty.clone());
    }

    // Push the completed frame.
    mut_scope_stack.push(frame);

    // Synth body in the extended scope.
    let body_result = synth(body, locals, mut_scope_stack, /* existing args */);

    // Pop the frame regardless of body outcome.
    mut_scope_stack.pop();

    // Return the body's type (or propagate the error).
    body_result
}
```

The exact return-tuple shape and the names of helpers (`unify`,
`render_type` for the type→String renderer) must match the existing
code conventions; the implementer reads the canonical form from
adjacent arms (e.g. the `Term::Let` arm for the unify pattern and
the type-renderer call shape).

The function `is_supported_mut_var_type` lives as a small helper at
file scope (top of `lib.rs` near the other `is_*` helpers) or inline.
Either is acceptable; pick whichever matches the existing convention.

- [ ] **Step 4: Run to verify pass**

Run: `cargo test --workspace -p ailang-check mut_block_typechecks_with_int_var_and_returns_int`
Expected: PASS.

---

## Task 5 — `Term::Assign` typecheck arm

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:3493-3497` — replace `Term::Assign` `Internal` stub.

- [ ] **Step 1: Write the failing positive pin**

Add to `#[cfg(test)] mod tests`:

```rust
#[test]
fn assign_to_in_scope_mut_var_synths_unit() {
    // Inside a mut frame with (var x Int 0), (assign x 1) :: Unit.
    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_in_builtins_env(&term);
    assert_eq!(ty, Type::unit(), "mut block whose body is a lone assign must synth as Unit");
}
```

- [ ] **Step 2: Run to verify red**

Run: `cargo test --workspace -p ailang-check assign_to_in_scope_mut_var_synths_unit`
Expected: FAIL with the `Term::Assign` `Internal` stub.

- [ ] **Step 3: Replace the `Term::Assign` stub with real logic**

At `crates/ailang-check/src/lib.rs:3493-3497`, replace:

```rust
Term::Assign { .. } => {
    Err(CheckError::Internal(
        "Term::Assign not yet supported in typecheck (deferred to iter mut.2)".into(),
    ))
}
```

with:

```rust
Term::Assign { name, value } => {
    // Walk mut_scope_stack innermost-first looking for `name`.
    let declared: Option<Type> = mut_scope_stack
        .iter()
        .rev()
        .find_map(|frame| frame.get(name).cloned());

    match declared {
        None => {
            // Flatten every mut-var name in every frame, innermost-
            // first, dedup-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) => {
            // Synth the value.
            let (value_ty, /* ... */) = synth(
                value,
                locals,
                mut_scope_stack,
                /* existing args */
            )?;
            // Compare to declared.
            if /* unifies, see existing convention */ != declared {
                return Err(CheckError::AssignTypeMismatch {
                    name: name.clone(),
                    declared: render_type(&declared_ty),
                    got: render_type(&value_ty),
                });
            }
            // Produce Unit.
            Ok((Type::unit(), /* whatever return-tuple shape */))
        }
    }
}
```

The unification step uses the same machinery as `Term::Let`'s init
check — read the adjacent arm to copy the canonical shape (likely
`unify(&value_ty, &declared_ty, &mut subst)?` or similar; the
implementer matches the existing convention).

- [ ] **Step 4: Run to verify pass**

Run: `cargo test --workspace -p ailang-check assign_to_in_scope_mut_var_synths_unit`
Expected: PASS.

Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
Expected: all check-side tests pass; build is green.

---

## Task 6 — Five fixtures + driver test

**Files:**
- Create: `examples/test_mut_assign_out_of_scope.ail.json`
- Create: `examples/test_mut_assign_type_mismatch.ail.json`
- Create: `examples/test_mut_var_unsupported_type.ail.json`
- Create: `examples/test_mut_assign_outside_mut.ail.json`
- Create: `examples/test_mut_nested_shadow_legal.ail.json`
- Create: `crates/ailang-check/tests/mut_typecheck_pin.rs`

These fixtures are `.ail.json` (canonical-form-rejection style)
because they exercise typecheck failures specifically; the form-A
parser would not necessarily reject them, but typecheck must. The
seven-file form-A carve-out list (per pd.3, journal 2026-05-14)
explicitly admits negative typecheck fixtures as `.ail.json`-only.
Note the existing convention precedent: `examples/broken_unbound.ail.json`
and `examples/test_22b2_*.ail.json`.

- [ ] **Step 1: Create `test_mut_assign_out_of_scope.ail.json`**

```json
{
  "name": "test_mut_assign_out_of_scope",
  "imports": [],
  "defs": [
    {
      "kind": "fn",
      "name": "main",
      "ty": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": ["IO"] },
      "params": [],
      "body": {
        "t": "mut",
        "vars": [
          { "name": "x", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }
        ],
        "body": {
          "t": "assign",
          "name": "y",
          "value": { "t": "lit", "lit": { "kind": "int", "value": 1 } }
        }
      }
    }
  ]
}
```

The exact module-level shape (root keys, FnDef field names) must
match the canonical schema; the implementer cross-checks against
`examples/broken_unbound.ail.json` as the closest precedent.

- [ ] **Step 2: Create the four remaining fixtures**

Each follows the same shape, varying:
- `test_mut_assign_type_mismatch.ail.json` — `var x : Int = 0`; `assign x 1.5` (Float).
- `test_mut_var_unsupported_type.ail.json` — `var s : Str = "hello"`.
- `test_mut_assign_outside_mut.ail.json` — fn body is `Term::Assign { name: "x", value: ... }` directly (no enclosing `Term::Mut`).
- `test_mut_nested_shadow_legal.ail.json` — outer mut has `var x : Int = 1`; inner mut has `var x : Float = 2.0` plus body that returns `x` (Float). The outer body returns whatever the inner mut returns.

The positive fixture's main fn returns Float and must typecheck
clean.

- [ ] **Step 3: Create the driver test**

`crates/ailang-check/tests/mut_typecheck_pin.rs`:

```rust
//! Iter mut.2: pin tests that the five typecheck fixtures produce
//! the expected diagnostic codes (or zero diagnostics for the
//! positive nested-shadow case).
//!
//! Spec: docs/specs/0029-mut-local.md §"Testing strategy /
//! Typecheck negative tests".

use std::path::PathBuf;

fn examples_dir() -> PathBuf {
    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
        .parent().unwrap()
        .parent().unwrap()
        .join("examples")
}

fn check_fixture(fixture_name: &str) -> Vec<String> {
    // Whatever the existing canonical helper is for the
    // load-then-check-then-collect-codes pattern. Inspect
    // crates/ailang-check/tests/show_dispatch_pin.rs (or whichever
    // pin test is closest) for the convention.
    todo!("convention from sibling pin tests");
}

#[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);
}
```

The `check_fixture` helper body must match the existing
sibling-pin-test convention. The implementer reads
`crates/ailang-check/tests/show_dispatch_pin.rs` (or whichever is
closest) and copies the canonical shape. **Do NOT leave a `todo!()`
in the final file** — that is a placeholder forbidden by the plan
discipline. Resolve to the canonical helper before declaring done.

- [ ] **Step 4: Run the driver**

Run: `cargo test --workspace -p ailang-check mut_typecheck_pin`
Expected: all five tests PASS.

- [ ] **Step 5: Run full check-crate tests**

Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
Expected: every test green, including all the new ones + the
existing baseline.

---

## Task 7 — Verify `examples/mut.ail` typechecks clean

**Files:**
- (no edits; verification only)

- [ ] **Step 1: Hand-check via `cargo run ail check`**

Run: `cargo run --quiet --bin ail -- check examples/mut.ail 2>&1`
Expected: zero diagnostics (all six fns in the fixture typecheck
clean — they were authored to do so).

If any of the six fns emit a diagnostic, that is a real bug in
either the spec semantics or the implementation. Stop, diagnose,
and either fix the typecheck logic or amend the fixture (the latter
needs Boss sign-off because the fixture is the spec's load-bearing
positive sample).

- [ ] **Step 2: Verify the workspace tests pass**

Run: `cargo test --workspace 2>&1 | tail -5`
Expected: every test green.

---

## Self-review checklist

- [ ] **Spec coverage:** every section of spec §"Iteration mut.2 —
  Typecheck" has a matching task. Cross-check: typecheck arm for
  `Term::Mut` (Task 4), typecheck arm for `Term::Assign` (Task 5),
  `Term::Var` resolution prepending (Task 3), three diagnostics
  (Task 1), five fixtures (Task 6). All covered.

- [ ] **Placeholder scan:** grep for "TBD" / "TODO" / "implement
  later" / "similar to Task" / "appropriate error handling" / "fill
  in later". The Task 6 Step 3 driver contains a `todo!()` in the
  *plan text* (intentional, as the helper convention is read off
  sibling tests at execution time) — but a literal `todo!()` MUST
  NOT survive into the committed file. The Step 3 instruction names
  this explicitly.

- [ ] **Type-name consistency:** `CheckError::MutAssignOutOfScope`,
  `CheckError::AssignTypeMismatch`, `CheckError::UnsupportedMutVarType`,
  `mut_scope_stack`, `IndexMap<String, Type>`, `Type::int()`,
  `Type::float()`, `Type::unit()`, the kebab codes (`mut-assign-out-of-scope`,
  `assign-type-mismatch`, `mut-var-unsupported-type`). Each appears
  identically across tasks.

- [ ] **Step granularity:** each step is 2-5 minutes (a single match
  arm; a single signature change; a single fixture).

- [ ] **No commit steps:** verified — the plan contains no `git commit`
  instructions.

- [ ] **Boss decisions named:** the four recon open questions are
  resolved in this plan: (1) fixtures go to `examples/` with the
  driver under `crates/ailang-check/tests/` (Task 6 lead paragraph);
  (2) `mut_scope_stack` is a `synth` parameter, not an `Env` field
  (Task 2 Step 1); (3) `MutAssignOutOfScope.available` is flattened
  across all enclosing frames innermost-first (Task 5 Step 3); (4)
  `mono.rs` re-synth sites verified at lines 712 + 1337 (Task 2
  Step 5).

---

## Acceptance gate for iteration mut.2

- `cargo build --workspace` green.
- `cargo test --workspace` green.
- All five new tests under `crates/ailang-check/tests/mut_typecheck_pin.rs`
  green.
- The three `CheckError` variants have `code()` arms returning the
  three kebab codes.
- `examples/mut.ail` (the six-fn round-trip fixture from mut.1)
  typechecks clean via `cargo run --bin ail -- check examples/mut.ail`.
- `Term::Mut` and `Term::Assign` reaching codegen still produce
  `CodegenError::Internal` (codegen recognition is deferred to mut.3
  and is NOT in scope for this iteration).

The iteration does NOT include any `examples/mut_counter.ail` or
`examples/mut_sum_floats.ail` end-to-end run; those land with mut.3.