Section 03: Bodies-Pass Integration

Resume context (2026-04-16): 03.0 complete and committed (e7d7e073 — BLOAT-gate split + build_method_sig helper). 03.1–03.4 were previously attempted and reverted because the pragmatic gate required to make tests pass was identified as INVERTED-TDD:gated-deliverable. Root cause resolved: BUG-02-008 (30695c0f, cf6a497d — scheme-var exemption in validator) and BUG-02-009 (fcb68f04, eb6ca3ce — fold/rfold accumulator param unification) are now fixed with full plan-section rigor. Fix sections: bug-tracker/plans/completed/BUG-02-008/, bug-tracker/plans/completed/BUG-02-009/. Section 03 is unblocked.

Status: In Progress Goal: Wire validate_body_types() (created in Section 02) into all 4 bodies-pass call sites so that every function, test, impl method, and def-impl method body surfaces unresolved Tag::Vars as E2005 diagnostics before handing typed IR to the next phase — enforcing the typeck.md PC-2 output contract at the producer boundary.

Success Criteria:

All 4 bodies-pass sites invoke the validator — verified EITHER by grep -rn 'validate_body_types' compiler/ori_types/src/check/bodies/ returning exactly 4 matches (inline shape, one per site across functions.rs and impls.rs) OR by the helper-extracted shape: (a) one validate_body_types(...) call inside run_validator, (b) four run_validator(...) call sites across functions.rs and impls.rs (one per body pass: check_function, check_test, check_impl_method, check_def_impl_method).
Rust integration test asserts BUG-04-074 repro type-checks cleanly end-to-end (unification + BUG-04-084 defaulting jointly resolve the empty-list element type); validator rejection-path coverage (firing E2005 on surviving Tag::Var) is retained via the unannotated_param / ungeneralizable_body_lambda tests across the four body passes
Annotated repro (let ages: [int] = []) compiles clean AND produces exit 0 via both interpreter (ori run) and AOT (ori build) with parity verified by diagnostics/dual-exec-verify.sh
test_let_polymorphism_for_lambda continues to pass (no regression from Section 01)
Known-failing spec tests between this section and 06.2 are documented; no undocumented new failures

Context: BUG-04-074’s root failure mode was exactly the typeck.md PC-2 contract gap: check_function and its three sibling call sites produced typed IR containing unbound Tag::Var (empty-list element types) without emitting any diagnostic. The IR propagated through canonicalization, ARC lowering, AIMS, and into LLVM codegen where it surfaced as an “unresolved type variable at codegen” error in type_info/store.rs:341-363 — a consumer-side symptom of a producer-side omission. Sections 01 and 02 respectively (a) stopped the premature generalization of empty-list element vars, and (b) built the validate_body_types() function that can detect and report any surviving Tag::Var. This section closes the loop: it threads the call into every body-checking exit path so the validator actually runs on every function body. Per impl-hygiene.md §Narrow the Front, all 4 sites are wired together — partial integration (some sites calling the validator, others not) leaves a gap where E2005 doesn’t fire in impl methods or def-impl methods, which are equally capable of producing unresolved vars.

The integration is mechanically simple — the same 4-line call pattern at each site — but the placement is load-bearing: the call must happen AFTER engine.take_expr_types() has already extracted the populated map from the engine but BEFORE checker.push_error() drains that data into the checker’s error accumulator. Reading the source reveals that each call site already extracts the 6-tuple (expr_types, errors, warnings, ...) from the inference closure, then iterates over errors to push them. The validator call slots between the extraction and the push — or more precisely it operates on the extracted expr_types and its own errors are pushed alongside the engine’s existing errors.

Round 5 research verified:

c.pool() is ModuleChecker::pool(&self) -> &Pool at accessors.rs:72-74
c.arena() is ModuleChecker::arena(&self) -> &'a ExprArena at accessors.rs:18-21
c.push_error(TypeCheckError) is the canonical accumulator path
engine.take_expr_types() returns FxHashMap<ExprIndex, Idx> (confirmed at compiler/ori_types/src/infer/mod.rs:56)
ExprIndex is a usize type alias (not a newtype), so span_of must map usize → Span

Reference implementations:

Ori compiler/ori_types/src/check/bodies/mod.rs (lines 39-167 for check_function, 175-253 for check_test, 319-440 for check_impl_method, 462-539 for check_def_impl_method) — the exact 4 call sites being modified. Each follows the same pattern: run inference inside a scope closure, extract (expr_types, errors, warnings, ...) as a tuple, then iterate the tuple’s members to push results onto checker.
Rust rustc_hir_typeck/fn_ctxt/checks.rs (in ~/projects/reference_repos/lang_repos/rust/) — check_fn() performs a wfcheck::check_fn_or_closure() call AFTER body inference concludes, inside the same FnCtxt scope that holds the inferred types. The diagnostic is accumulated into the shared diagnostic engine (analogous to checker.push_error()), not returned. Note: this is a path in the Rust reference repo, NOT in the Ori codebase.
Swift lib/Sema/TypeCheckDecl.cpp — checkFunctionBody() triggers a series of post-body checkers (definite initialization, effect checking, @discardableResult warns) after typeCheckFunctionBodyAtOffset. Each checker runs against the already-typed body, emitting into the engine’s diagnostic accumulator.

Depends on:

Section 01 — provides the Value Restriction policy (should_generalize) so that lambda-typed bindings are still generalized (they do not produce Tag::Vars that the validator would spuriously flag) while empty-list element vars remain as Unbound Tag::Var after inference.
Section 02 — provides ori_types::check::validators::validate_body_types() with the shipped six-parameter signature (per §02.1 + §02.R TPR-02-R3-003):
```
pub fn validate_body_types(
    pool: &Pool,
    expr_types: &FxHashMap<ExprIndex, Idx>,
    sig: &FunctionSig,
    sig_span: Span,
    span_of: &dyn Fn(ExprIndex) -> Span,
    errors: &mut Vec<TypeCheckError>,
)
```
The added sig: &FunctionSig + sig_span: Span parameters extend validator scope to the signature (param_types + return_type) per typeck.md §CK-4 hand-off contract — unannotated params/returns ship from the Signatures pass as fresh Tag::Var and the validator catches any that survive body inference. Module wiring (per §02.3 + §02.R TPR-02-R3-003): check/mod.rs declares pub(crate) mod validators; (private to the crate, not pub mod); lib.rs carries a narrow re-export pub use check::validators::validate_body_types; without promoting mod check to pub mod check (keeping the entire internal check-module layout out of the crate’s public API).

What this section uses from each dependency:

From Section 01: the guarantee that should_generalize gates all 3 engine.generalize() calls, so the only surviving Tag::Vars entering the validator are genuinely ambiguous (unannotated non-lambda initializers, including empty-list elements). Without Section 01, the validator would also flag legitimate lambda polymorphism (let id = x -> x produces a Tag::Scheme in the expr_types map, but the body Var for the param is resolved at the call site; without Value Restriction the element Var would be in a Scheme instead, suppressing the flag).
From Section 02: the validate_body_types function itself, imported via use crate::check::validators::validate_body_types; at the top of check/bodies/mod.rs. Also Section 02’s span_of closure contract: the function expects a &dyn Fn(ExprIndex) -> Span. Each call site must supply a span-lookup closure; the arena provides the span via arena.get_expr(ExprId).span but the mapping from ExprIndex (a usize) to ExprId requires the expr_types map to be consulted together with the arena.

Intelligence Reconnaissance

Queries run 2026-04-15:

scripts/intel-query.sh --human ori-inference — checked; graph available. Key symbols: check_function_bodies, check_impl_bodies, check_def_impl_bodies, validate_body_types (Section 02), ModuleChecker, InferEngine, FunctionSig.
scripts/intel-query.sh --human file-symbols "check/bodies" --repo ori — confirmed: bodies/mod.rs houses all 4 pass functions; no existing call to validate_body_types at any site (pre-Section-03 state).
scripts/intel-query.sh --human callers "validate_body_types" --repo ori — 0 callers (Section 02 just added the function; no call sites yet — this section creates them).
scripts/intel-query.sh --human similar "check_fn wfcheck" --repo rust --limit 5 — Rust rustc_hir_typeck::check_fn + wfcheck::check_fn_or_closure is the reference pattern: post-body validation call after inference completes, errors pushed to shared accumulator. Confirms the 4-site uniform insertion approach.

Results summary (≤500 chars) [ori]: validate_body_types at check/validators/mod.rs has 0 callers — this section creates all 4. Blast radius confined to check/bodies/ submodule (4 functions). FunctionSig availability differs per site: check_function/check_test have pre-collected sigs from Pass 1; check_impl_method constructs sig AFTER inference; check_def_impl_method never constructs one. Sites 03.3/03.4 require sig construction before the inference closure. Cross-repo: Rust wfcheck post-body pattern is the canonical prior art. [ori]

03.0 Prerequisite: split `bodies/mod.rs` (BLOAT gate)

File: compiler/ori_types/src/check/bodies/mod.rs Why this must happen first: bodies/mod.rs is currently 543 lines, already 43 lines over the 500-line limit (impl-hygiene.md §File Organization). Adding validator calls at all 4 sites will add approximately 60 more lines, pushing it to ~600. Per the “Split when touching” rule, any touch to a file over 500 lines requires splitting first.

Split plan:

Extract into two sibling files, keeping bodies/mod.rs as a thin re-export hub:

compiler/ori_types/src/check/bodies/functions.rs — owns check_function_bodies, check_test_bodies, the private helpers check_function and check_test, and their supporting locals (the top-level function Pass 2–3 group, lines 39–253). Each pub fn check_*_bodies lives in this file (the split file is the canonical home — the function is NOT duplicated in mod.rs).
compiler/ori_types/src/check/bodies/impls.rs — owns check_impl_bodies, check_def_impl_bodies, the private helpers check_impl_method, check_def_impl_method, and check_def_impl_block, plus the build_method_sig helper (the impl/def-impl method Pass 4–5 group, lines 260–540). Each pub fn check_*_bodies lives in this file (the split file is the canonical home — the function is NOT duplicated in mod.rs).
compiler/ori_types/src/check/bodies/mod.rs — after the split, mod.rs declares the submodules (pub mod functions;, pub mod impls;), re-exports the four public pass-dispatch functions via pub use functions::{check_function_bodies, check_test_bodies}; and pub use impls::{check_impl_bodies, check_def_impl_bodies};, houses any genuinely shared private helpers that both submodules use (e.g., resolve_type_with_self, resolve_parsed_type_simple, check_expr wrapper) if they cannot cleanly move to one submodule, and carries the #[cfg(test)] mod tests; declaration. Target: under 100 lines. Callers of check::bodies::check_impl_bodies / etc. continue to resolve through the pub use re-export without changing import paths. Rationale: one canonical home per function (SSOT per impl-hygiene.md §SSOT) — the function body lives in exactly one file; mod.rs is the re-export index, not a second definition.
compiler/ori_types/src/check/bodies/tests.rs — the existing sibling (unchanged by this split).

The private resolve_type_with_self, resolve_parsed_type_simple, check_expr, and other internal helpers shared between the two groups stay in mod.rs or move to a shared bodies/helpers.rs submodule (whichever keeps the split cleaner).

Why this is not optional: The impl-hygiene.md §BLOAT finding category (“file exceeds limits, mixes responsibilities, lacks submodule structure”) is a Minor finding under normal review, but the “Split when touching” rule elevates it to a gate: touching an over-limit file without splitting is itself a violation. Proceeding with 03.1–03.4 while bodies/mod.rs is over-limit would add a hygiene finding that must then be addressed in the TPR. Splitting first eliminates that finding.

Tasks:

Split bodies/mod.rs into functions.rs + impls.rs per the plan above
Verify cargo c compiles clean (no regressions from the split)
Verify timeout 150 cargo test -p ori_types passes clean (820 tests pass)
Each of the 3 resulting files (mod.rs, functions.rs, impls.rs) is under 500 lines (42 / 232 / 326)
Commit this split as its own commit via /commit-push before proceeding to 03.1 (combined with helper extraction per autonomous-mode pacing)

Algorithmic DRY — extract build_method_sig helper (per impl-hygiene.md §Algorithmic DRY):

The FunctionSig construction block (15+ lines, building param_names, param_defaults, required_params, param_hashes, return_hash, and the full struct literal) is structurally identical between check_impl_method (03.3) and check_def_impl_method (03.4). Four or more call sites of the same algorithm is a missing abstraction. Extract a helper before wiring:

/// Build a FunctionSig from the resolved method parameters and return type.
/// Used by check_impl_method and check_def_impl_method to construct the sig
/// early enough for validate_body_types coverage of param/return Tag::Var positions.
///
/// Note the `type_params: &[Name]` parameter type — `FunctionSig.type_params` is
/// `Vec<Name>` in the shipped struct (see `compiler/ori_types/src/output/mod.rs:378`:
/// `pub type_params: Vec<Name>`). The helper accepts `&[Name]` to match that shape;
/// the caller already has `type_params: &[Name]` in scope (e.g. `check_impl_method`
/// receives `type_params: &[Name]` at `check/bodies/mod.rs:320-325`). Do NOT use
/// a `&[TypeParam]` parameter — `TypeParam` is the AST-level node, not the
/// signature-level identifier, and would not compile against the struct field type.
fn build_method_sig(
    method_name: Name,
    params: &[Param],
    param_types: Vec<Idx>,
    return_type: Idx,
    type_params: &[Name],
    pool: &Pool,
) -> FunctionSig {
    let param_names: Vec<Name> = params.iter().map(|p| p.name).collect();
    let param_defaults: Vec<Option<ExprId>> = params.iter().map(|p| p.default).collect();
    let required_params = param_defaults.iter().filter(|d| d.is_none()).count();
    let param_hashes: Vec<u64> = param_types.iter().map(|&idx| pool.hash(idx)).collect();
    let return_hash = pool.hash(return_type);
    FunctionSig {
        name: method_name,
        type_params: type_params.to_vec(),
        const_params: vec![],
        param_names,
        param_types,
        return_type,
        capabilities: vec![],
        is_public: false,
        is_test: false,
        is_main: false,
        is_fbip: false,
        type_param_bounds: vec![],
        where_clauses: vec![],
        generic_param_mapping: vec![],
        scheme_var_ids: vec![],
        required_params,
        param_defaults,
        param_hashes,
        return_hash,
    }
}

Place this helper in bodies/impls.rs (private to the module) and call it from both check_impl_method and check_def_impl_method. Verify the FunctionSig field list against the actual struct definition before copying — the struct may gain or lose fields between now and implementation.

Extract build_method_sig helper into bodies/impls.rs BEFORE wiring 03.3/03.4 (signature (Name, &[Param], Vec<Idx>, Idx, &[Name], &Pool) -> FunctionSig per TPR-03-003-codex)
Commit the helper extraction as its own commit (separate from the split commit) — combined with the split commit per autonomous-mode pacing; both are BLOAT-gate prerequisites

03.1 Wire validator into `check_function`

File: compiler/ori_types/src/check/bodies/mod.rs Function: check_function (line 46–167) Insertion point: After the with_function_scope closure completes and the 6-tuple is destructured (line 148), immediately before the for (expr_index, ty) in expr_types loop that stores expression types into the checker (line 151). The validator runs on the local expr_types variable from the extraction before the types are forwarded into the checker’s module-wide map.

TDD — write failing test FIRST:

Before changing production code, add an integration test in compiler/ori_types/src/check/bodies/tests.rs (create the sibling if it doesn’t exist — the existing #[cfg(test)] mod tests; declaration at line 542 of bodies/mod.rs already covers this):

/// Regression: unannotated empty list binding with no element-constraining use
/// should produce E2005 (AmbiguousType) at typeck, not at codegen.
///
/// See: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md
#[test]
fn check_function_with_unannotated_empty_list_emits_ambiguous_type() {
    // Build: @main () -> int = { let ages = []; if ages.len() == 1 then 0 else 1 }
    // Expected: TypeCheckError with code E2005 (AmbiguousType) for the `ages` binding.
    // The test exercises check_function (Pass 2 per CK-1).
    //
    // Before 03.1 implementation: test fails (no E2005, or codegen-path error instead).
    // After 03.1: test passes.
    let (result, _interner) = parse_and_check(
        "@main () -> int = { let ages = []; if ages.len() == 1 then 0 else 1 }",
    );
    assert!(
        result.typed.errors.iter().any(|e| matches!(e.kind, TypeErrorKind::AmbiguousType { .. })),
        "expected E2005 AmbiguousType, got: {:?}",
        result.typed.errors
    );
}

Use the parse_and_check helper from compiler/ori_types/src/check/api/tests.rs — the verified working pattern:

fn parse_and_check(source: &str) -> (TypeCheckResult, StringInterner) {
    let interner = StringInterner::new();
    let tokens = lex(source, &interner);
    let parsed = parse(&tokens, &interner);
    assert!(parsed.errors.is_empty(), "parse errors: {:?}", parsed.errors);
    let result = check_module(&parsed.module, &parsed.arena, &interner);
    (result, interner)
}

Errors are accessed as &e.kind (public field), not e.kind() (no such method exists) — confirmed at compiler/ori_types/src/check/integration_tests.rs::error_kinds().

Implementation — before/after diff:

The call pattern inserts between the 6-tuple extraction (line 148 closing });) and the for (expr_index, ty) in expr_types storage loop (line 151).

Before (abridged, lines 148-157):

        });  // closes with_function_scope

    // Store expression types
    for (expr_index, ty) in expr_types {
        checker.store_expr_type(expr_index, ty);
    }

    // Store errors and warnings
    for error in errors {
        checker.push_error(error);
    }

After (the insertion point is the blank line before “Store expression types”):

        });  // closes with_function_scope

    // Validate PC-2 contract: no unbound Tag::Var in body expr_types
    // OR in the body's FunctionSig (param_types + return_type).
    // Runs after inference (expr_types fully populated) and before the types
    // are forwarded to the module-checker's map, so errors flow through the
    // normal push_error accumulator alongside inference errors.
    // Spec: docs/ori_lang/v2026/spec/14-expressions.md:1224-1228
    // Plan: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.1
    {
        let arena = checker.arena();
        let pool = checker.pool();
        let sig_span = func.span; // Function declaration span (func.span, NOT fn_decl.expr_id)
        let mut validation_errors = Vec::new();
        crate::check::validators::validate_body_types(
            pool,
            &expr_types,
            &sig,            // &FunctionSig from signatures pass (pass by reference)
            sig_span,        // function declaration span for sig-origin diagnostics
            &|expr_index| {
                // ExprIndex is a usize alias for ExprId.raw() — the InferEngine
                // records (ExprIndex, Idx) pairs keyed by the ExprId's raw u32
                // value (verified at compiler/ori_types/src/infer/mod.rs:56).
                // Convert back: ExprId::new(expr_index as u32).
                arena.get_expr(ori_ir::ExprId::new(expr_index as u32)).span
            },
            &mut validation_errors,
        );
        for err in validation_errors {
            checker.push_error(err);
        }
    }

    // Store expression types
    for (expr_index, ty) in expr_types {
        checker.store_expr_type(expr_index, ty);
    }

    // Store errors and warnings
    for error in errors {
        checker.push_error(error);
    }

Span lookup note: The span_of closure converts an ExprIndex (a usize type alias defined at compiler/ori_types/src/infer/mod.rs:56) back to a Span. The bridge is: ExprIndex is the u32 raw value of an ExprId cast to usize; ExprId::new(u32) is the public constructor (verified in compiler/ori_ir/src/expr_id/mod.rs). The span lookup is:

&|expr_index| {
    // ExprIndex (usize) == ExprId.raw() as usize — confirmed at infer/mod.rs:56.
    // ExprId::new(u32) is the only public ExprId constructor (no from_raw exists).
    let expr_id = ori_ir::ExprId::new(expr_index as u32);
    arena.get_expr(expr_id).span
},

The constructor ExprId::new(u32) is the correct form; ExprId::from_raw does NOT exist. Verify this remains accurate by checking compiler/ori_ir/src/expr_id/mod.rs before implementing.

