93%

Section 01: AST-based Value Restriction

Status: Complete (shipped 2026-04-14; 4 retrospectives R-HYGIENE / R-DRY / R-SIDE-LOGIC / R-TEST-HYGIENE closed 2026-04-18; frontmatter rewritten 2026-05-14 to reflect post-retrospective two-helper architecture) Goal: Replace unconditional generalization at 3 let-binding sites with a two-helper SSOT — should_generalize(arena, init, outer_vars) -> bool (policy decision SSOT) plus maybe_generalize(engine, arena, init, ty) -> Idx (apply-the-decision SSOT). maybe_generalize returns engine.generalize(ty) iff init is a direct non-capturing ExprKind::Lambda, otherwise returns ty unchanged. Preserves let-polymorphism for let id = x -> x while preventing empty-list element Vars from being prematurely generalized into Schemes AND preventing capturing lambdas (via any compound ExprKind child position) from being incorrectly generalized into schemes whose bound type variables include outer captures.

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 for the policy migration and 2026-04-18 for the four retrospectives R-HYGIENE / R-DRY / R-SIDE-LOGIC / R-TEST-HYGIENE)

  • Decision SSOT: pub(crate) fn should_generalize(arena, init, outer_vars) exists in blocks.rs:287 — one grep hit
  • Apply SSOT: pub(crate) fn maybe_generalize(engine, arena, init, ty) exists in blocks.rs:324 — one grep hit
  • All 3 let-binding generalization sites call maybe_generalize — blocks.rs:105, blocks.rs:191, sequences.rs:280 (grep verifiable: maybe_generalize\(engine returns exactly 3 hits)
  • body_captures_outer carries conservative _ => true default + exhaustive compound-shape descent (every ExprKind with child expressions walked; Ident honors outer_vars; SelfRef => true)
  • test_let_polymorphism_for_lambda_produces_function passes before and after; reverting the change breaks it
  • test_empty_list_let_binding_does_not_generalize_element_var passes
  • 5 non-capturing-shape negative pins pass (block-wrapped, aliased, conditional, infer_let path, infer_try_stmt path)
  • 7 capturing-lambda negative pins pass (Call.args, MethodCall.args, Block body, List, Map, Struct, Match arm) — added by 01.R.H
  • 3 should_generalize predicate pins pass (non-capturing-returns-true, capturing-returns-false, non-lambda-returns-false)
  • cargo test -p ori_types 840 passed / 0 failed in both debug and release (per 01.R.D F4 close-out)
  • ./test-all.sh shows 0 NEW failures over cache baseline (baseline 844 failures blocked-by §§09/§10/§11; umbrella Mission Success Criteria §139 in 00-overview.md owns the eventual failed:0 gate across interpreter + LLVM + AOT harness)
  • 0 pub(super) use *::* glob re-exports in infer/expr/mod.rs (01.R.T F14)
  • InferEngine::build private constructor + parity pin infer_engine_new_and_with_env_produce_identical_default_state (01.R.D F4)
  • Side-logic relocation to format.rs + collections.rs; mod.rs routing-only (01.R.S F2+F3)
  • All 3 let-binding sites use enter_rank_scope/exit_rank_scope (rank-only) — F8 unified infer_let to match infer_block + infer_try_stmt
  • typeck.md §GN-3 updated to reflect shipped two-helper architecture + conservative body_captures_outer direction

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 soundness direction (post-01.R.H flip): The shipped body_captures_outer function (blocks.rs:370+) carries the conservative direction — _ => true catch-all on the match-arm wildcard. Soundness contract: unknown / unhandled ExprKind shapes ASSUME capture (defaulting to false is the SOUNDNESS-VIOLATING direction because false negatives silently generalize capturing lambdas whose bound type variables include outer captures; downstream instantiation produces wrong types at every use site — a typeck-level soundness violation, NOT a detectable codegen failure). The pre-retrospective _ => false wildcard was the bug 01.R.H corrected; the AOT backend is NOT a safety net for capture analysis (a capturing lambda generalized to ∀α. α -> α where α includes the captured variable’s type is structurally well-typed at codegen — there is no unresolvable type variable to catch). False positives cost one missed polymorphic generalization; false negatives are type-soundness bugs. Every compound ExprKind with child expressions is walked exhaustively (Call.args slot — not just func; MethodCall.args — not just receiver; Block body — not skipped; List/Tuple elements, Map entries, Struct field values, Match arm guards + bodies, If cond + branches, Range start/end/step, For/Loop/Assign/WithCapability/Index/Break/Continue/Let/Await/Try/Unsafe/Cast/Ok/Err/Some/Field/Unary/Binary/Lambda descent with inner params; canonical-IR sugar variants CallNamed/MethodCallNamed/ListWithSpread/MapWithSpread/StructWithSpread/TemplateLiteral per types.md TL-4 — these forms appear at typeck time BEFORE ori_canon eliminates them). The Ident arm honors outer_vars: a bare identifier is a capture iff !param_names.contains(n) && outer_vars.contains(n) — where outer_vars is the lexically-bound subset of engine.env().names() (computed by collect_outer_vars/InferEngine::collect_lexical_outer via subtraction of engine.module_scope_snapshot). SelfRef => true because self inside a lambda body captures the enclosing method’s receiver. See typeck.md §GN-3 for the shipped invariant.

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: superseded by 01.R.D F5 (2026-04-18) — shipped call site at compiler_repo/compiler/ori_types/src/infer/expr/blocks.rs:105 is now maybe_generalize(engine, arena, *init, init_ty); should_generalize remains the policy SSOT consumed internally by maybe_generalize.

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.

  • TDD first — confirm test_empty_list_let_binding_does_not_generalize_element_var is a failing test stub BEFORE making any code change (the test must fail with current behavior to be a valid regression pin). Note: test already passes in unit-test context (confirmed during 01.1 close-out and re-verified here). Serves as semantic pin — must continue to pass after migration.

  • Replace the inlined L79-89 generalization block in infer_block with the if should_generalize(arena, *init) pattern shown above.

  • Verify test_let_polymorphism_for_lambda still passes (the lambda case must continue to produce a Tag::Scheme).

  • Verify test_empty_list_let_binding_does_not_generalize_element_var now passes (element Var is no longer wrapped in a Scheme for let xs = []).

  • Verify all tests pass in debug and release: timeout 150 cargo test -p ori_types and timeout 150 cargo test -p ori_types --release 802 tests pass, 0 failures in both debug and release.

  • Subsection close-out (01.2) — MANDATORY before starting 01.3:

    • 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.2: no tooling gaps. Straightforward single-Edit replacement of inlined logic with should_generalize() call. No diagnostic scripts or tracing needed — the change was mechanical and all 802 tests passed immediately. #[allow(dead_code)] removal was the only secondary change.
    • Repo hygiene check — diagnostics/repo-hygiene.sh --check clean (checked below).

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
    }
};

