Enable strict record-field typecheck: close fail-open infer_record_lit hole (§5)

dsl/shared/dag_util.dag

@@ -15,10 +15,10 @@ import std.types {
   Document,
   DocumentLine,
   DocumentSection,
+  DocumentFile,
   RenderedTextFile,
   StageResult,
   Summary,
-  TextFile,
   TextFilePath
 }
 // --- Result aggregation -----------------------------------------------
@@ -73,7 +73,7 @@ fn generated_header(tool: String) -> String {
 }
 
 // --- Structured document rendering -------------------------------------
-// Shared "rendering engine" for Document/TextFile trees.
+// Shared "rendering engine" for Document/DocumentFile trees.
 
 fn text_line(text: String) -> DocumentLine {
   { text: text, is_comment: false, is_blank: false }

dsl/std/types.dag

@@ -547,7 +547,7 @@ type Document {
   trailing_newline: Bool
 }
 
-type TextFile {
+type DocumentFile {
   path: String
   document: Document
 }

src/v1/04_infer.dag

@@ -2841,6 +2841,59 @@ fn record_lit_alias_struct_fields(type_name: String, scope: InferScope) -> List<
   }
 }
 
+// Strict record construction (§5 fail-closed): the SOURCE field-name set of the concrete
+// record a construction targets, or `none` whenever we cannot enumerate it with confidence —
+// so the undefined-field check stays silent rather than false-positive. We fire ONLY when the
+// constructed name resolves to a plain, fully-grounded record: non-generic (`params == 0`) and
+// a direct product (`connective == Conj`) with declared fields. Everything else returns `none`:
+//   - generics (`Monoid<T>`, `Vendor<Domain>`): newtype flattening rewrites a single-field
+//     wrapper to its innermost name (`Monoid` resolves to `[op, identity]`, not `[semigroup,
+//     identity]`), so the resolved set is not source-faithful;
+//   - concrete aliases of single-field generics (`Watt = Measure<Power, One, Nat>`): the wrapper
+//     dissolves to its `<M>` carrier, so the resolved node is not a record at all;
+//   - a name resolving to a coproduct/enum — including the losing side of a §3 name collision
+//     (the `Vendor` enum shadowing the `Vendor<Domain>` record): no product fields to check.
+// This keeps full teeth on plain records, where every real bug it finds lives (`BoolWitness
+// { holds }`, `NodeLocus { node }`, `PortLocus { port }`). Dissolution trigger: when field-name
+// resolution is source-faithful under flattening, widen the gate to generics and aliases.
+fn record_lit_construction_field_names(type_name: String, scope: InferScope) -> List<String>? {
+  let si = scope.type_env.source_indices
+  match lookup_type_by_name(env: scope.type_env, name: type_name) {
+    Present { value: decl } =>
+      if (decl.params |> count == 0) && (decl.connective == Conj) && (decl.children |> count > 0) {
+        Present { value: decl.children |> map(f => authored_name_at(source_indices: si, node: f)) }
+      } else {
+        none
+      }
+    Absent => none
+  }
+}
+
+// Strict record construction: a constructed NAME can legitimately arm two distinct coproducts
+// with different field sets (e.g. `TextNode` is `Fragment.TextNode { content }` in one and
+// `MarkupNode.TextNode { text }` in another). The import-scoped `struct_fields`/`arm_fields`
+// only see the arm reachable from `expected`; this secondary scan, run ONLY on a would-be
+// error, asks whether `field` is valid on a same-named arm of ANY coproduct in the env — so
+// `TextNode { text }` stays silent when *some* `TextNode` arm has `text`, while a field present
+// on NO same-named arm keeps its loud error (§5). Record-name collisions are NOT handled here:
+// duplicate record names across layers are a §3 violation that must be de-conflicted at the
+// source (cf. the `TextFile` → `DocumentFile` split), not papered over by a suppressor.
+fn field_in_any_variant_named(type_name: String, field: String, scope: InferScope) -> Bool {
+  let si = scope.type_env.source_indices
+  scope.type_env.bindings |> map_values |> any(binding =>
+    let node = binding.resolved
+    if (node.connective == Disj) {
+      node.children |> any(arm =>
+        if authored_name_at(source_indices: si, node: arm) == type_name {
+          let ea = expand_type_for_field_access(n: arm, env: scope.type_env, module_name: scope.module_name)
+          let fields = if (ea.connective == Conj) { ea.children } else { arm.children }
+          fields |> any(f => authored_name_at(source_indices: si, node: f) == field)
+        } else { false }
+      )
+    } else { false }
+  )
+}
+
 fn infer_record_lit(type_name: String?, field_inits: List<Node>, span: SourceSpan, name_span: SourceSpan, scope: InferScope, expected: Node?) -> InferResult {
   let struct_fields = match type_name {
     Present { value: tn } =>
@@ -2870,8 +2923,29 @@ fn infer_record_lit(type_name: String?, field_inits: List<Node>, span: SourceSpa
           }
       }
   }