03.2 Wire validator into `check_test`

File: compiler/ori_types/src/check/bodies/mod.rs Function: check_test (line 182–253) Insertion point: After the manual 6-tuple extraction (lines 229-235) and before the for (expr_index, ty) in expr_types storage loop (line 237). Note that check_test does NOT use with_function_scope — it creates the engine directly and calls take_* methods on it. The insertion sits between the last engine.take_*() call and the first storage loop.

Current structure (lines 229-252, abridged):

    // Extract results
    let expr_types = engine.take_expr_types();
    let errors = engine.take_errors();
    let warnings = engine.take_warnings();
    let pat_resolutions = engine.take_pattern_resolutions();
    let mono_instances = engine.take_mono_instances();
    let deferred_mono_calls = engine.take_deferred_mono_calls();

    // Store expression types
    for (expr_index, ty) in expr_types {
        checker.store_expr_type(expr_index, ty);
    }

After insertion:

    // Extract results
    let expr_types = engine.take_expr_types();
    let errors = engine.take_errors();
    // ... (remaining take_* calls unchanged) ...

    // Validate PC-2 contract: no unbound Tag::Var in body expr_types or FunctionSig.
    // Spec: docs/ori_lang/v2026/spec/14-expressions.md:1224-1228
    // Plan: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.2
    {
        let pool = checker.pool();
        let arena = checker.arena();
        let sig_span = test.span; // TestDef declaration span (test.span, NOT test.expr_id)
        let mut validation_errors = Vec::new();
        crate::check::validators::validate_body_types(
            pool,
            &expr_types,
            &sig,            // &FunctionSig fetched earlier (pass by reference, see below)
            sig_span,
            &|expr_index| {
                let expr_id = ori_ir::ExprId::new(expr_index as u32);
                arena.get_expr(expr_id).span
            },
            &mut validation_errors,
        );
        for err in validation_errors {
            checker.push_error(err);
        }
    }

    // Store expression types
    for (expr_index, ty) in expr_types { ... }

sig availability in check_test: check_test receives a &TestDef and a &FunctionSig that the Signatures pass already computed. Verify that the host function has sig: &FunctionSig available as a parameter (or that a sig fetch call is already present before the extraction block) before inserting the validator call. The sig_span should come directly from test.span (the TestDef struct has a .span field for the declaration span — do NOT use test.expr_id which does not exist on TestDef).

In check_test, arena was already bound earlier in the function body (line 200: let arena = checker.arena();) so the let arena = inside the scope block is a re-borrow of the checker — verify this compiles cleanly given lifetime constraints (arena() returns &'a ExprArena tied to the checker’s 'a lifetime, not to &self). If there is a borrow conflict with checker.pool(), use the split-borrow pattern: bind let arena = checker.arena(); before calling checker.pool(), or separate the borrows temporally.

TDD — failing test:

/// Test-body with unannotated empty list produces E2005 at typeck, not at codegen.
/// Exercises check_test (Pass 3 per CK-1).
///
/// See: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.2
#[test]
fn check_test_with_unannotated_empty_list_emits_ambiguous_type() {
    let (result, _interner) = parse_and_check(
        "use std.testing { assert_eq }
         @t tests @fn () -> void = { let xs = []; assert_eq(actual: xs.len(), expected: 0) }",
    );
    assert!(
        result.typed.errors.iter().any(|e| matches!(e.kind, TypeErrorKind::AmbiguousType { .. })),
        "expected E2005 AmbiguousType in test body, got: {:?}",
        result.typed.errors
    );
}

03.3 Wire validator into `check_impl_method` (TPR checkpoint)

File: compiler/ori_types/src/check/bodies/mod.rs (→ bodies/impls.rs after 03.0 split) Function: check_impl_method (lines 319–440 in current file) Insertion point: After the nested closure that calls with_impl_scope → with_function_scope returns its 6-tuple (line 390, closing });), before the for (expr_index, ty) in expr_types storage loop (line 393).

CRITICAL — FunctionSig ordering constraint:

Unlike check_function, check_impl_method constructs FunctionSig sig (at lines 418–438) AFTER expr_types is consumed (at line 393). This means the validator CANNOT be called with sig: &FunctionSig at the natural insertion point (after line 390) without restructuring.

The correct fix is to construct the FunctionSig before the inference closure runs. The param_types and return_type locals needed for FunctionSig are already computed at lines 335–348, before the closure. Move the sig construction up to just after line 351 (let fn_type = checker.pool_mut().function(...)) — the sig fields (param_names, param_types, return_type, etc.) are available at that point. The register_impl_sig call at line 439 stays in place (the sig is constructed early, used for validation, then registered at the end).

Restructured code (insertion at line 392):

    // === MOVED EARLIER: build FunctionSig before inference so validate_body_types can use it ===
    let param_names: Vec<Name> = params.iter().map(|p| p.name).collect();
    let param_defaults: Vec<Option<ori_ir::ExprId>> = params.iter().map(|p| p.default).collect();
    let required_params = param_defaults.iter().filter(|d| d.is_none()).count();
    let param_hashes: Vec<u64> = param_types.iter().map(|&idx| checker.pool().hash(idx)).collect();
    let return_hash = checker.pool().hash(return_type);
    let sig = FunctionSig {
        name: method.name, type_params: type_params.to_vec(), const_params: vec![],
        param_names, param_types: param_types.clone(), return_type, capabilities: vec![],
        is_public: false, is_test: false, is_main: false, is_fbip: false,
        type_param_bounds: vec![], where_clauses: vec![], generic_param_mapping: vec![],
        scheme_var_ids: vec![], required_params, param_defaults, param_hashes, return_hash,
    };
    // === END MOVED SECTION ===

    let (expr_types, errors, ...) = checker.with_impl_scope(self_type, |c| {
        c.with_function_scope(fn_type, FxHashSet::default(), |c| {
            // ... inference ...
            (engine.take_expr_types(), engine.take_errors(), ...)
        })
    });

    // Validate PC-2 contract: no unbound Tag::Var in body expr_types or FunctionSig.
    {
        let arena = checker.arena();
        let pool = checker.pool();
        let sig_span = method.span; // Method declaration span (method.span, NOT method.body.span)
        let mut validation_errors = Vec::new();
        crate::check::validators::validate_body_types(
            pool, &expr_types, &sig, sig_span,
            &|expr_index| {
                let expr_id = ori_ir::ExprId::new(expr_index as u32);
                arena.get_expr(expr_id).span
            },
            &mut validation_errors,
        );
        for err in validation_errors { checker.push_error(err); }
    }

    // Store results
    for (expr_index, ty) in expr_types { ... }

    // Export impl method signature (sig already built above; remove duplicate construction here)
    checker.register_impl_sig(method.name, sig);

Note on param_types.clone(): The original code moves param_types into FunctionSig at line 423. Moving construction earlier requires cloning param_types for the sig if it is still needed after that point. Inspect the actual usage: param_types is used to build fn_type at line 351 (already consumed into the pool) and then used again for the sig. Since the pool call takes &[Idx], param_types is not consumed there. The sig then takes the Vec<Idx> by move. Building the sig early means param_types moves into FunctionSig::param_types — if the field is still needed after that point, extract a slice first (&param_types[..]) for any remaining usages before constructing the sig. In practice param_types has no use after the sig consumes it, so a clone is not needed; move it into the sig directly.

The arena binding: inside check_impl_method there is no pre-existing arena binding in scope after the closure; checker.arena() is fresh. The pool and arena borrows from checker are read-only and do not conflict with checker.push_error (which takes &mut self) — use a scoped block to ensure the borrows end before push_error.

TDD — failing test:

/// Impl method body with unannotated empty list produces E2005 at typeck.
/// Exercises check_impl_method (Pass 4 per CK-1).
///
/// IMPORTANT: the return type is `-> int`, NOT `-> [int]`. A `-> [int]` return
/// would drive bidirectional propagation (`Check([int])` on the body → `Check(int)`
/// on `[]` elements per typeck.md BD-2) which resolves `xs` to `[int]` before
/// the validator runs, hiding a broken/missing validator wiring. With `-> int`
/// returned by `.len()`, the element type of `xs` is never constrained, so
/// body expr_types carries a surviving unbound `Tag::Var` that ONLY the
/// validator can observe — a true regression pin for PC-2 body coverage.
///
/// See: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.3
#[test]
fn check_impl_method_with_unannotated_empty_list_emits_ambiguous_type() {
    let (result, _interner) = parse_and_check(
        "type Foo = {}  impl Foo { @items (self) -> int = { let xs = []; xs.len() } }",
    );
    assert!(
        result.typed.errors.iter().any(|e| matches!(e.kind, TypeErrorKind::AmbiguousType { .. })),
        "expected E2005 AmbiguousType in impl method body, got: {:?}",
        result.typed.errors
    );
}

TDD first — add the test to bodies/tests.rs, confirm it FAILS.

Signature-path test — add a second test that catches broken FunctionSig construction specifically. A body-local let xs = [] passes the body-inference check; the test must have an unannotated parameter or return type where the surviving Tag::Var comes from the sig:

/// Impl method with unannotated PARAMETER (not body expr) produces E2005.
/// The Tag::Var in the sig's param_types — not body expr_types — is what fires.
/// This test catches regressions where sig is built incorrectly and the validator
/// fails to walk param_types/return_type at all.
///
/// See: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.3
#[test]
fn check_impl_method_unannotated_param_emits_ambiguous_type() {
    // The parameter `x` has no annotation — the sig's param_types[0] is Tag::Var.
    // If the validator only walks body expr_types and skips the sig, this test passes
    // silently (wrong). The correct behavior: E2005 fires for the parameter.
    let (result, _interner) = parse_and_check(
        "type Foo = {}  impl Foo { @process (self, x) -> void = { } }",
    );
    assert!(
        result.typed.errors.iter().any(|e| matches!(e.kind, TypeErrorKind::AmbiguousType { .. })),
        "expected E2005 for unannotated parameter in impl method sig, got: {:?}",
        result.typed.errors
    );
}