Note: superseded by 01.R.D F5 (2026-04-18) — shipped call site at compiler_repo/compiler/ori_types/src/infer/expr/blocks.rs:191 is now maybe_generalize(engine, arena, init, init_ty).

  • TDD first — add a targeted test test_let_expr_non_lambda_does_not_generalize to compiler/ori_types/src/infer/expr/tests.rs that exercises the ExprKind::Let path specifically (the ExprKind::Let case routes through infer_let, distinct from ExprKind::Block’s StmtKind::Let arm). This test must fail before the change and pass after. Confirmed: test FAILED before fix (bound type was Tag::Scheme), PASSES after fix.

  • Replace L167 (the unconditional engine.generalize(init_ty)) with the if should_generalize(arena, init) conditional shown above.

  • Verify test_let_polymorphism_for_lambda still passes (lambda via infer_let path).

  • Verify test_let_expr_non_lambda_does_not_generalize now passes.

  • Verify all tests pass in debug and release: timeout 150 cargo test -p ori_types and timeout 150 cargo test -p ori_types --release 803 tests pass, 0 failures in both debug and release.

  • Subsection close-out (01.3) — MANDATORY before starting 01.4:

    • 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.3: no tooling gaps. TDD cycle worked cleanly: test correctly failed before the fix (Tag::Scheme in env lookup via engine.env().lookup(name)) and passed after. The ExprKind::Let path has its own enter_scope()/exit_scope() which makes generalization effective in unit tests — good test infrastructure for catching the bug.
    • Repo hygiene check — diagnostics/repo-hygiene.sh --check clean (verified above, no changes since).

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: superseded by 01.R.D F5 (2026-04-18) — shipped call site at compiler_repo/compiler/ori_types/src/infer/expr/sequences.rs:280 is now maybe_generalize(engine, arena, *init, bound_ty); the unwrap-step contract landed inside maybe_generalize’s docstring per F5 close-out.

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.

  • TDD first — add test_try_block_let_non_lambda_does_not_generalize to compiler/ori_types/src/infer/expr/tests.rs (the shared test file for the expr module; sequences.rs is a flat file, not a directory, so there is no sequences/tests.rs). Test calls infer_try_stmt directly to exercise the try-block let path without scope exit hiding the binding.

  • Replace L247 (unconditional engine.generalize(bound_ty)) with the conditional shown above, noting that the argument to should_generalize is *init, not bound_ty.

  • Verify the import of should_generalize compiles (pub(super) use blocks::* in mod.rs already exposes it to sequences.rs when accessed via super::). Added explicit import in sequences.rs import list.

  • Verify test_let_polymorphism_for_lambda still passes (no regression in the primary lambda polymorphism guarantee).

  • Verify test_try_block_let_non_lambda_does_not_generalize now passes.

  • Verify the grep criterion: grep -n 'engine.generalize' compiler/ori_types/src/infer/expr/blocks.rs compiler/ori_types/src/infer/expr/sequences.rs returns exactly 3 hits, each immediately following an if should_generalize( line.

  • Verify all tests pass in debug and release: 804 tests pass, 0 failures in both debug and release.

  • Verify the full suite: timeout 150 ./test-all.sh — 15325 pass, 0 failures.

  • Subsection close-out (01.4) — MANDATORY before starting 01.R:

    • 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.4: no tooling gaps. The try-block test needed restructuring to call infer_try_stmt directly (try-block scope exit hides bindings), but this was a test-design issue, not a tooling gap. The grep criterion for verifying all 3 sites are migrated was effective.
    • Run /sync-claude on THIS subsection — 01.4 is the final migration subsection. Updated: - typeck.md §GN-3 — rewrote from “(target-only) all let-bindings generalizable” to shipped AST-based Value Restriction with should_generalize as SSOT. - typeck.md §EX-8 step 4 — added conditional generalization via GN-3. - typeck.md §BD-1 let x = e row — added “conditionally generalize per GN-3”. Verified clean (no update needed): - CLAUDE.md — no generalization claims found. - canon.md §4.2 — typed IR invariants unaffected (Value Restriction doesn’t introduce Vars; it prevents premature generalization). - docs/compiler/design/05-type-system/type-inference.md — describes the lambda case specifically, which is still correct.
    • Repo hygiene check — diagnostics/repo-hygiene.sh --check clean.

01.R Third Party Review Findings

  • [TPR-01-001-codex][high] section-02-validator-module.md:265 — GAP: Recurse into applied nominal types in the validator. Resolved: Valid finding, filed in Section 02’s scope. Section 02 must walk Tag::Applied arguments.
  • [TPR-01-002-codex][high] section-01-value-restriction.md:120 — GAP: body_captures_outer note said “over-approximation” / “safe direction” but the code is an under-approximation (unsafe direction). Resolved: Fixed on 2026-04-14. Corrected the note to accurately describe the under-approximation and the codegen safety net.
  • [TPR-01-003-codex][medium] section-05-test-matrix.md:121 — GAP: Missing negative pin for direct capturing lambda. Resolved: Fixed on 2026-04-14. Added test_capturing_lambda_does_not_generalize to 01.1 test stubs and 01.N completion checklist.
  • [TPR-01-004-codex][medium] section-03-bodies-pass-integration.md:255 — DRIFT: Placeholder span lookup in Section 03. Resolved: Valid finding, filed in Section 03’s scope. Section 03 must use ExprId::raw() as usize.
  • [TPR-01-005-codex][low] 00-overview.md:27 — DRIFT: Overview/index stale test paths. Resolved: Fixed on 2026-04-14. Updated overview L27 and L179 from blocks/tests.rs to tests.rs.
  • [TPR-01-001-gemini][medium] section-05-test-matrix.md:120 — Add negative pin tests to Section 05.1.1. Resolved: Valid finding, filed in Section 05’s scope. Section 05 must include the negative pin tests.
  • [TPR-01-002-gemini][medium] section-01-value-restriction.md:320 — Self-capture error rewriting DRY violation (3-site duplication adjacent to generalization). Resolved: Valid observation. The self-capture rewriting block is duplicated at 3 sites but is unchanged by this plan. Tracked as a follow-up: this is an existing impl-hygiene.md §Algorithmic DRY violation that should be addressed when Section 01’s should_generalize extraction proves the pattern works.
  • [TPR-01-006-codex][medium] compiler/ori_types/src/infer/expr/tests.rs:3532 — GAP: Missing positive lambda pins for infer_let and infer_try_stmt. Resolved: Fixed on 2026-04-14. Added test_let_expr_lambda_generalizes and test_try_block_let_lambda_generalizes to pin generalization IS preserved for non-capturing lambdas through both migrated paths.
  • [TPR-01-003-gemini][medium] compiler/ori_types/src/infer/expr/tests.rs:3098 — GAP: Missing positive semantic pins for lambda generalization in infer_let and infer_try_stmt. Resolved: Fixed on 2026-04-14. Same fix as [TPR-01-006-codex] (independent agreement — both reviewers flagged the same gap).
  • [TPR-01-004-gemini][low] compiler/ori_types/src/infer/expr/tests.rs:3017 — NAMING: should_generalize test names use wrong shape. Resolved: Fixed on 2026-04-14. Renamed 3 tests to <subject>_<scenario>_<expected> shape.
  • [TPR-01-005-gemini][low] .claude/rules/typeck.md:418 — DRIFT: EX-8 steps 3-4 ordering swapped vs implementation. Resolved: Fixed on 2026-04-14. Swapped steps 3 and 4 to match code: generalize at elevated rank, then exit scope.

01.N Completion Checklist

  • Single pub(super) fn should_generalize exists in blocks.rs — verified: exactly 1 hit
  • All 3 engine.generalize calls gated by if should_generalize(...) — verified: exactly 3 hits
  • No inlined Lambda-detection logic duplicating should_generalize’s behavior remains — verified: ExprKind::Lambda in blocks.rs appears only at self-capture detection, should_generalize’s body, and body_captures_outer
  • test_let_polymorphism_for_lambda passes in compiler/ori_types/src/infer/expr/tests.rs
  • test_empty_list_let_binding_does_not_generalize_element_var passes
  • test_let_expr_non_lambda_does_not_generalize passes
  • test_try_block_let_non_lambda_does_not_generalize passes
  • Negative pin tests for intentionally monomorphic patterns pass (all in tests.rs):
    • test_block_wrapped_lambda_does_not_generalize
    • test_variable_alias_does_not_generalize
    • test_conditional_lambda_does_not_generalize
    • test_capturing_lambda_does_not_generalize
  • All tests live in compiler/ori_types/src/infer/expr/tests.rs — no blocks/tests.rs or sequences/tests.rs created
  • Plan annotation cleanup: 0 stale-resolved annotations. 8 active-scaffolding are from active plans (expected). # Plan doc comment in should_generalize is intentional scaffolding for Section 07 close-out.
  • All intermediate subsection close-out tasks complete (01.1–01.4)
  • Plan sync — plan metadata updated (details below after overview/index updates)
  • timeout 150 ./test-all.sh green (debug build) — 15325 pass, 0 fail
  • timeout 150 cargo test --release -p ori_types green (release build) — 804 pass
  • timeout 150 ./clippy-all.sh clean
  • /tpr-review passed (final, full-section) — Round 1: 4 findings (codex/gemini independently flagged same matrix gap + 2 minor naming/doc drift). Round 2: clean (0 actionable). Both reviewers verified the fixes against actual code.
  • /impl-hygiene-review passed — 4 NAMING findings on pre-existing weak test names resolved in-pass (renamed). 4 BLOAT findings on pre-existing nesting/length filed as BUG-02-005 (architectural refactor, scope exceeds Value Restriction migration). SSOT verified: should_generalize is the single canonical home for the generalization decision.
  • /improve-tooling section-close sweep — all 4 subsections have documented retrospectives (01.1: no gaps; 01.2: no gaps; 01.3: no gaps; 01.4: no gaps). No cross-subsection patterns required new tooling — all subsections were mechanical single-function migrations with identical workflows. Section-close sweep: per-subsection retrospectives covered everything; no cross-subsection patterns required new tooling.
  • /sync-claude section-close doc sync — completed during 01.4 close-out:
    • typeck.md §GN-3 — updated from “(target-only) all generalizable” to shipped Value Restriction
    • typeck.md §EX-8 step 4 — added conditional generalization via GN-3
    • typeck.md §BD-1 — added conditional generalization note
    • CLAUDE.md — no generalization claims found (clean)
    • canon.md §4.2 — typed IR invariants unaffected (clean)
    • docs/compiler/design/05-type-system/ — lambda example still correct (clean)
  • Repo hygiene check — diagnostics/repo-hygiene.sh --check clean

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.H 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)

  1. 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.
  2. 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.
  3. 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)

  • TDD matrix first — write failing tests before any code change:
    • test_capturing_lambda_via_call_arg_does_not_generalize — capture via Call args
    • test_capturing_lambda_via_method_arg_does_not_generalize — capture via MethodCall args
    • test_capturing_lambda_via_block_does_not_generalize — capture via Block body
    • test_capturing_lambda_via_list_literal_does_not_generalize — capture via List
    • test_capturing_lambda_via_map_literal_does_not_generalize — capture via Map
    • test_capturing_lambda_via_struct_literal_does_not_generalize — capture via Struct
    • test_capturing_lambda_via_match_arm_does_not_generalize — capture via Match arm body
    • Verified all 7 tests FAILED pre-fix (same panic at assert_lambda_with_body_does_not_generalize), confirming the _ => false wildcard bug.
  • Architectural fix — flipped the conservative default and enumerated leaf arms in body_captures_outer:
    • Changed _ => false to _ => true — unknown shapes assume capture.
    • Explicit false-returning arms for verified leaf ExprKinds (literals, Unit, None, HashLength, Const, FunctionRef, TemplateFull, Error).
    • Complete recursion for every compound ExprKind with child expressions: Call walks func + args (previously only walked func); MethodCall walks receiver + args; plus Block, List, Tuple, Map, Struct, Match, If, Range, For, Loop, Assign, WithCapability, Index, Break, Continue, Let, Await, Try, Unsafe, Cast, Ok, Err, Some, Field, Unary, Binary, Lambda (descends with inner params).
    • Canonical-IR sugar variants also walked (CallNamed, MethodCallNamed, ListWithSpread, MapWithSpread, StructWithSpread, TemplateLiteral) — the sugar forms appear at typeck time (before ori_canon eliminates them), so they must be decoded here for the Value Restriction check to be complete.
    • SelfRef => true — self inside a lambda body captures the enclosing method’s receiver.
  • Ident arm now honors outer_vars — the architectural key insight. A bare identifier is a capture iff !param_names.contains(n) && outer_vars.contains(n). outer_vars is the set of LEXICALLY-bound names (function params, local lets, loop/match pattern binders), NOT module-level references (prelude, imports, same-module signatures). This is critical: without it, a lambda like xs -> len(collection: xs) would falsely flag len as a capture and block generalization.
  • Threaded outer_vars through the capture-analysis signature — should_generalize(arena, init, outer_vars) + body_captures_outer(arena, id, param_names, outer_vars). All 3 let-binding call sites (infer_block, infer_let, infer_try_stmt) now call collect_outer_vars(engine) before should_generalize.
  • InferEngine.module_scope_snapshot: Option<FxHashSet<Name>> — new field populated at engine creation time via set_module_scope_snapshot, called from ModuleChecker::create_engine_with_env. Captures the module-scope name set (prelude imports via import_env, same-module function signatures, test names) before any function-body lexical binder has run. engine.collect_lexical_outer() subtracts this snapshot from the current env’s names() to yield exactly the lexical-outer subset.
  • Update docstring — body_captures_outer’s docstring now correctly describes the conservative-direction invariant (“false negative is a type-soundness violation; false positive costs one missed polymorphic generalization”); the contradictory inline “codegen will catch it” comment was removed.
  • Verify all 7 new tests PASS — all 7 test_capturing_lambda_via_* pass; test_should_generalize_capturing_lambda_returns_false + test_should_generalize_non_capturing_lambda_returns_true also pass with the new signature (updated to pass appropriate outer_vars sets via the outer(&[...]) helper).
  • Verify all pre-existing tests STILL pass — test_let_polymorphism_for_lambda_produces_function passes unchanged; full ori_types suite: 839 passed / 0 failed. Full test-all.sh: 16381 passed / 844 failed / 160 skipped — exactly +7 passes over cache baseline (the 7 new tests) with 0 new failures.
  • Regression-check on tests/spec/inference/generalized_var_resolution.ori — a 6-test file that hit the lambda-body-CallNamed path (xs -> len(collection: xs)). Pre-fix: 6 pass. First iteration of the fix: 6 fail (false positive — len was being flagged as a capture because it was reachable via env.names() through import_env’s parent chain). Final fix with module_scope_snapshot subtraction: 6 pass.
  • Dual-execution verification — DEFERRED to Retrospective Close-Out - [ ] “Re-run /tpr-review on the combined diff” + “Re-run /impl-hygiene-review with scope=active-work-arc” (anchors in §Retrospective Close-Out at end of this section). The fix is purely a typeck-phase Tag::Scheme assignment change; it does not alter eval or LLVM backend semantics on any program that already type-checked, and the +7 new tests are #[test] Rust units that already exercise the in-process path. Dual-exec parity coverage will be re-validated once all 4 retrospectives land and the combined reviewer re-run executes.
  • Update typeck.md §GN-3 — amended to reflect the 3-arg should_generalize signature and the outer_vars lexical-outer set.
  • /tpr-review clean — DEFERRED to Retrospective Close-Out - [ ] “Re-run /tpr-review on the combined diff — expect clean”. Per-subsection review would be wasted reviewer cycles because the Close-Out batches review across 01.R.H + 01.R.D + 01.R.S + 01.R.T in a single pass.
  • /impl-hygiene-review clean — DEFERRED to Retrospective Close-Out - [ ] “Re-run /impl-hygiene-review with scope=active-work-arc — expect zero Critical/Major findings”. Same batching rationale.

