Intelligence Reconnaissance

Queries run 2026-04-23 (Phase 2 research for §09/§10/§11):

• scripts/intel-query.sh --human file-symbols "infer/expr" --repo ori — inventory body-inference surface before extending check_expr.
• scripts/intel-query.sh --human callers "infer_try_seq" --repo ori — identify the 1 dispatch site in infer/expr/mod.rs that feeds try-block inference.
• scripts/intel-query.sh --human callers "with_impl_scope" --repo ori — confirm check_impl_method uses it (impls.rs:179) but check_def_impl_method does NOT (impls.rs:324).
• scripts/intel-query.sh --human callers "infer_ok" --repo ori — verify dispatch from infer_expr in mod.rs; no other call sites.
• scripts/intel-query.sh --human similar "check_expr_block" --repo rust,lean4 --limit 5 — prior art for BD-2 block propagation (Rust check_expr_block at rustc_hir_typeck/src/fn_ctxt/checks.rs:1014, Lean 4 elabDo).
• scripts/intel-query.sh --human similar "unify_closure_param_with_iterator_elem" --repo ori — find existing lambda-param-from-receiver propagation for iterator tags (now at closure_unify.rs:127 post §10.0 split, limited to is_iterator() / Tag::List / Tag::Set / Tag::Str).
• scripts/intel-query.sh --human callers "infer_method_call" --repo ori (2026-05-14 §09.5 recon) — confirmed 2 entry points (check_expr BD-2 gate + infer_expr_inner synth-path) before adding the 5th BD-2 gate.

Results summary (≤500 chars) [ori]:

• check_expr at infer/expr/mod.rs:299-344 has only 2 BD-2 gates today — ExprKind::Int byte-coercion and MethodCall with Tag::Set for collect; all other expressions fall through to infer_expr + check_type.
• infer_try_seq at sequences.rs:54-109 has no Expected param.
• infer_ok/infer_err/infer_some/infer_none at constructors.rs:10-55 are pure synth.
• infer_lambda at blocks.rs:213-258 allocates fresh_var() for unannotated params regardless of call-site context.
• unify_closure_param_with_iterator_elem at method_call.rs:271-285 gates on tag.is_iterator() — fails for Tag::List / Tag::Set / Tag::Map / Tag::Str receivers.
• check_def_impl_method at bodies/impls.rs:324 uses with_function_scope only, missing with_impl_scope.

Section 09: Body-Inference Gaps

Goal: Extend existing check_expr BD-2 SSOT (infer/expr/mod.rs:299-439) + check_def_impl_method (check/bodies/impls.rs:288-406) with 5 targeted propagation / binding fixes that close the typeck body-inference gaps surfaced by §06.2C investigation (§09.1–§09.4) plus the method-call return BD-2 gap surfaced 2026-05-14 (§09.5). Establishes the §09.1 check_expr gate pattern that §09.3, §09.4, and §09.5 reuse; §09.2 is orthogonal (impl-scope binding, not BD-2 propagation).

Depends on (declared edge): §04 (section-04-codegen-assertions.md, complete+reviewed 2026-06-07) — the INV-19 single-predecessor edge depends_on: ["04"]. §03 (bodies-pass integration + defaulting pre-pass, complete+reviewed) is upstream of §04 in the linearized chain 01→02→03→05→08→04→09→…, so §09 inherits §03’s outputs transitively through §04 rather than via a second declared depends_on edge — restoring [03, 04] would re-violate INV-19’s single-predecessor form. All §09 work still lands after §03’s validator + defaulting pipeline is live so BD-2 propagation additions don’t interact with an un-gated PC-2 surface.

Execution-ordering note (NOT a depends_on edge): §09.4 + §09.5 touch compiler/ori_types/src/infer/expr/calls/method_call.rs. The §10.0 mechanical file split (extracted closure_unify.rs + trimmed method_call.rs from 524 to 503 lines) landed in commit a20bc41b1 BEFORE §09.4/§09.5 implementation work, materially reducing the file size though it remains 3 lines above impl-hygiene.md §File Organization strict 500-line cap (further consolidation owned by §09.7 inline file-split subsection — absorbed under umbrella, not routed to bug-tracker). §10.0’s frontmatter status: not-started reflects unflipped §10 close-out gate; flip absorbed into §09.N close-out task (umbrella-absorption discipline). Reframing: §10.0 is a SHARED-MECHANICAL-WORK item executed within Phase 2 sequencing per 00-overview.md Implementation Sequence — NOT a §09 hard predecessor in the depends_on: DAG (which is the INV-19 single-predecessor edge ["04"]). The §10 → §09 + §09 → §10 cycle that would arise if §10.0 were declared a §09 depends_on edge is intentionally avoided — under the linearized chain §10 already follows §09 (section-10-rigid-receiver-dispatch.md declares depends_on: ["09"]), so a reverse §09→§10 edge would close a cycle.

Sequencing rule: §09.1 establishes the check_expr gate pattern — it lands FIRST. §09.3, §09.4, and §09.5 reuse the pattern. §09.2 is orthogonal and can land at any point in §09. Implementation order delivered: §09.1 → §09.2 → §09.3 → §09.4 → §09.5 per dual-source consensus (Gemini 2.6B: “establishing the BD-2 propagation pattern on the hardest subsection first forces any HM friction to surface immediately”).

09.1 Try-block bidirectional propagation

Goal: Extend infer_try_seq (sequences.rs:54-109) with an Expected parameter and add a check_expr gate for ExprKind::FunctionSeq(Try) that propagates outer Check(Result<T, E>) expected type into the try-block body, unwrapping once so the final expression is checked against T (not Result<T, E>). Eliminates Result<Result<T, ?>, E> double-wrap that currently fails tests/compiler/typeck/control_flow.ori:184,194 + tests/compiler/typeck/let_bindings.ori.

Prior art (reference only — Ori does not adopt Rust’s Expectation enum): Rust’s check_expr_block at rustc_hir_typeck/src/fn_ctxt/checks.rs:1035 seeds a CoerceMany with expected.coercion_target_type() then checks the tail with the full expected. For try-blocks specifically, Rust’s desugar creates a Try::from_output(expr) wrap — the tail is checked with inner T, not outer Result<T, E>. Ori adopts the “unwrap once before checking tail” principle; skips the CoerceMany machinery since Ori has no subtyping.

09.1.1 Discovery + root cause verification

• Re-read compiler_repo/compiler/ori_types/src/infer/expr/sequences.rs:54-109 (infer_try_seq) and confirm the function signature has no Expected parameter. Line 85 reads let result_ty = infer_expr(engine, arena, result); — pure synthesis.
• Re-read compiler_repo/compiler/ori_types/src/infer/expr/mod.rs:299-344 (check_expr) and confirm the only existing BD-2 gates are ExprKind::Int byte coercion + ExprKind::MethodCall with Tag::Set. All others fall to infer_expr + check_type.
• Trace the call path: let r: Result<int, str> = try { ... Ok(42) } flows infer_let → check_expr(init, Expected { ty: Result<int, str>, origin: Annotation { name: "r" } }) → fall-through to infer_expr → ExprKind::FunctionSeq(Try) → infer_try_seq without Expected. Verify with cargo stf tests/compiler/typeck/control_flow.ori showing E2005 at the try-block final expression (NOT at the outer let binding).
• Write 3-cell TDD matrix in compiler/ori_types/src/infer/expr/tests.rs (new test file or existing) BEFORE implementation:
  • Positive test_try_block_propagates_expected_result_type — let r: Result<int, str> = try { ... Ok(42) } compiles clean.
  • Negative test_try_block_without_outer_annotation_falls_back_to_synthesis — let r = try { ... Ok(42) } still works via synthesis path (regression guard for no-expected-type case).
  • Negative test_try_block_with_wrong_outer_type_reports_mismatch_not_double_wrap — let r: str = try { ... Ok(42) } reports E2001 mismatch (expected str, got Result<int, _>), NOT a double-wrap internal error.

09.1.2 Design

Fix shape (load-bearing):

1. Add Expected parameter to infer_try_seq signature — existing callers pass Expected::NoExpectation (or whatever the flat-Expected default is — see context.rs).
2. In infer_try_seq, when expected.ty is Tag::Result:
   • Extract inner_ok_ty = pool.result_ok(expected.ty) and inner_err_ty = pool.result_err(expected.ty).
   • Check the final result expression with Check(inner_ok_ty) via check_expr(engine, arena, result, &Expected { ty: inner_ok_ty, origin: ExpectedOrigin::Context { span, kind: ContextKind::TryBlockResult } }).
   • Unify the accumulated error_ty (from let-bindings tracked at line 77-79) with inner_err_ty so ? operators in let-bindings match the outer expected Err type.
   • Wrap result: the try-block’s type is expected.ty (verified by unification above).
3. When expected.ty is NOT Tag::Result (e.g., NoExpectation, or something else), fall back to existing synthesis behavior at sequences.rs:84-108.
4. In check_expr at infer/expr/mod.rs:299-344, add an ExprKind::FunctionSeq(Try) gate BEFORE the default fallback that threads expected into infer_try_seq. Store the result type via engine.store_type(expr_id.raw(), result_ty) and return.

Why NOT postponement infrastructure: Gemini 2.6B: “Ori’s HM inference engine is fundamentally eager. Adding postponement introduces a shadow constraint system, violating Algorithmic DRY and eager-resolution invariants.” If expected.ty is Tag::Var (unresolved), fall back to synthesis — unification downstream will catch mismatches. Codex 2.6B agrees: “resolve the expected type at the gate, check its tag only when concrete, and otherwise let the expression form introduce structure.”

SSOT discipline: the check_expr gate is the SSOT for BD-2 on FunctionSeq(Try). All callers of infer_try_seq must go through check_expr when an expected type is available. No side-channel propagation.

09.1.3 Implementation

