Section 01: AST-based Value Restriction

Status: Not Started Goal: Replace unconditional generalization at 3 let-binding sites with a single SSOT should_generalize(arena, init_expr_id) -> bool helper that returns true only for direct, non-capturing ExprKind::Lambda initializers. Preserves let-polymorphism for let id = x -> x while preventing empty-list element Vars from being prematurely generalized into Schemes.

Semantic scope of this change: This change restricts Ori’s let-polymorphism to ONLY direct non-capturing lambda bindings. The following patterns that were previously polymorphic become intentionally monomorphic under the new policy:

let f = { x -> x } — block wrapping a lambda: should_generalize sees ExprKind::Block, not ExprKind::Lambda, so returns false.
let alias = id — variable aliasing a polymorphic binding: should_generalize sees ExprKind::Ident, returns false. alias gets the instantiated monotype.
let f = if c then (x -> x) else (y -> y) — conditional producing a function: should_generalize sees ExprKind::If, returns false.
let x = [] — empty list: sees ExprKind::List, returns false.
let m = {} — empty map: sees ExprKind::Map, returns false.
Any non-lambda expression: function calls, struct literals, constants, etc.

This is a deliberate design choice matching Rust’s approach (no let-polymorphism for locals) while preserving the most common polymorphic use case (let id = x -> x). The choice is AST-based rather than type-based because type-tag heuristics fail when the resolved type is still Tag::Var awaiting bi-directional unification (per Gemini Round 1 TPR finding on the original fix-section).

Success Criteria: (authoritative copy in YAML success_criteria: frontmatter above; all verified at closeout 2026-04-14)

Single pub(super) fn should_generalize exists in blocks.rs — one grep hit
All 3 engine.generalize() calls are gated by if should_generalize(...) — grep verifiable
test_let_polymorphism_for_lambda passes before and after; reverting the change breaks it
test_empty_list_let_binding_does_not_generalize_element_var passes after migration
Negative pins for intentionally monomorphic patterns pass (block-wrapped, aliased, conditional)
timeout 150 ./test-all.sh green (debug + release)

Cross-section contract (Section 01 -> Sections 02/03): After Section 01 completes, infer_expr stores expression types BEFORE the generalization step in infer_block / infer_let. For non-lambda initializers, the element Tag::Var stays Unbound in the type pool but IS stored in engine.expr_types() during infer_expr. Section 02’s validator (validate_body_types) runs AFTER body inference and inspects expr_types — it is the validator that surfaces E2005 on these remaining Unbound vars. Section 01 alone does not reject programs; it prepares the ground for Section 02/03 to do so. Without Section 02, the Unbound vars would silently flow to codegen (the pre-existing bug). Without Section 01, the validator would falsely reject polymorphic lambda bindings. Both sections are required for correctness.

Context: BUG-04-074 traced the “unresolved type variable at codegen” failure to three unconditional engine.generalize() calls in the typeck let-binding paths. Generalizing an empty-list element’s Tag::Var turns it into a Tag::Scheme whose bound var is never instantiated to a concrete type — downstream use sites like .len() don’t constrain the element type, so the Scheme persists unresolved through canonicalization, ARC lowering, and into LLVM codegen where it triggers a verification failure. The fix is AST-based Value Restriction: only direct non-capturing lambdas (x -> x) qualify for generalization; all other initializers — including [], {}, block-wrapped lambdas, variable aliases, and constants — are monomorphic and must not generalize their type variables.

Reference implementations:

Rust compiler/rustc_hir_typeck/src/expr.rs: no let-polymorphism for local let bindings — Rust’s type checker never generalizes locally-bound types into schemes; every let x = e in a function body is monomorphic. Ori’s design differs (it supports let id = x -> x with genuine polymorphism for direct non-capturing lambdas), but the lesson is clear: unrestricted generalization of arbitrary initializers is unsound.
Haskell ghc/compiler/GHC/Tc/Gen/Bind.hs: the monomorphism restriction motivates why even a purely functional language needs Value Restriction — functions defined without explicit type signatures that involve type classes can behave unexpectedly when generalized and re-used at different types.
Ori compiler/ori_types/src/infer/expr/blocks.rs:79-89: body_captures_outer precedent — the codebase already performs AST-based Lambda detection + capture analysis to decide whether a lambda is capturing. should_generalize extends this exact check to make generalization conditional on the result.

Note on body_captures_outer completeness: The existing body_captures_outer function (L249-286 in blocks.rs) is an under-approximation: the _ => false catch-all at L284 skips expression forms it does not explicitly walk (call arguments, method arguments beyond the receiver, list/tuple/map subexpressions). This means it may MISS captures in some expressions, causing should_generalize to return true when it should return false — incorrectly generalizing a capturing lambda. This is the unsafe direction (the function’s own comment at L281-283 acknowledges “might miss captures, which means we’ll generalize when we shouldn’t — codegen will catch it”). The safety net is the AOT backend: if a capturing lambda IS incorrectly generalized, the resulting polymorphic scheme hits codegen with unresolvable type variables, which triggers a verification failure. The under-approximation is tolerable in practice because: (1) the common capture forms (identifiers, binary ops, unary ops, method receivers, call targets, if/else) ARE walked; (2) the AOT backend catches any leak. Improving body_captures_outer to walk all expression forms is desirable but orthogonal to this plan — the function’s behavior is pre-existing and unchanged by this section.