01.R.D 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.H; 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.H 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.D: 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.H + 01.R.D + 01.R.S + 01.R.T — same rationale as §01.R.H’s deferral).

Retrospective on 01.R.D itself

  • /improve-tooling retrospective (01.R.D): 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.S 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.T 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.H + 01.R.D 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.H / §01.R.D — 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.S: 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.S itself

  • /improve-tooling retrospective (01.R.S): 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.T 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.T: 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.T itself

  • /improve-tooling retrospective (01.R.T): 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.H + 01.R.D + 01.R.S + 01.R.T 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.H. Result: body_captures_outer semantics (outer_vars + conservative _ => true default) already current. Updated the rule to reflect the 01.R.D 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.

HISTORY

  • 2026-05-14 — Frontmatter success_criteria: + body narrative rewrite to reflect post-retrospective shipped architecture (/review-plan Step 5 editor re-review per user “substantial changes since this plan was last created” directive). Codex + Gemini + Opencode reviewers independently flagged convergent drift: pre-rewrite success_criteria: described pre-retrospective design (pub(super) fn should_generalize(arena, init) -> bool 2-arg, three inline if should_generalize(...) gates) while shipped code at compiler/ori_types/src/infer/expr/blocks.rs:287 carries the post-retrospective two-helper architecture: pub(crate) fn should_generalize(arena, init, outer_vars: &FxHashSet<Name>) (3-arg, pub(crate) not pub(super)) + pub(crate) fn maybe_generalize(engine, arena, init, ty) -> Idx (apply SSOT) with 3 call sites at blocks.rs:105 (infer_block), blocks.rs:191 (infer_let), sequences.rs:280 (infer_try_stmt) invoking maybe_generalize directly vs inlining. Rewrites applied: (1) frontmatter goal: + success_criteria: array replaced with 16 criteria covering decision SSOT, apply SSOT, 3 call sites, body_captures_outer conservative _ => true direction, outer_vars lexical-vs-module-scope separation, positive lambda pins (3), non-capturing-shape negative pins (5), capturing-lambda negative pins (7 from 01.R.H), should_generalize predicate pins (3), ori_types unit matrix gate (840/0 debug+release at section close), pub(super) use *::* glob-elimination (01.R.T F14), InferEngine::build constructor + parity pin (01.R.D F4), side-logic relocation to format.rs + collections.rs (01.R.S F2+F3), enter_rank_scope unification (01.R.T F8), typeck.md §GN-3 sync. (2) Body line 58 **Status:** Not Started → **Status:** Complete (shipped 2026-04-14; 4 retrospectives R-HYGIENE / R-DRY / R-SIDE-LOGIC / R-TEST-HYGIENE closed 2026-04-18; frontmatter rewritten 2026-05-14) matching status: complete frontmatter. (3) Body **Success Criteria:** checkbox block expanded from 6 to 16 items mirroring frontmatter. (4) Body **Note on body_captures_outer completeness:** rewritten from pre-retrospective under-approximation + AOT-codegen-safety-net narrative (INVERTED soundness direction — the AOT backend is NOT a safety net for capture analysis; a capturing lambda generalized to a polymorphic scheme is structurally well-typed at codegen) to post-retrospective conservative _ => true + soundness-contract narrative (false positives = missed polymorphic generalization; false negatives = type-soundness violation at every instantiation; exhaustive compound-shape descent covers Call.args, MethodCall.args, Block body, List/Map/Struct/Match/If/Range/For/Loop/Assign/WithCapability/Index/Break/Continue/Let/Await/Try/Unsafe/Cast/Ok/Err/Some/Field/Unary/Binary/Lambda + canonical-IR sugar variants CallNamed/MethodCallNamed/ListWithSpread/MapWithSpread/StructWithSpread/TemplateLiteral; Ident arm honors outer_vars; SelfRef => true). (5) Test-gate scope split: §01 owns the ori_types unit matrix (cargo test -p ori_types 840/0 debug + release at section close); umbrella Mission Success Criteria §139 in 00-overview.md owns the eventual ./test-all.sh failed: 0 gate across interpreter + LLVM + AOT harness; §01 close-out’s recorded 16382 passed / 844 failed / 160 skipped baseline blocked-by §§09/§10/§11 typeck body-inference / dispatch / fallback gaps absorbed into this plan per 2026-04-23 scope expansion (00-overview.md:120-135), NOT regressions caused by §01.

  • 2026-05-14 — STRUCTURE:section-not-promoted finding disposition (opencode-only judgment call; routing.md §4 promotion mechanics). Audit + opencode reviewer flagged §01 at 837 lines / 122 top-level checked items vs routing.md §5 cap 20, with 4 retrospective subsections (01.R.H / 01.R.D / 01.R.S / 01.R.T) each meeting the routing.md §4 independence test (own success_criteria, own deliverable, cold-pickup-ready, cross-references work outside parent’s scope). Promotion cure per routing.md §4: lift each ## 01.R-* into section-01[A-Z]-<topic>.md siblings (e.g., section-01A-body-captures-outer-soundness.md, section-01B-maybe-generalize-and-constructor-dry.md, section-01C-side-logic-relocation.md, section-01D-test-helper-hygiene.md), update parent’s sections: array, update 00-overview.md roster, update depends_on: graph for §02/§03/§09 consumers that reference §01.R-* anchors, run scripts/intel-query.sh dag-ascii typeck-inference-completeness post-promotion + diff against pre-promotion DAG. Disposition rationale per Step 5 editor judgment: (a) §01 is CLOSED + REVIEWED (status: complete, reviewed: true, third_party_review.status: resolved 2026-04-18); the retrospectives themselves are CLOSED + REVIEWED; promotion of a fully-shipped section would touch the DAG graph for sibling sections (§02 validator, §03 bodies-pass-integration, §09 body-inference gaps) that already reference §01 as a unit and would require coherent cross-section re-anchoring without behavioral change. (b) audit-summary.json finding text explicitly classifies this as “promotion is moot post-close; informational for §01 historical record, signal for future authoring” — halt_gating: false. (c) Per routing.md §4 “default-of-least-resistance correction” option 1 (split into letter-suffix siblings) is the canonical compliance path for OPEN sections meeting the trigger; for CLOSED sections, the cure surfaces as a known-state acknowledgment rather than a live promotion (compaction option 3 cannot be applied without information loss to the historical retrospective record per state-discipline.md §7 HISTORY block conventions). (d) The promotion would be a behavioral no-op against the shipped compiler: all 4 retrospectives ship the same code as today regardless of which section file holds the documentation. Concrete deferral anchor per CLAUDE.md §ALL Deferrals MUST Have Implementation Anchors: this finding is tracked as STRUCTURE:section-not-promoted against §01 and resolves via a future plan-corpus structural-migration pass (governed by routing.md §4’s scripts/plan_corpus/promote_subsection.py tool — delivered by plans/skill-ecosystem-coherence/ §12 per routing.md §4 Tool line) that would lift the 4 retrospectives en bloc, re-validate the cross-section DAG, AND update the 00-overview.md Implementation Sequence Phase 1 marker. Until that migration tool ships AND covers shipped-and-reviewed sections, §01 stays single-file. No new - [ ] item added to §01 body because §01 is status: complete, reviewed: true — adding an item would violate STRUCTURE:unchecked-items-under-complete. Anchor lives in this HISTORY entry + plans/skill-ecosystem-coherence/ §12 (promote_subsection.py migration tool). Subsection ordering per opencode finding 3: F5 (DRY maybe_generalize extraction) consumed the outer_vars parameter threaded through by F1+F7 (R-HYGIENE) — actual code-shipping order was R-HYGIENE → R-DRY → R-SIDE-LOGIC → R-TEST-HYGIENE per the retrospective close-out commit sequence. The implicit ordering is recorded in this HISTORY entry rather than via subsection_depends_on: frontmatter (which routing.md §5 schema-v2 fields target NEW sections; back-filling closed sections risks DAG-edge drift that would surface at next /verify-roadmap run without behavioral cure).