• Write failing tests FIRST (per CLAUDE.md §TDD for Bugs).
• Extend infer_try_seq signature: add expected: &Expected parameter. Update all call sites to pass Expected::NoExpectation (or equivalent) for now.
• Implement expected-type propagation in infer_try_seq: when engine.resolve(expected.ty) resolves to a type with Tag::Result, unwrap and propagate.
• Add ExprKind::FunctionSeq(Try) gate in check_expr at infer/expr/mod.rs before the default fallback. Pass expected to the updated infer_try_seq. Store result type.
• Run cargo test -p ori_types infer::expr::tests::test_try_block_propagates_expected_result_type — pass.
• Run cargo test -p ori_types infer::expr::tests::test_try_block_without_outer_annotation_falls_back_to_synthesis — pass.
• Run cargo test -p ori_types infer::expr::tests::test_try_block_with_wrong_outer_type_reports_mismatch_not_double_wrap — pass.
• Run timeout 150 cargo stf tests/compiler/typeck/control_flow.ori — green; targets §09.1 try-block residual E2005 at lines 184, 194.
• Run timeout 150 cargo stf tests/compiler/typeck/let_bindings.ori — green; targets §09.3 naked-Ok in try-blocks E2005 clusters.
• Matrix verification: type × pattern × usage:
  • Types: int, str, Option<int>, Result<int, str>, user-struct, user-enum.
  • Patterns: annotated outer let / unannotated outer let / function return with declared type / function return with inferred type.
  • Usage: try-block final expression with Ok(v) / Err(e) / bare value / compound expression.
  • Total cells: at least 6 × 4 × 4 = 96 matrix cells verified via existing spec corpus + new unit tests.
• Verify timeout 150 cargo st tests/ green (full spec corpus regression).
• Verify timeout 150 cargo test -p ori_types --release green (debug + release parity).

09.1.4 Close §09.1

• All §09.1.3 checkboxes marked [x].
• timeout 150 diagnostics/dual-exec-verify.sh on touched files reports zero parity divergences.
• /tpr-review on §09.1 diff → clean across codex + gemini + opencode.
• /impl-hygiene-review on §09.1 diff → clean.
• /improve-tooling retrospective: capture lessons about BD-2 gate extension pattern (informs §09.3, §09.4 implementations).
• /sync-claude retrospective: any typeck.md §BD-2 / §EX-16 rule clarifications discovered.
• Frontmatter 09.1 status: complete.

09.2 Def-impl Self binding

Goal: Extend check_def_impl_method (check/bodies/impls.rs:288-406) to wrap its body-checking closure in checker.with_impl_scope(self_ty, ...) where self_ty is the registered Tag::RigidVar for Self from the def-impl registration pass (NOT a fabricated fresh var at body-check time). Closes tests/spec/lexical/keywords.ori def-impl-with-self E2005.

Design constraint (Codex 2.6B): MUST NOT fabricate Self. The RigidVar for Self is registered at check/registration/impls.rs during the def-impl registration pass — §09.2 discovery must identify where, then retrieve it at body-check time.

09.2.1 Discovery + root cause verification

• Re-read compiler_repo/compiler/ori_types/src/check/bodies/impls.rs:288-406 (check_def_impl_method) and confirm line 324 calls checker.with_function_scope(fn_type, FxHashSet::default(), |c| { ... }) WITHOUT with_impl_scope.
• Re-read compiler_repo/compiler/ori_types/src/check/scope.rs:218-226 (with_impl_scope) and confirm its save-restore mechanism: saves current_impl_self, replaces with supplied self_ty, runs closure, restores.
• Re-read compiler_repo/compiler/ori_types/src/check/scope.rs:157-188 (create_engine_with_env) and confirm it reads impl_self = self.current_impl_self at line 157 and calls engine.set_impl_self_type(self_ty) at lines 185-187.
• Re-read compiler_repo/compiler/ori_types/src/check/registration/impls.rs (def-impl registration path) and identify:
  • Does the registration pass allocate a Tag::RigidVar for Self when registering a def-impl?
  • If yes, where is it stored? (TraitEntry? A dedicated def-impl entry? Module-level?)
  • What DefImplDef structure carries the registered RigidVar through to body-checking?
• If the registration pass does NOT currently register a Self RigidVar for def-impl: split §09.2 into two phases — (a) Registration-pass extension to register Self RigidVar, (b) Body-pass consumption via with_impl_scope. This is a legitimate internal scope split; it does NOT expand §09.2’s public success criterion.
• Re-read compiler_repo/compiler/ori_types/src/infer/expr/type_resolution.rs:184-186 (ParsedType::SelfType resolution) and confirm it calls engine.impl_self_type().unwrap_or_else(|| engine.fresh_var()) — this is the current fabrication fallback §09.2 closes.
• Write 3-cell TDD matrix BEFORE implementation:
  • Positive test_def_impl_method_body_binds_self_to_registered_rigid_var — def impl Trait { @m (self) -> int = 99 } compiles clean and the method body sees self: Tag::RigidVar(registered).
  • Positive test_def_impl_method_body_dispatches_self_method_calls — def impl Trait { @m (self) -> int = self.inner() } resolves self.inner() via trait-method lookup.
  • Negative test_def_impl_without_self_param_does_not_bind_self — def impl Trait { @m () -> int = 42 } (no self param) works without with_impl_scope fabricating Self.

09.2.2 Design

Fix shape:

1. Registration-pass change (if needed per Discovery): During def-impl registration in check/registration/impls.rs, allocate a fresh Tag::RigidVar for Self and store it on the def-impl entry. This makes Self a parametric placeholder (analogous to a generic type parameter).
2. Body-pass change (mandatory): In check_def_impl_method at impls.rs:324, wrap the with_function_scope call with checker.with_impl_scope(registered_self_rigid_var, |c| { c.with_function_scope(...) }). Retrieve the registered RigidVar via checker.trait_registry() or the appropriate def-impl accessor.
3. Type resolution change (incidental): type_resolution.rs:184-186 already handles ParsedType::SelfType via impl_self_type() — no change needed if the RigidVar is in place before body-checking starts.

Key detail: for def impl Trait { @m () -> int = 42 } (no self param), the with_impl_scope wrap is still conceptually fine — the RigidVar is available but no expression references Self, so nothing triggers impl_self_type(). Passing tests: make sure no-self case does NOT regress.

09.2.3 Implementation

• Write failing tests FIRST.
• Registration-pass extension (if Discovery confirms it’s needed): allocate RigidVar for Self at def-impl registration, store on def-impl entry.
• Body-pass wrap: checker.with_impl_scope(registered_self_ty, |c| { c.with_function_scope(...) }) in check_def_impl_method.
• Run cargo test -p ori_types check::bodies::tests::test_def_impl_method_body_binds_self_to_registered_rigid_var — pass.
• Run cargo test -p ori_types check::bodies::tests::test_def_impl_method_body_dispatches_self_method_calls — pass.
• Run cargo test -p ori_types check::bodies::tests::test_def_impl_without_self_param_does_not_bind_self — pass.
• Run timeout 150 cargo stf tests/spec/lexical/keywords.ori — green; targets §09.2 def-impl-with-self E2005.
• Matrix verification: def-impl shape × Self usage × trait-method dispatch:
  • Shapes: def impl Trait { @m (self) -> T = body }, def impl Trait { @m (self, other: Self) -> T = body }, def impl Trait { @m () -> T = body } (no-self), def impl Trait { @m<U> (self, x: U) -> U = body } (generic method).
  • Self usage: field access, method call, pattern match, type annotation.
  • Trait dispatch: self.trait_method() resolves via trait registry; self.non_trait_method() errors with E2003 or equivalent.
• Verify timeout 150 cargo st tests/ green.
• Verify debug + release parity.

09.2.4 Close §09.2

• All §09.2.3 checkboxes marked [x].
• /tpr-review on §09.2 diff → clean.
• /impl-hygiene-review on §09.2 diff → clean.
• /improve-tooling retrospective.
• /sync-claude retrospective.
• Frontmatter 09.2 status: complete.

09.3 Result<T, user-Error> LHS propagation

Goal: Add BD-2 gates in check_expr for ExprKind::Ok(inner), ExprKind::Err(inner), ExprKind::Some(inner) that propagate Check(Result<T, E>) / Check(Option<T>) from an outer let-type-annotation into the constructor’s polymorphic slots. Extract check_ok, check_err, check_some helper functions into constructors.rs following the check_collect_method_call extraction pattern. Closes the constructor-side LHS propagation gap. tests/spec/traits/into/str_to_error.ori may require §09.4 to also land before it goes fully green (the .into() issue is a method-call-return propagation, not a constructor-side fix) — file-level close-out for that file is §09 aggregate, not §09.3 alone.

Reuses §09.1 pattern: check_expr gate before default fallback, unwrap expected type to extract inner slot types, propagate inner types via recursive check_expr or direct unification, store result type and return.

09.3.1 Discovery + root cause verification

• Re-read compiler_repo/compiler/ori_types/src/infer/expr/constructors.rs:10-55 (infer_ok, infer_err, infer_some, infer_none) and confirm all are pure synthesis — they allocate fresh vars for unconstrained slots (err_ty in infer_ok, ok_ty in infer_err, etc.) without consulting expected type.
• Confirm tests/spec/traits/into/str_to_error.ori fails with E2005 at let e: Error = msg.into() — the .into() return fresh-var is not constrained by the LHS Error annotation.
• Re-read tests/spec/traits/traceable/definition.ori and confirm the @mk_ok/@mk_err helper workaround — functions with explicit Result<int, Error> return types wrap Ok(v) / Err(e) calls.
• Write TDD matrix BEFORE implementation:
  • Positive test_result_user_error_lhs_propagates_ok_type — let r: Result<int, MyError> = Ok(42) compiles clean; r.unwrap() has type int.
  • Positive test_result_user_error_lhs_propagates_err_type — let r: Result<int, MyError> = Err(my_error) compiles clean; r.unwrap_err() has type MyError.
  • Positive test_option_lhs_propagates_some_type — let o: Option<int> = Some(42) compiles clean with correct inner type.
  • Negative test_result_lhs_mismatch_reports_type_error — let r: Result<int, MyError> = Ok("string") reports E2001 mismatch on inner type, NOT E2005.
  • Negative test_result_ok_without_lhs_annotation_still_synthesizes — let r = Ok(42) (no annotation) still works via synthesis path; r’s err type remains fresh var, defaulted to Never by §11.1 if unconstrained downstream.