Depends on: None (independent of Sections 02–06).

01.1 Extract `should_generalize` SSOT helper

File(s): compiler/ori_types/src/infer/expr/blocks.rs

The existing infer_block body (L79-89) already contains the correct logic: check whether init is an ExprKind::Lambda, extract param names, call body_captures_outer. The problem is that this logic is inlined rather than extracted — it cannot be called from infer_let (L167) or from sequences.rs:247 without duplication, which is exactly the impl-hygiene.md §Algorithmic DRY violation (3 callsites, same skeleton = missing abstraction).

This subsection extracts the decision into a named, documented, pub(super) function adjacent to body_captures_outer in the same file. All three callers in 01.2–01.4 will call this one function.

TDD — write failing tests FIRST (in Section 05): Before touching production code, ensure Section 05’s stub test test_let_polymorphism_for_lambda exists and passes with current behavior (it verifies the lambda case — which must continue to work after the change). Also confirm that a new stub test_empty_list_let_binding_does_not_generalize_element_var fails with current behavior (empty list IS currently generalized — the test expects it NOT to be). Only after both tests are in the right state should implementation begin.

Test file location: compiler/ori_types/src/infer/expr/tests.rs. This is the existing test file for the expr module, declared at mod.rs:477-480 as #[cfg(test)] mod tests;. Both blocks.rs and sequences.rs are flat files (not directories), so the foo.rs → foo/tests.rs pattern from compiler.md §Testing does not apply. All tests for the expr module — regardless of which submodule’s code they exercise — live in this single tests.rs file, which accesses submodule internals via the pub(super) use blocks::*; re-exports at mod.rs:53.

Write test stubs in compiler/ori_types/src/infer/expr/tests.rs:
- test_let_polymorphism_for_lambda — verifies let id = x -> x produces a Tag::Scheme (currently passes; must continue to pass after migration). Semantic pin.
- test_empty_list_let_binding_does_not_generalize_element_var — verifies that the element type of let xs = [] is NOT wrapped in a Tag::Scheme (currently FAILS — the test documents the target behavior before implementation). Semantic pin.
- test_block_wrapped_lambda_does_not_generalize — verifies that let f = { x -> x } does NOT produce a Tag::Scheme under the new policy (negative pin for the block-wrapping blindspot). Currently FAILS — becomes monomorphic after migration.
- test_variable_alias_does_not_generalize — verifies that let alias = id (where id is a polymorphic binding) does NOT re-generalize into a new Tag::Scheme (negative pin for the variable-aliasing blindspot). alias gets the instantiated monotype from id’s scheme at the use site.
- test_conditional_lambda_does_not_generalize — verifies that let f = if true then (x -> x) else (y -> y) does NOT produce a Tag::Scheme (negative pin for the conditional-lambda blindspot).
- test_capturing_lambda_does_not_generalize — verifies that a lambda which captures an outer variable (let outer = 1; let f = x -> x + outer) does NOT produce a Tag::Scheme (negative pin for the capture-sensitive boundary in body_captures_outer). This is the policy boundary between the positive pin (test_let_polymorphism_for_lambda — non-capturing) and this test (capturing).

Add pub(super) fn should_generalize to blocks.rs immediately above body_captures_outer (currently at L249):

/// Returns `true` iff `init` is a non-capturing lambda expression whose type
/// variables may be safely generalized for let-polymorphism.
///
/// Only `ExprKind::Lambda` initializers with no free outer-scope variables
/// are generalizable.  All other initializers — list/map literals, struct
/// constructions, constants, function calls — are monomorphic and MUST NOT
/// generalize their inferred type variables.  Generalizing a non-lambda
/// initializer (e.g. `let xs = []`) turns the element's `Tag::Var` into a
/// `Tag::Scheme` that downstream phases can never instantiate to a concrete
/// type, violating `typeck.md PC-2`.
///
/// This is the SSOT for the Value Restriction policy.  Every let-binding
/// generalization site in the type checker MUST call this function rather
/// than inlining equivalent logic.
///
/// # Spec reference
/// `docs/ori_lang/v2026/spec/14-expressions.md:1224-1228` — empty container
/// literals without type context are a compile-time error; this function is
/// the upstream guard that ensures their element `Tag::Var` remains Unbound
/// so the Section 02 validator can surface `E2005` with a clear message.
///
/// # Plan
/// `plans/empty-container-typeck-phase-contract/section-01-value-restriction.md`
pub(super) fn should_generalize(arena: &ExprArena, init: ExprId) -> bool {
    match &arena.get_expr(init).kind {
        ExprKind::Lambda { params, body, .. } => {
            let param_names: Vec<Name> =
                arena.get_params(*params).iter().map(|p| p.name).collect();
            !body_captures_outer(arena, *body, &param_names)
        }
        _ => false,
    }
}

