Section 02 — Validator Module: validate_body_types()

Context

Section 01 (AST-based Value Restriction) and Section 02 are independent. Both feed into Section 03, which threads the new producer-side enforcement into the bodies pass.

The type checker’s output contract (typeck.md §PC-2, mirrored in types.md §PC-2) requires that no Tag::Var survive in any type position of the typed IR. Today this contract is documented but not enforced at the producer boundary — the only enforcement that exists is downstream (consumers debug_assert! on entry, per impl-hygiene.md §Cross-Phase Invariant Contracts). This section introduces the missing producer-side validator so that violations are caught inside ori_types with a proper E2005 diagnostic, before the IR is handed off to eval, ARC, canon, and codegen.

The validator lives in a new submodule compiler_repo/compiler/ori_types/src/check/validators/ modelled on the pub(crate) pattern of compiler_repo/compiler/ori_types/src/check/object_safety.rs (not a pub pattern — object_safety.rs exposes pub(crate) fn, not pub fn). Section 03 will call it from compiler_repo/compiler/ori_types/src/check/bodies/mod.rs after engine.take_errors() drains the inference accumulator.

Scope expansion (from Phase 2 /tp-help + Phase 1 plan-audit)

The draft version of this section was architecturally incomplete. Four issues surfaced under dual-source Plan TPR (Codex + Gemini) and six more via scripts/plan-audit.py. The corrections are woven into §§02.0–02.N:

1. Signature validation gap (CONSENSUS critical). typeck.md §PC-2 and §CK-4 make it explicit that FunctionSig.param_types and FunctionSig.return_type may carry fresh Tag::Var for unannotated params/returns at signatures-pass exit; those vars MUST be resolved by Bodies-group exit. The validator MUST walk the signature in addition to expr_types, or unannotated @f(x) = 42 leaks an unbound Var directly to codegen. Addressed by §02.1 and §02.2.
2. Public-API exposure scope (CONSENSUS critical). Promoting mod check to pub mod check would leak the entire type-checker internal layout (bodies/, exports/, imports/, registration/, …) as stable API. object_safety.rs — the cited precedent — is actually pub(crate) fn, NOT pub. Fix: keep mod check; private; add a single narrow re-export pub use check::validators::validate_body_types; at lib.rs. Addressed by §02.1 and §02.3.
3. Redundant bound-var tracking (CONSENSUS critical). The draft tracked FxHashSet<u32> of scheme-bound var ids. Per types.md §TF-1, Tag::BoundVar sets HAS_BOUND_VAR, NOT HAS_VAR. So HAS_VAR alone distinguishes “free unbound var” from “scheme-bound var”. The parameter is redundant — the walker simply recurses into the scheme body and silently skips any Tag::BoundVar it meets. Addressed by §02.2.
4. Latent pool bug: Tag::Scheme flag propagation. types.md §TF-3 requires PROPAGATE_MASK flags to be OR’d from every child into the parent, explicitly including schemes. The original compute_flags arm returned bare IS_SCHEME with no child-flag propagation — consequence: scheme wrapping body with HAS_VAR = true had HAS_VAR = false on the outer Idx, defeating types.md §TF-5 fast-path gate. Fix landed at compiler_repo/compiler/ori_types/src/pool/flags_compute.rs:169 (compute_flags_scheme()) — compute_flags moved out of pool/mod.rs to a dedicated sibling module during a subsequent pool refactor; bare pool/mod.rs:652 references in this section are stale anchors superseded by the current pool/flags_compute.rs:169 location. Addressed by §02.0.
5. plan-audit DEAD_PATH findings (6, major). Bare paths (lib.rs, check_error/mod.rs, infer/mod.rs, pool/accessors.rs, check/validators/mod.rs, check/validators/tests.rs) must be fully qualified or annotated as forward references (the last two are created by this section). Addressed inline throughout §§02.0–02.N.
6. plan-audit COMPLETION_TPL finding (1, major). Section 02 lacked a 02.N — Completion Checklist. Added in §02.N.
7. plan-audit BLOAT_RISK (1, minor). compiler_repo/compiler/ori_types/src/check/mod.rs is 408 lines (under the 500-line limit per compiler.md §File Organization). New validator logic lands in compiler_repo/compiler/ori_types/src/check/validators/mod.rs, a sibling submodule — check/mod.rs gains exactly one line (pub(crate) mod validators;). No refactor required.

Other high-value findings woven in:

• HAS_VAR cache staleness after unification (DRIFT). Flags are cached at intern time; VarState::Link(target) changes after. A Var with HAS_VAR = true may actually be resolved via link. Fix: call pool.resolve_fully(idx) before every HAS_VAR check at every walk step — not just the top level. Addressed by §02.2.
• Catch-all _ => {} leaking compound tags (LEAK). let x: Option<_> produces Tag::Applied containing an unbound Var. A catch-all would silently pass through. Fix: explicit handling of every compound tag; no silent drops. Addressed by §02.2.
• Algorithmic duplication (LEAK). compiler_repo/compiler/ori_types/src/pool/descriptor.rs:303 — Pool::visit_children — already performs tag-dispatched child recursion over every compound tag. Writing a second parallel ladder would be a second SSOT for “how to reach every child of a type” (impl-hygiene.md §Algorithmic DRY). Fix: reuse Pool::visit_children in the walker. Addressed by §02.2.
• One E2005 per ExprIndex (LEAK dedup). Multiple unbound Vars under one ExprIndex (e.g. {} produces key-var + value-var both unbound) must collapse to one diagnostic at that ExprIndex (impl-hygiene.md §Deduplication by (Code, Span) with Follow-On Suppression). Addressed by §02.2 and §02.4 T8.

02.0 Pool Scheme-Flag Propagation Fix (Prerequisite)

