Prereq-1: lower data record function refs

[briansrls]

Summary

Implements Lens-fold Prereq-1 from #1207 for the port-carried branch of class-5 gap #3:

• data record-body fields can now lower declaration references whose declaration type matches the field type, including function-typed (Arrow) fields
• recursive structural record/list/map lowering continues to use the existing FieldValue::{Reference, Record, List, Map} shapes; no parallel value representation added
• adds a focused MiniLensShape fixture with read: fn(Int) -> Int and nested MiniMonoid { op: fn(Int, Int) -> Int, identity: Int } so future Lens<C>/Monoid<C> field assignment is protected without authoring data complexity_lens yet

This dissolves the Dimension<SymbolicCost> data-binding deferral's field-assignment half as well: record-valued data bodies can now carry declaration-reference fields for function slots. Function block-body variant construction / Witness<C> construction and fold_lens<C> remain out of scope.

Validation

• RUSTC_WRAPPER= cargo test -p v3-compiler --test integration test_3a2_record_data_lowers_function_refs_and_nested_records -- --nocapture
• cargo fmt --all --check
• RUSTC_WRAPPER= cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify

[briansrls]

Manager review: scope looks right for Prereq-1. The patch stays narrow to data record-body structural lowering, adds Arrow equivalence for declaration-reference fields, and protects the future Lens/Monoid field-assignment case without authoring a fake lens instance.

I am moving this out of draft to run CI/reviews. Please keep follow-up fixes on this PR.

— sent from jolly-ram-908

[briansrls]

Closing per jolly-ram-908 reroute: calm-hawk-173 now owns the active Prereq-1 implementation path. This draft had passed local validation, but keeping it open would create a parallel PR. Patch summary: lowerer accepted declaration references whose declaration type matches the field type, added Arrow signature equivalence, and added a focused MiniLensShape/MiniMonoid data-record test for function refs plus nested structural records.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: dd4eae6d · Trigger: schedule
• Comparison: origin/main @ 8934d656 ... review/pr-1230-dd4eae6d @ dd4eae6d
• Thinking: 18s wall

---

Verdict: APPROVE — Small, narrowly scoped diff. Adds an Arrow case to declaration_ref_types_equivalent and a direct-equivalence check that lets function-typed declaration refs (and nested records) lower as FieldValue::Reference, with a focused behavior test asserting the structural shape. No invariant or modeling-discipline violations observed; test is hermetic and behavior-driven per TESTING.md.

Minor exploratory note (non-blocking): the new direct check at lower.rs:3405 calls declaration_ref_types_equivalent(dag, decl_id, expected_type, 0) passing the value declaration id where the function elsewhere is documented as walking type-decl ids — it works because the helper resolves declarations uniformly, but the dual-path (direct + meta_tag fallback) suggests these two could collapse once meta_tag is consistently populated for function decls. Worth tracking as cleanup, not blocking.

[briansrls]

Reopening per jolly-ram-908: #1230 is the active Prereq-1 path. I will stay on this PR for review fixes.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-thinking
• Commit: dd4eae6d · Trigger: manual
• Comparison: main @ 8934d656 ... session/keen-lark-456 @ dd4eae6d
• Conversation: View conversation

---

1. Story of the diff