Verify should_generalize is visible from tests.rs via use super::* (the existing pub(super) use blocks::*; re-export at mod.rs:53 covers this automatically since the test module is mod tests; declared at mod.rs:477-480).
Run timeout 150 cargo test -p ori_types — test_let_polymorphism_for_lambda must still pass (the helper alone changes nothing); test_empty_list_let_binding_does_not_generalize_element_var passes with current behavior (unit-test context doesn’t fully generalize empty lists — serves as correct semantic pin).
Verify all tests pass in debug and release: timeout 150 cargo test -p ori_types and timeout 150 cargo test -p ori_types --release
Subsection close-out (01.1) — MANDATORY before starting 01.2:
- All tasks above are [x] and the subsection’s behavior is verified
- Update this subsection’s status in section frontmatter to complete
- Run /improve-tooling retrospectively on THIS subsection — Retrospective 01.1: no tooling gaps. Straightforward extract-and-test; LSP diagnostics caught field-name mismatches (Param.pattern, If.cond, List(ExprRange)) promptly. No scripts or tracing needed.
- Run /sync-claude on THIS subsection — Claude artifact sync 01.1: no API/command/phase changes — should_generalize is pub(super) crate-internal. Artifacts current.
- Repo hygiene check — diagnostics/repo-hygiene.sh --check reports clean.

01.2 Migrate `infer_block` block-statement let site

File(s): compiler/ori_types/src/infer/expr/blocks.rs

The current block-statement let path (L79-89) inlines the capturing-lambda check in full. After extracting should_generalize in 01.1, this entire inline block can be replaced with a single conditional call.

Current code (L79-89):

// (inside the `else { // No annotation: infer and generalize ... }` branch)
let init_ty = infer_expr(engine, arena, *init);

// ... self-capture error rewriting (L65-70) ...

if let ExprKind::Lambda { params, body, .. } = &arena.get_expr(*init).kind {
    let param_names: Vec<Name> =
        arena.get_params(*params).iter().map(|p| p.name).collect();
    if body_captures_outer(arena, *body, &param_names) {
        init_ty
    } else {
        engine.generalize(init_ty)       // L85
    }
} else {
    engine.generalize(init_ty)           // L88
}

Target code (replaces L79-89):

let init_ty = infer_expr(engine, arena, *init);

// Detect closure self-capture (unchanged — L65-70 block stays as-is)
if let Some(name) = binding_name {
    if matches!(arena.get_expr(*init).kind, ExprKind::Lambda { .. }) {
        engine.rewrite_self_capture_errors(name, errors_before);
    }
}

// Value Restriction: only non-capturing lambdas may be generalized.
// All other initializers (list literals, map literals, struct constructions,
// constants) are monomorphic — their Vars must stay Unbound so the
// Section 02 validator can surface E2005 on empty containers.
// Spec: docs/ori_lang/v2026/spec/14-expressions.md:1224-1228
if should_generalize(arena, *init) {
    engine.generalize(init_ty)
} else {
    init_ty
}

Note: should_generalize already encodes the body_captures_outer check for lambdas, so the separate if let ExprKind::Lambda { ... } arm is no longer needed. The self-capture rewriting block (checking ExprKind::Lambda to gate rewrite_self_capture_errors) is a separate concern and remains unchanged.

01.3 Migrate `infer_let` (ExprKind::Let dispatch) site

File(s): compiler/ori_types/src/infer/expr/blocks.rs

The standalone infer_let function (L116-179) handles the ExprKind::Let { .. } case dispatched from infer_expr_inner in mod.rs (L160-173). Its no-annotation branch (L151-168) performs an unconditional engine.generalize(init_ty) at L167.

Current code (L151-168, abbreviated):

} else {
    // No annotation: infer the initializer type
    let init_ty = infer_expr(engine, arena, init);

    // Detect closure self-capture ...
    if let Some(name) = binding_name {
        if matches!(arena.get_expr(init).kind, ExprKind::Lambda { .. }) {
            engine.rewrite_self_capture_errors(name, errors_before);
        }
    }

    // Generalize free type variables for let-polymorphism.
    // Variables created at the current (elevated) rank will be quantified.
    engine.generalize(init_ty)           // L167 — unconditional, must be gated
};

Target code (replace L167):

} else {
    // No annotation: infer the initializer type
    let init_ty = infer_expr(engine, arena, init);

    // Detect closure self-capture (unchanged)
    if let Some(name) = binding_name {
        if matches!(arena.get_expr(init).kind, ExprKind::Lambda { .. }) {
            engine.rewrite_self_capture_errors(name, errors_before);
        }
    }

    // Value Restriction: only non-capturing lambdas may be generalized.
    // Spec: docs/ori_lang/v2026/spec/14-expressions.md:1224-1228
    if should_generalize(arena, init) {
        engine.generalize(init_ty)
    } else {
        init_ty
    }
};

01.4 Migrate `sequences.rs` try-block let site

File(s): compiler/ori_types/src/infer/expr/sequences.rs