Source of truth: types.md §TF-3 — PROPAGATE_MASK flags SHALL be OR’d from every child into the parent for every compound tag, explicitly including schemes.

Shipped location: compiler_repo/compiler/ori_types/src/pool/flags_compute.rs:169 compute_flags_scheme(). pool/mod.rs:63 dispatches to this helper. Pool module was split during a later refactor; the historical pool/mod.rs:652 anchor in the original §02 audit trail is superseded by this path.

Original state (pre-fix at compiler_repo/compiler/ori_types/src/pool/mod.rs compute_flags):

// Scheme
Tag::Scheme => TypeFlags::IS_SCHEME,

The arm returns a bare IS_SCHEME bit with no child-flag propagation. This is a spec violation (types.md §TF-3) and a latent bug that would defeat the HAS_VAR fast-path gate (types.md §TF-5) that §02.2 depends on.

BLOAT_RISK status (post-refactor): pool/mod.rs is now 355 lines (under 500-line limit) after a subsequent module split moved compute_flags into the sibling pool/flags_compute.rs. pool/descriptor.rs gained pub(crate) visibility on Pool::visit_children per §02.2; otherwise unchanged in §02 scope. The historical BLOAT_RISK finding against pool/mod.rs is resolved by the split.

02.0.1 — Fix

• At compiler_repo/compiler/ori_types/src/pool/flags_compute.rs:169, compute_flags_scheme() returns:

  // Scheme: propagate PROPAGATE_MASK from the body (types.md §TF-3)
  Tag::Scheme => {
      // Spec: types.md §SC-1 — Scheme extra layout is
      // [var_count, var_id_1, ..., var_id_N, body_idx].
      // The body Idx is the LAST u32 in extra.
      let body_idx = extra[extra.len() - 1] as usize;
      let mut flags = TypeFlags::IS_SCHEME;
      flags |= TypeFlags::propagate_from(self.flags[body_idx]);
      flags
  }

  Verify the body-index offset against Pool::scheme_body (in compiler_repo/compiler/ori_types/src/pool/accessors.rs) — whatever the canonical accessor reads, compute_flags MUST read from the same layout slot. compute_flags runs during Pool::intern before the body Idx is re-wrapped by accessors, so it computes the offset directly from the extra slice rather than calling scheme_body(idx).

• Confirm that propagate_from exists and already masks to PROPAGATE_MASK per types.md §TF-3. If it does not (or its mask is stale), update it in the same change — flag-propagation asymmetries between Scheme and other compound tags are themselves DRIFT findings.

02.0.2 — Regression test

• Add to compiler_repo/compiler/ori_types/src/pool/tests.rs:

  #[test]
  fn scheme_wrapping_unbound_var_body_propagates_has_var() {
      // Spec: types.md §TF-3 — PROPAGATE_MASK must OR from scheme body.
      let mut pool = Pool::new();
      let var_idx = pool.fresh_var(/* rank */ 0);
      assert!(pool.flags(var_idx).contains(TypeFlags::HAS_VAR));
      let scheme_idx = pool.intern_scheme(&[], var_idx); // ∀. Var — body is the unbound var
      assert!(
          pool.flags(scheme_idx).contains(TypeFlags::HAS_VAR),
          "Tag::Scheme must propagate HAS_VAR from body per types.md §TF-3"
      );
      assert!(pool.flags(scheme_idx).contains(TypeFlags::IS_SCHEME));
  }

  Exact constructor names (fresh_var, intern_scheme) must be resolved against the real API in compiler_repo/compiler/ori_types/src/pool/construct/ at implementation time. If no public constructor exists for an empty-vars scheme, add one via #[cfg(test)] helper on Pool OR use the existing generalization path to build a scheme whose body is the unbound var.

• Add a negative companion to prove that a resolved body no longer sets HAS_VAR on the outer scheme:

  #[test]
  fn scheme_wrapping_resolved_body_does_not_set_has_var() {
      let pool = Pool::new();
      // Scheme whose body is `int` — fully resolved, HAS_VAR must not propagate up.
      let scheme_idx = pool.intern_scheme(&[], Idx::INT);
      assert!(!pool.flags(scheme_idx).contains(TypeFlags::HAS_VAR));
  }

02.0.3 — Completion criteria

• cargo test -p ori_types --lib pool::tests passes with both new tests.
• ORI_DUMP_AFTER_TYPECK=1 on any program containing a non-generalized scheme with an unbound body shows HAS_VAR = true on the scheme (observable via the flags column in the dump).
• No other compute_flags arm regressed — types.md §TF-3 compliance is uniform across every compound tag.

02.0b End-of-Body Defaulting Pre-Pass × Validator Interaction

InferEngine::default_unbound_vars_in_scope (compiler_repo/compiler/ori_types/src/infer/body_finalize/mod.rs:76) and the convenience wrapper default_unbound_vars_from_empty_literals (body_finalize/mod.rs:42) run BEFORE validate_body_types in every body-group pass per typeck.md §PC-2 “End-of-body defaulting pre-pass”.

• Scope-by-var, not scope-by-position: the pre-pass only defaults vars reachable from empty-literal roots; unrelated signature holes remain Unbound and correctly fire E2005 at validator time per typeck.md §PC-2 end-of-body defaulting pre-pass rationale.
• Site classification for empty-literal positions is AmbiguousTypeSite::EmptyList (selected by site_from_expr_kind at validators/mod.rs:95); the pre-pass elides most of these by substituting to NEVER before the validator runs.
• Caller invocation sites: compiler_repo/compiler/ori_types/src/check/bodies/functions.rs:197, functions.rs:318, compiler_repo/compiler/ori_types/src/check/bodies/impls.rs:369, impls.rs:614.
• This pre-pass is NOT documented inside validators/mod.rs itself by design (compiler.md §Phase-Specific Purity): the validator is a pure walker over post-inference state; defaulting policy lives in infer::body_finalize.