Restructure check_impl_method so the PC-2 validator sees post-defaulted sig inputs. Architectural improvement over the plan’s literal text: the plan prescribed building the sig BEFORE the inference closure with param_types.clone() into FunctionSig.param_types. That ordering captures PRE-defaulted values, which would defeat default_unbound_vars_in_scope (running inside the closure) and cause the validator to fire on positions legitimately defaulted to Idx::NEVER. The shipped implementation (compiler/ori_types/src/check/bodies/impls.rs) builds the sig AFTER the closure returns, using the already-post-defaulted param_types and return_type, then calls run_validator(checker, &expr_types, &sig, method.span) before storing results. This matches functions.rs’s end-state invariant (“sig seen by validator is post-defaulted”). DRY refactor landed alongside: promoted run_validator from a private helper in functions.rs to pub(super) in bodies/mod.rs so functions.rs, impls.rs (§03.3), and the future §03.4 wiring in impls.rs (check_def_impl_method) all call a single canonical helper per impl-hygiene.md §Algorithmic DRY (“3+ sites → always extract”). §03.N success grep shape is the “helper-extracted” branch: one validate_body_types(...) call inside run_validator, plus four run_validator(...) call sites across functions.rs + impls.rs (three live after §03.3; the fourth lands in §03.4).
Confirm both tests PASS.
timeout 150 cargo test -p ori_types — no regressions (828/828 pass).
Subsection close-out (03.3) — MANDATORY before starting 03.4:
- All tasks above are [x] and behavior is verified
- Update subsection status in frontmatter to complete
- Run /improve-tooling retrospectively on THIS subsection — Retrospective: no tooling gaps. Subsection relied on cargo test -p ori_types, cargo clippy, ./test-all.sh (summary table at end was sufficient despite verbose failure output during the plan-expected E2005 rollout), and diagnostics/repo-hygiene.sh --check — all sufficient. No manual env-var incantations or dbg!/eprintln! needed (mechanical wiring, compile-or-not). No scripts created or modified. Ori’s own parse-error diagnostic when the first TDD test used expression-body = () was exemplary (“expected ; after item declaration” + help: “Block bodies ending with } don’t need ;, but expression bodies do”) — no improvement needed.
- Repo hygiene — diagnostics/repo-hygiene.sh --check (reported clean)
TPR checkpoint — run /tpr-review covering subsections 03.1, 03.2, and 03.3 before proceeding to 03.4. Note: the three sites are NOT structurally identical due to the FunctionSig availability difference at the impl-method site (see 03.3 above) — the TPR should evaluate whether the early sig construction in check_impl_method is architecturally sound, not flag the divergence as a “call pattern mismatch”. Reviewers should focus on: (a) correctness of ExprId::new(u32) as the ExprIndex bridge, (b) correctness of the sig construction ordering in 03.3, and (c) whether the early-construction approach should be extracted into a helper to reduce the boilerplate across 03.3 and 03.4. Resolve all critical and major findings before proceeding. Record findings in 03.R. Round 3 (2026-04-17): dual-source clean (codex + gemini, both findings: []); see §03.R Round 3 for full reviewer summaries. All three focus questions answered with consensus: ExprId bridge sound, post-closure sig construction architecturally correct, run_validator DRY extraction clean. Loop exited at iter 1 per §5 stop #1.

03.4 Wire validator into `check_def_impl_method`

File: compiler/ori_types/src/check/bodies/mod.rs (→ bodies/impls.rs after 03.0 split) Function: check_def_impl_method (lines 462–540 in current file) Insertion point: After the with_function_scope closure returns its 6-tuple (line 525, closing });), before the for (expr_index, ty) in expr_types storage loop (line 528).