09.3.2 Design

Fix shape:

1. Create check_ok, check_err, check_some functions in constructors.rs following check_collect_method_call extraction pattern:
   • Takes engine, arena, inner: ExprId, span, expected: &Expected.
   • If expected.ty resolves to Tag::Result (for Ok/Err) or Tag::Option (for Some): extract inner slot via pool.result_ok/result_err/option_inner, check inner against the extracted type with appropriate ExpectedOrigin.
   • Construct and return the full Result<T, E> / Option<T> type using the extracted slots.
2. In check_expr at infer/expr/mod.rs, add gates BEFORE the default fallback:
   • ExprKind::Ok(inner) → check_ok(engine, arena, *inner, span, expected).
   • ExprKind::Err(inner) → check_err(...).
   • ExprKind::Some(inner) → check_some(...).
   • ExprKind::None is pure-synth (no inner payload to check); the existing infer_none remains. §11.1 handles unconstrained None defaulting.
3. When expected does NOT match expected tag (e.g., Check(int) on ExprKind::Ok(42)): fall back to infer_ok + check_type, which reports E2001 mismatch.

Why this does NOT fix str_to_error.ori’s .into() issue directly: the failure is let e: Error = msg.into(), which is a method call returning a fresh var, not an Ok/Err/Some constructor. §09.3 closes the constructor-side gap; the .into() issue is §09.4’s lambda-parameter-style propagation applied to method-call return types. Monitor str_to_error.ori state after §09.3 — if residual, §09.4 closes it.

09.3.3 Implementation

• Write failing tests FIRST.
• Create check_ok, check_err, check_some in constructors.rs.
• Add gates in check_expr at infer/expr/mod.rs.
• Run unit tests — all pass.
• Run timeout 150 cargo stf tests/spec/traits/into/str_to_error.ori — verify state (may still fail if §09.4 is the actual fix; classify accordingly).
• Run timeout 150 cargo stf tests/spec/traits/traceable/definition.ori — MUST remain green (regression guard; helpers still work after §09.3).
• Run timeout 150 cargo stf tests/spec/traits/traceable/result_delegation.ori — MUST remain green.
• Matrix verification: constructor × expected-type-shape × inner-payload-shape:
  • Constructors: Ok(v), Err(e), Some(v).
  • Expected shapes: user-struct, user-enum, user-newtype, primitive, generic-instance (e.g., Option<T>), nested (e.g., Result<Option<int>, str>).
  • Inner payloads: literal, variable, expression, nested constructor.
• Verify timeout 150 cargo st tests/ green.
• Verify debug + release parity.

09.3.4 Close §09.3

• All §09.3.3 checkboxes marked [x].
• /tpr-review on §09.3 diff → clean.
• /impl-hygiene-review on §09.3 diff → clean.
• /improve-tooling retrospective.
• /sync-claude retrospective.
• Frontmatter 09.3 status: complete.

09.4 Lambda-parameter propagation from receiver element type

Goal (as shipped): Lambda-parameter propagation lands via the SSOT helper unify_closure_param_with_iterator_elem in compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127, extended to unwrap Tag::List / Tag::Set / Tag::Str receiver element types in addition to the pre-existing Tag::Iterator / Tag::DoubleEndedIterator arms. The helper is invoked from unify_higher_order_constraints and unify_flat_map_constraints (same file) when a method-call receiver carries a known element type and the closure parameter is unannotated. infer_lambda at blocks.rs:223 remains the single lambda entry point; element-type propagation flows through unify_closure_param_with_iterator_elem after infer_lambda allocates fresh vars, NOT via a separate check_lambda entry point. Tag::Map coverage owned by §09.6 inline subsection (tuple-shaped receiver projection — (K, V) element type requires tuple-element unification not present in unify_closure_param_with_iterator_elem; see exclusion comment at closure_unify.rs:122-126). Closes the §06.2B lambda-parameter class root cause.

Shipped path vs proposed §09.1-analogy design:

• Proposed design: check_lambda function in blocks.rs + ExprKind::Lambda BD-2 gate in check_expr mirroring §09.1.
• Shipped path: SSOT-helper extension of unify_closure_param_with_iterator_elem at closure_unify.rs:127; no check_lambda, no ExprKind::Lambda BD-2 gate.
• Invariant preserved: single lambda entry point (infer_lambda at blocks.rs:223); one helper cures both unify_higher_order_constraints and unify_flat_map_constraints call sites.
• §09.6 reuses the same SSOT-helper discipline for the Map arm (success_criterion at lines 83-90).
• §09.4 success_criterion (lines 36-45) reflects the shipped path.

§09.4 execution-ordering — §10.0 file splits landed first (historical note): §09.4 touches infer/expr/calls/method_call.rs (extending unify_closure_param_with_iterator_elem). §10.0’s mechanical file split landed in commit a20bc41b1 BEFORE §09.4 implementation work, extracting closure_unify.rs from method_call.rs and trimming the parent file to under the 500-line impl-hygiene.md §File Organization guidance. unify_closure_param_with_iterator_elem now lives in compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127. This is an EXECUTION-ORDERING fact recorded for audit trail — NOT a depends_on: DAG edge (per the section-level Execution-ordering note above; declaring §10.0 a §09.4 hard predecessor would create a §10→§09 + §09→§10 cycle since section-10-rigid-receiver-dispatch.md declares depends_on: ["09"] post-INV-19 linearization — §10 follows §09 in the linear chain 04→09→10).

09.4.1 Discovery + root cause verification

• Re-read compiler_repo/compiler/ori_types/src/infer/expr/blocks.rs:213-258 (infer_lambda) and confirm it allocates engine.fresh_var() for each unannotated parameter (line 229-232). No Expected parameter.
• Re-read compiler_repo/compiler/ori_types/src/infer/expr/calls/method_call.rs:271-285 (unify_closure_param_with_iterator_elem) and confirm the tag.is_iterator() gate at line 278. Tag::List / Tag::Set / Tag::Map / Tag::Str do NOT pass this gate.
• Confirm list.map(x -> x + 1) (unannotated lambda, Tag::List receiver) fails to propagate: x has Tag::Var(unbound), leaks E2005.
• Identify §06.2B’s 15-file annotation-sweep workaround pattern: every .map((d: Duration) -> int = d.minutes()) is a typed_lambda annotation that check_lambda would obviate.
• Write TDD matrix BEFORE implementation:
  • Positive test_lambda_param_inferred_from_call_site_function_type — direct call f(x -> x + 1) where f: ((int) -> int) -> int resolves x: int.
  • Positive test_lambda_param_inferred_from_list_map_receiver — [1, 2, 3].map(x -> x + 1) resolves x: int.
  • Positive test_lambda_param_inferred_from_map_entries_receiver — {"a": 1}.map(pair -> pair.value + 1) resolves pair: (str, int) or element type per spec.
  • Positive test_lambda_param_inferred_from_string_chars_receiver — "abc".map(c -> c.to_upper()) resolves c: char.
  • Negative test_lambda_param_mismatch_reports_type_error — list.map(x -> x.nonexistent()) where x: int reports E2003 method-not-found on int, NOT E2005 on x.
  • Negative test_lambda_without_call_site_context_still_uses_fresh_var — let f = x -> x + 1 (no call context) keeps x: Tag::Var(unbound) — it defaults or errors per normal PC-2 rules. Regression guard.

09.4.2 Design (as shipped)

Fix shape (shipped path):

1. Extend unify_closure_param_with_iterator_elem at compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127 to unwrap receiver element type for Tag::List / Tag::Set / Tag::Str arms in addition to the pre-existing Tag::Iterator / Tag::DoubleEndedIterator arms. Each arm extracts the receiver’s element Idx via the same unwrapping functions used by infer_for_pattern at sequences.rs:128-135. Tag::Map is intentionally excluded — Map iteration shape is (K, V) tuples and unification needs tuple-element resolution; owned by §09.6 inline subsection per closure_unify.rs:122-126 exclusion comment.
2. The helper is invoked from unify_higher_order_constraints (closure_unify.rs:57, closure_unify.rs:76) and unify_flat_map_constraints (closure_unify.rs:176). Both call sites pre-resolve the closure parameter Idx and the receiver type Idx before invoking the helper. SSOT-helper design: one unify call site cures .map / .filter / .fold / .any / .all / .for_each (via unify_higher_order_constraints) AND .flat_map (via unify_flat_map_constraints) simultaneously.
3. infer_lambda at blocks.rs:223 remains the lambda entry point. It allocates engine.fresh_var() for each unannotated parameter. Element-type propagation happens AFTER infer_lambda returns, via the receiver-driven unify_closure_param_with_iterator_elem call. No check_lambda function, no ExprKind::Lambda BD-2 gate in check_expr.

SSOT-helper rationale: routing lambda-parameter propagation through unify_closure_param_with_iterator_elem preserves the single lambda entry point (infer_lambda), avoids parallel BD-2 gate logic, and reuses one helper for both the higher-order-constraints and flat-map-constraints code paths. §09.6 extends the same helper with the Map arm.

Composition with §09.3 / §09.5: let e: Error = msg.into() flows method-call return propagation through §09.5’s check_expr 5th BD-2 gate at infer/expr/mod.rs:390, not through §09.4’s lambda-parameter helper. §09.4 closes the receiver-driven lambda-parameter gap; §09.5 closes the LHS-driven method-call generic-return gap. The two gaps land via independent code paths.

09.4.3 Implementation