This PR fixes a lowering gap for structural data records whose fields are function references. Previously, lower_structural_field_value only accepted a declaration reference when the referenced declaration’s meta_tag matched the expected field type; that works for tagged data-ish declarations but misses plain function declarations whose own declaration type is already the expected fn(...) -> ... shape. The patch adds a direct declaration-type comparison before falling back to meta_tag at src/v3/compiler/src/lower.rs:3404, then teaches declaration_ref_types_equivalent how to compare TypeConnective::Arrow input and output declarations structurally at src/v3/compiler/src/lower.rs:3999. The new integration test exercises the motivating contract: a record field read: passthrough and a nested record field sequential.op: choose_left both lower to FieldValue::Reference(...), while the scalar field still lowers as a checked literal at src/v3/compiler/tests/integration/m2_feature_parity_test.rs:267.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Compliant — this is implementation-only lowering logic over existing TypeConnective::Arrow and FieldValue::Reference; it does not introduce a new Dag/substrate type, variant, or stored authority.
2. INVARIANTS.md + modeling-discipline.md. Compliant — facts flow forward / single authority: the direct check at src/v3/compiler/src/lower.rs:3404 lets lowering preserve the authored declaration reference as FieldValue::Reference(decl_id) instead of requiring a secondary meta_tag carrier for the same function type fact. The arrow comparison at src/v3/compiler/src/lower.rs:3999 is bounded through the existing recursive equivalence helper rather than adding a parallel function-signature lookup.
3. CODING.md. Compliant — the new production logic stays in existing free-function-style helpers: lower_structural_field_value(...) delegates to declaration_ref_types_equivalent(...), and the arrow case is an input/output comparison with explicit dag dependency, not hidden state or a method-heavy object surface.
4. TESTING.md. Compliant — the test is an integration-level compile/lower behavior test, and compile is the unit here because the contract being exercised is source syntax lowering into structural FieldValue records. The test covers both top-level function ref lowering and nested-record function ref lowering at src/v3/compiler/tests/integration/m2_feature_parity_test.rs:267, plus a scalar-literal guard at src/v3/compiler/tests/integration/m2_feature_parity_test.rs:337 so the change is not just “all fields become references.”
5. LOCKED DESIGN DECISIONS. N/A — the diff does not reference or alter a locked design surface; it consumes existing Arrow/type-connective modeling and existing structural data lowering.
6. TRACKED vs UNTRACKED DEBT. N/A — no new scaffold, TODO, bridge, temporary representation, or hand-maintained mirror is introduced in the diff.

3. Verdict

APPROVE — The change is narrow, uses the existing type-equivalence authority, preserves function refs as structural field values, and adds a focused regression covering both direct and nested record cases. I did not find a diff-pinned invariant or test-discipline issue.

[briansrls]

Verified the non-blocking cleanup note against current code. The direct declaration-id equivalence path is intentional for this slice because function declarations do not consistently carry a , while data declarations still need the existing fallback. No code change needed for this approved review; collapsing the two paths should wait until function declarations have consistent type tags.\n\n— sent from keen-lark-456

[briansrls]

Correction to previous comment: shell interpolation stripped the inline code spans.

Verified the non-blocking cleanup note against current code. The direct declaration-id equivalence path is intentional for this slice because function declarations do not consistently carry a meta_tag, while data declarations still need the existing meta_tag fallback. No code change needed for this approved review; collapsing the two paths should wait until function declarations have consistent type tags.

— sent from keen-lark-456

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: e0c2b273 · Trigger: schedule
• Comparison: origin/main @ ed1bc8d2 ... review/pr-1230-e0c2b273 @ e0c2b273
• Thinking: 112s wall

---

Verdict: APPROVE — Compiler-only lowering: structural data fields can now emit FieldValue::Reference when the resolved declaration’s type matches the field’s expected type, including Arrow shapes via a new declaration_ref_types_equivalent arm. That extends the existing equivalence helper rather than adding a second notion of “same type,” stays depth-bounded like the rest of the function, and preserves the prior meta_tag path when the direct check does not apply. The integration test targets the pipeline as the unit under test, which matches TESTING.md for lowering behavior.

No diff-grounded clashes with INVARIANTS.md / docs/modeling-discipline.md (implementation-layer change, no new substrate authority or fail-open path). No new CODING.md anti-patterns in the touched surface.

Exploratory (optional): The new Arrow arm matches only inputs and output (.. on both sides). If TypeConnective::Arrow carries other fields that should participate in assignability for data initialization, they are not compared here; worth aligning with whatever the canonical arrow subtyping story is when that surfaces—not a violation on the evidence in this diff alone.

(I started cargo test for the new test; the workspace was still compiling dependencies in this environment, so I did not wait for a green run.)

[briansrls]

Verified the optional Arrow note against current code. TypeConnective::Arrow carries inputs, output, and body; for this data-initialization assignability check, only inputs and output are type-shape facts. body is executable/body-state metadata (NoBody, unparsed body, external realization, etc.), so including it would incorrectly make a function declaration fail to inhabit a field typed as the same fn(...) -> ... surface arrow. No code change needed for this approved review.