check_def_impl_method uses only with_function_scope (no with_impl_scope — def-impl methods are stateless). The structure is:

    let (expr_types, errors, warnings, ...) =
        checker.with_function_scope(fn_type, FxHashSet::default(), |c| {
            // ... inference ...
            (engine.take_expr_types(), engine.take_errors(), ...)
        });

    // Store results   ← INSERT VALIDATOR CALL HERE
    for (expr_index, ty) in expr_types {

CRITICAL — no FunctionSig in check_def_impl_method:

check_def_impl_method (lines 462–540) NEVER constructs a FunctionSig — unlike check_impl_method, it does not call checker.register_impl_sig(). However, param_types (line 474–481) and return_type (line 485) are computed as locals before the closure. These are the same data fields that FunctionSig would hold.

The correct approach is the same as 03.3: construct a temporary FunctionSig inline before the inference closure, using the available param_types and return_type. The sig is used only for the validator call and can be a local temporary (not registered anywhere, since def-impl methods have their sig handled differently at the type-checker level).

Restructured code (insertion at line 527):

    // Build a temporary FunctionSig for validator scope (param/return type coverage).
    // check_def_impl_method does not register a sig externally; this is validator-only.
    let param_names: Vec<Name> = params.iter().map(|p| p.name).collect();
    let param_defaults: Vec<Option<ori_ir::ExprId>> = params.iter().map(|p| p.default).collect();
    let required_params = param_defaults.iter().filter(|d| d.is_none()).count();
    let param_hashes: Vec<u64> = param_types.iter().map(|&idx| checker.pool().hash(idx)).collect();
    let return_hash = checker.pool().hash(return_type);
    let validator_sig = FunctionSig {
        name: method.name, type_params: vec![], const_params: vec![],
        param_names, param_types, return_type, capabilities: vec![],
        is_public: false, is_test: false, is_main: false, is_fbip: false,
        type_param_bounds: vec![], where_clauses: vec![], generic_param_mapping: vec![],
        scheme_var_ids: vec![], required_params, param_defaults, param_hashes, return_hash,
    };

    let (expr_types, errors, ...) = checker.with_function_scope(...);

    // Validate PC-2 contract
    {
        let arena = checker.arena();
        let pool = checker.pool();
        let sig_span = method.span; // Method declaration span (method.span, NOT method.body.span)
        let mut validation_errors = Vec::new();
        crate::check::validators::validate_body_types(
            pool, &expr_types, &validator_sig, sig_span,
            &|expr_index| {
                let expr_id = ori_ir::ExprId::new(expr_index as u32);
                arena.get_expr(expr_id).span
            },
            &mut validation_errors,
        );
        for err in validation_errors { checker.push_error(err); }
    }

    // Store results
    for (expr_index, ty) in expr_types { ... }

Note: The param_types local moves into validator_sig.param_types when building the sig. If param_types is still needed after the sig construction (e.g., for building fn_type), move the sig construction AFTER the fn_type pool call but BEFORE the inference closure. In check_def_impl_method the flow is: build param_types → build fn_type (using &param_types) → build return_type → enter closure. The sig construction should follow fn_type construction, at which point param_types can move into the sig.

TDD — failing test:

/// Def-impl method body with unannotated empty list produces E2005 at typeck.
/// Exercises check_def_impl_method (Pass 5 per CK-1).
///
/// IMPORTANT: the return type is `-> int`, NOT `-> [int]`. A `-> [int]` return
/// would drive bidirectional propagation (`Check([int])` on the body → `Check(int)`
/// on `[]` elements per typeck.md BD-2) which resolves `xs` to `[int]` before
/// the validator runs, hiding a broken/missing validator wiring. With `-> int`
/// returned by `.len()`, the element type of `xs` is never constrained, so
/// body expr_types carries a surviving unbound `Tag::Var` that ONLY the
/// validator can observe — a true regression pin for PC-2 body coverage.
///
/// See: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.4
#[test]
fn check_def_impl_method_with_unannotated_empty_list_emits_ambiguous_type() {
    let (result, _interner) = parse_and_check(
        "trait Fooable { @items () -> int }  pub def impl Fooable { @items () -> int = { let xs = []; xs.len() } }",
    );
    assert!(
        result.typed.errors.iter().any(|e| matches!(e.kind, TypeErrorKind::AmbiguousType { .. })),
        "expected E2005 AmbiguousType in def-impl method body, got: {:?}",
        result.typed.errors
    );
}

TDD first — add the test, confirm it FAILS.

Signature-path test — add a second test that verifies the validator covers the temporary validator_sig’s param_types (not just body expr_types):

/// Def-impl method with unannotated PARAMETER produces E2005.
/// The Tag::Var in validator_sig.param_types — not body expr_types — fires.
/// This test catches regressions where validator_sig is built incorrectly
/// and the validator skips param_types/return_type coverage.
///
/// See: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.4
#[test]
fn check_def_impl_method_unannotated_param_emits_ambiguous_type() {
    // Trait declares @process(x) without annotation; def impl body is trivially ok.
    // The surviving Tag::Var must come from the sig's param_types[0].
    let (result, _interner) = parse_and_check(
        "trait Processable { @process (x) -> void }  pub def impl Processable { @process (x) -> void = { } }",
    );
    assert!(
        result.typed.errors.iter().any(|e| matches!(e.kind, TypeErrorKind::AmbiguousType { .. })),
        "expected E2005 for unannotated parameter in def-impl method sig, got: {:?}",
        result.typed.errors
    );
}

In check_def_impl_method: construct the validator_sig (FunctionSig local) BEFORE the with_function_scope closure (after fn_type is built so param_types can move in), then insert the validator call block after the closure returns (before the for (expr_index, ty) in expr_types storage loop). See the “Restructured code” block above for the exact validator_sig field list and validator call.
Confirm both tests PASS.
Verify the grep criterion: grep -rn 'validate_body_types' compiler/ori_types/src/check/bodies/ returns 4 matches (all four sites now call the validator; post-03.0 split, calls live in functions.rs and impls.rs).
timeout 150 cargo test -p ori_types — no regressions.

Def-impl corpus test — add a Rust-level test that exercises check_def_impl_method directly on a hand-crafted source fragment containing a def impl block. This must actually route through check_def_impl_bodies (Pass 5 per CK-1), NOT through prelude extension methods. library/std/prelude.ori contains ZERO def impl blocks (verified: grep -c "def impl" library/std/prelude.ori returns 0), so spec-test programs using [int].push() do NOT exercise check_def_impl_method at all:

/// def impl block with clean bodies checks OK (no false-positive E2005 from the validator).
/// Exercises check_def_impl_method (Pass 5 per CK-1) with a well-typed body.
///
/// See: plans/empty-container-typeck-phase-contract/section-03-bodies-pass-integration.md §03.4
#[test]
fn check_def_impl_method_well_typed_body_produces_no_errors() {
    let (result, _interner) = parse_and_check(
        "trait Printable2 { @display (self) -> str }
         type MyNum = { val: int }
         pub def impl Printable2 for MyNum { @display (self) -> str = \"num\" }",
    );
    assert!(
        result.typed.errors.is_empty(),
        "expected no errors for well-typed def-impl body, got: {:?}",
        result.typed.errors
    );
}

If the def impl Trait for Type syntax is not yet accepted by the parser, use the form actually supported (pub def impl TraitName { @method ... }) — check the existing bodies tests and spec tests for the correct syntax before writing.

Subsection close-out (03.4) — MANDATORY before starting 03.5:
- All tasks above are [x] and behavior is verified
- Update subsection status in frontmatter to complete
- Run /improve-tooling retrospectively on THIS subsection — Retrospective: no tooling gaps. The DRY extraction landed in §03.3 (run_validator promoted to pub(super) in bodies/mod.rs) reduced §03.4 to a single-line dispatch at the post-closure insertion point — exactly the abstraction §03.N anticipated. No dbg!/eprintln!/ad-hoc scripts needed. The parser diagnostic on = "hi" (“Block bodies ending with } don’t need ;, but expression bodies do”) pointed directly at the fix when the negative-control test initially parse-errored; zero friction. Matches §03.3’s “no tooling gaps” retrospective finding.
- Run /sync-claude on THIS subsection — Retrospective: no doc updates needed. Both typeck.md §PC-2 (“Producer-side enforcement: validate_body_types … walks the body’s expr_types and FunctionSig … after InferEngine body-checking completes”) and canon.md §4.2 already describe the producer-side enforcement contract without naming specific call sites. §03.4 MAKES those claims universally true (all 4 body passes now call run_validator), so the existing doc language is correct. No rules file claims “the bodies pass does not validate PC-2 inline” (grep confirmed clean). impls.rs already imported run_validator via use super::run_validator; from §03.3; §03.4 added no new imports.
- Repo hygiene — diagnostics/repo-hygiene.sh --clean ran (removed 47 stale TPR scratch dirs from prior /tpr-review runs; no compiler-code hygiene issues).

03.5 End-to-end regression suite and dual-execution parity

Files touched:

compiler/ori_llvm/tests/aot/ — new AOT integration test
compiler/ori_types/src/check/bodies/tests.rs — BUG-04-074 repro assertion

This subsection verifies the full round-trip: the original BUG-04-074 repro (unannotated) produces E2005 at typeck; the annotated version compiles and runs correctly via both the interpreter and AOT path.

03.5.1 — BUG-04-074 repro: end-to-end typeck regression pin

Repro program:

@main () -> int = {
    let ages = [];
    ages = ages.push(value: 10);
    if ages.len() == 1 then 0 else 1
}

This is the exact program from BUG-04-074. After Sections 01–03.4 PLUS the BUG-04-084 end-of-body defaulting pre-pass documented in typeck.md §PC-2, the bug is fixed end-to-end through TWO coordinated mechanisms:

Unification from push(value: 10) — the builtin push signature (self: [T], value: T) -> [T] unifies T := int via the value: 10 argument during body inference. The element Tag::Var is bound before body-pass exit, so the validator’s PC-2 rejection path is not exercised on this particular input.
BUG-04-084 defaulting pre-pass — if unification had NOT resolved the element type (e.g., a shape like let ages = []; with no subsequent constraining use), the defaulting pass would substitute the unbound element var to Idx::NEVER, producing [Never] — also a concrete, codegen-safe representation.

Either way, no surviving Tag::Var reaches codegen and the “unresolved type variable at codegen” symptom of BUG-04-074 cannot recur on this input. The integration test below pins this behavior end-to-end by asserting the original repro type-checks cleanly (no diagnostics). Validator coverage for surviving Tag::Var — the complementary PC-2 rejection path — lives in the existing check_*_with_unannotated_param_emits_ambiguous_type + check_*_with_ungeneralizable_body_lambda_emits_ambiguous_type tests for the four body passes (§03.1–§03.4), which remain the canonical validator exercise.

Add an integration test in compiler/ori_types/src/check/bodies/tests.rs:

/// End-to-end regression pin for the BUG-04-074 repro program.
/// The program must type-check cleanly — unification + BUG-04-084
/// defaulting jointly eliminate the surviving Tag::Var before codegen.
///
/// See: plans/empty-container-typeck-phase-contract/00-overview.md §Mission Success Criteria
#[test]
fn empty_list_with_push_and_len_typechecks_without_errors_end_to_end() {
    let (result, _interner) = parse_and_check(
        "@main () -> int = { let ages = []; ages = ages.push(value: 10); if ages.len() == 1 then 0 else 1 }",
    );
    assert!(
        result.typed.errors.is_empty(),
        "expected BUG-04-074 repro to type-check cleanly after Sections 01–03.4 + BUG-04-084 defaulting pass, got: {:?}",
        result.typed.errors
    );
}

03.5.2 — Annotated form compiles and runs: AOT integration test

Annotated repro program:

@main () -> int = {
    let ages: [int] = [];
    ages = ages.push(value: 10);
    if ages.len() == 1 then 0 else 1
}

This program MUST compile clean AND exit with code 0.

Add AOT tests in a new file compiler/ori_llvm/tests/aot/empty_container.rs (module wired into compiler/ori_llvm/tests/aot/main.rs alphabetically between elem_dec_scope and enum_discriminant):

/// Annotated empty list with push + len compiles clean and exits 0 via AOT.
/// Confirms the annotation path works end-to-end.
#[test]
fn annotated_empty_list_with_push_and_len_compiles_and_exits_zero() {
    let src = r#"
        @main () -> int = {
            let ages: [int] = [];
            ages = ages.push(value: 10);
            if ages.len() == 1 then 0 else 1
        }
    "#;
    assert_aot_success(src, "annotated_empty_list_with_push_and_len");
}

/// Unannotated form — the original BUG-04-074 surface repro — compiles
/// clean and exits 0 via AOT. Pins that unification + BUG-04-084
/// defaulting keep the bug fixed without requiring the user to annotate.
#[test]
fn unannotated_empty_list_with_push_and_len_compiles_and_exits_zero() {
    let src = r#"
        @main () -> int = {
            let ages = [];
            ages = ages.push(value: 10);
            if ages.len() == 1 then 0 else 1
        }
    "#;
    assert_aot_success(src, "unannotated_empty_list_with_push_and_len");
}

The assert_aot_success helper from crate::util drives the AOT pipeline and asserts exit 0. Dual-execution parity (interpreter vs AOT) is verified separately by §03.5.3’s diagnostics/dual-exec-verify.sh invocation against the same repro program.

03.5.3 — Dual-execution parity via diagnostic script

Run diagnostics/dual-exec-verify.sh against the annotated repro program to confirm the interpreter and LLVM produce identical observable results. This is the plan-level dual-execution gate referenced in 00-overview.md §Mission Success Criteria.

# Create a temporary test file matching the annotated repro
echo '@main () -> int = {
    let ages: [int] = [];
    ages = ages.push(value: 10);
    if ages.len() == 1 then 0 else 1
}' > /tmp/ages_repro.ori
diagnostics/dual-exec-verify.sh /tmp/ages_repro.ori
# Expected: "PASS: interpreter and AOT produce identical output (exit 0)"

03.5.4 — Full test suite