+  let construction_field_names = match type_name {
+    Present { value: tn } => record_lit_construction_field_names(type_name: tn, scope: scope)
+    Absent => none
+  }
+  let tn_str = match type_name {
+    Present { value: tn } => tn
+    Absent => ""
+  }
   let fi_infer_results = map(field_inits, fi =>
     let fi_name = field_init_node_name_at(n: fi, source_indices: scope.type_env.source_indices)
+    // Strict record construction (§5 fail-closed): a field that matches no field of a
+    // confidently-RESOLVED type is a loud, located error, not silently ignored. `none`
+    // (unresolved / generic / anonymous record) keeps the path silent — closes the
+    // fail-open `infer_record_lit` hole without false-positives.
+    let unknown_field_diags = match construction_field_names {
+      Present { value: names } =>
+        if (names |> any(n => n == fi_name)) || field_in_any_variant_named(type_name: tn_str, field: fi_name, scope: scope) {
+          []
+        } else {
+          [make_error_node(diagnostic: FieldNotFound { field: fi_name, type_name: tn_str, span: fi.span }, module_name: scope.module_name)]
+        }
+      Absent => []
+    }
     let field_expected = match struct_fields |> filter(sf => authored_name_at(source_indices: scope.type_env.source_indices, node: sf) == fi_name) |> first {
       Present { value: sf } =>
         let ft = match sf.inferred {
@@ -2908,7 +2982,7 @@ fn infer_record_lit(type_name: String?, field_inits: List<Node>, span: SourceSpa
     FieldInferResult {
       typed_field: make_field_init_node(name: fi_name, value: ar_typed, span: fi.span, name_span: node_name_span(n: fi)),
       infer_result: ar,
-      diagnostics: concat(ar_diags, field_type_diags)
+      diagnostics: concat(concat(ar_diags, field_type_diags), unknown_field_diags)
     }
   )
   let typed_fields = fi_infer_results |> map(fir => fir.typed_field)

src/v1/stage0/src/v1_compiler_infer.rs

@@ -5465,6 +5465,100 @@ pub fn record_lit_alias_struct_fields(
     }
 }
 
+pub fn record_lit_construction_field_names(
+    type_name: String,
+    scope: Rc<InferScope>,
+) -> Option<Rc<Vec<String>>> {
+    {
+        let si = scope.type_env.clone().source_indices.clone();
+        match lookup_type_by_name(scope.type_env.clone(), type_name) {
+            Some(decl) => {
+                if ((((decl.params.clone().len() as i64) == 0)
+                    && (decl.connective.clone() == Connective::Conj))
+                    && ((decl.children.clone().len() as i64) > 0))
+                {
+                    Some(Rc::new({
+                        let mut __result = Vec::new();
+                        for f in decl.children.clone().iter().cloned() {
+                            __result.push(authored_name_at(si.clone(), f.clone()));
+                        }
+                        __result
+                    }))
+                } else {
+                    None
+                }
+            }
+            None => None,
+        }
+    }
+}
+
+pub fn field_in_any_variant_named(type_name: String, field: String, scope: Rc<InferScope>) -> bool {
+    {
+        let si = scope.type_env.clone().source_indices.clone();
+        {
+            let mut __found = false;
+            for binding in Rc::new(v1_rt::map_values(&scope.type_env.clone().bindings.clone()))
+                .iter()
+                .cloned()
+            {
+                if {
+                    let node = binding.resolved.clone();
+                    if (node.connective.clone() == Connective::Disj) {
+                        {
+                            let mut __found = false;
+                            for arm in node.children.clone().iter().cloned() {
+                                if if (authored_name_at(si.clone(), arm.clone()).as_str()
+                                    == type_name.clone().as_str())
+                                {
+                                    {
+                                        let ea = expand_type_for_field_access(
+                                            arm.clone(),
+                                            scope.type_env.clone(),
+                                            scope.module_name.clone(),
+                                        );
+                                        let fields = if (ea.connective.clone() == Connective::Conj)
+                                        {
+                                            ea.children.clone()
+                                        } else {
+                                            arm.children.clone()
+                                        };
+                                        {
+                                            let mut __found = false;
+                                            for f in fields.clone().iter().cloned() {
+                                                if (authored_name_at(si.clone(), f.clone())
+                                                    .as_str()
+                                                    == field.clone().as_str())
+                                                {
+                                                    __found = true;
+                                                    break;
+                                                }
+                                            }
+                                            __found
+                                        }
+                                    }
+                                } else {
+                                    false
+                                } {
+                                    __found = true;
+                                    break;
+                                }
+                            }
+                            __found
+                        }
+                    } else {
+                        false
+                    }
+                } {
+                    __found = true;
+                    break;
+                }
+            }
+            __found
+        }
+    }
+}
+
 pub fn infer_record_lit(
     type_name: Option<String>,
     field_inits: Rc<Vec<Rc<Node>>>,
@@ -5512,6 +5606,14 @@ pub fn infer_record_lit(
                 },
             },
         };
+        let construction_field_names = match type_name.clone() {
+            Some(tn) => record_lit_construction_field_names(tn.clone(), scope.clone()),
+            None => None,
+        };
+        let tn_str = match type_name.clone() {
+            Some(tn) => tn.clone(),
+            None => "".to_string(),
+        };
         let fi_infer_results = Rc::new({
             let mut __result = Vec::new();
             for fi in field_inits.iter().cloned() {
@@ -5520,6 +5622,36 @@ pub fn infer_record_lit(
                         fi.clone(),
                         scope.type_env.clone().source_indices.clone(),
                     );
+                    let unknown_field_diags = match construction_field_names.clone() {
+                        Some(names) => {
+                            if ({
+                                let mut __found = false;
+                                for n in names.clone().iter().cloned() {
+                                    if (n.clone().as_str() == fi_name.clone().as_str()) {
+                                        __found = true;
+                                        break;
+                                    }
+                                }
+                                __found
+                            } || field_in_any_variant_named(
+                                tn_str.clone(),
+                                fi_name.clone(),
+                                scope.clone(),
+                            )) {
+                                Rc::new(vec![])
+                            } else {
+                                Rc::new(vec![make_error_node(
+                                    Rc::new(CompilerDiagnostic::FieldNotFound {
+                                        field: fi_name.clone(),
+                                        type_name: tn_str.clone(),
+                                        span: fi.span.clone(),
+                                    }),
+                                    scope.module_name.clone(),
+                                )])
+                            }
+                        }
+                        None => Rc::new(vec![]),
+                    };
                     let field_expected = match Rc::new({
                         let mut __result = Vec::new();
                         for sf in struct_fields.clone().iter().cloned() {
@@ -5594,7 +5726,10 @@ pub fn infer_record_lit(
                             node_name_span(fi.clone()),
                         ),
                         infer_result: ar.clone(),
-                        diagnostics: v1_rt::concat(ar_diags.clone(), field_type_diags.clone()),
+                        diagnostics: v1_rt::concat(
+                            v1_rt::concat(ar_diags.clone(), field_type_diags.clone()),
+                            unknown_field_diags.clone(),
+                        ),
                     })
                 });
             }

src/v2/compiler/manual/infer_ground_add_mvp.dag

@@ -124,7 +124,7 @@ fn infer_receipt_runtime_value() -> RuntimeValue {
 fn infer_receipt_runtime_diagnostic(n: Node) -> Diagnostic {
   Diagnostic {
     reason: ^infer_receipt_extdeps,
-    at: NodeLocus { node: n },
+    at: node_locus(node: n),
     correction: Unavailable { reason: AmbiguousIntent }
   }
 }

src/v2/extdeps/formats/spice_passive_projection_test.dag

@@ -22,16 +22,6 @@ import v2.std.timeseries_signal {
   InductorPassive,
   ResistorPassive,
 }
-import v2.std.verification {
-  BoolWitness,
-  BoolWitnessClaim,
-  ManualAnchorAbsent,
-  TestClaim,
-  TestClassification,
-  Tier1,
-  Unit,
-  manual_claim_anchor
-}
 
 test fn spice_resistor_projects_resistor_passive_topology_holds() -> Bool {
   let component = Resistor {
@@ -84,31 +74,3 @@ test fn passive_topology_preserves_component_name_holds() -> Bool {
     Absent => false
   }
 }
-
-data claim_spice_resistor_passive_spec: TestClaim = BoolWitnessClaim {
-  label: "extdeps/formats/spice_passive_projection: spice Resistor projects ResistorPassive topology",
-  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
-  witness: BoolWitness { holds: spice_resistor_projects_resistor_passive_topology_holds() },
-  classification: TestClassification { tier: Tier1, layer: Unit }
-}
-
-data claim_spice_capacitor_passive_arm: TestClaim = BoolWitnessClaim {
-  label: "extdeps/formats/spice_passive_projection: spice Capacitor projects CapacitorPassive arm",
-  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
-  witness: BoolWitness { holds: spice_capacitor_projects_capacitor_passive_arm_holds() },
-  classification: TestClassification { tier: Tier1, layer: Unit }
-}
-
-data claim_spice_inductor_passive_arm: TestClaim = BoolWitnessClaim {
-  label: "extdeps/formats/spice_passive_projection: spice Inductor projects InductorPassive arm",
-  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
-  witness: BoolWitness { holds: spice_inductor_projects_inductor_passive_arm_holds() },
-  classification: TestClassification { tier: Tier1, layer: Unit }
-}
-
-data claim_passive_topology_preserves_name: TestClaim = BoolWitnessClaim {
-  label: "extdeps/formats/spice_passive_projection: passive_topology_from_component preserves name",
-  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
-  witness: BoolWitness { holds: passive_topology_preserves_component_name_holds() },
-  classification: TestClassification { tier: Tier1, layer: Unit }
-}

src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag

@@ -10,7 +10,7 @@ import v2.compiler.compile {
   compile_lens_gate_rejected_diagnostic
 }
 import v2.compiler.infer { InferredTree }
-import v2.std.diagnostic { Accepted, Diagnostics, None, Outcome, PortLocus, Rejected, Some, outcome_rejected }
+import v2.std.diagnostic { Accepted, Diagnostics, None, Outcome, Rejected, Some, outcome_rejected, port_locus }
 import v2.std.logic { Bool }
 import v2.std.node { Atom, Conj, Node, Symbol, TypeNode, SyntheticOccurrence }
 import v2.std.verification {
@@ -43,7 +43,7 @@ fn apply_lens_mode_tree() -> InferredTree {
 
 fn apply_lens_mode_rejecting_gate(_tree: InferredTree) -> Outcome<Witness<Node>> {
   outcome_rejected(
-    compile_lens_gate_rejected_diagnostic(at: PortLocus { port: ^apply_lens_mode_gate_at })
+    compile_lens_gate_rejected_diagnostic(at: port_locus(port: ^apply_lens_mode_gate_at))
   )
 }
 

src/v2/lens/application/enforce_rejecting_gate_fires.dag

@@ -8,7 +8,7 @@ import v2.compiler.compile {
   compile_lens_gate_rejected_diagnostic
 }
 import v2.compiler.infer { InferredTree }
-import v2.std.diagnostic { Accepted, Outcome, PortLocus, Rejected, outcome_rejected }
+import v2.std.diagnostic { Accepted, Outcome, Rejected, outcome_rejected, port_locus }
 import v2.std.logic { Bool }
 import v2.std.node { Atom, Conj, Node, Symbol, TypeNode, SyntheticOccurrence }
 import v2.std.verification {
@@ -41,7 +41,7 @@ fn enforce_reject_tree() -> InferredTree {
 
 fn enforce_rejecting_gate(_tree: InferredTree) -> Outcome<Witness<Node>> {
   outcome_rejected(
-    compile_lens_gate_rejected_diagnostic(at: PortLocus { port: ^enforce_reject_gate_at })
+    compile_lens_gate_rejected_diagnostic(at: port_locus(port: ^enforce_reject_gate_at))
   )
 }