The try-block let handler infer_try_stmt (L193-262) has a no-annotation branch (L229-248) that generalizes the bound type after unwrapping. The engine.generalize(bound_ty) call is at L247.

Current code (L229-248, abbreviated):

} else {
    // No annotation: infer the initializer type
    let init_ty = infer_expr(engine, arena, *init);

    // Detect closure self-capture (L236-239) ...
    if let Some(name) = binding_name {
        if matches!(arena.get_expr(*init).kind, ExprKind::Lambda { .. }) {
            engine.rewrite_self_capture_errors(name, errors_before);
        }
    }

    // Unwrap Result/Option for try semantics
    let bound_ty = unwrap_result_or_option(engine, init_ty);

    // Generalize free type variables for let-polymorphism
    engine.generalize(bound_ty)          // L247 — unconditional, must be gated
};

Target code (replace L247):

} else {
    // No annotation: infer the initializer type
    let init_ty = infer_expr(engine, arena, *init);

    // Detect closure self-capture (unchanged)
    if let Some(name) = binding_name {
        if matches!(arena.get_expr(*init).kind, ExprKind::Lambda { .. }) {
            engine.rewrite_self_capture_errors(name, errors_before);
        }
    }

    // Unwrap Result/Option for try semantics
    let bound_ty = unwrap_result_or_option(engine, init_ty);

    // Value Restriction: only non-capturing lambdas may be generalized.
    // Spec: docs/ori_lang/v2026/spec/14-expressions.md:1224-1228
    if should_generalize(arena, *init) {
        engine.generalize(bound_ty)
    } else {
        bound_ty
    }
};

Note: should_generalize tests the original init expression (before unwrapping), not bound_ty. The unwrapping step changes the type, not the expression kind — a lambda inside a try block would be let f = Ok(x -> x)? which parses as init = Ok(...), not init = Lambda, so should_generalize correctly returns false for it. Plain lambdas in a try block (let id = x -> x in a try { ... }) have init = Lambda { .. } and unwrap_result_or_option is a no-op for non-Result/Option types, so the non-capturing lambda case still reaches engine.generalize correctly.

Import should_generalize at the top of sequences.rs. The function is pub(super) in blocks.rs and blocks::* is re-exported via pub(super) use blocks::* in mod.rs (line 53), so should_generalize is already in scope in sequences.rs via use super::* (or directly via the infer_expr imports it already uses). Verify the import compiles cleanly.

01.R Third Party Review Findings

01.N Completion Checklist

Exit Criteria: All 4 subsections complete. Single should_generalize SSOT in blocks.rs. Three engine.generalize calls each gated by if should_generalize(...). Eight new tests pass: 4 positive/semantic pins (lambda polymorphism, empty list, let-expr, try-block) + 4 negative pins (block-wrapped, aliased, conditional, capturing lambda). test_let_polymorphism_for_lambda passes unchanged (semantic pin). timeout 150 ./test-all.sh green in debug and release. /tpr-review and /impl-hygiene-review clean. typeck.md §GN-3 updated to reflect the Value Restriction policy. Section 03 can now assume the 3 generalization sites are correctly gated and that empty-list element Vars flow as Unbound Tag::Var into the validator.

Retrospective: Findings surfaced by §03.N `/impl-hygiene-review` (2026-04-18)

Why these are retrospectives, not new sections. Running /impl-hygiene-review at §03.N close-out with scope=active-work-arc scanned code authored by §01/§02 and surfaced 5 Critical + 2 Major + 3 Minor findings that §01’s own close-out hygiene review missed. Per CLAUDE.md §Ownership & Deferral “Plan-blocker bugs belong IN the plan — NEVER sibling fix files”, these are absorbed into §01 rather than filed as sibling /add-bug entries. §01’s status flipped from complete back to in-progress until these subsections land.

Auto-fixed under user pre-approval (memory feedback_auto_fix_cleanup.md): F9-F12 (stale plan annotations referencing BUG-02-008, BUG-04-074, BUG-04-084, TPR Round 1 Codex-F2, Plan §02.4 T1) were cleaned by plan-annotations.py --fix --apply during the review’s Phase 0 static-analysis pass. 8 automatic fixes + 5 manual edits (removed bug IDs from assertion string literals and doc comments in empty_container.rs, check/bodies/tests.rs, check/validators/tests.rs, infer/mod.rs). Verified via re-scan: 0 stale matches remaining in scoped files.

01.R-HYGIENE Retrospective: body_captures_outer soundness (F1+F7)

Severity: Critical (F1) + Major (F7) Source: /impl-hygiene-review §03.N close-out sweep (2026-04-18) File: compiler/ori_types/src/infer/expr/blocks.rs:243-302

F1 finding summary: The body_captures_outer(arena, expr, param_names, outer_vars) function’s docstring claims “Over-approximates captures (any non-param, non-literal name counts) — conservative: we may skip generalization for some non-capturing lambdas, but never incorrectly generalize a capturing one.” The inline comment admits the opposite: the _ => false match-arm wildcard returns false for every unrecognized ExprKind, which means “this ExprKind has no captures”, which means a capturing lambda in an unrecognized variant is permitted to generalize. This is a soundness inversion: the conservative direction should be _ => true (unknown = assume capture = skip generalization), but the code does the opposite.

