0%

Intelligence Reconnaissance

Queries run 2026-04-23 (Phase 2 Pass 3 + 2.6B consultation):

  • scripts/intel-query.sh --human file-symbols "body_finalize" --repo ori — inventory the existing defaulting pre-pass. Result: default_unbound_vars_from_empty_literals + default_unbound_vars_in_scope + helpers is_empty_collection_literal + collect_unbound_reachable_vars all live in body_finalize/mod.rs (267 lines). 4 call sites in check/bodies/{functions,impls}.rs.
  • scripts/intel-query.sh --human similar "never_type_fallback" --repo rust --limit 10 — surface Rust’s complete fallback algorithm (rustc_hir_typeck/src/fallback.rs:22-400). Uses coercion-graph DFS from diverging roots.
  • scripts/intel-query.sh --human callers "infer_none" --repo ori — single call site from infer_expr in mod.rs. Same for infer_ok/infer_err/infer_some.
  • Prior /tp-help consultation (2026-04-23 round 1) and /tpr-review Phase 2.6B confirm: Ori’s simple predicate-extension approach is sufficient; coercion-graph port is unwarranted complexity given Ori’s invariance and lack of subtyping.

Results summary (≤500 chars) [ori]: is_empty_collection_literal matches 4 ExprKind variants — List, ListWithSpread, Map, MapWithSpread. collect_unbound_reachable_vars walks type structure via Pool::visit_children, collecting VarState::Unbound vars not in the exempt set (from FunctionSig.scheme_var_ids). Substitution via substitute_in_pool covers expr_types + param_types + return_type in one pass; defense-in-depth via direct VarState::Link { target: Idx::NEVER } assignment. §11.1 extends the predicate to 3 additional ExprKind variants: None, Ok, Err (Some INTENTIONALLY EXCLUDED per R7-010 introducer-only rule — see §11.1.3 Design for the infer_some vs infer_none/infer_ok/infer_err asymmetry rationale). The collector’s existing behavior (walks Option<Var> / Result<T, Var> / Result<Var, E> and collects Var children) works without modification — just the entry predicate needs extension.

Section 11: Inference Fallback for Unconstrained Bottom-Instantiable Roots

Goal: Close the last root-cause class of the §06.2C 28-file ledger — unconstrained None/Ok(x)/Err(x)/Some(x) leaking Tag::Var to PC-2 validation. Extends the existing empty-literal defaulting pre-pass with constructor root predicates. Ships silent fallback per Rust 2024 Edition direction (both reviewers 2.6B: NO lint).

Depends on: §03 (the existing defaulting pre-pass §11.1 extends), §09 (MUST complete first — landing §11.1 before §09 would mask §09 BD-2 failures with fallback, per both reviewers 2.6B).

Sequencing rule: §11.1 MUST run AFTER §09.1 + §09.2 + §09.3 + §09.4 + §10.0 + §10.1 + §10.2 all complete. The pipeline ordering in check/bodies/{functions,impls}.rs (inference → default_unbound_vars_from_empty_literals → normalize_body_generalized_to_bound_var → validate_body_types) ensures that any vars §09 BD-2 would have pinned are already pinned before §11.1’s defaulting pass runs. Landing §11.1 first without §09 in place would silently default vars that BD-2 should have constrained — inverting correctness.

11.1 Polymorphic-constructor defaulting — extend predicate

Goal: Extend is_empty_collection_literal at body_finalize/mod.rs:225-233 to also match ExprKind::None, ExprKind::Ok(inner), ExprKind::Err(inner). Rename to is_defaulting_root for accuracy. ExprKind::Some(inner) is EXCLUDED from the defaulting-root predicate per TPR Round 7 R7-010 (codex finding, editor-confirmed via infer/expr/constructors.rs:40-49 source inspection: infer_some uses inner_ty = infer_expr(inner) — NOT fresh_var() — so Some never introduces a root-level unbound payload var; the only Tag::Var reachable from a Some(x) expression is whatever inner itself introduces, which is owned by its own defaulting-root classification, not by Some). Adding Some to the root predicate would cause collect_unbound_reachable_vars to walk into inner_ty and aggressively default payload vars that §09.3’s check_some BD-2 gate was supposed to pin — inverting correctness. No changes to collect_unbound_reachable_vars — the existing tree-walking behavior works correctly for Option<Var> / Result<T, Var> / Result<Var, E> shapes produced by None / Ok(x) / Err(x).