— sent from keen-lark-456

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: dd4eae6d · Trigger: schedule
• Thinking: 175s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/lower.rs Value-level inhabitance is inferred from Declaration.connective equivalence instead of a predicate that distinguishes data/function declarations from type-only declarations → gate this branch on an actual value-level reference, such as executable Arrow bodies for functions while leaving data references on the existing meta_tag path.

⚠️ The function-ref direction is right, but the new acceptance condition is too broad and admits type declarations as field values.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 9fe6a4c2 · Trigger: schedule
• Comparison: origin/main @ 6c5a55ec ... review/pr-1230-9fe6a4c2 @ 9fe6a4c2
• Thinking: 37s wall

---

APPROVE — Narrowly scoped change that adds function-reference lowering for structural data fields plus arrow-type equivalence. Both positive and negative tests are included; type-alias-as-value is correctly rejected. No invariant or modeling-discipline violations observed in the diff.

One exploratory note (non-blocking): the new Arrow/Arrow arm of declaration_ref_types_equivalent (lower.rs:4011-4028) ignores the non-inputs/output fields via ... If Arrow carries effect/purity/variadic metadata, two arrows that differ only in those tags would be treated as equivalent here. Worth confirming that's intentional for this prereq, or tightening later.

[briansrls]

Fixed the blocking type/value conflation in 471fd55: the direct declaration-reference path now only accepts value-level Arrow declarations (Pending, UserDefined, ExternalRealization, or Unparsed) and continues to reject NoBody arrows used for type aliases / arrow-as-data. The existing meta_tag path remains the route for data references.

Validated locally:

• cargo fmt --all --check
• RUSTC_WRAPPER= cargo test -p v3-compiler --test integration test_3a2_record_data_lowers_function_refs_and_nested_records -- --nocapture
• RUSTC_WRAPPER= cargo test -p v3-compiler --test integration test_3a2_record_data_rejects_type_alias_as_function_ref_value -- --nocapture
• RUSTC_WRAPPER= cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify

— sent from keen-lark-456

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 1ad231e1 · Trigger: schedule
• Comparison: origin/main @ 338257ef ... review/pr-1230-1ad231e1 @ 1ad231e1
• Thinking: 37s wall

---

Verdict: APPROVE — Narrowly scoped prereq. Adds (1) a fast-path in lower_structural_field_value to accept value-level arrow declarations whose arrow type matches the expected field type, (2) arrow-vs-arrow structural equivalence in declaration_ref_types_equivalent, and (3) a guard rejecting type-level arrows (aliases) being used as value refs, covered by a positive and a negative test. Findings: none against INVARIANTS.md / MODELING.md / CODING.md / TESTING.md based on the diff.

Exploratory (non-blocking): the new arrow-equivalence arm compares only inputs + output and ignores any other Arrow {..} fields (effect labels, purity, etc.) via ... If those fields ever become semantically load-bearing for ref compatibility, this branch will silently accept mismatches — worth a comment or follow-up once arrows grow more structure.

[briansrls]

Verified against current TypeConnective::Arrow: it currently carries only inputs, output, and body. The equivalence arm intentionally compares the signature fields only; value-vs-type admissibility is handled before this call by the value-level Arrow gate, which excludes NoBody aliases. If Arrow later grows effect/purity/variadic metadata, this equivalence branch should be revisited with that new field’s compatibility semantics.

— sent from keen-lark-456

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 1ad231e1 · Trigger: schedule
• Thinking: 237s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/lower.rs data structural lowering consumes callable signatures before refinement facts flow into those signatures → validate function-reference fields after refinement lowering or make the direct-reference check read the final callable/refinement facts.

⚠️ The type-alias fix is in place, but the new function-ref path still accepts a pre-refinement signature as authoritative.

[briansrls]

BLOCKING: The new direct reference branch runs during the data pre-pass against seed Arrow signatures, before lower_parameter_refinements_phase installs where-refined parameter declarations, so a refined function can be stored in an unrefined fn field without DB-11 refinement discharge.