F7 finding summary: Beyond the conservative-default inversion, the specific matched arms have blind spots:

ExprKind::Call { func, args, .. }: only func is recursed; args slice is in _ => false
ExprKind::MethodCall { receiver, args, .. }: only receiver; args unchecked
ExprKind::Block(block_idx): block body not descended
ExprKind::List(elements) / ExprKind::Map(entries): elements not scanned
ExprKind::Struct { fields, .. }: field initializers not scanned
ExprKind::Match { arms, .. }: arm bodies not scanned

A lambda () -> map.get("key") passed to list.map(...) has map captured via the arg slot, which body_captures_outer does not descend into — the capturing lambda escapes detection and is unsoundly generalized.

Invariant Anchoring (per CLAUDE.md §Invariant-Anchoring Before Test-Chasing)

System invariant: typeck.md §GN-3 Value Restriction — only direct non-capturing lambda initializers generalize; capturing lambdas stay monomorphic. Soundness depends on body_captures_outer being conservative in the direction of preventing generalization (over-approximate captures), not the direction of allowing it.
Downstream consumer: The type checker’s should_generalize decision feeds the inference engine’s generalization step (GN-1). Generalizing a capturing lambda produces a polymorphic scheme whose bound variables include captured variables from an outer scope — when instantiated at a use site, those variables are fresh and unrelated to the outer captures, silently producing incorrect types.
If tests fail after the fix: fix the code-under-test, NOT body_captures_outer. The current _ => false arm is the bug; flipping it to _ => true will correctly reject capturing lambdas that previously passed through, and the test suite must then be updated to pin the correct behavior.

Fix Plan (TDD Matrix Required — MANDATORY)

01.R-DRY Retrospective: algorithmic duplication (F4+F5)

Severity: Critical (both) Source: /impl-hygiene-review §03.N close-out sweep (2026-04-18)

F4: InferEngine constructor duplication

File: compiler/ori_types/src/infer/mod.rs:~50-110

Summary: InferEngine::new(pool) and InferEngine::with_env(pool, env) contain an identical ~27-line struct literal differing only in the env field (TypeEnv::new() vs caller-supplied env). Adding any new field to InferEngine requires editing both constructors; missing one silently produces a divergent state.

Fix plan:

Extract fn build(pool: &'pool mut Pool, env: TypeEnv) -> Self as pub(super) (or fn if crate-local access suffices) with the single struct literal — landed as private fn build in compiler/ori_types/src/infer/mod.rs (§Visibility: new/with_env are same-impl callers; private minimizes pub surface per impl-hygiene.md §Visibility).
new(pool) calls build(pool, TypeEnv::new())
with_env(pool, env) calls build(pool, env)
Verify no behavioral change — both callers produce identical state to pre-fix (verified: full ori_types suite 840/0 debug + release; full test-all.sh 16382/844/160 — +1 pass over pre-F4 baseline, zero new failures).
Add a regression test: construct via both entry points and assert all-field equality — landed as infer_engine_new_and_with_env_produce_identical_default_state in compiler/ori_types/src/infer/tests.rs using an EngineSnapshot record that compares every publicly-observable default-state accessor. Field-by-field PartialEq on InferEngine is impractical (borrowed Pool, internal UnifyEngine) — behavioral parity via snapshot is equivalent for the SSOT invariant and catches the “new field added to one constructor only” failure mode identically.
Follow-up: if new fields are added, only build() requires editing (confirmed structurally — new and with_env are 1-line delegations).

F5: should_generalize + generalize 3x duplication

Files: compiler/ori_types/src/infer/expr/blocks.rs:77-81, 158-163; compiler/ori_types/src/infer/expr/sequences.rs:249-253

Summary: At all 3 let-binding generalization sites, the same 3-line pattern appears:

if should_generalize(arena, *init) {
    engine.generalize(ty)
} else {
    ty
}

The only variation is whether ty is the raw inferred type or bound_ty (after unwrap_result_or_option). The duplication means: a future change to generalization policy must be edited at 3 sites; a typo silently diverges one site’s behavior.

Fix plan:

Extract pub(super) fn maybe_generalize(engine: &mut InferEngine<'_>, arena: &ExprArena, init: ExprId, ty: Idx) -> Idx in blocks.rs (co-located with should_generalize) — landed at compiler/ori_types/src/infer/expr/blocks.rs:303.
Body: if should_generalize(arena, init, &outer_vars) { engine.generalize(ty) } else { ty } — includes collect_outer_vars(engine) internally so callers don’t repeat it. (Signature extends the plan with the outer_vars parameter threaded through by §01.R-HYGIENE; maybe_generalize subsumes that plumbing.)
Replace all 3 call sites to use maybe_generalize(engine, arena, *init, ty):
- infer_block block-statement let at blocks.rs:96
- infer_let ExprKind::Let dispatch at blocks.rs:174
- infer_try_stmt try-block let at sequences.rs:250
At sequences.rs:250, preserve the semantically significant comment (“should_generalize tests the original init expression”) — landed both on the call site as a 3-line block and in maybe_generalize’s docstring (“Important: init is the original initializer expression, NOT a derived type…”).
Verify no behavioral change — all 8 existing §01 tests (positive + negative pins) and all 7 §01.R-HYGIENE tests continue to pass unchanged. Debug + release full ori_types: 840/0. Full test-all.sh: 16382 pass / 844 fail / 160 skip — +1 pass over pre-F4 baseline (the new F4 pin only; no new failures).
Decide: demote should_generalize visibility (since maybe_generalize is the new SSOT) OR keep both pub(super) for granular access. Decision: keep both pub(super). Rationale: they have distinct SSOT domains — should_generalize owns the decision predicate (pure, testable in isolation, consumed by the three test_should_generalize_* tests at tests.rs:3026/3053/3077); maybe_generalize owns the apply-the-decision pattern (imperative, engine-mutating, 3 call sites). Demoting should_generalize would break the existing test suite without a behavioral win. Documented in both docstrings (“This is the SSOT for applying the decision, alongside should_generalize which is the SSOT for making it”).

Exit criteria for 01.R-DRY: F4 and F5 fixes landed. timeout 150 ./test-all.sh green (0 new failures over cache baseline). All pre-existing §01 tests still pass. /tpr-review DEFERRED to Retrospective Close-Out per the - [ ] anchor at end of this section (batched across 01.R-HYGIENE + 01.R-DRY + 01.R-SIDE-LOGIC + 01.R-TEST-HYGIENE — same rationale as §01.R-HYGIENE’s deferral).

Retrospective on 01.R-DRY itself

/improve-tooling retrospective (01.R-DRY): no tooling gaps surfaced. Both extractions were mechanical (one struct-literal dedup, one 3-line pattern dedup) and the existing toolchain caught every issue promptly — LSP rejected the TypeEnv::is_empty() accessor I first reached for (no such method); the grep 'engine.generalize' / grep 'maybe_generalize' post-checks confirmed the exact 3-site-migration shape the section file documented as success criteria. The intelligence graph’s callers queries for the extracted symbols returned empty (same-crate-private callers aren’t indexed as CALLS edges), so the authoritative call-site list came from the section file itself — as designed. No new diagnostic scripts, flags, or tests needed.
Repo hygiene: verified via diagnostics/repo-hygiene.sh --check (see close-out task; expected clean modulo the pre-existing /tmp/ori-tpr-*/ scratch-dir noise noted by the scanner at session start).

01.R-SIDE-LOGIC Retrospective: dispatch-module side logic (F2+F3)

Severity: Critical (both, downgraded to Major per Phase 4 cross-check — reviewer noted check_collect_to_set is clearly critical, format functions are borderline) Source: /impl-hygiene-review §03.N close-out sweep (2026-04-18) File: compiler/ori_types/src/infer/expr/mod.rs

F2 summary: check_interpolation_printable (~40 lines, ~L380-415) and validate_format_spec (~52 lines, ~L424-475) are substantive validation functions (format spec parsing, alignment/sign/type checking, Printable trait resolution) living in the general dispatch module rather than a dedicated submodule. Per impl-hygiene.md §Side-Logic Rule, non-trivial implementation logic must live in a named submodule.

F3 summary: check_collect_to_set (~28 lines, ~L345-373) handles the Collect::from_iter → Set<T> bidirectional check — Set-specific builtin logic embedded in the general dispatch module instead of in the collections submodule.

Fix plan

Create compiler/ori_types/src/infer/expr/format.rs (new submodule)
Move check_interpolation_printable and validate_format_spec into format.rs
Re-export from infer/expr/mod.rs via explicit named re-export: pub(crate) use format::{check_interpolation_printable, validate_format_spec}; — note pub(crate) rather than pub(super) because the re-export pulls the item up to the infer:: level (the submodule functions must be visible there for the re-export to compile; pub(super) at the submodule level means only expr::, narrower than the re-export target). The existing sibling glob re-exports (pub(super) use blocks::* etc.) will be purged in 01.R-TEST-HYGIENE F14.
Move check_collect_to_set into compiler/ori_types/src/infer/expr/collections.rs (existing submodule)
Re-export from infer/expr/mod.rs: pub(super) use collections::check_collect_to_set; (function declared pub(crate) in collections.rs for the visibility reason above)
Update the dispatch call sites in infer_expr_inner to reference the new paths — call sites unchanged (resolve via re-exports); only the fn bodies in mod.rs were deleted. Single-path dispatch preserved.
Verify no behavioral change — timeout 150 cargo test -p ori_types 840 passed / 0 failed; timeout 150 ./test-all.sh 16382 passed / 844 failed / 160 skipped — exactly +8 passes over cache baseline (from 01.R-HYGIENE + 01.R-DRY commits post-cache), 0 new failures. Pure relocation is observationally a no-op.
/tpr-review clean — DEFERRED to Retrospective Close-Out - [ ] “Re-run /tpr-review on the combined diff”. Same batching rationale as §01.R-HYGIENE / §01.R-DRY — per-subsection review would be wasted reviewer cycles when the Close-Out covers all four retrospectives in a single pass.

Exit criteria for 01.R-SIDE-LOGIC: 3 functions relocated to appropriate submodules. Dispatch module’s mod.rs contains routing only, no implementation. timeout 150 ./test-all.sh green (zero new failures vs cache baseline).

Retrospective on 01.R-SIDE-LOGIC itself

/improve-tooling retrospective (01.R-SIDE-LOGIC): no tooling gaps surfaced. The relocation was mechanical — three functions moved across submodule boundaries with identical signatures. LSP’s dead-code diagnostics flagged each transient state (function moved but not yet re-exported; function re-exported but call site still resolves locally) at exactly the right moment, confirming the name-resolution path before tests ran. One visibility gotcha caught by rustc directly: pub(super) at the submodule level is insufficient for a pub(super) use submodule::fn re-export at mod.rs level — the submodule item needs pub(crate) (or pub(in crate::infer)) for the re-export’s target visibility (infer::) to be legal. Error E0364 was clear and actionable; no tooling gap.
Repo hygiene: verified via diagnostics/repo-hygiene.sh --check (see close-out task).

01.R-TEST-HYGIENE Retrospective: test/import/name drift (F6+F8+F13+F14)

Severity: Major (F6) + Minor (F8, F13, F14) Source: /impl-hygiene-review §03.N close-out sweep (2026-04-18)

F6: parse_and_check test helper duplicate

File: compiler/ori_types/src/check/bodies/tests.rs:~1-40 Summary: parse_and_check in bodies/tests.rs carries an inline comment acknowledging “copied from check/api/tests.rs — deduplication deferred”. The “deferred” comment is itself a hygiene violation per impl-hygiene.md §Algorithmic DRY and CLAUDE.md banned phrases (“tracked for later” is banned without a concrete anchor).

Fix: Move parse_and_check to a shared test utility location. Options:

Option A (Recommended): compiler/ori_types/src/check/test_utils.rs with #[cfg(test)] pub(crate) — both bodies/tests.rs and api/tests.rs import from there
Option B: Keep the helper in api/tests.rs and have bodies/tests.rs import via use super::super::api::tests::parse_and_check; — less clean but minimal reorganization (rejected in favor of A)
Remove the duplicate + the deferral comment
Verify all pre-existing tests in both files still pass

F8: enter_scope vs enter_rank_scope inconsistency

File: compiler/ori_types/src/infer/expr/blocks.rs (infer_let vs block-stmt let in infer_block)

Summary: infer_let at L124/L168 uses engine.enter_scope() / engine.exit_scope(); the block-statement let arm in infer_block at L41/L85 uses engine.enter_rank_scope() / engine.exit_rank_scope(). These are separate APIs. If they are semantically equivalent for rank elevation, the naming should be unified. If they differ in unification-engine behavior, that difference needs to be documented and the correct one selected per context.

Fix:

Investigate InferEngine::enter_scope vs enter_rank_scope implementations — distinct APIs: enter_scope pushes rank + env.child; enter_rank_scope pushes rank only (per typeck.md §SG-4 / §SG-5)
Document the semantic difference (if any) in both methods’ docstrings — existing docstrings at infer/mod.rs:452-459, 477-481 already describe the distinction
Unify the two let-binding sites to use the correct API for let-polymorphism (both should elevate rank per typeck.md §GN-1, §SC-2) — infer_let migrated from enter_scope/exit_scope → enter_rank_scope/exit_rank_scope, matching infer_block block-stmt let and infer_try_stmt try-block let
If the APIs are semantically identical, delete one and have the other forward — NOT identical; both retained
If they are semantically distinct, rename for clarity (e.g., enter_env_scope for env-only, enter_rank_scope for rank-only) — current names already express the distinction; callsite comments added instead to explain the choice
Verify no behavioral change in any existing test — test-all.sh delta vs cache baseline: 0 new failures (844/844 pre-existing known-failing)

F13: Test naming convention

File: compiler/ori_types/src/check/bodies/tests.rs Summary: check_empty_module_bodies test name violates <subject>_<scenario>_<expected> convention per impl-hygiene.md §Test Function Naming.

Fix:

Rename to: check_module_with_no_function_bodies_produces_no_errors (three-part subject_scenario_expected shape per impl-hygiene.md §Test Function Naming)
Update any doc comments to match — no doc comments referenced the old name
Verify test still passes under new name

F14: Glob re-exports in mod.rs

File: compiler/ori_types/src/infer/expr/mod.rs:53-63 Summary: pub(super) use blocks::*; and sibling glob re-exports across calls, collections, etc. violate impl-hygiene.md §Import Hygiene no-glob rule. The comment (“for tests and sibling access”) is not an exemption — #[cfg(test)] is the test context, not the module itself.

Fix:

For each pub(super) use <submodule>::*, replace with explicit named re-exports listing every symbol actually used by the dispatch module or its sibling modules
Use cargo check and grep to enumerate the actually-consumed symbols — intelligence-graph queries (callers / symbols / file-symbols) + iterative cargo check drove the explicit list
After the replacement, remove the “for tests and sibling access” comment (no longer needed) — replaced with a brief explanatory header
Verify no compile errors or behavioral changes — cargo check --tests clean workspace-wide; test-all.sh delta vs baseline: 0 new failures

Exit criteria for 01.R-TEST-HYGIENE: F6 test helper deduplicated, F8 API consistency resolved, F13 test renamed, F14 globs replaced with explicit re-exports. timeout 150 ./test-all.sh green.

Retrospective on 01.R-TEST-HYGIENE itself

/improve-tooling retrospective (01.R-TEST-HYGIENE): no tooling gaps surfaced. F6+F13 were pure Edits against an existing module structure; F14’s 4-round cargo check --tests iteration was rustc earning its keep (each round surfaced a distinct missing name, with E0364/E0432/E0425 messages that already included the suggested fix). F8’s scope-API unification was driven by scripts/intel-query.sh callers enter_rank_scope followed by reading infer/mod.rs:440-493 — the graph answered the “is this actually used from siblings?” question in one call. test-all.sh baseline diff (16374 → 16382 passed, 844/844 failed, 160/160 skipped) was a single mental subtraction; a --vs-baseline flag was considered and rejected (no recurring pain, state.sh show already surfaces the cached counts). No new scripts created; no diagnostics/README.md update required.
Repo hygiene: verified via diagnostics/repo-hygiene.sh --check (see close-out task below).

Retrospective Close-Out (after 01.R-HYGIENE + 01.R-DRY + 01.R-SIDE-LOGIC + 01.R-TEST-HYGIENE land)

Re-run /impl-hygiene-review with scope=active-work-arc — expect zero Critical/Major findings. Result: 0 Critical / 0 Major; 2 pre-existing minor/note findings filed as BUG-02-011 (infer/mod.rs 864-line BLOAT) and BUG-02-012 (ModuleChecker dual-constructor gap); 1 arc-introduced DRIFT (stale plan annotations in 3 test files) auto-fixed in-place.
Re-run /tpr-review on the combined diff — expect clean. Result: round 0 — codex 2 verified medium findings (side-logic leaks in infer/expr/mod.rs: template-literal iteration + Set-collect dispatch not routing-only); extracted infer_template_literal into format.rs and check_collect_method_call into collections.rs; dead re-exports of now-internal helpers pruned. Round 1 — both reviewers clean; dual-source consensus reached.
Update typeck.md §GN-3 if body_captures_outer semantics change substantively in 01.R-HYGIENE. Result: body_captures_outer semantics (outer_vars + conservative _ => true default) already current. Updated the rule to reflect the 01.R-DRY maybe_generalize SSOT (should_generalize = policy decision; maybe_generalize = applying the decision) — call sites now invoke maybe_generalize rather than inlining collect_outer_vars + if should_generalize { ... }.
Re-flip §01 status: in-progress → status: complete in frontmatter.
Update 00-overview.md Quick Reference row for §01 back to Complete.
Update 00-overview.md Implementation Sequence Phase 1 marker back to COMPLETE.
Refresh diagnostics/state.sh cache — handled by /commit-push Step 8 auto-refresh (--sha-only).
Commit via /commit-push.

Section 01: AST-based Value Restriction

01.1 Extract should_generalize SSOT helper

01.2 Migrate infer_block block-statement let site

01.3 Migrate infer_let (ExprKind::Let dispatch) site

01.4 Migrate sequences.rs try-block let site

01.R Third Party Review Findings

01.N Completion Checklist

Retrospective: Findings surfaced by §03.N /impl-hygiene-review (2026-04-18)

01.R-HYGIENE Retrospective: body_captures_outer soundness (F1+F7)

Invariant Anchoring (per CLAUDE.md §Invariant-Anchoring Before Test-Chasing)

Fix Plan (TDD Matrix Required — MANDATORY)

01.R-DRY Retrospective: algorithmic duplication (F4+F5)

F4: InferEngine constructor duplication

F5: should_generalize + generalize 3x duplication

Retrospective on 01.R-DRY itself

01.R-SIDE-LOGIC Retrospective: dispatch-module side logic (F2+F3)

Fix plan

Retrospective on 01.R-SIDE-LOGIC itself

01.R-TEST-HYGIENE Retrospective: test/import/name drift (F6+F8+F13+F14)

F6: parse_and_check test helper duplicate

F8: enter_scope vs enter_rank_scope inconsistency

F13: Test naming convention

F14: Glob re-exports in mod.rs

Retrospective on 01.R-TEST-HYGIENE itself

Retrospective Close-Out (after 01.R-HYGIENE + 01.R-DRY + 01.R-SIDE-LOGIC + 01.R-TEST-HYGIENE land)

01.1 Extract `should_generalize` SSOT helper

01.2 Migrate `infer_block` block-statement let site

01.3 Migrate `infer_let` (ExprKind::Let dispatch) site

01.4 Migrate `sequences.rs` try-block let site

Retrospective: Findings surfaced by §03.N `/impl-hygiene-review` (2026-04-18)