02.0b.1 — Completion criteria

• InferEngine::default_unbound_vars_in_scope is invoked by every body-group pass before validate_body_types.
• Empty-literal pre-pass substitutes via canonical pool::substitute::substitute_in_pool; flags + Merkle hashes refreshed (types.md §TF-3).
• Validator’s AmbiguousTypeSite::EmptyList arm fires ONLY for empty-literal positions the pre-pass could not default (e.g., positions outside expr_types reachable scope; positions whose vars are exempt yet still surface).
• Cross-section pointer: plans/typeck-inference-completeness/section-03-bodies-pass-integration.md carries the call-site wiring; this section documents the validator-facing contract only.

02.1 Validator Signature, Public Contract, and Narrow Re-Export

02.1.1 — New files

• compiler_repo/compiler/ori_types/src/check/validators/mod.rs
• compiler_repo/compiler/ori_types/src/check/validators/tests.rs

02.1.2 — Canonical signature

The shipped signature is 7-parameter — pool, expr_types, sig, sig_span, scheme_var_ids, ctx, errors — at compiler_repo/compiler/ori_types/src/check/validators/mod.rs:172. The three source-attribution closures (span, kind, param_span) are bundled into a single ValidatorContext<'a> config struct per compiler.md §API (>3 params → config struct).

pub struct ValidatorContext<'a> {
    /// Callable: `ExprIndex` → source `Span` for body diagnostics.
    pub span: &'a dyn Fn(ExprIndex) -> Span,
    /// Callable: `ExprIndex` → `ExprKind` for site classification.
    pub kind: &'a dyn Fn(ExprIndex) -> Option<ExprKind>,
    /// Callable: `(Lambda ExprIndex, param_index)` → parameter-token span.
    pub param_span: &'a dyn Fn(ExprIndex, usize) -> Option<Span>,
}

pub fn validate_body_types(
    pool: &Pool,
    expr_types: &FxHashMap<ExprIndex, Idx>,
    sig: &FunctionSig,
    sig_span: Span,
    scheme_var_ids: &[u32],
    ctx: &ValidatorContext<'_>,
    errors: &mut Vec<TypeCheckError>,
)

Per-parameter contract:

Per-ExprIndex site classification:

LambdaParam sites narrow the primary diagnostic span via narrow_to_lambda_param_span (validators/mod.rs:249) so the message points at the unresolved parameter token, not the whole lambda. Falls back to the lambda’s own span when no parameter carries HAS_VAR or ctx.param_span returns None.

Walker properties (load-bearing):

• The closure types in ValidatorContext keep the validator free of any typed-IR handle types (impl-hygiene.md §Phase Boundaries — Minimal boundary types).
• FunctionSig reused as-is from compiler_repo/compiler/ori_types/src/output/mod.rs (the typed-IR output module, NOT check/signatures/) — validator SHALL NOT duplicate or flatten its shape (impl-hygiene.md §SSOT).
• Validator is pure: inputs are immutable refs + closures; outputs are appended errors. No Salsa, no global state — trivially callable from any Salsa-tracked query (typeck.md §SL-1).
• Section 03’s check_def_impl_method site constructs a FunctionSig inline at the call site (plain pub struct with all-pub fields, verified at compiler_repo/compiler/ori_types/src/output/mod.rs:373); the validator’s interface remains uniform across all four body-checking call sites.

02.1.3 — Shipped imports

Verified at compiler_repo/compiler/ori_types/src/check/validators/mod.rs:46-53:

use rustc_hash::{FxHashMap, FxHashSet};

use ori_ir::{ExprKind, Span};

use crate::output::FunctionSig;
use crate::pool::VarState;
use crate::tag::Tag;
use crate::{AmbiguousTypeSite, ExprIndex, Idx, Pool, TypeCheckError, TypeFlags};

FxHashSet covers the exempt-set return type of build_exempt_var_ids; ExprKind and VarState were added when the site-classification + leak-alarm contracts shipped post-§08.3b.1.

02.1.4 — Narrow public re-export (TWO symbols)

• compiler_repo/compiler/ori_types/src/lib.rs:16 keeps mod check; private. The re-export at lib.rs:32 exposes exactly TWO symbols:

  pub use check::validators::{build_exempt_var_ids, validate_body_types};

  build_exempt_var_ids is the caller-side helper exposed for scheme-var exempt set construction; callers in check::bodies consume it when composing arguments to both the end-of-body defaulting pre-pass (§02.0b) and validate_body_types. The rest of check/ stays internal (impl-hygiene.md §API Stability — minimize pub surface).

02.1.5 — Completion criteria

• Signature at compiler_repo/compiler/ori_types/src/check/validators/mod.rs:172 matches §02.1.2 verbatim (7 parameters in declared order; ValidatorContext config struct at mod.rs:78).
• compiler_repo/compiler/ori_types/src/lib.rs:16 retains mod check; (no pub mod check); lib.rs:32 re-exports {build_exempt_var_ids, validate_body_types} exactly.
• cargo doc -p ori_types renders the rustdoc block cleanly with cross-references to Pool, FunctionSig, TypeCheckError, AmbiguousTypeSite, ValidatorContext.

02.2 Core Algorithm: Tag-Dispatch Child Recursion (Reusing Pool::visit_children)

02.2.1 — Algorithmic DRY: reuse, don’t clone

compiler_repo/compiler/ori_types/src/pool/descriptor.rs:303 already defines Pool::visit_children(&self, idx: Idx, mut f: impl FnMut(Idx)) — a tag-dispatch ladder covering every compound tag: simple containers (via has_child_in_data), Map, Result, Borrowed, Function, Tuple, Struct, Enum, Applied, Scheme, plus fallthrough for Named/Alias/Projection/primitives/ variables.