• Write failing tests FIRST.
• Create check_lambda in blocks.rs. SUPERSEDED — shipped path routes propagation through unify_closure_param_with_iterator_elem in compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127; no check_lambda function exists per §09.4 HISTORY entry below.
• Add ExprKind::Lambda gate in check_expr. SUPERSEDED — no ExprKind::Lambda BD-2 gate in check_expr; infer_lambda at blocks.rs:223 remains the single lambda entry point per §09.4 HISTORY entry below.
• Extend unify_closure_param_with_iterator_elem to handle Tag::List / Tag::Set / Tag::Str. (Tag::Map owned by §09.6 inline subsection per §09.4 SC 4.)
• Run unit tests — all pass.
• Run timeout 150 cargo stf tests/spec/traits/iterator/methods.ori — green (lambda-param-from-receiver cells pass).
• Check str_to_error.ori state — classify residual if any.
• §06.2B residual check: the 15 files §06.2B annotated with typed_lambda form CONTINUE to pass (annotations are spec-compliant typed_lambda syntax; §09.4 fix is additive, enabling untyped form). Do NOT remove annotations in §09.4 commits.
• Matrix verification: receiver × method × lambda-arity × annotation:
  • Receivers: [T], Set<T>, str, Tag::Iterator (via .iter() chain), Tag::DoubleEndedIterator. {K:V} (Tag::Map) excluded — owned by §09.6 inline subsection (tuple-shaped receiver projection); Map receiver lambda still requires explicit param annotation until §09.6 lands.
  • Methods: .map, .filter, .fold, .any, .all, .find, .for_each, .flat_map.
  • Lambda arity: unary, binary (for fold), closure returning unit (for for_each).
  • Annotation: all-typed, all-untyped, mixed.
• Verify timeout 150 cargo st tests/ green.
• Verify debug + release parity.

09.4.4 Close §09.4

• All §09.4.3 checkboxes marked [x].
• /tpr-review on §09.4 diff → clean.
• /impl-hygiene-review on §09.4 diff → clean.
• /improve-tooling retrospective.
• /sync-claude retrospective.
• Frontmatter 09.4 status: complete.

09.R — Third Party Review Findings

• [TPR-09-R2-001-codex][high] STRUCTURE:work-order-violation — RESOLVED 2026-06-07 (§04 flipped complete + reviewed: true; see resolution note at end of this finding). §09 depends_on: ['03', '04'] while §04 is status: in-progress (not complete). Per state-discipline.md §4 + impl-hygiene.md §STRUCTURE:work-order-violation, consumer section MAY enter status: in-progress ONLY when every predecessor satisfies status: complete AND reviewed: true. Currently §09 is in-review (pre-in-progress flip), so the gate has not yet fired; the finding documents the structural blockage at section-close. (deferred-with-anchor: plans/typeck-inference-completeness/section-04-codegen-assertions.md §04.S.N — cross-scope blocked on aims-burden §06 burden-lowering per section-04 HISTORY entries 2030/2032/2033). Resolution path: §09 cannot flip in-review → in-progress until §04 is complete; §04 cannot complete until §04.S.4 unblocks; §04.S.4 cross-scope blocked on aims-burden §06 BurdenInc/BurdenDec LLVM lowering. When aims-burden §06 lands, §04 unblocks → §04.S.4 verifies → §04.S.N closes → §04 flips complete → §09’s work-order constraint satisfies → §09 flip eligible. Filed 2026-05-15 per /review-plan Round 2 /tpr-review cycle on §09; adjudicator-verdict-r2.yaml. RESOLUTION 2026-06-07: §04 flipped status: complete + reviewed: true (aims-burden §06 BurdenInc/BurdenDec lowering landed; narrowing::test_narrowed_list_derived_eq passes, test-all baseline-matching per section-04-codegen-assertions.md HISTORY). The depends_on edge is now the INV-19 single-predecessor form ["04"] (§03 reaches §09 transitively, complete+reviewed). §09’s work-order constraint is satisfied; flip eligibility hinges only on §09.N/§09.R residuals + the §09.7 cross-scope ./test-all.sh gate.
• [Informational] All other Round-1 and Round-2 findings cured inline this cycle (BUG-citation strip, history-keyword strip, “all 4” → “all 5”, overview Implementation Sequence + ASCII tree §09.5 addition).

09.R — Third Party Review Findings (Round 5 cap-exit — 2026-05-15)

Round 5 reached max_rounds=5 cap with 4 verified actionable findings + 1 meta (duplicate of TPR-09-R2-001-codex) — exit reason cap_reached_max_rounds. Filed per §7 cap-exit protocol; cure ownership routes to §09.N close-out OR inline absorption per per-finding fix-shape. These 4 findings are the EXPECTED mid-pipeline shape (third_party_review.status: cap_reached_with_substantive, reviewed: false) — each is already tracked in-plan with cure ownership routed to §09.N (R5-001 BUG-02-031 3-signal disposition; R5-002 §10.0 status-flip at the §09.N §10.0 integration item; R5-003 impl_lookup.rs +22 overrun; R5-004 mechanical, cured). They are NOT new audit findings surfaced by the current /review-plan pass.

• [TPR-09-R5-004-opencode][low] LEAK:scattered-knowledge — plans/typeck-inference-completeness/section-09-body-inference-gaps.md:13 plan cites Expected struct as infer/context.rs; actual location is compiler_repo/compiler/ori_types/src/type_error/expected/mod.rs:27. CURED — the §09 goal (line 13) now cites the corrected path type_error/expected/mod.rs; mechanical direct-path edit, no further work.
• [TPR-09-R5-001-codex][critical] DRIFT:finding-disposition — RESOLVED 2026-06-08 via option (b): 3-signal relatedness test (routing.md §2) recorded, separate bug-tracker route for BUG-02-031 justified. Outcome: Signal 1 (file-set) technically fires — BUG-02-031’s cure surface (method_call.rs:399-416 hardcoded INFINITE_CONSUMING_METHODS / TRANSPARENT_ADAPTERS constants consumed by find_infinite_source) coexists in method_call.rs, a file §09 edited (§09.5 BD-2 param + §09.7 split). Signal 2 (symbol) does NOT fire — find_infinite_source / resolve_named_type_method / INFINITE_CONSUMING_METHODS are NOT §09 deliverable symbols (§09’s are infer_method_call / check_expr / unify_closure_param_with_iterator_elem / resolve_impl_signature; §09 never touched find_infinite_source, which lives in infer/expr/calls/infinite_iterator.rs). Signal 3 (success-criteria) does NOT fire — BUG-02-031’s resolution (registry-driven method-name dispatch replacing the hardcoded constants, a LEAK:scattered-knowledge cure) is not a subset of any §09 success_criterion (all are BD-2-propagation correctness). Disposition: the lone file-set signal is INCIDENTAL coexistence (infinite-iterator detection is topically orthogonal to §09’s BD-2 body-inference work; the §09.7 split of method_call.rs was for the 500-line cap, not the LEAK), and BUG-02-031 is independently-workable per routing.md §4 (own LEAK deliverable, own success criteria, cold-pickup-able, cross-references iterator-consumption analysis outside §09’s scope). Separate bug-tracker route is the architecturally-correct home; /review-bugs is the safety net if re-triage disagrees.
• [TPR-09-R5-002-gemini+opencode][high] PLAN_COHERENCE_DRIFT / STRUCTURE:work-order-violation — RESOLVED 2026-06-08 (verify-first re-check). The drift it flagged (§10.0 split landed in commits a20bc41b1 + 131c771ea but section-10 frontmatter status: not-started) is cured: section-10-rigid-receiver-dispatch.md §10.0 sections: entry is now status: complete AND top-level status: in-progress — the §10.0 frontmatter flip integrated into this §09 close (see the §09.N “§10.0 status-flip integration” item above). Plan coherence restored.
• [TPR-09-R5-003-opencode][major] BLOAT — RESOLVED 2026-06-08 (verify-first re-check). compiler/ori_types/src/infer/expr/calls/impl_lookup.rs is now 456 lines (≤500-line cap, impl-hygiene.md §File Organization); the +91 overrun flagged at the 591L authoring snapshot was cured by the §09.7 / §10.0 split work (resolve_impl_signature extracted to impl_signature.rs, apply_impl_binder_substitution helper extraction). No residual split target; no §09.R accepted-overrun note needed.
• [Informational] TPR-09-R5-005-opencode (meta) verified pre-existing as TPR-09-R2-001-codex (cross-scope §04 work-order blocker on aims-burden §06 BurdenInc/BurdenDec lowering); no separate filing.

09.N Completion Checklist

• 09.1 complete — try-block BD-2 propagation; check_expr gate pattern established for §09.3/§09.4 to reuse; control_flow.ori, let_bindings.ori green. Production code landed in commit a20bc41b1 per RESUME POINTER.
• 09.2 complete — def-impl Self binding via registered RigidVar; keywords.ori green; no Self fabrication. Production code landed in commits a20bc41b1 + 131c771ea; unit tests landed 2026-05-05 session-2 per RESUME POINTER.
• 09.3 complete — check_ok/check_err/check_some BD-2 gates; Result<T, user-Error> LHS annotation compiles clean; traceable/definition.ori + result_delegation.ori regression-guard green (helpers still work; verified 2026-05-14: 5/5 + 7/7 = 12/12).
• 09.4 complete — lambda-parameter propagation via closure_unify.rs::unify_closure_param_with_iterator_elem (SSOT helper at compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127) extended to unwrap Tag::List/Tag::Set/Tag::Str receiver element types in addition to Tag::Iterator/Tag::DoubleEndedIterator; .map/.filter/.fold on those receivers work with untyped lambdas. No check_lambda function exists; infer_lambda at blocks.rs:223 remains the sole lambda entry point. Production code + unit tests landed 2026-05-05. Tag::Map receiver coverage owned by §09.6 inline subsection (tuple-shaped receiver projection — (K, V) element type requires tuple-element unification) per closure_unify.rs:122-126 exclusion comment.
• 09.5 complete — method-call return BD-2 gate in check_expr for ExprKind::MethodCall(Named); Error type registered as well-known (scope expansion); str_to_error.ori passes clean (2 cells); 5+1-cell matrix 3 passed + 3 tracked-ignored (BUG-02-028/029/030). Landed 2026-05-14 via /tp-dev 2-cycle pair-program.
• §09.5 ignored-cell follow-ups — BUG-02-028/029/030 dispositions (concrete close-out anchors per impl-hygiene.md §DISPOSITION_DRIFT + CLAUDE.md §ALL Deferrals MUST Have Anchors): the 3 #[ignore]’d cells in the test_method_call_return_bd2_* matrix at compiler/ori_types/src/check/bodies/tests.rs each track an orthogonal typeck defect; close-out re-verifies each cell flips from #[ignore] to passing when its bug resolves. Parent header for the three blocked cells below; gated on the three open bugs resolving.
  • cell 3 (let _n: int = msg.into() silent-accept on missing impl)
  • cell 5 (map_err(msg -> msg.into()) nested closure-return propagation)
  • cell 6 (impl str: Convert<MyErr> user-defined verification)
