E6-G0 substitute generic Conj fields for Lens values

[briansrls]

Summary

Implements the E6-G0 first gate lens_value_generic_conj_field_substitution_lands from docs/briefs/r3-pr-e6-g0-first-gate-narrowing.md and the lens-value authoring stop receipt.

Structural data-body checking now walks instantiated generic Conj fields with the active substitution frame before validating record field values. This lets data ...: Lens<Int> validate against the live generic Lens<C> carrier and nested Monoid<C> fields as C := Int, without adding Lens<Int> / Monoid<Int> mirrors, evaluator behavior, parser field-call support, or Rust lens registries.

The resolved-reference mismatch path now emits structured Diagnostic::TypeMismatch { expected, actual } when a function/data declaration reference resolves but fails the substituted expected type. The negative fixture verifies declaration identity for actual Witness<String> versus substituted expected Witness<Int> without asserting on diagnostic message text.

Nested aggregate field lowering also carries the active LowerSubstStack through list/map values. Map<String, C> values are resolved under C := Int before recursive structural lowering.

Validation

• cargo fmt --all --check
• cargo test -p v3-compiler --test integration test_3a2_ -- --nocapture
• cargo test -p v3-compiler --test integration prereq_x_call_on_field_access_ratchet_test -- --nocapture
• cargo test -p v3-compiler lower::tests::structural_map_field_lowers_values_with_active_substitution -- --nocapture

Scope Notes

• Lens<C>, Monoid<C>, Witness<C>, OptionalDiagnostic, and DimensionReport<C> carrier shapes are unchanged.
• Existing Prereq-X call-on-field-access ratchets remain unchanged and passing as blockers.
• No evaluator, parser, field-call lowering, fold_lens, or fold_lens_over_reflected_program changes are included.

[briansrls]

Verified against current branch state. This review is an approval/no-change item; no code change is required for it. The branch is now at 009d033 after merging origin/main, and the current CI run is in progress.

— sent from crisp-ibex-569

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 009d0331 · Trigger: schedule
• Comparison: origin/main @ 822b6e0d ... review/pr-1640-009d0331 @ 009d0331
• Thinking: 87s wall

---

Verdict: APPROVE

Diff is narrowly scoped to lower-time substitution for generic structural data fields and matching regression coverage. I don’t see a concrete violation of the pinned invariants, coding guidance, or test discipline in the changed lines. I did not run builds or tests, per instruction.

[briansrls]

Verified against current head 009d033. This is an approval/no-change review item, so no code change is needed. Current checks: fmt is green; ci and v3 are still in progress.

— sent from crisp-ibex-569

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 009d0331 · Trigger: schedule
• Thinking: 253s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/lower.rs aggregate field kind detection remains split between substitution-blind shape predicates and substitution-aware recursive value lowering → make list/map/disj shape discovery consume the active LowerSubstStack before deciding support.

⚠️ One generic aggregate path still drops an active substitution fact before structural field lowering gets to use it.

[briansrls]

Invariant violation: BLOCKING: Passing subst only into lower_string_map_entries is too late for Map<K,V> fields because map_value_type/map_key_type_is_not_string have already made a substitution-blind key decision, so Generic<K,V> instantiated with K := String still drops that boundary fact (Facts Flow Forward).

[briansrls]

Verified the aggregate shape-discovery blocker against current code and pushed a fix. Current head is dec5e9c.

Fix: list/map/disj structural field kind discovery now consumes the active LowerSubstStack before deciding support. Added regression coverage for generic record fields where T := List and T := Maybe, so the shape decision itself depends on the substituted type, not the raw TypeParam.

Validation run:

• cargo fmt --all --check
• cargo test -p v3-compiler --test integration test_3a2_record_data_discovers -- --nocapture
• cargo test -p v3-compiler --test integration test_3a2_ -- --nocapture
• cargo test -p v3-compiler --test integration idempotency_lens_instance_blocker_test -- --nocapture
• cargo test -p v3-compiler --test integration prereq_x_call_on_field_access_ratchet_test -- --nocapture

— sent from crisp-ibex-569

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: dec5e9c1 · Trigger: schedule
• Comparison: origin/main @ 822b6e0d ... review/pr-1640-dec5e9c1 @ dec5e9c1
• Thinking: 47s wall

---

Findings

None. Nothing in the diff clearly violates INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md. This is compiler-internal lowering (lower.rs), not new substrate on the DAG; the change threads an explicit substitution stack through structural lowering, adds typed TypeMismatch paths instead of silent acceptance where declaration refs disagree with substituted expectations, and replaces the old idempotency “blocker” test’s string/span substring diagnostic probing with compile success + FieldValue structure assertions — aligned with fail-closed / typed-carrier discipline (contrast C-5 per rubric).

Verdict

APPROVE — Scoped generic substitution for structural record/list/map/sum lowering, with regression coverage (unit + integration) and cleaner tests. No rubric-grounded blocking issues spotted in the diff.

Exploratory observations (optional)

• Depth caps (32) that return current / false / None without an explicit diagnostic are a long-standing lowering pattern; only worth tightening if pathological nesting should be a first-class error (P3 angle), not specific regression evidence here.
• In the sum (Disj) arm, nested lower_structural_field_value calls pass the outer subst while payload types come from variant_payload_fields_for_lowering_with_subst(..., &disj_subst); given the new substitution tests, this likely matches intent, but it is the subtlest wiring if a future bug appears around partially resolved payload types.

[briansrls]

Addressed the latest blocking Map<K,V> substitution review in head 3a2ea5b.

What changed:

• map_value_type_with_subst now handles Map<K,V> directly, resolving the key under the active LowerSubstStack before deciding string-key support and resolving the value under the same substitution.
• map_key_type_is_not_string_with_subst now makes the same substitution-aware key decision instead of falling back to the substitution-blind helper.
• The focused lower unit test now covers both Map<String, C> with C := Int and Map<K, V> with K := String, V := Int.

Validation:

• cargo fmt --all --check
• cargo test -p v3-compiler lower::tests::structural_map_field_lowers_values_with_active_substitution -- --nocapture
• cargo test -p v3-compiler --test integration test_3a2_ -- --nocapture
• cargo test -p v3-compiler --test integration prereq_x_call_on_field_access_ratchet_test -- --nocapture

— sent from crisp-ibex-569