Per impl-hygiene.md §Algorithmic DRY (and specifically the “cross-crate / cross-module” heading + Remediation Hierarchy step 2 “higher-order function”), the validator SHALL call Pool::visit_children instead of building a parallel tag ladder. Concrete plan:

• Promote Pool::visit_children from its current fn (private to the pool::descriptor module) to pub(crate) fn in compiler_repo/compiler/ori_types/src/pool/descriptor.rs, so check::validators can call it. If the shape must change to cover Tag::Projection receiver + Tag::Applied args uniformly (it already does), no change is needed beyond visibility.
• If additional compound tags are reachable from typed IR that visit_children does NOT cover today (e.g., Tag::Option, Tag::Set, Tag::Range, Tag::Iterator, Tag::DoubleEndedIterator, Tag::Channel — which are has_child_in_data() simple containers — or Tag::List / Tag::Map which are already handled), verify coverage by reading the helper. If any compound tag reachable from post-inference IR is missing, EXTEND the helper (the fix lands in pool/descriptor.rs, not in the validator). Adding per-tag arms only in validators/ would re-introduce the algorithmic duplication this section is removing.

02.2.2 — Walker (post-§08.3b.1 BodyFinalize migration)

Shipped algorithm at compiler_repo/compiler/ori_types/src/check/validators/mod.rs:324 (collect_first_unbound_var) + mod.rs:402 (check_var_tag helper extracted to keep parent nesting depth ≤ 4 per impl-hygiene.md §Style):

fn collect_first_unbound_var(
    pool: &Pool,
    ty: Idx,
    span: Span,
    site: AmbiguousTypeSite,
    exempt: &FxHashSet<u32>,
    errors: &mut Vec<TypeCheckError>,
) -> bool {
    // Gate order: resolve_fully → HAS_ERROR → HAS_VAR
    // per TPR-02-R4-001-codex (typeck.md §ER-4 cascade suppression
    // precedes types.md §TF-5 fast-path).
    let ty = pool.resolve_fully(ty);
    let flags = pool.flags(ty);
    if flags.contains(TypeFlags::HAS_ERROR) { return false; }
    if !flags.contains(TypeFlags::HAS_VAR)  { return false; }

    match pool.tag(ty) {
        Tag::Var      => check_var_tag(pool, ty, span, site, exempt, errors),
        Tag::BoundVar => false,
        _             => /* recurse via Pool::visit_children, short-circuit on first emit */
    }
}

fn check_var_tag(...) -> bool {
    let var_id = pool.data(ty);
    match pool.var_state(var_id) {
        // Post-§08.3b.1: Unbound AND Generalized treated identically.
        // After BodyFinalize normalizes every generalized leaf to Tag::BoundVar
        // (typeck.md §PC-2), a surviving VarState::Generalized at validator
        // time is a leak alarm — emits E2005 unless the var is in the exempt
        // scheme-var set.
        VarState::Unbound { .. } | VarState::Generalized { .. }
            => emit_ambiguous_if_not_exempt(var_id, span, site, exempt, errors),
        VarState::Link { target }
            => collect_first_unbound_var(pool, *target, span, site, exempt, errors),
        // Rigid: user-annotated parametric type parameter, legitimate at PC-2 exit (typeck.md §UN-6).
        VarState::Rigid { .. } => false,
    }
}

Contract by VarState (post-§08.3b.1):

The previous version of this section (pre-§08.3b.1) documented Generalized as unconditionally exempt with multi-paragraph let-polymorphism rationale; that contract is OBSOLETE. The current discipline is scheme-var exempt set: legitimate polymorphism is named via scheme_var_ids at the call site, not inferred from VarState::Generalized membership. The exempt set covers union-find roots of scheme vars (built by build_exempt_var_ids), so rank-weighted union-find direction making a fresh instantiation var the root does not produce false positives.

Key properties:

• No bound_vars parameter. Tag::BoundVar sets HAS_BOUND_VAR, not HAS_VAR (types.md §TF-1); HAS_VAR gate admits only types reachable to an unbound Var; Tag::BoundVar arm is a no-op. Scheme bodies are reached via visit_children → pool.scheme_body(idx).
• resolve_fully at every step. Flags are cached at intern time (types.md §TF-2); VarState::Link { target } may resolve later (types.md §SC-3 substitution, typeck.md §UN-7 union-find). Resolved before flag reads at every recursive call.
• No _ => {} dropping compound tags. Catch-all recurses via visit_children; future tag landing in the pool is handled by the canonical walker (leak-hardening property).
• Tag::Projection treated as a leaf. Pool::visit_children does NOT recurse into Tag::Projection’s receiver child; safe because typeck.md §PC-2 bullet 3 guarantees normalization before bodies-pass exit.
• Short-circuit after first diagnostic. bool return lets callers collapse N unbound Vars under one (ExprIndex, site) into one E2005 (impl-hygiene.md §Deduplication). Each (ExprIndex, site) contributes at most one error.
• Exempt-set construction lives at build_exempt_var_ids. scheme_var_ids resolution to union-find roots is centralized via Pool::var_idx_for_id per impl-hygiene.md §Algorithmic DRY — no scattered linear scans across the typeck crate.

02.2.3 — Entry point (shipped)

