0%

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 (method_call.rs:271-285, limited to is_iterator()).

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-344) + check_def_impl_method (check/bodies/impls.rs:288-406) with 4 targeted propagation / binding fixes that close the typeck body-inference gaps surfaced by §06.2C investigation. Establishes the §09.1 check_expr gate pattern that §09.3 and §09.4 reuse; §09.2 is orthogonal (impl-scope binding, not BD-2 propagation).

Depends on: §03 (bodies-pass integration + defaulting pre-pass), §04 (codegen assertions). All §09 work lands after §03’s validator + defaulting pipeline is live so BD-2 propagation additions don’t interact with an un-gated PC-2 surface.

Sequencing rule: §09.1 establishes the check_expr gate pattern — it lands FIRST. §09.3 and §09.4 reuse the pattern. §09.2 is orthogonal and can land at any point in §09. Implementation order: §09.1 → §09.2 → §09.3 → §09.4 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 (previously 2 residual E2005 at lines 184, 194).
  • Run timeout 150 cargo stf tests/compiler/typeck/let_bindings.ori — green (previously 4 E2005 clusters on naked Ok in try-blocks).
  • 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 (previously 1 E2005 at def-impl-with-self).
  • 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: Add check_lambda function in blocks.rs + check_expr gate for ExprKind::Lambda that propagates Check(Function(param_types) -> ret_ty) from the call-site expected type into lambda parameter typing. Extend unify_closure_param_with_iterator_elem at method_call.rs:271-285 to also handle Tag::List, Tag::Set, Tag::Map, Tag::Str receivers (currently only Tag::Iterator/Tag::DoubleEndedIterator). Closes the §06.2B lambda-parameter class root cause and potentially also str_to_error.ori’s .into() propagation.

Reuses §09.1 pattern: check_expr gate, unwrap expected function type, propagate param types into check_lambda.

§09.4 prerequisite — §10.0 file splits MUST land first: §09.4 touches infer/expr/calls/method_call.rs (extending unify_closure_param_with_iterator_elem). At 524 lines (24 over the 500-line impl-hygiene.md §File Organization limit), touching without first splitting is a BLOAT violation. §10.0’s split extracts method_call/receiver_dispatch.rs before §09.4 edits. See 00-overview.md Implementation Sequence — §10.0 is execution-ordered between §09.3 and §09.4.

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

Fix shape:

  1. Create check_lambda(engine, arena, params, ret_ty_annotation, body, span, expected: &Expected) -> Idx in blocks.rs:
    • If expected.ty resolves to Tag::Function: extract param types via pool.function_params(expected.ty) and return type via pool.function_return(expected.ty).
    • For each lambda param WITHOUT source annotation, bind to the extracted param type instead of engine.fresh_var().
    • For each lambda param WITH source annotation, unify the annotated type with the extracted param type (via check_type → unify) so mismatches report E2001.
    • Check body with Check(extracted_return_type).
  2. In check_expr at infer/expr/mod.rs, add ExprKind::Lambda gate BEFORE default fallback, calling check_lambda when expected.ty is Tag::Function.
  3. Extend unify_closure_param_with_iterator_elem at method_call.rs:271-285 to unwrap Tag::List / Tag::Set / Tag::Map / Tag::Str element types, not just Tag::Iterator. Use the same unwrapping functions already used by infer_for_pattern at sequences.rs:128-135.

Composition with §09.3: let e: Error = msg.into() flows check_expr with Check(Error) → ExprKind::MethodCall(.into()). The receiver msg is inferred; the method into has signature <T>(self) -> T (generic). §09.4 does NOT directly solve this — method-call return type propagation from LHS annotation is a separate gap that may or may not be in §09.4’s scope. If residual after §09.4, classify as additional gap and address in a follow-up.

09.4.3 Implementation

  • Write failing tests FIRST.
  • Create check_lambda in blocks.rs.
  • Add ExprKind::Lambda gate in check_expr.
  • Extend unify_closure_param_with_iterator_elem to handle Tag::List / Tag::Set / Tag::Map / Tag::Str.
  • 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>, {K:V}, str, Tag::Iterator (via .iter() chain).
    • 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

  • None.

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.
  • 09.2 complete — def-impl Self binding via registered RigidVar; keywords.ori green; no Self fabrication.
  • 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).
  • 09.4 complete — check_lambda propagation from method-call receiver element type; .map/.filter/.fold on Tag::List/Tag::Set/Tag::Map/Tag::Str receivers work with untyped lambdas.
  • §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).
  • Dual-execution parity — timeout 150 diagnostics/dual-exec-verify.sh zero divergences on §09-touched files.
  • §09 aggregate /tpr-review on full §09 diff (after all 4 subsections land) → clean. Required even though per-subsection TPR ran.
  • §09 aggregate /impl-hygiene-review → clean.
  • /improve-tooling section-close sweep — any new hygiene rules about BD-2 gate extension pattern.
  • /sync-claude section-close doc sync — update typeck.md §EX-16, §BD-2 with lessons; update CLAUDE.md memory if new Ori patterns discovered.
  • Plan sync — §09 frontmatter status: complete; §00-overview 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).

Exit criteria: All 4 subsections complete with TPR + hygiene 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 may begin.