• §09.6 inline subsection — Tag::Map receiver lambda-parameter propagation (umbrella-absorbed; NOT routed to bug-tracker per user directive): extended compiler/ori_types/src/infer/expr/calls/closure_unify.rs:122-126 Map exclusion arm to unwrap (K, V) tuple element via pool.map_key() + pool.map_value() + tuple constructor, then unify lambda param with constructed tuple Idx. Rust unit test test_lambda_param_from_map_receiver_propagates_kv_tuple lands plus .flat_map-path + negative-pin cells. Done 2026-06-07 (frontmatter 09.6 status: complete; dual-exec parity verified). Helper-backed reachability note recorded in §09.6 subsection body. See §09.6 subsection body below.
• §09 full regression — timeout 150 ./test-all.sh counts the §09 delta (should be -4 to -6 files from the §06.2C unresolved ledger moved to green). Cross-scope-blocked on the parallel aims-burden-tracking §09 (test-all red from uncommitted ori_arc/AIMS/burden work; ori_types per-crate suite 1063/1063 green) — same blocker as the §09.7 frontmatter blocked status; re-runs on the loop iteration after that section reaches complete per the §09.N cross-scope re-detection protocol.
• §10.0 status-flip integration (umbrella-absorbed): DONE — verify-first re-check 2026-06-08. §10.0 split verified landed (closure_unify.rs 222, method_call.rs 445 ≤503, registry/traits/mod.rs 486 ≤500, registry/traits/lookup.rs 513). plans/typeck-inference-completeness/section-10-rigid-receiver-dispatch.md §10.0 sections: entry is status: complete AND top-level status: in-progress (both already flipped, reflecting §10.0/§10.1 production code in commits a20bc41b1 + 131c771ea). The residual lookup.rs 513 / method_call.rs / impl_lookup.rs cap overruns are §10.R-007/009/010 follow-ups owned by §10, not §10.0 split blockers.
• §09.7 inline subsection — file-split larger files (umbrella-absorbed): split compiler/ori_types/src/check/bodies/impls.rs (+181 over 500-line cap), infer/expr/operators.rs (+299), infer/expr/control_flow.rs (+250), infer/expr/blocks.rs (+117) via compiler_repo/scripts/extract_tests.py + cohesive submodule extraction per §10.0 precedent. Anchor: compiler/ori_types/src/check/bodies/impls.rs:1 (smallest overrun — mechanical first split). See §09.7 subsection body below. DONE (committed 59f645300; verify-first re-check 2026-06-08): all targets ≤500 — impls.rs 369, blocks.rs 202, method_call.rs 445; operators.rs + control_flow.rs extracted into submodules (parent files no longer present at the flat path). The §09.7 frontmatter sections: entry stays blocked only on the cross-scope ./test-all.sh gate, not the splits.
• §09.N follow-up (non-blocking discovery-insertion) — fold/rfold receiver-tag parity in closure_unify.rs: CURED 2026-06-08 (verify-first re-check). The fold/rfold receiver-tag match arm in compiler/ori_types/src/infer/expr/calls/closure_unify.rs:78-99 now binds the closure’s SECOND param (the element) via the shared SSOT receiver_element_type(engine, receiver_ty) helper (closure_unify.rs:117-136), which covers Tag::Map (synthetic (K, V) tuple via map_key/map_value) and Tag::Str (Idx::CHAR) at parity with unify_closure_param_with_iterator_elem. The asymmetry flagged by codex-F1 + agy-F1 (/review-plan 2026-06-07) is closed — the fold/rfold arm and the first-param helper share one element-projection SSOT. Matrix tests landed in infer/expr/calls/tests.rs mod fold_rfold_receiver_lambda_param (Map→(K,V) semantic pin, Str→char semantic pin, List→int regression cell, non-element negative pin). Non-blocking discovery-insertion — was never a §09 close blocker.
• Dual-execution parity — timeout 150 diagnostics/dual-exec-verify.sh zero divergences on §09-touched files. Cross-scope-blocked: dual-exec needs a clean LLVM/AOT build, which the parallel session’s uncommitted ori_arc/burden work breaks (LLVM spec CRASH in test-all) — same blocker as §09.7; re-runs once aims-burden-tracking §09 is complete.
• §09 aggregate /tpr-review on full §09 diff (after all 5 subsections land) → clean. Required even though per-subsection TPR ran. Section-close gate — runs when §09 enters close-out (all subsections complete), gated on §09.7’s cross-scope ./test-all.sh (parallel aims-burden-tracking §09).
• §09 aggregate /impl-hygiene-review → clean. Section-close gate, runs after the aggregate /tpr-review at §09 close-out (gated on §09.7 cross-scope test-all).
• /improve-tooling section-close sweep — any new hygiene rules about BD-2 gate extension pattern. Section-close gate (gated on §09.7 cross-scope test-all).
• /sync-claude section-close doc sync — update typeck.md §EX-16, §BD-2 with lessons; update CLAUDE.md memory if new Ori patterns discovered. Section-close gate (gated on §09.7 cross-scope test-all).
• Plan sync — §09 frontmatter status: complete; 00-overview.md Quick Reference updates to Complete; index.md section 09 status updated; mission success criteria SC-1, SC-2 advance (carries into §06.4 regression verification). Terminal §09 close-out flip — gated on every preceding §09.N gate + §09.7’s cross-scope test-all.
• §09 bug-ID grounding sweep (per HISTORY 2026-06-07 residual): DONE 2026-06-08. Audited all 16 distinct BUG-XX-NNN cited in section-09-body-inference-gaps.md + 00-overview.md against bug-tracker/open-bugs.json + closed-bugs.json — every cited ID resolves to a tracker entry; titles match the cited defects. Exact matches: BUG-02-028 (open, “Silent-accept on msg.into() where no Into<T> impl”) ↔ §09.5 cell 3; BUG-02-029 (open, “Closure-return BD-2 propagation absent — map_err(msg -> msg.into())”) ↔ cell 5; BUG-02-030 (open, “Parse error on impl str: Convert<MyErr>”) ↔ cell 6; BUG-02-031 (open, “LEAK:scattered-knowledge — hardcoded method-name string-match”) ↔ the §09.R-001 cited LEAK. The remaining (BUG-01-002 closed, BUG-02-032/044, BUG-04-* codegen, BUG-02-023/034) are contextual cross-refs that resolve correctly. No misattributed ID — no in-place correction required.
• §09.7 cross-scope blocker re-detection protocol (per /review-plan 2026-06-07 blind-spots architectural-risk opencode-F1): on the next /continue-roadmap loop iteration re-check the blocked-by anchor plans/aims-burden-tracking/section-09-post-convergence-partial-retirement.md; when that section reaches status: complete, flip §09.7 sections: entry blocked → in-progress and run timeout 150 ./test-all.sh. Green → flip §09.7 complete and strip the <!-- blocked-by:plans/aims-burden-tracking/section-09-post-convergence-partial-retirement.md --> anchor at section-09-body-inference-gaps.md:676; RED with only AIMS/ARC/burden-class failures → blocker unresolved, re-defer one loop.
• §09 exit_reason reconciliation (per /review-plan 2026-06-07 blind-spots cross-cutting codex-F2 + opencode-F3): DONE 2026-06-08. The ## §09 Autopilot Discipline table’s exit_reason column now uses canonical scripts/plan_corpus/exit_reasons.py CANONICAL_EXIT_REASONS members directly: subsection_complete/section_complete → gate_passed; failed → validation_failed; architectural_decision_required → materiality_architectural_escalation; predecessor-unsatisfied → section_advance_blocked. The prior-mnemonic→canonical map is recorded in the table preamble per decisions/31; no divergent plan-local enum remains.

Exit criteria: §09.1–§09.5 complete (TPR + hygiene clean per subsection); §09.6 inline subsection complete (Tag::Map receiver lambda-parameter propagation); §09.7 inline subsection complete (file-split of impls.rs / operators.rs / control_flow.rs / blocks.rs per 500-line cap); §10.0 split status-flip integration complete; §09 aggregate /tpr-review + /impl-hygiene-review clean; §09-touched test files green; dual-exec parity preserved; §06.2C-ledger files owned by §09 (control_flow.ori, let_bindings.ori, keywords.ori, str_to_error.ori in part) all pass. §10 remaining subsections may begin.

09.5 Method-call return BD-2 — propagate expected type into generic-return method slots (Error::into, Iterator::collect)

Goal: Add a 5th BD-2 gate in check_expr for ExprKind::MethodCall + ExprKind::MethodCallNamed that propagates outer Check(T) into the method’s generic-return slot. Closes the let e: Error = msg.into() shape from tests/spec/traits/into/str_to_error.ori.

Status: complete (2026-05-14). /tp-dev pair-cycle protocol executed; 2 cycles + 1 user-approved scope expansion.

09.5.1 Implementation summary