pub fn validate_body_types(
    pool: &Pool,
    expr_types: &FxHashMap<ExprIndex, Idx>,
    sig: &FunctionSig,
    sig_span: Span,
    scheme_var_ids: &[u32],
    ctx: &ValidatorContext<'_>,
    errors: &mut Vec<TypeCheckError>,
) {
    // Build exempt root set from scheme vars + their union-find roots.
    let exempt = build_exempt_var_ids(pool, scheme_var_ids);

    // 1. Signature positions first (declaration order).
    //    No ExprKind in scope → site is Expression (generic fallback per plan §06.1 item 4).
    let sig_site = AmbiguousTypeSite::Expression;
    for param_ty in &sig.param_types {
        collect_first_unbound_var(pool, *param_ty, sig_span, sig_site, &exempt, errors);
    }
    collect_first_unbound_var(pool, sig.return_type, sig_span, sig_site, &exempt, errors);

    // 2. Body expressions in ascending ExprIndex order.
    // FxHashMap iteration is non-deterministic; sort once (impl-hygiene.md
    // §Pass determinism).
    let mut entries: Vec<(ExprIndex, Idx)> = expr_types
        .iter()
        .map(|(&k, &v)| (k, v))
        .collect();
    entries.sort_unstable_by_key(|(idx, _)| *idx);

    for (expr_idx, ty) in entries {
        let site = site_from_expr_kind((ctx.kind)(expr_idx));
        // LambdaParam: narrow span to the specific parameter token carrying HAS_VAR.
        let primary_span = match site {
            AmbiguousTypeSite::LambdaParam => {
                narrow_to_lambda_param_span(pool, ty, expr_idx, ctx.param_span)
                    .unwrap_or_else(|| (ctx.span)(expr_idx))
            }
            _ => (ctx.span)(expr_idx),
        };
        collect_first_unbound_var(pool, ty, primary_span, site, &exempt, errors);
    }
}

02.2.4 — Completion criteria

• collect_first_unbound_var delegates compound-tag recursion to pool.visit_children — grep shows no duplicated per-tag arms for List, Map, Tuple, Struct, Enum, Applied, Function, Scheme inside validators/ beyond the Tag::Var / Tag::BoundVar discrimination above.
• pool.resolve_fully(idx) is called at the top of every recursive step (enforce via a rustdoc assertion + a test that inserts a Link chain and verifies no false positive).
• No _ => {} arm in the match pool.tag(ty) block that drops a compound variant (the catch-all explicitly recurses).

02.3 lib.rs and check/mod.rs Wiring (No pub mod check)

02.3.1 — check/mod.rs

File: compiler_repo/compiler/ori_types/src/check/mod.rs (currently 408 lines; compiler.md §File Organization 500-line limit is respected — new logic lives in validators/, not in check/mod.rs).

Existing submodule declarations (private): accessors, api, bodies, exports, imports, object_safety, registration, scope, signatures, well_known, plus #[cfg(test)] mod integration_tests; and #[cfg(test)] mod tests;.

• Add, in alphabetical order immediately after mod signatures;:

  pub(crate) mod validators;

  The pub here is load-bearing: the re-export at lib.rs is pub use check::validators::validate_body_types;, which requires at least pub(crate) visibility on validators. Using pub(crate) mod validators; keeps the submodule callable from outside ori_types when the single re-exported function is accessed via its canonical path for testing. Verified at compiler_repo/compiler/ori_types/src/check/mod.rs:77.

02.3.2 — lib.rs

File: compiler_repo/compiler/ori_types/src/lib.rs

Current state (verified):

// Line 16:
mod check;
// Line 25:
pub mod reporting;
// Lines 32–35:
pub use check::{
    check_module, check_module_with_imports, check_module_with_pool,
    check_module_with_registries, ModuleChecker,
};

• KEEP mod check; (line 16) — do NOT promote to pub mod check. (The earlier draft of this section proposed promotion mirroring pub mod reporting;; Phase 2 /tp-help rejected that because the check-module hierarchy is strictly internal compiler plumbing — bodies, exports, imports, registration, scope, signatures, etc. — and object_safety.rs’s pub(crate) is the real precedent, not reporting’s pub.) Verified at compiler_repo/compiler/ori_types/src/lib.rs:16.
• Extend the existing pub use check::{ ... }; block to include validators::validate_body_types:

  pub use check::{
      check_module, check_module_with_imports, check_module_with_pool,
      check_module_with_registries, ModuleChecker,
  };
  pub use check::validators::validate_body_types;

  The two pub use lines stay separated: the first re-exports names directly from check; the second reaches into a submodule. Keeping them on distinct pub use statements matches the crate’s existing re-export style and makes the narrow scope of the validator export grep-visible. Verified at compiler_repo/compiler/ori_types/src/lib.rs:32-36.

02.3.3 — validators/mod.rs test module declaration

At the bottom of compiler_repo/compiler/ori_types/src/check/validators/mod.rs:

• Add:

  #[cfg(test)]
  mod tests;

  Body in compiler_repo/compiler/ori_types/src/check/validators/tests.rs (compiler.md §File Organization — sibling tests.rs, not inline). Verified at compiler_repo/compiler/ori_types/src/check/validators/mod.rs:231-232; scaffold tests.rs exists from §02.1 and §02.4 will populate it.

02.3.4 — Completion criteria

• grep -n "^pub mod check" compiler_repo/compiler/ori_types/src/lib.rs returns zero lines (the internal layout is not leaked). Verified 2026-04-15.
• grep -n "^pub use check::validators::validate_body_types;" compiler_repo/compiler/ori_types/src/lib.rs returns exactly one line. Verified 2026-04-15 — matches lib.rs:32.
• External consumers compile against ori_types::validate_body_types via the re-export; internal consumers use crate::check::validators:: validate_body_types as usual. Verified — cargo check -p ori_types --tests --lib succeeds on the current wiring.

02.4 Unit Test Matrix

Validator-specific tests live in compiler_repo/compiler/ori_types/src/check/validators/tests.rs (1187 lines, 27 cells). The cross-plan authoritative test matrix lives in plans/typeck-inference-completeness/section-05-test-matrix.md — §02.4 lists the validator’s per-cell pins; §05 cites them in the cross-plan matrix.

Use the behavioral naming shape <subject>_<scenario>_<expected> (impl-hygiene.md §Test Function Naming). Cells T1–T12 form the baseline matrix; T13+ extends coverage for the 7-param API + ValidatorContext + AmbiguousTypeSite + scheme-var exempt set contracts shipped post-§08.3b.1.