Scoped-descendants invariant (Codex 2.6B + R7-010 refinement): defaulting-root classification is introducer-only — a constructor is a defaulting root ONLY if it introduces a fresh var at the constructor level that no other call site will constrain. Per constructors.rs:10-55:

  • infer_none → Option<fresh_var> — fresh var INTRODUCED at None, defaulting-root. ✓
  • infer_ok(inner) → Result<inner_ty, fresh_var> — err-slot fresh var INTRODUCED at Ok(x), defaulting-root. ✓
  • infer_err(inner) → Result<fresh_var, inner_ty> — ok-slot fresh var INTRODUCED at Err(e), defaulting-root. ✓
  • infer_some(inner) → Option<inner_ty> — NO fresh var introduced at Some level; inner_ty comes from infer_expr(inner). NOT a defaulting root. For Some([]), the List([]) inner expression IS a defaulting root (its own classification); the cascade happens through the inner’s classification, not through Some’s. Tests test_naked_some_with_empty_list_cascades_defaulting verify the cascade works via inner classification.

Load-bearing pass-ordering invariant (R7-009 + R7-011): §11.1 defaulting assumes §09 BD-2 propagation has run and every var §09 would have pinned is already VarState::Link (not VarState::Unbound) at defaulting time. This invariant is enforced at two layers:

  1. Code-location ordering — check/bodies/{functions,impls}.rs call default_unbound_vars_from_empty_literals AFTER InferEngine body inference (which includes §09.1/§09.3/§09.4’s check_expr BD-2 gates) and BEFORE validate_body_types. See call sites: compiler/ori_types/src/check/bodies/functions.rs:134,256 + impls.rs:203,347.
  2. Runtime debug-assert — body_finalize/mod.rs adds a debug_assert! at the entry of default_unbound_vars_from_empty_literals / default_unbound_vars_in_scope confirming that any expression ExprId marked for defaulting has had its body-inference pass complete. Shape: debug_assert!(engine.body_inference_complete(), "§11.1 defaulting ran before body inference finished — this would mask §09 BD-2 bugs by defaulting vars that BD-2 should have pinned. See plans/typeck-inference-completeness/00-overview.md §Design Principle 3."). The engine.body_inference_complete() method is a new InferEngine flag set to true at the end of body inference (after check_expr has run over the body root) and checked here. This turns pass-order inversion from a silent masking bug into a panic in debug builds.

Why the debug_assert is load-bearing: prose-only ordering notes in a plan file are invisible to a future refactor. If someone moves the defaulting call site earlier in the pipeline (e.g., attempts to run it inside check_expr for perf), the silent masking manifests as green tests + wrong semantics (vars that BD-2 should have pinned get defaulted to Never). The debug_assert surfaces the inversion at the exact point of violation, with a pointer to this overview rule.