• compiler/ori_types/src/infer/expr/calls/method_call.rs: added expected: Option<&Expected> parameter to infer_method_call and infer_method_call_named. When Some(exp) AND resolve_impl_signature returns a sig, call engine.check_type(sig.ret, exp, span) BEFORE check_positional_args so the generic return slot is constrained by the LHS annotation. Mirror propagation in the builtin-dispatch ReceiverDispatch::Return arm so collect-style builtins also propagate.
• compiler/ori_types/src/infer/expr/mod.rs: added 5th BD-2 gate in check_expr for ExprKind::MethodCall + ExprKind::MethodCallNamed that passes Some(expected) to the inference entry points. Runs AFTER check_collect_method_call so the Set-specific gate keeps priority. Existing infer_expr_inner call sites pass None.
• Scope expansion (user-approved 2026-05-14 via AskUserQuestion): Error was unregistered in TypeRegistry and fell through to fresh_named_var("Error") at type_resolution.rs:175, leaving the BD-2 gate unifying two fresh vars without resolution. Cure: register Error as a well-known concrete type in well_known/mod.rs::resolve_primitive returning Idx::ERROR, plus belt-and-suspenders match arm at type_resolution.rs:135 for the non-cached path. Preparatory expansion per CLAUDE.md §Scope Expansion §3 — surrounding shape blocked §09’s str_to_error.ori success criterion.

09.5.2 Test matrix outcome

Five-cell matrix in compiler/ori_types/src/check/bodies/tests.rs::test_method_call_return_bd2_*:

Ignored cells are orthogonal defects discovered during §09.5 implementation; each has a tracked BUG-XX-NNN with concrete cure surface filed in bug-tracker/section-02-typeck.md.

09.5.3 Spec corpus verification

• tests/spec/traits/into/str_to_error.ori passes clean (2 cells green) — the §09 success_criterion 5 deliverable.
• tests/spec/traits/into/ corpus: 11/11 passing.
• tests/spec/traits/traceable/definition.ori + result_delegation.ori regression-clean (5/5 + 7/7 = 12/12) — §09.3 helper workarounds unaffected.
• tests/spec/types/empty_literals/ corpus: 5/5 passing — success_criterion 7 regression baseline preserved.

09.5.4 Pair-cycle log

Two cycles recorded in pair_cycle_log: frontmatter array (per state-discipline.md §1):

• Cycle 1 (cycle_terminus: subsection_continues): TDD matrix authored + 2 passed/3 failed pre-fix shape per CLAUDE.md §TDD step 4. Navigator verdict: proceed with advisory rename to test_method_call_return_bd2_* prefix (applied).
• Cycle 2 (cycle_terminus: subsection_complete): gate + Error registration. Navigator verdict: proceed (clarified constraint-propagation vs structural-decomposition distinction from §09.3).

09.6 Tag::Map receiver lambda-parameter propagation — tuple-shaped receiver projection

Status: complete (2026-06-07). Umbrella-absorbed inline subsection (user directive 2026-05-15) — Tag::Map receiver propagation lands in this plan as §09.6, NOT a separate bug-tracker entry. Tracked in aggregate success_criteria (umbrella-absorbed entry) as §09-aggregate close-out gate. All §09.6 success criteria below are [x]; frontmatter sections: entry 09.6 is status: complete; dual-exec parity verified. The new arm is HELPER-BACKED — reachable only via direct helper invocation until map HOFs land (no registry HOF dispatches a bare Tag::Map receiver; map.iter() returns MapIterator → Tag::Iterator), per the empirical reachability note in the §09.6 success criteria.