Baseline matrix (T1–T12)

Extension matrix (T13+ — shipped post-§08.3b.1)

02.4.1 — Scaffolding pattern

Tests construct a minimal Pool, allocate vars + types via the real pool construction API (no #[cfg(test)] helpers on Pool per impl-hygiene.md §Visibility), build a synthetic FxHashMap<ExprIndex, Idx>, a synthetic FunctionSig, and a ValidatorContext carrying three closures, invoke validate_body_types, assert on accumulated errors. ctx.span returns Span::new(0, 1) for every ExprIndex; sig_span uses Span::new(100, 101) so T3 can distinguish signature-origin from body-origin. ctx.kind returns the test’s intended ExprKind per ExprIndex (drives site classification); ctx.param_span returns None by default, populated only for LambdaParam cells.

Canonical T1 reference (shipped shape — see validators/tests.rs:164 for the live cell): construct Pool + fresh var; insert var into expr_types at one ExprIndex; build FunctionSig inline with the all-pub field set from output/mod.rs:373 (defaults vec![] / false / 0; return_type: Idx::INT); build ValidatorContext { span: &|_| Span::new(0,1), kind: &|_| None, param_span: &|_, _| None }; invoke validate_body_types(&pool, &expr_types, &sig, Span::new(100,101), &[], &ctx, &mut errors); assert errors.len() == 1 + matches!(errors[0].kind(), TypeErrorKind::AmbiguousType { .. }).

FunctionSig field count growth → add #[cfg(test)] helper in output/tests.rs (sibling test file for output/mod.rs), NOT in validators/tests.rs (keeps construction local to the SSOT module per impl-hygiene.md §SSOT).

02.4.2 — Completion criteria

• All 27 cells (T1–T12 baseline + T13–T26 extensions + T27 structural invariant) present in compiler_repo/compiler/ori_types/src/check/validators/tests.rs with behavioral <subject>_<scenario>_<expected> names + /// doc comments citing spec clause / rule anchor.
• T10 semantic pin: reverting compute_flags_scheme at pool/flags_compute.rs:169 to return bare IS_SCHEME causes scheme_wrapping_unbound_var_body_emits_one_e2005 to fail per the defensive HAS_VAR assertion; restoring the propagation block makes it pass.
• T7 leak-alarm pin: substituting VarState::Generalized into expr_types outside the scheme-var exempt set fires E2005 (post-§08.3b.1 BodyFinalize migration); pre-migration behavior (exempt-on-Generalized) would silently pass.
• T13–T15 union-find chain pins: rank-weighted union-find direction (typeck.md §UN-7) making fresh instantiation vars the roots is covered by build_exempt_var_ids resolution.
• T21 + T25 + T26 site-classification pins: AmbiguousTypeSite::EmptyList, LambdaParam, Expression each have at least one cell verifying message wording per plan §06.1.
• cargo test -p ori_types --lib check::validators::tests passes (27/27).
• No cell uses an ephemeral identifier (plan name, section number, bug ID) in its test function name per impl-hygiene.md §Test Function Naming. Provenance lives in /// doc comments only.

02.R Third-Party Review — Round Summary

Per state-discipline.md §4 review_pipeline frontmatter discipline, per-round commit attribution lives in the section’s review_pipeline: frontmatter (above); per-finding details live in the cited commit messages. The four-round close-out resolved 15 findings.

Post-R4 contract evolution (NOT reviewed under R1–R4; documented retroactively for plan completeness):

• §08.3b.1 BodyFinalize migration changed VarState::Generalized from exempt to leak-alarm (treated identically to Unbound unless var_id ∈ exempt). See typeck.md §PC-2 for the unified contract; §02.4 T7 + T18 are the validator-side pins.
• 7-param API + ValidatorContext config-struct refactor (parameter bundling per compiler.md §API) + scheme_var_ids + build_exempt_var_ids helper landed for §06.1 site-classification (AmbiguousTypeSite::EmptyList | LambdaParam | Expression); §02.4 T13–T15 + T21 + T25 + T26 are the validator-side pins.
• The historical R1–R4 cure preserved the validator’s invariants (cascade suppression, dedup, deterministic order, scheme-var exempt set); post-R4 evolution extended the surface (Generalized leak alarm, site classification, exempt root resolution) without invalidating those invariants.

Commit audit trail (canonical sequence — state-discipline.md §6 known-state.json cross-reference):

6e47956a (§02.0 pool fix) → 19f68757 (§02.1–02.3 validator skeleton + wiring) → c41c2bcd (§02.4 twelve-cell matrix) → 342731aa (TPR-02-R4-001 gate-order fix) → 3a9b24fb (§02 hygiene review — banner removal + bug filings) → dd267552 (§02 tooling section-close sweep — BUG-07-012 filing) → 0d5dd41f (§02 docs sync — rules + downstream plan sections).

02.N Completion Checklist

At section completion (mirrors 01.N / 03.N shape), before flipping status: complete:

• All of §§02.0, 02.1, 02.2, 02.3, 02.4 checkboxes ticked.
• timeout 150 ./test-all.sh passes (debug build). Verified 2026-04-15: 15,341 tests across Rust unit / runtime / AOT / interpreter spec pass. LLVM spec backend crash filed as BUG-04-085 (unrelated subsystem — ArcIrEmitter + monomorphization of imported assert_eq); gate treats as non-failing per existing BUG-04-030 weakening (note: BUG-04-030 is resolved; retargeting the gate’s reference to BUG-04-085 is a follow-up tracked in the BUG-04-085 filing).
• timeout 150 cargo test --release -p ori_types passes (release build). Verified 2026-04-15: 820/820 lib tests pass.
• timeout 150 ./clippy-all.sh clean — no new warnings.
• cargo doc -p ori_types renders the new validate_body_types rustdoc block without broken intra-doc links. Verified 2026-04-15: no warnings mentioning validators or validate_body_types; 11 pre-existing warnings in unrelated files (type_error/problem/mod.rs etc.) predate this section.
• diagnostics/repo-hygiene.sh --check clean — no untracked temp files.
• /tpr-review run on this section’s diff; findings accepted into 02.R and resolved per CLAUDE.md §NEVER reason out of TPR findings. Run on 2026-04-15, scratch /tmp/ori-tpr-CTYOnQbk. Codex-only best-effort clean (user-accepted): gemini-3.1-pro-preview hit gemini_api_capacity on 5/5 retry attempts (~45min total, persistent upstream capacity pressure, not a prompt issue). Codex completed 4 full runs with deep investigation (7 rules consulted, 25 files read, 2 tests rerun incl. §02.0 semantic pin, basis=fresh_verification, confidence=high). One finding surfaced — TPR-02-R4-001-codex [medium] DRIFT [ER-4, TF-5] in gate order at validators/mod.rs:161 — independently verified against the code per CLAUDE.md §Reviewer grounding, fixed in commit 342731aa, and recorded in §02.R above. Prior §02 review-plan cycles (R1 + R3) were full dual-source; 11 findings resolved across those rounds. User accepted codex-only on 2026-04-15 as the best-effort close-out path given the upstream infra block — gemini retry to reach full dual-source consensus remains open as a backlog item if the user wants to re-verify once capacity recovers.
• /impl-hygiene-review run AFTER /tpr-review is clean — no new LEAK / DRIFT / GAP findings introduced by this section. Run on 2026-04-15, auto-scoped to the §02 work arc. Four passes (LEAK/SSOT, Algorithmic DRY, Boundary/Flow, Surface Hygiene) + Phase 0 auto-lint. Phase 4 /tp-help cross-check skipped — codex-only for the same gemini capacity reason as Phase B1; the earlier codex TPR already served as the third-party review for this work and cited impl-hygiene.md rule anchors. Outcome: §02-scope code is clean — no NEW LEAK/DRIFT/GAP introduced. Two pre-existing findings surfaced in adjacent code (not §02’s responsibility but tracked per CLAUDE.md “ownership irrelevant” rule): (1) [BUG-02-007][high] LEAK:algorithmic-duplication in unify/generalization.rs::collect_free_vars_inner — clones Pool::visit_children’s tag-dispatch ladder. Extraction path documented in the bug entry. (2) [BUG-02-006][minor] BLOAT in ori_types/src/pool/ — mod.rs 699 LOC, descriptor.rs 510 LOC, three over-100-line functions. Submodule-extraction plan documented in the bug entry. Eight self-introduced BLOAT banners in validators/tests.rs were auto-fixed by hygiene-lint.py --fix --apply (no commit ref on that alone — bundled into the same commit as the bug-tracker entries and this checklist update).
• /improve-tooling retrospective sweep — any pain points encountered while implementing §§02.0–02.4 captured as concrete tracked items. Run on 2026-04-15 as the Phase B3 section-close safety net. Verified per-subsection retrospectives ran: §§02.0–02.3 closed out in prior session commits with their own retrospectives (per the plan’s standard close-out pattern); §02.4 retrospective documented “no tooling gaps — pool construction API, FunctionSig::simple, and cargo test path selectors worked fluently.” Cross-subsection pattern analysis surfaced ONE concrete tooling gap invisible at per-subsection scope: (1) [BUG-07-012][minor] dual-tpr transport discards codex’s successful envelopes when gemini fails persistently — no codex.final.envelope.json preserved on infra failure. Filed with full repro + proposed fix. Blast radius across all dual-source consumer skills (tpr-review, review-work, tp-help, review-plan), so /fix-bug BUG-07-012 will run full TPR + hygiene review on the transport change. Not implemented inline because the fix touches the shared dual-tpr transport which is used by multiple skills and deserves its own dedicated review cycle. Two other observations did NOT warrant filing: intel-graph underuse in Pass 2 DRY scan is a process improvement (documentation, not tooling); T10 semantic-pin revert/restore is one-off enough that automating it would be premature abstraction.
• /sync-claude — .claude/rules/typeck.md, types.md, and CLAUDE.md audited for drift introduced by the new public symbol and the §02.0 flag-propagation fix; updates committed if needed. Run on 2026-04-15 as the Phase C1 doc sync. Drift audit found two gaps: (1) typeck.md §PC-2 (output contract) did not mention validate_body_types as the producer-side enforcement point. Added a paragraph documenting the gate order, visit_children delegation, and the consumer-only debug_assert! risk without it. (2) typeck.md §17 Key Files did not list compiler_repo/compiler/ori_types/src/check/validators/mod.rs or its sibling test file. Added two rows after check/object_safety.rs (the pattern precedent). (3) canon.md §4.2 (type-checker output invariants) likewise did not point at the producer-side enforcement. Added a paragraph. types.md §TF-3 already specified the correct PROPAGATE_MASK behavior for Tag::Scheme — the §02.0 fix brought code into compliance with existing docs, no doc update needed. CLAUDE.md §Key Paths is a top-level directory index; adding a validator submodule would bloat it. No CLAUDE.md changes.
• Sections 03, 05, 00-overview.md synced to final §02 API (TPR-02-R3-001, R3-003, R3-004 resolutions). Completed as Phase C2 alongside /sync-claude: §03’s dependency block rewritten to the shipped six-parameter validator signature with narrow re-export (resolves TPR-02-R3-003); §03’s code-example span placeholder replaced with the concrete arena.get_expr(ExprId::from_raw(expr_index as u32)).span recipe (resolves TPR-02-R3-004); §05’s test matrix table synced to the twelve shipped test names with behavioral naming + T10 semantic-pin note (resolves TPR-02-R3-001); 00-overview.md effort table updated from “11 cells” to “12 cells”.
• /commit-push — single commit or ordered commit sequence per CLAUDE.md §Stabilization Discipline (multi-commit ordering). Completed as an ordered commit sequence across the §02 close-out: 6e47956a (§02.0 pool fix), 19f68757 (§02.1-02.3 validator skeleton + wiring), c41c2bcd (§02.4 twelve-cell matrix), 342731aa (TPR-02-R4-001 gate-order fix), 3a9b24fb (§02 hygiene review — banner removal + bug filings), dd267552 (§02 tooling section-close sweep — BUG-07-012 filing), 0d5dd41f (§02 docs sync — rules + downstream plan sections to final API). This final commit closes out the section.
• Frontmatter: this section’s status → complete; all subsection status → complete. All §§02.0–02.4 subsection statuses: complete. §02.R: complete (15/15 findings resolved across R1, R3, R4). §02.N: complete (this checklist). Section frontmatter status flipped from in-progress to complete in this commit.
• plans/typeck-inference-completeness/00-overview.md “Quick Reference” table: Section 02 row → Complete. Updated in this commit. (Plan renamed from empty-container-typeck-phase-contract on 2026-04-23 per scope expansion documented in 00-overview.md; historical anchors in this section preserved at their original commit SHAs.)
• plans/typeck-inference-completeness/index.md updated if corpus convention requires. index.md Quick Reference uses ID/Title/File layout (no Status column); no update needed. Plan’s index.md frontmatter is for the reroute registry and not section-specific.
• plans/typeck-inference-completeness/section-03-bodies-pass-integration.md frontmatter depends_on: ["01", "02"] — verified on 2026-04-15: depends_on: ["01", "02"] at section-03-bodies-pass-integration.md:22. Both §01 and §02 are status: complete, so §03 has zero unresolved external blockers when /continue-roadmap plans/typeck-inference-completeness resumes.
• Sections 03, 05, 00-overview.md, and index.md updated to reference the shipped 7-parameter validate_body_types API (pool, expr_types, sig, sig_span, scheme_var_ids, ctx: &ValidatorContext<'_>, errors), the private mod check; design (no pub mod check), and the 27-cell validator matrix (T1–T12 baseline + T13–T27 extensions). Phase C2 sync landed at commit 0d5dd41f for the original 6-param API; the API has since evolved to 7-param + ValidatorContext + AmbiguousTypeSite per typeck.md §PC-2 post-§08.3b.1; downstream sections re-verified for the current signature shape — 00-overview.md architecture diagram + §03 + §05 carry the current API.

Cross-Section File Contention

The following files are touched by §02 AND by other sections. The ordering dependency is noted to prevent merge conflicts and partial-state commits (CLAUDE.md §Stabilization Discipline):

API Divergences from User Instructions

The following divergences from earlier drafts / the Phase 1 /tp-help briefing were identified by reading the actual source files and the /tp-help consensus. The plan above uses the verified real API throughout:

1. pool.children(ty) does not exist. The earlier draft listed this as the child-recursion API. The real pool has tag-specific accessors only. The canonical tag-dispatch walker is Pool::visit_children at compiler_repo/compiler/ori_types/src/pool/descriptor.rs:303 — §02.2 reuses it (impl-hygiene.md §Algorithmic DRY).

2. pool.var_id(ty) does not exist. The earlier draft listed pool.var_id(ty) as the accessor for the var_id of a Tag::Var. The real API is pool.data(ty) which returns the u32 var_id for a Tag::Var per types.md Appendix B (“data = var_id” for the type- variable range).

3. pool.scheme_vars(idx) returns &[u32], not Vec<u32>. Not a concern for this section anymore — the scheme-aware walk no longer consults scheme_vars at all. Scheme bodies are reached via Pool::visit_children → pool.scheme_body(idx), and HAS_VAR on the outer scheme (given §02.0’s fix) is sufficient to decide whether to recurse.

4. TypeCheckError::ambiguous_type is confirmed. Real at compiler_repo/compiler/ori_types/src/type_error/check_error/constructors.rs (the earlier bare path check_error/mod.rs was imprecise — the TypeCheckError::ambiguous_type constructor lives in the sibling constructors.rs module inside check_error/; the plan-audit DEAD_PATH finding is addressed by citing the qualified directory compiler_repo/compiler/ori_types/src/type_error/check_error/ and deferring the exact file to implementation time).

5. lib.rs:16 has mod check; (private). The earlier draft promoted this to pub mod check; mirroring the pub mod reporting; pattern at line 25. Phase 2 /tp-help CONSENSUSED against the promotion — it would leak the whole internal check/ hierarchy as stable API. This section §02.3.2 instead adds a single narrow re-export pub use check::validators::validate_body_types;, matching the pub(crate) / single-function-exposure pattern of compiler_repo/compiler/ori_types/src/check/object_safety.rs.

6. ExprIndex is a type alias usize, not a newtype (verified at compiler_repo/compiler/ori_types/src/infer/mod.rs). The FxHashMap<ExprIndex, Idx> uses usize keys; sorting by *idx works directly.

7. bound_vars: &[u32] parameter removed. The earlier draft threaded a scheme-bound-var-id set through every recursive call. Phase 2 /tp-help CONSENSUSED that HAS_VAR alone distinguishes free from bound vars per types.md §TF-1 (Tag::BoundVar sets HAS_BOUND_VAR, not HAS_VAR), so the set is redundant. Signature dropped.

8. Tag::Scheme compute_flags arm is a bug, not a constraint. The earlier draft treated the pool’s HAS_VAR = false on schemes as fixed. §02.0 fixes it per types.md §TF-3; T10 in §02.4 is the semantic pin.