11.1.1 Discovery + root cause verification

  • Re-read compiler_repo/compiler/ori_types/src/infer/body_finalize/mod.rs:42-267 — confirm the current flow: iterate expr_types, gate on is_empty_collection_literal, walk via collect_unbound_reachable_vars, substitute via substitute_in_pool, link vars in pool.
  • Confirm is_empty_collection_literal at lines 225-233 matches only 4 ExprKind variants: List(range) if empty, ListWithSpread(range) if empty, Map(range) if empty, MapWithSpread(range) if empty.
  • Confirm infer_none/infer_ok/infer_err/infer_some at infer/expr/constructors.rs:10-55 allocate fresh_var() for unconstrained slots: infer_none → Option<fresh_var>; infer_ok → Result<inner_ty, fresh_var>; infer_err → Result<fresh_var, inner_ty>; infer_some → Option<inner_ty> (inner_ty comes from infer_expr(inner), NOT fresh).
  • Verify collect_unbound_reachable_vars at lines 241-267 correctly walks Option<Var> via Pool::visit_children — Option is a single-child tag; visit_children yields the inner.
  • Verify the scoped-descendants invariant: test that Some(x) with constrained x does NOT default any var. Example: let y: int = 42; let z = Some(y); — z: Option<int>; no Tag::Var to default.
  • Write TDD matrix BEFORE implementation:
    • Positive test_naked_none_defaults_to_option_never — let x = None; x compiles clean; x: Option<Never>.
    • Positive test_naked_ok_with_payload_defaults_err_to_never — let r = Ok(42); r compiles clean; r: Result<int, Never>.
    • Positive test_naked_err_with_payload_defaults_ok_to_never — let r = Err(\"boom\"); r compiles clean; r: Result<Never, str>.
    • Positive test_naked_some_with_empty_list_cascades_defaulting — let o = Some([]) defaults outer Some’s wrap + inner List<Never>.
    • Scoped-descendants test_some_with_constrained_payload_does_not_default_unrelated_vars — fixture where Some(x) has x constrained elsewhere; Some is not a defaulting root because its payload var is Link, not Unbound.
    • Negative test_non_constructor_root_does_not_default — random unbound Tag::Var from a different expression (not reachable from a defaulting root) continues to fire E2005.
    • Interaction with §09 test_ok_under_check_result_does_not_default_because_bd2_pinned — let r: Result<int, str> = Ok(42) has §09.3 BD-2 propagation pin the err var to str; §11.1 finds no Unbound var to default. Regression guard for §09/§11 ordering.
    • Regression guard test_empty_literals_corpus_unchanged — run tests/spec/types/empty_literals/ pre/post §11.1; identical pass/fail counts (21 files, 0 failures each).

11.1.2 Design

Fix shape:

  1. Rename is_empty_collection_literal → is_defaulting_root (or similar; name choice TBD but should NOT imply “empty” since Ok(x)/Err(x) may have non-empty payloads).
  2. Extend the match at lines 225-233 — Some is INTENTIONALLY OMITTED per R7-010 introducer-only rule above: 
    fn is_defaulting_root(arena: &ExprArena, kind: &ExprKind) -> bool {
    match kind {
        ExprKind::List(range) => arena.get_expr_list(*range).is_empty(),
        ExprKind::ListWithSpread(range) => arena.get_list_elements(*range).is_empty(),
        ExprKind::Map(range) => arena.get_map_entries(*range).is_empty(),
        ExprKind::MapWithSpread(range) => arena.get_map_elements(*range).is_empty(),
        // §11.1 additions — constructors that INTRODUCE a fresh var at the
        // constructor level (per introducer-only rule, R7-010 codex):
        ExprKind::None => true,   // Option<fresh_var> introduced by infer_none
        ExprKind::Ok(_) => true,  // Result<inner_ty, fresh_var> — err slot introduced by infer_ok
        ExprKind::Err(_) => true, // Result<fresh_var, inner_ty> — ok slot introduced by infer_err
        // ExprKind::Some INTENTIONALLY OMITTED — infer_some uses inner_ty
        // from infer_expr(inner), not fresh_var; no root-level var is
        // introduced at Some, so adding it here would default payload vars
        // that §09.3's check_some BD-2 gate should have pinned.
        _ => false,
    }
}
  3. NO changes to collect_unbound_reachable_vars — existing Pool::visit_children walk handles Option<Var> / Result<T, Var> / Result<Var, E> correctly. The introducer-only invariant falls out of (a) the predicate match excluding Some and (b) VarState::Unbound filter — if a var is Linked (constrained), it’s skipped.
  4. NO changes to substitute_in_pool or the defense-in-depth VarState::Link { target: Idx::NEVER } assignment — existing logic handles the additional vars.
  5. Add engine.body_inference_complete flag to InferEngine: initialized false, set to true at the end of check_function / check_impl_method / check_def_impl_method / check_test body inference (after the top-level check_expr on the body root returns, BEFORE the defaulting pass runs). default_unbound_vars_from_empty_literals and default_unbound_vars_in_scope open with debug_assert!(self.body_inference_complete, "…") per the load-bearing invariant above. The flag is reset to false at the start of each body-check scope via a save-restore in with_function_scope (pattern: same as other scoped engine state).

Why this simple extension is sufficient (both reviewers 2.6B):

  • Ori has no subtyping (only Never <: T). Rust’s coercion-graph DFS exists to distinguish coercion edges from unification edges — Ori’s unification-only model collapses that distinction.
  • Ori runs defaulting AFTER body-exit inference (including §09 BD-2 propagations). Any var constrained by propagation is no longer Unbound at defaulting time.
  • The existing exempt set (FunctionSig.scheme_var_ids) handles the “legitimately polymorphic” case — top-level generic function parameters are exempt from defaulting.

Ordering constraint reinforcement: check/bodies/{functions,impls}.rs call the defaulting pass AFTER InferEngine body inference and BEFORE validate_body_types. §09 extensions live inside inference (in check_expr). So §09 BD-2 propagations pin vars BEFORE §11.1’s defaulting walks. Inverting this order (defaulting before §09) would break correctness — land §11.1 ONLY after all §09 subsections are complete.

11.1.3 Implementation

  • Write failing tests FIRST in compiler/ori_types/src/infer/body_finalize/tests.rs (create if absent).
  • Extend is_empty_collection_literal (rename to is_defaulting_root) to match None/Ok/Err — NOT Some (per R7-010 introducer-only rule in Design block above).
  • Update any callers of the old function name (should be only 1 within body_finalize/mod.rs).
  • Add body_inference_complete: bool field to InferEngine with save-restore wrapping around with_function_scope (new-scope = false, set true at end of body check).
  • Add debug_assert!(self.body_inference_complete, "…") at the entry of default_unbound_vars_from_empty_literals + default_unbound_vars_in_scope (pass-order invariant enforcement per R7-009).
  • Add a new negative test test_some_never_defaulting_root_when_payload_unbound — construct an ExprKind::Some(inner) where inner introduces an unbound var that §09.3’s BD-2 would normally pin (but is intentionally unpinned for the test); verify is_defaulting_root(&arena, &ExprKind::Some(_)) returns false. Regression guard that a future refactor doesn’t re-add Some to the predicate.
  • Add a new test test_debug_assert_fires_on_pass_order_inversion — call default_unbound_vars_from_empty_literals with body_inference_complete = false; verify the debug_assert! panics in debug builds with the expected message. Regression guard that a future refactor doesn’t remove the assert.
  • Run unit tests — all pass.
  • Run timeout 150 cargo stf tests/spec/types/empty_literals — identical pre/post counts (regression guard).
  • Run new spec test for assert(cond: !is_some(opt: None)) — green.
  • Matrix verification: constructor × payload × outer-context:
    • Constructors: None, Some(x), Ok(x), Err(x).
    • Payloads: literal, constrained var, unconstrained var, empty-literal, nested constructor.
    • Outer contexts: no annotation (defaulting applies), LHS type annotation (§09.3 BD-2 pins vars; no defaulting), function argument (parameter type pins), function return (return type pins).
  • Verify timeout 150 cargo st tests/ green.
  • Verify debug + release parity.
  • Verify timeout 150 ./test-all.sh — this is the final regression run validating failed: 0 target.

11.1.4 Close §11.1

  • All §11.1.3 checkboxes marked [x].
  • timeout 150 diagnostics/dual-exec-verify.sh on §11-touched files — zero divergences.
  • tests/spec/types/empty_literals/ corpus identical pre/post §11.1 — regression guard.
  • /tpr-review on §11.1 diff → clean across codex + gemini + opencode.
  • /impl-hygiene-review on §11.1 diff → clean.
  • /improve-tooling retrospective — any defaulting-pre-pass generalization lessons.
  • /sync-claude retrospective — update typeck.md §PC-2 “End-of-body defaulting pre-pass” description to note the extension.
  • Frontmatter 11.1 status: complete.

11.R Third Party Review Findings

  • None.

11.N Completion Checklist

  • 11.1 complete — polymorphic-constructor defaulting extension; assert(cond: !is_some(opt: None)) green; empty_literals/ corpus regression-guard clean.
  • §11 aggregate /tpr-review → clean.
  • §11 aggregate /impl-hygiene-review → clean.
  • §11 full ./test-all.sh regression run — failed: 0 confirmed (the mission success criterion the plan has chased since §06.2C).
  • Plan sync — §11 frontmatter status: complete; §00-overview Quick Reference updates; §index.md section 11 status updated.

Exit criteria: §11.1 complete with TPR + hygiene clean; ./test-all.sh reports failed: 0; tests/spec/types/empty_literals/ regression-guard clean. §06.4 regression verification runs against this state. §07 close-out may begin.

Note on §11.2 (dropped): The original proposal included a §11.2 fallback-visibility lint (mirror of Rust’s NEVER_TYPE_FALLBACK_FLOWING_INTO_UNSAFE lint). Both 2026-04-23 /tp-help reviewers recommended DROPPING §11.2 — Ori has no ()-to-! migration to warn about (start-at-Never design), and Rust 2024 Edition direction is silent fallback. Silent fallback is the correct UX: assert(cond: !is_some(opt: None)) should just compile, not emit a confusing warning. If ergonomic concerns surface post-§11.1 deployment, §11.2 can be filed as a separate future proposal.