[briansrls]

Fixed in cfb80ae. The blocking finding was valid: the data pre-pass could see a seeded function Arrow before lower_parameter_refinements_phase updated its inputs with refined declaration ids.

The direct data-field function-reference path now receives a pre-pass denylist of functions whose surface params still have pending where refinements, and fail-closes instead of treating the seeded base signature as authoritative. Added test_3a2_record_data_rejects_refined_function_ref_before_discharge to pin that shape while preserving the existing positive function-ref case and the type-alias rejection.

Validated locally:

• cargo fmt --all --check
• RUSTC_WRAPPER= cargo test -p v3-compiler --test integration test_3a2_record_data_lowers_function_refs_and_nested_records -- --nocapture
• RUSTC_WRAPPER= cargo test -p v3-compiler --test integration test_3a2_record_data_rejects_type_alias_as_function_ref_value -- --nocapture
• RUSTC_WRAPPER= cargo test -p v3-compiler --test integration test_3a2_record_data_rejects_refined_function_ref_before_discharge -- --nocapture
• RUSTC_WRAPPER= cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify

— sent from keen-lark-456

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-thinking
• Commit: e0c2b273 · Trigger: manual
• Conversation: View conversation

---

1. Story of the diff

This PR fixes a narrow lowering gap for structural data records whose fields are declared as function types. Previously, lower_structural_field_value could lower a declaration reference through the referenced declaration’s meta_tag, but it did not first accept the declaration itself when its type already matched the expected field type; the new direct equivalence check at src/v3/compiler/src/lower.rs:3405-3406 lets read: passthrough and similar function references become FieldValue::Reference. To support that, declaration_ref_types_equivalent now knows how to compare two Arrow connectives structurally by arity, input types, and output type at src/v3/compiler/src/lower.rs:3999-4017. The regression test builds a nested record with both a top-level function field and a nested function field, then asserts those lower to declaration references while the scalar identity remains a literal at src/v3/compiler/tests/integration/m2_feature_parity_test.rs:267-342.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this touches compiler lowering and an equivalence helper, not new Dag substrate shape; the Dag-facing output remains the existing FieldValue::Reference at src/v3/compiler/src/lower.rs:3406, so no new parallel substrate representation is introduced.

1. INVARIANTS.md + modeling-discipline.md.

Compliant — single authority / facts-flow-forward: the new lowering path delegates acceptance to declaration_ref_types_equivalent(dag, decl_id, expected_type, 0) at src/v3/compiler/src/lower.rs:3405 rather than adding an ad hoc “function-looking identifier” check. The Arrow comparison is structural and fail-closed: mismatched arity returns false via lhs_inputs.len() == rhs_inputs.len() at src/v3/compiler/src/lower.rs:4011, and every input/output pair must recursively match at src/v3/compiler/src/lower.rs:4012-4016.

1. CODING.md.

Compliant — the implementation extends the existing file-local free function declaration_ref_types_equivalent instead of adding methods or scattering new type-comparison logic; the helper remains data + function style at src/v3/compiler/src/lower.rs:3996-4017.

1. TESTING.md.

Compliant — the PR adds a behavior-driven regression test for the failure mode: a source program with function-typed record fields at src/v3/compiler/tests/integration/m2_feature_parity_test.rs:269-283, followed by assertions on the lowered Dag shape at src/v3/compiler/tests/integration/m2_feature_parity_test.rs:297-341. Integration level is reasonable here because the contract is source-to-Dag lowering, including nested record lowering.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not reference or alter any locked thesis/design decision; it only broadens an existing lowering equivalence case for Arrow connectives.

1. TRACKED vs UNTRACKED DEBT.

N/A — no new TODOs, temporary scaffolds, feature flags, or bridge shapes appear in the added diff lines.

3. Verdict

APPROVE — The change is small, targeted, and keeps function-reference lowering gated by the existing type-equivalence authority. The added regression test covers both the direct top-level function field and the nested-record function field, with no new substrate representation or untracked debt.