Run the SAME audit roots that Section 06.2 audits — tests/spec/, tests/valgrind/, and library/. The §06.2 sweep expands post-E2005 coverage beyond the spec harness precisely because empty-list regressions are not confined to cargo st (the canonical reference is plans/empty-container-typeck-phase-contract/section-06-diagnostics-audit.md frontmatter and §06.2, which cites tests/valgrind/cow/cow_list_concat.ori as a known operator-position hit outside tests/spec/). Running only cargo st here would under-approximate the transitional failure surface — a tests/valgrind/*.ori or library/std/*.ori regression could pass §03.5 silently and only surface when 06.2 runs. Document any new failures in the Known Failing Tests section below. Do NOT investigate them individually — Section 06.2 resolves them via annotation. Confirm that the number of newly-failing tests across all three roots is bounded and explainable (they are programs with [] or empty collection literals lacking type context).

Known Failing Tests (Expected Until Section 06.2 Lands)

Once the validator fires on all 4 bodies-pass sites, every program that leaves any Tag::Var unbound at body exit will now correctly emit E2005. Two distinct E2005 paths are expected between this section landing and §06.2 resolving them via annotation:

Class	Pattern	Example	§06.2 resolution
Empty-literal, no constraining use	`let x = []` / `[].iter()` / `[].is_empty()` / `[].len()` / `{}.keys()`	`tests/spec/collections/`, `tests/spec/traits/iterator/`	Add `let x: [T] = []` / `{str: int} = {}` annotation
Lambda-parameter inference in method chains	`list.map(x -> x.method())` / `list.filter(x -> ...)` — the receiver’s element type does not propagate bidirectionally into the closure body, leaving the closure-parameter `Tag::Var` unresolved	`tests/spec/types/primitives.ori:1584` `[Duration...].map(d -> d.minutes())`; similar in `option/map.ori`, `result/map.ori`, `traits/core/*.ori`	Annotate the closure parameter: `.map((d: Duration) -> d.minutes())`

Failing files captured via timeout 150 ./test-all.sh + rg '\[\s*\]' ... --glob '*.ori' cross-check (35 files total across tests/spec/ and tests/compiler/; 386 E2005 diagnostics):

tests/spec/ (31 files):

~~tests/spec/capabilities/propagation.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/declarations/stdlib/testing_assert_eq.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/declarations/test_variant_match.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/declarations/traits.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/expressions/field_access.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/imports/generic_import.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/inference/generics.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/inference/unification.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/lexical/delimiters.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/lexical/keywords.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/lexical/operators.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/patterns/data.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/patterns/match.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/core/comparable.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/core/compound_equals.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/core/compound_hash.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/core/option.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/debug/join.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/into/str_to_error.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/iterator/methods.ori~~ [REMEDIATED IN §06.2B]
~~tests/spec/traits/traceable/definition.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/traits/traceable/result_delegation.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/types/duration_size_default.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/types/enum/niche/niche_cross_feature.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/types/enum/niche/option_str.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/types/existential.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/types/never.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/types/option/map.ori~~ [REMEDIATED IN §06.2B]
~~tests/spec/types/option/ok_or.ori~~ [REMEDIATED IN §06.2]
~~tests/spec/types/primitives.ori~~ [REMEDIATED IN §06.2B]
~~tests/spec/types/result/map.ori~~ [REMEDIATED IN §06.2B]

tests/compiler/ (4 files):

~~tests/compiler/typeck/collections.ori~~ [REMEDIATED IN §06.2]
~~tests/compiler/typeck/control_flow.ori~~ [REMEDIATED IN §06.2]
tests/compiler/typeck/generics.ori [§06.2C scope — polymorphic-constructor class; no §06.2 / §06.2B per-file entry fires]
tests/compiler/typeck/let_bindings.ori [§06.2C scope — polymorphic-constructor + residual lambda-parameter class]

tests/valgrind/ (0 files) and library/ (0 files): no failures captured from these roots — empty-literal occurrences in valgrind and library shipping code all have constraining uses that resolve the element type before body exit.

Expanded scope note: the initial plan anticipated only the empty-literal class. Section 03.5 exercise surfaced the lambda-parameter class as an equally prevalent E2005 source once the validator fires at all body-pass sites. Both classes share the same root: a Tag::Var survives to body exit because no type-channel constraint (literal element, bidirectional propagation, or end-of-body defaulting) bound it. §06.2 annotation resolves both uniformly.

Commit the updated table alongside the §03.5 implementation. Do NOT fix individual failing tests — that is §06.2’s job.

Per 00-overview.md §Known Bugs:

TPR-04-005-codex audit finding: tests/spec/ uses [].iter(), [].is_empty() patterns beyond just let x = [] bindings; these WILL trip E2005 once live. §06.2 resolves them via annotation.

03.R Third Party Review Findings

Round 0 Findings (all accepted and integrated)

[TPR-03-001-codex] HIGH — Replace stale snippet APIs with the current checker interfaces

Finding: All TDD tests in 03.1–03.5 used non-existent helpers (compile_snippet_for_errors, compile_test_body_for_errors, compile_impl_method_for_errors, compile_def_impl_method_for_errors, compile_program_for_errors, is_internal_compiler_error()). Error kind accessed as e.kind() (method) instead of e.kind (public field).
Fix applied: All tests rewritten using parse_and_check from check/api/tests.rs. Error access changed to e.kind throughout. 03.5 codegen-gate test changed to assert only E2005 fires and no unexpected additional errors appear (since is_internal_compiler_error() does not exist on TypeCheckError).

[TPR-03-002-codex] HIGH — Add signature-path tests for impl and def-impl validator wiring

Finding: The body-local let xs = [] test passes even if the sig was wrong/missing. No tests for the path where a surviving Tag::Var comes from unannotated parameters or return types in the sig (the validator’s param_types/return_type coverage).
Fix applied: Added check_impl_method_unannotated_param_emits_ambiguous_type to 03.3 and check_def_impl_method_unannotated_param_emits_ambiguous_type to 03.4 — both use an unannotated parameter so only the sig’s param_types[0] carries Tag::Var.

[TPR-03-003-codex] MEDIUM — Make BLOAT split plan and completion gate agree on file ownership

Finding: 03.0 splits bodies/mod.rs into functions.rs + impls.rs, but all success criteria and the 03.N completion checklist used grep -c ... bodies/mod.rs (would return 0 after split). Inconsistency between post-split file layout and verification commands.
Fix applied: All grep commands changed to grep -rn ... compiler/ori_types/src/check/bodies/ (recursive, covering all files in the directory). Prose updated to note calls live in functions.rs and impls.rs post-split.

[TPR-03-004-codex] MEDIUM — Replace prelude safety gate with real def-impl verification target

Finding: The “Prelude safety gate” exercised [int].push() / .len() etc. — these are NOT def-impl methods (library/std/prelude.ori has 0 def impl blocks). The gate tested list extension methods (different code path), not check_def_impl_method.
Fix applied: Replaced the prelude gate with a concrete Rust-level parse_and_check test (check_def_impl_method_well_typed_body_produces_no_errors) using a hand-crafted source fragment with an actual def impl block. Added a note explaining why prelude programs do NOT exercise check_def_impl_method.

[TPR-03-001-gemini] HIGH — Fix compilation errors in validator call arguments and AST span extractions

Finding: Multiple wrong variable references:
- 03.1: fn_decl.expr_id → func is the parameter (&Function), not fn_decl; correct: func.span
- 03.2: test_decl.expr_id → test is the parameter (&TestDef), no .expr_id; correct: test.span
- 03.3/03.4: method.body.span → gets body block span; correct declaration span: method.span
- 03.1/03.2: sig, → should be &sig, (pass by reference)
Fix applied: All span references corrected to func.span, test.span, method.span. sig, changed to &sig, in 03.1 and 03.2.

[TPR-03-002-gemini] MEDIUM — Extract FunctionSig construction helper for def-impl methods

Finding: The ~15-line FunctionSig construction block is structurally identical in 03.3 and 03.4, violating impl-hygiene.md §Algorithmic DRY (same algorithm at 2+ sites = missing abstraction; with 03.3 and 03.4 plus any future sites, threshold reached).
Fix applied: Added build_method_sig helper extraction task to 03.0 (with full field list and rationale). The helper takes (method_name, params, param_types, return_type, type_params, pool) and returns FunctionSig. Both check_impl_method and check_def_impl_method call it.

Round 1 Findings (single-source codex; gemini stalled watchdog-killed — 2026-04-15)

Round 1 ran via /tpr-review --skill review-plan. Codex produced 5 specific architecturally-grounded findings in 578s with full tool use (HIGH trust, thorough review). Gemini stalled at 23 min with zero tool_use events and was watchdog-killed; its half of the envelope was empty. Per .claude/skills/tpr-review protocol, codex findings were independently verified by Claude against the actual code (compiler/ori_types/src/output/mod.rs:373-378, compiler/ori_types/src/check/bodies/mod.rs:300-539) and plan text before accepting.

[TPR-03-001-codex] HIGH — 03.3/03.4 body-side tests are return-type-constrained, masking broken validator wiring

Finding: GAP against typeck.md PC-2, typeck.md CK-1, canon.md §4.2, and tests.md §Semantic Pins / §Negative Testing. The proposed impl test at §03.3 (check_impl_method_with_unannotated_empty_list_emits_ambiguous_type) and the def-impl twin at §03.4 both declared return type -> [int] with body { let xs = []; xs }. Per typeck.md §BD-2, bidirectional Check([int]) on the body propagates Check(int) to the [] elements, so xs is unified to [int] BEFORE the validator runs (compiler/ori_types/src/check/bodies/mod.rs:367-377 for check_impl_method, and lines 503-513 for check_def_impl_method apply the declared return_type as the body’s expected type). The body’s expr_types map therefore carries no surviving unbound Tag::Var, meaning the test passes even if validate_body_types is never called at those sites — the signature-path sibling tests remain the only real coverage for passes 4 and 5.
Impact: Section 03 could claim all four CK-1 body sites covered while two of the stated negative pins cannot observe a surviving Tag::Var. A bad pass-4/pass-5 integration slips through green tests; the producer-side PC-2 contract is only partially verified.
Resolved: Changed both body-side tests’ return types from -> [int] to -> int and bodies from { let xs = []; xs } to { let xs = []; xs.len() }. .len() returns int (unchanged return type), so the body’s expected type does not propagate into [] — xs remains typed as [Tag::Var] in expr_types, which is exactly what the validator must observe. Added doc comments on both tests explaining the load-bearing return-type choice (so a future refactor does not reintroduce the bidirectional-propagation hiding path). Plan §03.3 and §03.4 updated in-place.

[TPR-03-002-codex] MEDIUM — 03.0 split plan assigns impl dispatchers to both impls.rs and mod.rs

Finding: BLOAT/GAP against impl-hygiene.md §BLOAT, impl-hygiene.md §SSOT, and compiler.md §File Organization. §03.0 Split Plan line 192 assigned check_impl_bodies and check_def_impl_bodies to impls.rs, and lines 195-197 simultaneously assigned them to mod.rs as “retained public pass-dispatch functions”. Two canonical homes for the same function is an SSOT violation and an internally-contradictory spec — an implementer must contradict one half of 03.0 to satisfy the other.
Impact: The first required step of the section was not executable as written. The split gate was supposed to de-risk the over-500-line file BEFORE validator wiring; instead it created churn at exactly the prerequisite step.
Resolved: Rewrote §03.0 Split Plan to designate impls.rs as the canonical home for check_impl_bodies and check_def_impl_bodies (alongside their private helpers), and redefined mod.rs as a thin re-export hub using pub use functions::{...}; and pub use impls::{...};. Added explicit SSOT rationale in the plan (impl-hygiene.md §SSOT — one function, one file). Existing callers of check::bodies::check_impl_bodies continue to resolve through the pub use without changing import paths. Plan §03.0 updated in-place.

[TPR-03-003-codex] MEDIUM — build_method_sig helper typed against TypeParam but FunctionSig uses Name

Finding: GAP against typeck.md §CK-4 hand-off contract. §03.0’s proposed build_method_sig(..., type_params: &[TypeParam], ...) -> FunctionSig signature would not compile: FunctionSig.type_params is Vec<Name> (compiler/ori_types/src/output/mod.rs:378: pub type_params: Vec<Name>), and check_impl_method already receives type_params: &[Name] (compiler/ori_types/src/check/bodies/mod.rs:320-325: fn check_impl_method(checker, method, self_type, type_params: &[Name])). Following the plan literally produces an element-type mismatch when the helper’s type_params.to_vec() feeds FunctionSig.type_params.
Impact: The helper extraction that §03.0 requires BEFORE 03.3/03.4 is a compile-time dead end as written. That blocks the BLOAT gate and obscures whether later errors come from the validator wiring or the helper prototype.
Resolved: Corrected the helper signature from type_params: &[TypeParam] to type_params: &[Name] to match both the shipped FunctionSig.type_params: Vec<Name> and the caller’s check_impl_method/check_def_impl_method parameter type. Added a doc comment on the helper explaining the &[Name] choice with citations to compiler/ori_types/src/output/mod.rs:378 and compiler/ori_types/src/check/bodies/mod.rs:320-325 so a future reader cannot mistake Name for the AST-level TypeParam. Plan §03.0 updated in-place.

[TPR-03-004-codex] MEDIUM — Success criteria disagree: exact-4 grep vs helper-extraction

Finding: DRIFT against impl-hygiene.md §Algorithmic DRY. Frontmatter success criterion (lines 11-12) and §03.N (lines 1143-1144) required grep -rn 'validate_body_types' ... to return exactly 4 matches, and §03.N line 1145 expected exactly one use crate::check::validators import line. Meanwhile §03.4 Algorithmic DRY review (lines 892-896) recommended extracting a shared run_validator(...) helper to eliminate 4-site duplication. These gates cannot all be true: a helper collapses the raw validate_body_types matches below 4, while direct inline calls make the single-import gate brittle (two files require the use-statement). §03.N line 1158-1159 already accepted “either a shared helper OR the 4-line pattern consistently identical at all 4 sites”, so the gates at lines 11-12 and 1143-1145 contradicted the DRY directive the same section endorsed.
Impact: Section completion was self-contradictory. An implementation could satisfy the DRY direction OR the grep-based exit criteria, but not both reliably — success criteria non-verifiable as written.
Resolved: Rewrote both the frontmatter success criterion and the §03.N grep gate to explicitly accept EITHER (a) the inline 4-match shape OR (b) the helper-extracted shape (1 internal validate_body_types call + 4 run_validator call sites). Rewrote the use crate::check::validators criterion to accept either one import per split file (inline shape) or one import in the helper-owning file (extracted shape). Both shapes now satisfy the gate because the contract is site-coverage, not raw grep count. Plan frontmatter and §03.N updated in-place.

[TPR-03-005-codex] MEDIUM — Known Failing Tests audit only runs cargo st, but §06.2 surface includes tests/valgrind/ and library/

Finding: GAP against tests.md §Cross-Phase Verification and the plan’s own documented failure surface. §03.5.4 (lines 1022-1033) only instructed running timeout 150 cargo st and documenting new failures in the local Known Failing Tests block. But §06 success criteria (section-06-diagnostics-audit.md:13) and §06.2 (section-06-diagnostics-audit.md:78) expand the post-E2005 audit roots to tests/spec/, tests/valgrind/, AND library/ — specifically because empty-list regressions are not confined to the spec harness. tests/valgrind/cow/cow_list_concat.ori is already cited as a known operator-position hit outside tests/spec/ (section-06-diagnostics-audit.md:124, :210). Section 03’s transitional bookkeeping therefore under-approximated the failure surface §06.2 would later remediate.
Impact: Section 03 could report “no undocumented new failures” while expected E2005 breakage outside cargo st (valgrind programs, library/std programs) remained undocumented and only surfaced when ./test-all.sh ran. That weakens the section’s transitional-state bookkeeping and creates a silent audit-scope handoff gap between §03.5 and §06.2.
Resolved: Expanded §03.5.4 to (a) run ./test-all.sh as the authoritative multi-root gate covering tests/spec/, tests/valgrind/, and library/std/; (b) run the same rg '\[\s*\]' tests/spec/ tests/valgrind/ library/ --glob '*.ori' sweep that §06.2 uses, and cross-check the hit list against the Known Failing Tests table; (c) updated the “populate this list” instructions to scan all three roots, prefixing tests/valgrind/ and library/ entries so §06.2 picks them up from the same table. Added explicit rationale citing section-06-diagnostics-audit.md §06.2 so the expanded scope is anchored, not arbitrary. Plan §03.5.4 and Known Failing Tests guidance updated in-place.

Gemini half: empty envelope. Gemini was watchdog-killed at 23 min with zero tool_use events and no emitted findings (transport stall, not a review conclusion). Per the single-source fallback in .claude/skills/tpr-review/step-2-round-triage.md, Round 2 will re-run both reviewers with the same scope to confirm (a) the five fixes above hold under independent review, and (b) gemini completes a thorough investigation. Round 1 found 5 real defects — Round 2 must verify regression-freedom, not declare clean until gemini actually reviews.

Round 2 Findings — Carryforward from BUG-04-084 Phase 5 Code TPR (2026-04-17, dual-source)

Surfaced during /tpr-review of BUG-04-084’s implementation (end-of-body defaulting pass). Codex (HIGH trust) produced three findings; gemini returned clean. All three cite the PC-2 producer-side enforcement gap at check_test / check_impl_method / check_def_impl_method that this section’s §03.2, §03.3, §03.4 already exist to close. Filed here as plan-owned TPR items per .claude/skills/tpr-review/SKILL.md §7 (better-location deferral — concrete - [ ] anchors for the wiring work exist in §03.2/3/4 above). BUG-04-084’s fix intentionally pre-plumbs the defaulting pass in all four body-group passes so that when this section’s validator wiring lands, empty-literal-reachable vars do not spuriously fire E2005; the code comments in compiler/ori_types/src/check/bodies/functions.rs::check_test and bodies/impls.rs::check_impl_method / check_def_impl_method document this intent.

[TPR-03-004-codex-R2-F1][high] compiler/ori_types/src/check/bodies/functions.rs:~282 — Test-body path skips PC-2 validation after defaulting. Evidence: check_test calls engine.default_unbound_vars_from_empty_literals(...) and stores expr_types without a follow-up validate_body_types call. Mirror of the check_function body-pass surface (lines 161–183) is absent. Rule violated: typeck.md §CK-1 Pass 3, typeck.md §PC-2 producer-side enforcement note, typeck.md §DI-1 E2005 AmbiguousType emission. Required plan update: §03.2 “Wire validator into check_test” — already scoped. This finding confirms the scope and cites the PC-2 requirement as the driving rule. No plan edit needed; tracked by the existing §03.2 - [ ] items. Basis: direct code inspection + code TPR verification. Confidence: high. Resolved: Accepted on 2026-04-17. Code gap confirmed: functions.rs:282 calls default_unbound_vars_from_empty_literals with no follow-up validate_body_types call; validate_body_types has exactly 1 call site in the codebase (check_function only, line 161). Blocker verified: a spike wiring all three paths surfaced 169 pre-existing unresolved-var failures (documented in test-impact preview); systematic regression handling lives in §03.5.
§03.2 is now complete (2026-04-17). Code verified: `check_test` calls
run_validator at functions.rs:265 (shared helper extracted from check_function’s inline block for impl-hygiene.md §Algorithmic DRY). This finding is fully resolved — code gap closed.
[TPR-03-005-codex-R2-F2][high] compiler/ori_types/src/check/bodies/impls.rs:~202 — Impl methods default empties without enforcing E2005. Evidence: check_impl_method calls engine.default_unbound_vars_in_scope(...) inside the inference closure; no validate_body_types call runs after the closure returns or before build_method_sig / register_impl_sig exports the sig. Unrelated unresolved vars in impl method bodies and sig positions leak silently. Rule violated: typeck.md §CK-1 Pass 4, typeck.md §PC-2, typeck.md §DI-1. Additionally impl-hygiene.md §Cross-Phase Invariant Contracts — the typed IR the method exports may carry Tag::Var through register_impl_sig. Required plan update: §03.3 “Wire validator into check_impl_method (TPR checkpoint)” — already scoped. This finding cites the PC-2 + export-path invariant; tracked by existing §03.3 - [ ] items. Basis: direct code inspection + code TPR verification. Confidence: high. Resolved: Accepted on 2026-04-17. Code gap confirmed: impls.rs:202 calls default_unbound_vars_in_scope with no follow-up validate_body_types; build_method_sig
- register_impl_sig (line 246) export the sig with potential surviving Tag::Var. impls.rs does not import validate_body_types at all — the gap is deeper than just a missing call site. Blocker verified: same 169-failure spike (test-impact preview); systematic regression handling in §03.5. Additionally, impls.rs needs the import added before the call can land.
Concrete implementation in §03.3 "Wire validator into check_impl_method"
existing - [ ] items. Will be unblocked when §03.3 is complete.
[TPR-03-006-codex-R2-F3][high] compiler/ori_types/src/check/bodies/impls.rs:~328 — Def-impl methods also skip the post-inference validator. Evidence: check_def_impl_method calls engine.default_unbound_vars_in_scope(...) but does not call validate_body_types. Stateless trait defaults are inlined at use sites, so the validator gap is subtler than for impl methods, but PC-2 is still unenforced at this body pass. Rule violated: typeck.md §CK-1 Pass 5, typeck.md §PC-2, typeck.md §DI-1. Required plan update: §03.4 “Wire validator into check_def_impl_method” — already scoped. Tracked by existing §03.4 - [ ] items. Note: def-impl methods need a transient FunctionSig for validation (no register_impl_sig export path); see build_method_sig usage pattern. Basis: direct code inspection + code TPR verification. Confidence: high. Resolved: Accepted on 2026-04-17. Code gap confirmed: impls.rs:328 calls default_unbound_vars_in_scope with no follow-up validate_body_types; unlike check_impl_method, there is no register_impl_sig export, but check_expr-produced expr_types may still carry surviving Tag::Var. impls.rs does not import validate_body_types — import must be added. Blocker verified: same 169-failure spike (test-impact preview) + transient FunctionSig construction needed (no existing export sig to validate against); §03.5 handles regression triage.
Concrete implementation in §03.4 "Wire validator into check_def_impl_method"
existing - [ ] items. Will be unblocked when §03.4 is complete.

Test-impact preview (measured 2026-04-17): a spike that wired validate_body_types into all three paths (reverted) moved the spec suite from 3781 passed / 674 failed to 3612 passed / 843 failed — 169 pre-existing latent unresolved-var bugs surfaced. §03.5 “End-to-end regression suite and dual-execution parity” is the designed place to triage and fix those 169 failures as §03.2–03.4 wiring lands. Expect the failure count to grow during §03.2/3/4 implementation and shrink as root-cause bugs are fixed or filed via /add-bug.

Gemini Round 2 status: clean. Gemini explicitly verified the fix is well-scoped to empty-literal-reachable variables, is correctly wired into all four body-checking passes (defaulting side), respects phase-purity and signature-export invariants, and the accompanying test matrix is comprehensive. Gemini’s summary confirms no issues found with BUG-04-084’s implementation as-shipped — the PC-2 gap is a plan-sectioned deliverable, not a BUG-04-084 defect.

Round 3 Findings — §03.3 TPR Checkpoint (2026-04-17, dual-source clean)

Run via /tpr-review custom-objective covering §03.1, §03.2, §03.3 wiring code (compiler/ori_types/src/check/bodies/{mod,functions,impls,tests}.rs) per the §03.3 TPR-checkpoint requirement at line 789. Three focus questions: (a) ExprId::new(u32) bridge from ExprIndex (usize), (b) post-closure FunctionSig construction in check_impl_method (deviation from plan’s pre-closure prescription), (c) run_validator helper extraction at bodies/mod.rs:66 (pub(super), called from 3 sites today).

Codex (HIGH trust, 4.6 min, 4 tool uses): status: clean, findings: []. Summary verbatim: “ExprIndex is sourced from ExprId::raw(), the impl-method sig must be built after defaulting to reflect end-of-body truth, and run_validator is the correct DRY extraction for the three live sites.” Files read include all four bodies/ files plus check/validators/mod.rs, infer/mod.rs, output/mod.rs, and ori_ir/expr_id/expr.rs to verify the bridge.

Gemini (LOWER trust, 2.5 min, 7 tool uses): status: clean, findings: []. Summary verbatim: “(a) The ExprIndex to ExprId bridge is safe, using u32::try_from to handle a lossless cast guaranteed by the u32-based ExprId design. (b) Post-closure FunctionSig construction in check_impl_method is a deliberate and correct deviation from the initial plan, ensuring the validator sees post-defaulted types. (c) The run_validator helper is a clean extraction that correctly applies the Algorithmic DRY principle. No issues found.”

Consensus: Both reviewers independently validated all three architectural choices flagged by the §03.3 TPR-checkpoint scope. Loop exited at iteration_counter == 1 per §5 stop condition #1 (both status: clean AND verified findings empty). §03.3 wiring (check_impl_method site at impls.rs:239 calling run_validator after post-closure build_method_sig) confirmed architecturally sound.

03.N Completion Checklist

Exit Criteria: All 4 bodies-pass sites call validate_body_types via the run_validator helper (DRY-compliant). BUG-04-074 repro now type-checks cleanly via the combined §01 Value Restriction + §02 validator + §03 wiring + §03.BUG-FIXES defaulting path (not rejected at codegen, and specifically not rejected at typeck either when push(value: 10) or end-of-body defaulting resolves the element type). Annotated form compiles and runs with exit 0 via interpreter and AOT with parity verified. test_let_polymorphism_for_lambda_produces_function passes. Known spec-test failures (35 files, 844 E2005:AmbiguousType tests) are documented above with §06.2 remediation anchor. timeout 150 ./test-all.sh confirms the documented state. /tpr-review (full-section and intermediate 03.3 checkpoint) clean per §03.R resolved. /impl-hygiene-review found 14 findings (5 Critical + 6 Major + 3 Minor); F9-F12 auto-fixed; F1-F8 + F13-F14 plan-anchored in §01 retrospective subsections. Section 04 can now enable its debug_assert! hooks without them firing on legitimate well-typed IR.

03.N Close-Out Entry (2026-04-18)

/impl-hygiene-review findings

Scope: auto (active work arc since §01 started). Phase 3 deep analysis (Opus) surfaced 14 findings; Phase 4 cross-check (/tp-help Codex) validated severity. Summary:

ID	Severity	Category	Location	Disposition
F1	Critical	INVERTED-TDD:goal-drift	`blocks.rs:243-302` body_captures_outer	Plan-anchored in §01.R-HYGIENE
F2	Critical→Major	LEAK:side-logic	`infer/expr/mod.rs:~380-475` format functions	Plan-anchored in §01.R-SIDE-LOGIC
F3	Critical	LEAK:side-logic	`infer/expr/mod.rs:~345-373` check_collect_to_set	Plan-anchored in §01.R-SIDE-LOGIC
F4	Critical	LEAK:algorithmic-duplication	`infer/mod.rs:~50-110` InferEngine::new/with_env	Plan-anchored in §01.R-DRY
F5	Critical	LEAK:algorithmic-duplication	`blocks.rs:77,158 + sequences.rs:249` should_generalize+generalize 3x	Plan-anchored in §01.R-DRY
F6	Major	LEAK:algorithmic-duplication	`check/bodies/tests.rs:~1-40` parse_and_check duplicate	Plan-anchored in §01.R-TEST-HYGIENE
F7	Major	GAP	`blocks.rs:265-302` body_captures_outer blind spots	Plan-anchored in §01.R-HYGIENE (paired with F1)
F8	Minor	NOTE	`blocks.rs` enter_scope vs enter_rank_scope inconsistency	Plan-anchored in §01.R-TEST-HYGIENE
F9-F12	Major	DRIFT	Stale bug-ID annotations across 4 files	Auto-fixed (user pre-approved mechanical cleanup)
F13	Minor	NAMING	`check_empty_module_bodies` test name	Plan-anchored in §01.R-TEST-HYGIENE
F14	Minor	BLOAT	`pub(super) use blocks::*;` glob re-exports	Plan-anchored in §01.R-TEST-HYGIENE

Rationale for plan-anchoring (not /add-bug): Per CLAUDE.md §Ownership & Deferral “Plan Blockers Stay In Plan”, findings in code authored by active plan sections belong IN the plan, not filed as sibling /add-bug entries. All 10 actionable findings (F1-F8, F13, F14) are in code authored or touched by §01 or §02. Filing via /add-bug would create a plan→bug→bug chain that stalls forever (ref: 2026-04-17 empty-container commit-wall incident).

Plan impact: §01 status: complete → status: in-progress until the 4 retrospective subsections land. §03 can close cleanly now because its own deliverable (4-site validator wiring via run_validator helper) is structurally complete and reviewed; the findings are in §01 territory.

/improve-tooling section-close sweep

Verified every §03 subsection (03.0, 03.1, 03.2, 03.3, 03.4, 03.BUG-FIXES, 03.5) has a documented close-out per the section body’s audit trail. No cross-subsection tooling patterns required new tooling — the 4 sites were mechanically identical (the run_validator helper is the single cross-subsection pattern, and it was already captured by §03.0’s BLOAT-gate prerequisite work). Section-close sweep: per-subsection retrospectives covered everything; no cross-subsection patterns required new tooling.

/sync-claude section-close doc sync

Verified rules files are in sync with §03’s implementation:

typeck.md §PC-2 — already documents validate_body_types producer-side enforcement, the end-of-body defaulting pre-pass, and the fresh_instance_var_ids / scheme_var_ids exemption set. No update needed.
canon.md §4.2 — already documents the PC-2 output contract that §03’s wiring enforces. References validate_body_types and the four body-group passes. No update needed.
canon.md §4.0–4.6 — per-phase output invariants reflect the active pipeline. No drift.
CLAUDE.md §Type Checker Patterns — section already includes the Borrow dance for TraitRegistry and Tag guards; §03’s run_validator helper pattern is narrow enough that codifying it in CLAUDE.md would be premature (single-use 4-site pattern, not yet a broader idiom). No update.
No drift surfaced on §03 content; docs are fact-bound per user preference feedback_fact_bound_sync.md.

Repo hygiene

diagnostics/repo-hygiene.sh --check reports noise only (27 stale /tmp/ori-tpr-*/ scratch dirs from parallel TPR sessions). Per user preference feedback_never_destructive_git.md, these are NOT auto-cleaned — they may belong to parallel agent sessions with uncommitted work. This is a known chronic state tracked in state.sh hygiene status.

