diff --git a/src/v3/compiler/src/dag.rs b/src/v3/compiler/src/dag.rs index 64205a3f3be..9b35cb9919f 100644 --- a/src/v3/compiler/src/dag.rs +++ b/src/v3/compiler/src/dag.rs @@ -1653,6 +1653,10 @@ fn classify_call_argument( return relation; } + if let Some(relation) = match_payload_field_projection_descent_relation(dag, param, arg) { + return relation; + } + SubValueRelation::SubValueUnknown } @@ -1729,6 +1733,85 @@ fn match_payload_descent_relation( None } +/// Phase-1 broadening Slice 2: classify recursive-call arguments produced by +/// a single `FieldProject` transform whose input is the payload port of a +/// match arm whose scrutinee is the parameter directly. This is the +/// record-payload sibling of [`match_payload_descent_relation`]'s +/// positional-payload case. +/// +/// Surface shape: +/// +/// ```ignore +/// type EpRec = EpLeaf | EpNode { left: EpRec } +/// fn ep_depth(t: EpRec) -> Int = +/// match t { EpNode { left: l } => ep_depth(l), EpLeaf => 0 } +/// ``` +/// +/// `lower.rs` lowers `EpNode { left: l }` by allocating a payload binding +/// and synthesizing a `FieldProject { field_label: "left", .. }` transform +/// whose input is the payload port (see `lower_field_projection_from_port`). +/// The recursive call's argument is therefore the projection's output port, +/// not the payload port itself — Slice 1's direct-equality check misses it. +/// +/// Same fail-closed discipline + structural-fact derivation as Slice 1. +/// `field_name` here is the `FieldProject.field_label` — already structural, +/// established by the lowering, NOT a user-pattern-binding name. The label +/// must also appear in the variant's `Conj` children (validation; if not, the +/// projection isn't on this variant's payload). Cross-slice invariants +/// preserved: no new `CallPattern` variant, no `TransformNode` widening, +/// fail-closed discipline. +fn match_payload_field_projection_descent_relation( + dag: &Dag, + param: PortId, + arg: PortId, +) -> Option { + let Behavior::Transform(transform) = dag.resolve_producer_opt(&arg)? else { + return None; + }; + let TransformTarget::FieldProject { field_label, .. } = &transform.target else { + return None; + }; + if transform.inputs.len() != 1 { + return None; + } + let projected_input = transform.inputs[0]; + + for branch in dag.nodes().iter().filter_map(Behavior::as_branch) { + if branch.input != param { + continue; + } + for path in &branch.paths { + let Some(binding) = &path.binding else { + continue; + }; + if binding.payload_port != projected_input { + continue; + } + let facts = variant_structural_facts(dag, &path.pattern)?; + // Validate the projection's structural label appears in the + // resolved variant's Conj field set; otherwise this isn't a + // descent on the variant payload. + let payload_ty = facts + .payload_fields + .iter() + .find(|(label, _)| label == field_label) + .map(|(_, ty)| *ty)?; + let element_type = named_type_name(dag, payload_ty)?; + return Some(SubValueRelation::StrictSubValue { + field: InductiveField { + type_name: facts.type_name, + variant_name: facts.variant_name, + field_name: field_label.clone(), + shape: RecursionShape::DirectRecursion, + element_type, + }, + factor: ShrinkFactor::UnitShrink, + }); + } + } + None +} + /// Authoritative variant-structural facts derived from a resolved variant /// declaration. Returns `None` for `UnresolvedVariant` and for `ResolvedVariant` /// whose parent `Disj` cannot be located by scanning declarations — same diff --git a/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs b/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs index 385512980b4..eb808fb208c 100644 --- a/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs +++ b/src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs @@ -614,6 +614,64 @@ fn ep_count(xs: EpList) -> Int = } } +#[test] +fn e_p_per_call_descent_evidence_classifies_match_field_projection_self_call_as_strict_sub_value() { + // Phase-1 broadening Slice 2 — record-payload sibling of Slice 1. + // For `match t { EpNode { left: l } => ep_depth(l) }`, `lower.rs` + // synthesizes a FieldProject transform between the payload port and the + // user-scope name `l`, so the recursive arg is one indirection beyond the + // payload port that Slice 1's direct-equality check catches. + // + // Same structural-fact discipline as Slice 1: field_name is the + // FieldProject.field_label (the lowered Conj field label, NOT the user's + // `l` binding name), and type_name/variant_name come from the parent-Disj + // lookup of the resolved variant declaration. + let dag = compile_to_dag( + "\ +type EpRec = EpLeaf | EpNode { left: EpRec } +fn ep_depth(t: EpRec) -> Int = + match t { EpNode { left: l } => ep_depth(l), EpLeaf => 0 } +", + "e_p_match_field_projection.v3", + ) + .expect("recursive record-payload fixture compiles"); + + let entries = per_call_descent_evidence(&dag); + let depth = entries + .iter() + .find(|entry| entry.caller == "ep_depth" && entry.callee == "ep_depth") + .expect("expected ep_depth self-call evidence in per-call side table"); + + assert_eq!(depth.evidence.len(), 1); + match &depth.evidence[0] { + SubValueRelation::StrictSubValue { field, factor } => { + assert_eq!( + field.field_name, "left", + "FieldProject.field_label is the variant Conj's structural field name" + ); + assert_eq!( + field.variant_name, "EpNode", + "variant_name comes from the parent Disj's variant label" + ); + assert_eq!( + field.type_name, "EpRec", + "type_name is the parent Disj declaration name" + ); + assert_eq!( + field.element_type, "EpRec", + "element_type is the resolved name of the projected field's type" + ); + assert_eq!( + factor, + &ShrinkFactor::UnitShrink, + "record-payload field-projection descent is a unit-shrink: \ + one constructor + one field peeled" + ); + } + other => panic!("expected StrictSubValue for ep_depth(l), got {other:?}"), + } +} + #[test] fn e_p_per_call_descent_evidence_fails_closed_for_non_self_call() { let dag = compile_to_dag(