Goal: Extend unify_closure_param_with_iterator_elem at compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127-149 to handle Tag::Map receivers by unwrapping the (K, V) tuple element type. Map iteration shape is (K, V) tuples; the current else { return; } at line 142 falls through for Map (exclusion documented in lines 122-126 // intentionally excluded for now comment). Cure: insert Tag::Map branch BEFORE the return;, extract via engine.pool().map_key(resolved_recv) + engine.pool().map_value(resolved_recv), construct synthetic tuple Idx via engine.pool_mut().tuple(&[k, v]), bind as source_elem.

Dual-path coverage — unify_closure_param_with_iterator_elem is the SSOT for receiver→lambda-param propagation (§09.4 design choice). Invoked from BOTH call sites in closure_unify.rs: unify_higher_order_constraints (line 99, the .map/.filter/.fold path) and unify_flat_map_constraints (line 176, the .flat_map path). A single Map arm in the shared helper cures BOTH call paths simultaneously — no separate fix required for .map(...) vs .flat_map(...) receivers. Test matrix below covers BOTH paths.

Files:

• compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127-149 (unify_closure_param_with_iterator_elem) — insert else if recv_tag == Tag::Map { let k = engine.pool().map_key(resolved_recv); let v = engine.pool().map_value(resolved_recv); engine.pool_mut().tuple(&[k, v]) } arm BEFORE the else { return; } fallthrough at line 142.
• compiler/ori_types/src/infer/expr/calls/closure_unify.rs:122-126 — strip the // intentionally excluded for now exclusion comment as the gate lifts.
• compiler/ori_types/src/infer/expr/calls/tests.rs (sibling tests module per compiler.md §Testing) — add 4-cell matrix per tests.md §Matrix Testing Rule: two positive cells covering BOTH call paths (.map via unify_higher_order_constraints, .flat_map via unify_flat_map_constraints), one positive destructure cell (((k, v)) -> ...), one negative pin (Tag::Iterator receiver unchanged — regression guard the new Map arm did NOT widen beyond Map).

Success criteria (each carries a concrete file-path + line / commit-anchor pointer per feedback_no_nice_to_have_deferrals):

• compiler/ori_types/src/infer/expr/calls/closure_unify.rs:142 exclusion gate narrowed: new else if recv_tag == Tag::Map { ... } branch inserted immediately BEFORE the else { return; } fallthrough; branch body extracts engine.pool().map_key(resolved_recv) + engine.pool().map_value(resolved_recv) and constructs engine.pool_mut().tuple(&[k, v]) as source_elem. Comment at lines 122-126 stripped. Done 2026-06-07. Empirical grounding recorded during implementation: (a) NO registry higher-order method dispatches with a bare Tag::Map receiver today (ori_registry map def carries no map/filter/fold/flat_map; kvs.iter() returns ReturnTag::MapIterator, so chained .map receivers are Tag::Iterator) — the arm is reachable only through direct helper invocation until map HOFs land; the unit matrix exercises the helper + BOTH dispatch fns directly. (b) Lambda tuple-pattern destructure ((k, v)) -> ... is NOT grammar-legal per grammar.ebnf lambda_params (identifiers only) — the destructure cell is replaced by tuple-component cells (kv.0 / kv.1). (c) kvs.map(...) on a bare map silently poisons with 3 misleading E2005s and NO unknown-method diagnostic (silent-accept class) — the relatedness test redirected it inline as a discovery insertion in THIS plan at §06.5 (Unknown-method diagnostic + follow-on E2005 suppression), NOT a separate bug-tracker entry.
• Rust unit test tests::test_lambda_param_from_map_receiver_propagates_kv_tuple (positive — direct helper invocation with Map receiver) passes at compiler/ori_types/src/infer/expr/calls/tests.rs map_receiver_lambda_param module; companion test_lambda_param_from_map_via_higher_order_map_path exercises the unify_higher_order_constraints “map” arm. Done 2026-06-07.
• (amended 2026-06-07) Destructure cell REPLACED: ((k, v)) -> ... lambda params are not grammar-legal per grammar.ebnf:550-556 lambda_params (identifiers only; parser correctly rejects with E1002). Coverage of both tuple components lands as kv.0 / kv.1 cells in the unit matrix + the spec test’s key/value component tests.
• Rust unit test tests::test_lambda_param_from_map_via_flat_map_path (positive — unify_flat_map_constraints call path; name amended from the planned ..._flat_map_propagates_kv_tuple) passes; asserts BOTH the (K, V) param binding AND the result-elem unification. Verifies the shared helper cures BOTH SSOT call sites in one fix. Done 2026-06-07.
• Rust unit test tests::test_lambda_param_from_iterator_receiver_unchanged_by_map_arm (negative pin per tests.md §Matrix Clamping) passes — unit cell (helper direct, Tag::Iterator<int> receiver binds param to int, not a tuple) + full-pipeline pin of the same name in check/integration_tests.rs plus test_lambda_param_from_map_iter_iterator_elem_unchanged (map-iterator pipeline pin). Done 2026-06-07.
• Ori spec test compiler_repo/tests/spec/collections/map/lambda_param_from_receiver.ori (path amended: the existing map corpus lives at tests/spec/collections/map/, no tests/spec/types/map/ dir exists) covers untyped lambda over map-ITERATOR receivers via .map (both kv.0 and kv.1 components) + .flat_map; destructuring dropped per the grammar finding above. Verified 2026-06-07: ori test <file> 3 passed / 0 failed.
• Dual-exec parity confirmed: diagnostics/dual-exec-verify.sh tests/spec/collections/map/lambda_param_from_receiver.ori reports DUAL-EXECUTION: ALL VERIFIED (3 tests), zero mismatches (2026-06-07).
• §09.6 close-out flips frontmatter sections: entry id: '09.6' status: not-started → complete.

09.7 File-split larger files in check/bodies/ + infer/expr/

Status: blocked (2026-06-07). Umbrella-absorbed inline subsection (user directive 2026-05-15) — the 500-line-cap file-splits land in this plan as §09.7, NOT a separate bug-tracker entry. All 5 file-splits landed (committed 59f645300); the only residuals are the cross-scope ./test-all.sh gate (blocked-by plans/aims-burden-tracking/section-09-post-convergence-partial-retirement.md) + the §09.7 close-out flip. Frontmatter sections: entry 09.7 is status: blocked.

Goal: Split files exceeding impl-hygiene.md §File Organization 500-line cap into cohesive submodules per §10.0 precedent. Targets (overrun line counts AS OF §09.7 authoring / pre-split — post-split sizes recorded in the §09.7 success criteria + HISTORY 2026-06-07):

• compiler/ori_types/src/check/bodies/impls.rs — 681 lines (+181 over cap) — smallest overrun; mechanical first split.
• compiler/ori_types/src/infer/expr/operators.rs — 799 lines (+299) — extract per-operator-class submodules.
• compiler/ori_types/src/infer/expr/control_flow.rs — 750 lines (+250) — extract try / if-let / for / while per-form submodules.
• compiler/ori_types/src/infer/expr/blocks.rs — 617 lines (+117) — extract infer_lambda to dedicated lambdas.rs submodule (precedent: §09.4’s closure_unify.rs split from method_call.rs).
• compiler/ori_types/src/infer/expr/calls/method_call.rs — 503 lines (+3 over cap) — final consolidation of remaining helpers.

Tooling: use compiler_repo/scripts/extract_tests.py to lift tests during the split per compiler.md §Testing discipline.

Success criteria (concrete artifact anchors per feedback_no_nice_to_have_deferrals):

• Each of the 5 files above ≤500 lines post-split. Verified 2026-06-07: impls.rs 314 (+ def_impls.rs 255 + method_sig.rs 138), operators.rs → operators/ dir (max 467), control_flow.rs → control_flow/ dir (max 414), blocks.rs 202 (+ lambdas.rs 441), method_call.rs 397 (+ infinite_iterator.rs 113). Every touched/created file ≤500 (max 467).
• All public APIs preserved (no exported-symbol drift). Verified 2026-06-07 via mod.rs pub use re-exports at the prior paths + cargo check/cargo clippy -D warnings as arbiter (all external consumers resolve unchanged); two recorded deltas: operators::has_comparable_trait gained #[cfg(test)] (usage was test-only; non-test re-export tripped -D unused) and the bare substitute_type_params re-export was dropped from control_flow/mod.rs (zero external consumers; remains crate-internal via control_flow::substitution). Graph-side file-symbols cross-check re-runs post-commit when the intel graph re-indexes.
• timeout 150 cargo test -p ori_types --lib passes after each per-file split AND at sequence end (1063 passed / 0 failed; clippy —tests -D warnings clean). 2026-06-07.

• timeout 150 ./test-all.sh passes post-split-sequence (full regression covering Ori spec + LLVM + valgrind per compiler.md §Verification Test Suites). 2026-06-07 run: RED from cross-scope in-flight work — all failures are AIMS/ARC/burden/reuse-class (ori_arc full_pipeline_on_reuse_pattern + pipeline_determinism, AOT aims_*/arc_*/burden-alias cells, LLVM spec CRASH) owned by the parallel session’s uncommitted emit_unified.rs/aims_pipeline + staged monomorphize edits; zero failures in ori_types scope (per-crate suite 1063/1063 green). Re-verify on next loop iteration once the parallel tree settles; §09.7’s own gate evidence is the per-crate suite above.
• §09.7 close-out flips frontmatter sections: entry id: '09.7' status: blocked → complete — gated on the blocked-by re-check (per the §09.N “§09.7 cross-scope blocker re-detection protocol” item): re-verify plans/aims-burden-tracking/section-09-post-convergence-partial-retirement.md is complete AND timeout 150 ./test-all.sh is green BEFORE flipping; until then the <!-- blocked-by:... --> anchor at section-09-body-inference-gaps.md:676 stays live.

Hygiene Findings (2026-05-14)

Findings

[F1 — COMMENT_HYGIENE_DRIFT:stale-plan-annotation] Major — 17 stale BUG-01-002 references across compiler/ori_types/src/:

• check/bodies/impls.rs:145 — Phase B Step 5 (BUG-01-002): pool.rigid_var(name)...

• check/bodies/impls.rs:343 — Phase B Step 5 (BUG-01-002): rank scope

• infer/expr/calls/constraints.rs:241 — BUG-01-002 §05 Phase B residual: wc.ty is the fresh-Var Idx

• infer/expr/calls/impl_lookup.rs:37 — Tag::Scheme instantiation. BUG-01-002 §05 Phase B residual.

• infer/expr/calls/impl_lookup.rs:93 — BUG-01-002 §05 Phase B residual: the engine half of the dispatch fix

• infer/expr/calls/impl_lookup.rs:174 — E2023. BUG-01-002 §05 Phase B residual.

• infer/expr/calls/impl_lookup.rs:251 — Two-phase lookup per BUG-01-002 §05 Phase B residual

• infer/expr/calls/impl_lookup.rs:438 — Phase B residual (BUG-01-002): apply impl-level binder substitution

• infer/expr/calls/impl_lookup.rs:452 — Phase B Step 5b (BUG-01-002): if the registered signature is a

• infer/expr/calls/impl_lookup.rs:462 — Phase B residual (BUG-01-002): use instantiate_with_subst

• check/registration/impls.rs:69 — BUG-01-002 sub-gap (b): explicit user-written impl methods

• check/registration/impls.rs:96 — (BUG-01-002 sub-gap (b)).

• check/registration/impls.rs:121 — with a populated overlay (BUG-01-002 §05 Phase B residual).

• check/registration/impls.rs:169 — Pre-BUG-01-002 sub-gap

• check/registration/impls.rs:213 — BUG-01-002 sub-gap (b) — Inherited default-method binder remapping:

• check/registration/impls.rs:404 — Phase B Step 5b (BUG-01-002): when the method declares method-level type

• check/registration/impls.rs:443 — BUG-01-002 sub-gap (b): merge trait_substitutions into the resolver

• BUG-01-002 is closed (bug-tracker/section-01-parser-lexer.md:20 [x]; plan dir at bug-tracker/plans/completed/BUG-01-002/).

• Cure: §09.N close-out cleanup sweep — strip stale references per .claude/skills/impl-hygiene-review/plan-annotations.sh.

• For each site: drop the BUG-01-002 reference if comment is historical scaffolding; OR rewrite to permanent form (// Why:, // INVARIANT:, // Spec: Clause N.M) per impl-hygiene.md §Allowed comment categories C-A2/C-A3.

[F2 — STRUCTURE:budget-overrun] Minor — 8 §09-touched files over 500-line limit: check/bodies/impls.rs (+181), infer/expr/operators.rs (+299), infer/expr/control_flow.rs (+250), infer/expr/blocks.rs (+117), infer/expr/calls/monomorphization.rs (+54), infer/expr/calls/impl_lookup.rs (+24), infer/expr/calls/method_call.rs (+3), check/registration/impls.rs (+32). Cure: split immediately for method_call.rs (+3) via extract_tests.py; larger splits (operators.rs, control_flow.rs, impls.rs, blocks.rs, etc.) owned by §09.7 inline subsection per routing.md §4.

[F3 — NOTE] Informational — operators.rs:614 (comparison_trait_name), registry_bridge/mod.rs:452 (extract_elem), registry_bridge/mod.rs:474 (type_tag_to_idx) _ => unreachable!() arms are legitimate exhaustive matches over invariant-narrowed inputs. All 3 are GAP-free per impl-hygiene.md §Compiler-Specific Invariants. No action required.

[F4 — LEAK:scattered-knowledge] Major — 6 string-identity comparisons PARTIALLY REFUTED + DEFERRED (2026-05-14): §09.5’s Error well-known registration IS the canonical landing for type-name interner-driven recognition. F4’s remaining sites split into 2 categories on re-read:

• (a) Method-name pattern detection in find_infinite_source (method_call.rs:469,485) + resolve_named_type_method (methods/mod.rs:97): these match method names against string literals alongside const BOUNDING_METHODS: &[&str] / TRANSPARENT_ADAPTERS: &[&str] constants. Pre-interning ONLY the 'cycle'/'repeat'/'unwrap'/'inner'/'value' names while leaving sibling constants as &[&str] creates internal inconsistency. The genuine cure surface — registry-driven method-name dispatch (move infinite_source: bool + newtype_accessor: bool into ori_registry::MethodDef) — crosses subsystem scope (compiler/ori_registry + compiler/ori_types + spec touch). DEFERRED with concrete anchor: file BUG-02-031 (tracker entry) at §09.N close.
• (b) Trait-name dispatch in registry_bridge/mod.rs:68,80,98,103: these match trait names (Eq/Comparable/Hashable/DoubleEndedIterator) inside the registry-bridge layer that converts TypeDef.operators bitflags into trait-satisfaction queries. WellKnownNames already pre-interns these trait names (self.hashable, self.printable, trait_bit_map at well_known/mod.rs:111-143). The bridge layer’s string compare against engine.lookup_name(*name) is the standard interner-output access pattern, not a bypass — it’s bridge-layer design. NOT a LEAK; refute classification.

§09.N close-out remediation: file BUG-02-031 tracker entry for (a) method-name registry-driven dispatch refactor (out-of-scope for §09 — crosses ori_registry/ori_types/spec).

Lines (preserved for tracker-index reference):

• infer/expr/calls/method_call.rs — 'cycle', 'repeat' string-matches for iterator-method name recognition

• infer/expr/methods/mod.rs — 'unwrap', 'inner' string-matches

• infer/expr/registry_bridge/mod.rs — 'DoubleEndedIterator', 'Eq', 'Comparable' string-matches for trait name recognition

• These bypass the Name interning layer (typeck.md §EX-1 / types.md §RG-3).

• Cure: extend WellKnownNames at well_known/mod.rs:40 with pre-interned slots for the above names following the §09.5 'Error' pattern (well_known/mod.rs:251 name == self.error).

• Replace each string-match site with Name == name comparison via WellKnownNames cache.

• Per CLAUDE.md §Scope Expansion (litter-pickup): all 3 files were touched by §09 commits; expansion is mandatory.

• Cure scope: extend struct + replace ~6 call sites.

[F5 — NOTE] Informational — BD-2 SSOT discipline confirmed: check_expr at infer/expr/mod.rs:304-439 is the sole BD-2 dispatch point. 5 gates share gate-skeleton but differ structurally; no extractable duplication. No action required.

[F6 — NOTE] Informational — Error type registration SSOT confirmed: well_known/mod.rs:228-262 resolve_primitive is sole canonical entry; type_resolution.rs:134 belt-and-suspenders arm is legitimate redundancy (not algorithmic duplication). No action required.

[F7 — NOTE] Informational — All 3 §09.5 #[ignore] cells (check/bodies/tests.rs:639,683,705) satisfy test-disposition.md §Required reason format with BUG-02-028/029/030 tokens verified filed-open. No DISPOSITION_DRIFT. No action required.

[F8 — NOTE] Informational — §09 commit-range test names conform to <subject>_<scenario>_<expected> per impl-hygiene.md §Test Function Naming. Phase-0 test-weak findings (propagates/falls_back/reports/all_simple flagged as weak descriptors) are confirmed false positives — these are domain verbs. No action required. Tooling improvement: update hygiene-lint test-weak scanner to recognize compiler-internal domain verbs at §09.N close-out.

[F9 — DRIFT:registration-sync] Out-of-scope: DerivedTrait match completeness drift at compiler/ori_llvm/src/codegen/derive_codegen/field_ops/mod.rs:185 missing Clone/Debug/Default/Printable variants. REFUTED (2026-05-14): pre-filing verification on the cure attempt found the match’s discriminant is op: FieldOp, not DerivedTrait. FieldOp (ori_ir/src/derives/strategy.rs:73) has exactly 3 variants — Equals/Compare/Hash — by design; the match is exhaustive over FieldOp and projects each to its corresponding DerivedTrait value (Eq/Comparable/Hashable). Clone/Default/Printable/Debug flow through CloneFields/DefaultConstruct/FormatFields strategies (ori_ir/src/derives/strategy.rs:147-202), which never enter field_ops/mod.rs. Per ir.md §DerivedTrait, the canonical ori_llvm sync point is codegen/derive_codegen/ strategy dispatcher — NOT this per-field-op projection. The /impl-hygiene-review Phase 3 reviewer pattern-matched on DerivedTrait::* arm-name shapes without reading the surrounding context to confirm the match discriminant. No cure needed; no bug filed. Same false-positive pattern as F10 (reviewer reads arm shape, skips discriminant verification). Tooling improvement candidate: hygiene-lint variant-coverage detector should verify the match’s discriminant type before flagging “missing variants” — DerivedTrait sync requires reading ir.md §DerivedTrait’s canonical sync-point list (ori_types/check/registration/, ori_eval/interpreter/derived_methods.rs, ori_eval/derives/mod.rs, ori_llvm/codegen/derive_codegen/mod.rs), not arm-name pattern matching.

[F10 — LEAK:swallowed-error] Minor — infer/expr/structs/field_access.rs:42 Tuple branch missing else arm. REFUTED (2026-05-14): independent verification on cure attempt found the else arm DOES exist at field_access.rs:55-63: else { engine.push_error(TypeCheckError::undefined_field(span, resolved, field, vec![])); Idx::ERROR }. The /impl-hygiene-review Phase 3 reviewer misread the source. No cure needed; finding is a false-positive that mirrors the pattern of /tpr-review Round 1 gemini F1 (different file, same misread-without-reading-the-else-arm shape). Tooling improvement candidate: hygiene-lint.py swallowed-error detector should verify NO sibling else arm exists before flagging if let Ok(...) patterns.

Next-action for §09.N close

• Unblocks §09.N close upon: F1 sweep complete (21 sites cured 2026-05-14), F4 partial-cure via Error registration (BUG-02-031 anchor for method-name registry-driven dispatch refactor), F10 refuted (no cure needed), F9 refuted (no cure needed).
• Does not block §09.N close: F2 (tracked §09.N follow-up checkbox; defer larger splits).
• Tooling improvements (queue for §09.N close-out sweep): AA-01 (hygiene-lint scanner helper-call indirection), AA-02 (plan_annotations.py tracker-index scan), AA-03 (DerivedTrait /add-bug).

§09 Autopilot Discipline — Banned Patterns + Exit Reasons

Per .claude/rules/skill-vocabulary.md §2 + §3 + .claude/rules/skill-control-contract.md §Execution Modes, autopilot execution of §09 work surfaces:

Banned patterns (Critical autopilot-pause-leak when emitted during autopilot)

• “Should I continue to §09.6?” / “Want me to proceed with the file-split?” / “Shall I run the matrix?” — STRUCTURE:autopilot-pause-leak Critical per impl-hygiene.md §STRUCTURE:autopilot-pause-leak.
• “Pausing here for a checkpoint” / “Natural stopping point” / “Context is getting heavy” — context-pressure prose banned per skill-control-contract.md §Banned Patterns.
• “§04 is blocked so I’ll defer §09” — work-order violation routes through depends_on: frontmatter declaration + §09.R finding; §09 work IS gated, NOT deferred via prose.
• “Architectural depth in §09.6 warrants a fresh session” / “Better to revisit after compaction” — architectural-depth-as-defer rationalization banned per CLAUDE.md §Failing Tests Mid-Work → Architectural depth ≠ defer license.
• “Cap-exhaustion at /tp-help round 3 means we proceed with reduced rigor” — banned per skill-control-contract.md §Banned cap-aggregation rationalizations.

Exit reason mapping (consumed by /continue-roadmap Step 6 + /fix-bug Phase 4 + autopilot drivers)

The exit_reason column below uses the canonical scripts/plan_corpus/exit_reasons.py CANONICAL_EXIT_REASONS members directly (reconciled 2026-06-08 per decisions/31 — no divergent plan-local enum). The prior plan-local mnemonics map: subsection_complete / section_complete → gate_passed; failed → validation_failed; architectural_decision_required → materiality_architectural_escalation; the predecessor-unsatisfied case → section_advance_blocked.

Per state-discipline.md §4, all exit-reason transitions write to review_pipeline: frontmatter on the section; autopilot consumers read frontmatter, not prose.

HISTORY

• 2026-06-07 (later): §09 /review-plan close-out ran the full pipeline (Step 1.7 audit clean -> Step 2/3 audit -> Step 4 /tp-help blind-spots [6 cohesion + 1 arch-risk + 1 cross-cutting] -> Step 5 editor [16 stale-text/cohesion cures] -> Step 6 /tpr-review 3-round cap). TPR surfaced + CURED 10 findings inline across 3 rounds (per-round 2/3/5, non-monotonic): a systematic pre-existing misattributed-bug-ID class authored in prior sessions (BUG-02-044 cited for the bare-Map unknown-method silent-poison [actually the while-loop break/continue bug] -> corrected to the §06.5 inline discovery-insertion anchor; BUG-02-032 cited for Tag::Map [actually drop_early] + BUG-02-034 cited for the file-split [actually the validate_assoc_types ICE] -> reframed as umbrella-absorbed inline §09.6/§09.7; propagated instance in 00-overview cured) + index.md/§09.R/§09.6 status-label drifts + an impl_lookup.rs path/line correction (check/bodies/->infer/expr/calls/, 522L->591L) + a not-started->blocked close-out-flip-text correction. Verdict: SIGNIFICANT REWORK APPLIED, 26 findings resolved, 0 deferred. reviewed:true flip GATED by the mechanical baseline regression (newly_failing = aims_burden_alias/aims_interactions/arc/burden-class — ALL cross-scope, owned by the parallel aims-burden-tracking §09 session’s 59f645300 burden-only RC-emission default flip; ori_types scope is 1063/1063 green). Section stays status: in-review. Disposition per skill-control-contract.md §Autopilot Mode unified hook-failure clause: cross-scope baseline regression, proceed without flipping reviewed:true (clears when aims-burden-tracking §09 lands green OR the baseline is rebased). Residual at next user touchpoint: a bug-ID grounding sweep over remaining BUG-XX-NNN citations (the cap-with-substantive + non-monotonic trend suggests the misattribution class may not be exhausted).

• 2026-06-07 (later): splits COMMITTED in compiler_repo 59f645300 (swept with parallel session’s burden-only RC default flip). Re-ran test-all on the clean committed tree: still 367 RED, all AIMS/ARC/AOT-class — owned by plans/aims-burden-tracking section-09 (status: in-progress, live parallel session; 59f645300 flipped default burden-only RC emission mid-arc). Zero failures in ori_types scope. §09.7 remaining gate (suite green + close-out flip) marked blocked with blocked-by anchor to the owning plan section per the §06.4 precedent; re-opens when aims-burden-tracking §09 lands green. Walk advances past §09.7.

• 2026-06-07: §09.7 all 5 file-splits landed in working tree (method_call.rs 397 + infinite_iterator.rs 113; blocks.rs 202 + lambdas.rs 441; impls.rs 314 + def_impls.rs 255 + method_sig.rs 138; operators/ dir max 467; control_flow/ dir max 414). Per-crate verification green: cargo test -p ori_types —lib 1063/1063, clippy —tests -D warnings clean, public paths preserved via mod.rs re-exports. Full ./test-all.sh RED from cross-scope parallel-session in-flight work (uncommitted emit_unified.rs/aims_pipeline + staged monomorphize edits; failures all AIMS/ARC-class, zero in ori_types). Disposition per skill-control-contract.md §Autopilot Mode unified hook-failure clause: proceed without committing this round’s work. Remaining §09.7 gate (test-all green + close-out flip) re-verifies on next loop iteration (/loop 5m active).

• 2026-05-15 — §09.4 design body re-aligned with shipped SSOT-helper path: Proposed design called for check_lambda function in blocks.rs + ExprKind::Lambda BD-2 gate in check_expr mirroring §09.1’s pattern. Shipped path: SSOT-helper extension of unify_closure_param_with_iterator_elem at compiler/ori_types/src/infer/expr/calls/closure_unify.rs:127 to unwrap Tag::List / Tag::Set / Tag::Str receiver element types. infer_lambda at blocks.rs:223 remains the lambda entry point; no check_lambda function, no ExprKind::Lambda BD-2 gate. Two §09.4.3 checkboxes marked ~~strikethrough~~ SUPERSEDED with pointer to this entry. §09.4 success_criterion at lines 36-45 accurate; only §09.4 design body re-aligned. Verified via grep -rn "fn check_lambda" compiler_repo/compiler/ori_types/src/ returning empty. Filed via /tpr-review F4 (opencode, PLAN_COHERENCE_DRIFT) on /review-plan Round 2.

• 2026-06-07 — Stale review_pipeline: marker cleared by /continue-roadmap orchestrator: marker carried stage: tpr-done, next_step: 7, updated: ?. Per /review-plan SKILL.md §Step 1a stale-marker rule (reviewed: false + marker present → STALE by definition), marker invalid; prior diagnosis preserved here for traceability. Cure rooted in scripts/plan_orchestrator/markers.py:clear_stale_marker_if_unreviewed.