State cache refresh

After /commit-push lands §03.N’s changes, diagnostics/state.sh cache SHA will be refreshed by the commit-push skill’s Step 8 automation.

Section 03: Bodies-Pass Integration

Intelligence Reconnaissance

03.0 Prerequisite: split bodies/mod.rs (BLOAT gate)

03.1 Wire validator into check_function

03.2 Wire validator into check_test

03.3 Wire validator into check_impl_method (TPR checkpoint)

03.4 Wire validator into check_def_impl_method

03.5 End-to-end regression suite and dual-execution parity

03.5.1 — BUG-04-074 repro: end-to-end typeck regression pin

03.5.2 — Annotated form compiles and runs: AOT integration test

03.5.3 — Dual-execution parity via diagnostic script

03.5.4 — Full test suite

Known Failing Tests (Expected Until Section 06.2 Lands)

03.R Third Party Review Findings

Round 0 Findings (all accepted and integrated)

Round 1 Findings (single-source codex; gemini stalled watchdog-killed — 2026-04-15)

Round 2 Findings — Carryforward from BUG-04-084 Phase 5 Code TPR (2026-04-17, dual-source)

Round 3 Findings — §03.3 TPR Checkpoint (2026-04-17, dual-source clean)

03.N Completion Checklist

03.N Close-Out Entry (2026-04-18)

/impl-hygiene-review findings

/improve-tooling section-close sweep

/sync-claude section-close doc sync

Repo hygiene

State cache refresh

03.0 Prerequisite: split `bodies/mod.rs` (BLOAT gate)

03.1 Wire validator into `check_function`

03.2 Wire validator into `check_test`

03.3 Wire validator into `check_impl_method` (TPR checkpoint)

03.4 Wire validator into `check_def_impl_method`