From 2d14830f67858b9f3e94c7e4d5da13d7718c4c66 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 13:58:08 +0000 Subject: [PATCH 1/5] Delete malformed dead {holds} BoolWitness rows; re-home 5 dark signal predicates as test fn MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 13 `data claim_*: TestClaim = BoolWitnessClaim { witness: BoolWitness { holds: f() } }` rows (timeseries_passive_map_fold_anchor_test ×7, timeseries_signal_passives_test ×6) are triple-malformed dead spec that compiled only because the v1-seed record typechecker is fail-open (`infer_record_lit` silently ignores undefined fields and never validates missing required ones): - `holds` is not a field on `BoolWitness` (which has only `entry`, `function`); - they are typed `: TestClaim`, but `BoolWitnessClaim` is an arm of `UnifiedTestClaim`, not of `TestClaim` (whose arms are Compiles/Diagnostic/Equals/StructuralEquals/RoundTrip); - wrong inner shape. The live floor discovers only `data unified_claim_*` (never `data claim_*`), so these never ran — pure dead specification, and a §3 fork of the canonical `{ entry, function }` form ratified by consolidation #4553. Asymmetry handled per §5 (do not silently drop coverage): - anchor file: its 7 predicates were already live `test fn` (#5257) — pure deletion. - signal file: only 1 of its 6 predicates was a live `test fn`; the other 5 (spice_capacitor/inductor_projects_*, passive_topology_preserves_component_name, named_affine_voltage_preserves_ground_reference, absolute_potential_from_named_preserves_reference) were plain `fn` wired ONLY through the dead `{holds}` rows — re-homed as `test fn` to RESTORE their intended floor coverage rather than orphan the assertions. Drop the now-unused `BoolWitness`/`BoolWitnessClaim` imports from both files. Green by execution: `claim_batch --source-root src/v2` over all 13 witnesses → 13 PASS, including the 5 newly-live signal predicates. Their assertions discriminate on Present/Absent (not tautological), so floor coverage is strictly increased, not faked. Co-Authored-By: Claude Opus 4.8 --- ...imeseries_passive_map_fold_anchor_test.dag | 51 ------------------ .../std/timeseries_signal_passives_test.dag | 54 ++----------------- 2 files changed, 5 insertions(+), 100 deletions(-) diff --git a/src/v2/compiler/manual/timeseries_passive_map_fold_anchor_test.dag b/src/v2/compiler/manual/timeseries_passive_map_fold_anchor_test.dag index 3efb85a8f39..9c95442c181 100644 --- a/src/v2/compiler/manual/timeseries_passive_map_fold_anchor_test.dag +++ b/src/v2/compiler/manual/timeseries_passive_map_fold_anchor_test.dag @@ -44,8 +44,6 @@ import v2.std.timeseries_signal { voltage_count, } import v2.std.verification { - BoolWitness, - BoolWitnessClaim, CompilesClaim, ManualAnchorAbsent, TestClaim, @@ -216,55 +214,6 @@ test fn timeseries_anchor_inductor_fold_holds() -> Bool { } } -data claim_timeseries_resistor_map: TestClaim = BoolWitnessClaim { - label: "manual/timeseries_passive_map_fold_anchor: resistor map v=R·i", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: timeseries_anchor_resistor_map_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_timeseries_signed_magnitude_resistor_map: TestClaim = BoolWitnessClaim { - label: "manual/timeseries_passive_map_fold_anchor: signed negative current map v=R·i", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: timeseries_signed_magnitude_resistor_map_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_timeseries_signed_magnitude_capacitor_fold: TestClaim = BoolWitnessClaim { - label: "manual/timeseries_passive_map_fold_anchor: signed negative current Form-B capacitor fold", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: timeseries_signed_magnitude_capacitor_fold_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_timeseries_capacitor_fold: TestClaim = BoolWitnessClaim { - label: "manual/timeseries_passive_map_fold_anchor: capacitor fold step", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: timeseries_anchor_capacitor_fold_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_timeseries_capacitor_fold_chronological: TestClaim = BoolWitnessClaim { - label: "manual/timeseries_passive_map_fold_anchor: capacitor fold chronological", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: timeseries_anchor_capacitor_fold_chronological_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_timeseries_capacitor_zero_rejects: TestClaim = BoolWitnessClaim { - label: "manual/timeseries_passive_map_fold_anchor: capacitor zero rating rejects", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: timeseries_anchor_capacitor_zero_rating_rejects() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_timeseries_inductor_fold: TestClaim = BoolWitnessClaim { - label: "manual/timeseries_passive_map_fold_anchor: inductor fold step", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: timeseries_anchor_inductor_fold_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - data claim_timeseries_passive_map_fold_compiles: TestClaim = CompilesClaim { label: "manual/timeseries_passive_map_fold_anchor: S1 map/fold passives compile", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), diff --git a/src/v2/std/timeseries_signal_passives_test.dag b/src/v2/std/timeseries_signal_passives_test.dag index 7aa40db8a4c..1184e2000ef 100644 --- a/src/v2/std/timeseries_signal_passives_test.dag +++ b/src/v2/std/timeseries_signal_passives_test.dag @@ -36,8 +36,6 @@ import v2.extdeps.formats.spice { SpiceValue } import v2.std.verification { - BoolWitness, - BoolWitnessClaim, CompilesClaim, ManualAnchorAbsent, StructuralEqualsClaim, @@ -65,7 +63,7 @@ test fn spice_resistor_projects_resistor_passive_topology_holds() -> Bool { } } -fn spice_capacitor_projects_capacitor_passive_arm_holds() -> Bool { +test fn spice_capacitor_projects_capacitor_passive_arm_holds() -> Bool { let component = Capacitor { name: ^c1, n_plus: Named { node: NamedNode { name: ^n2 } }, @@ -78,7 +76,7 @@ fn spice_capacitor_projects_capacitor_passive_arm_holds() -> Bool { } } -fn spice_inductor_projects_inductor_passive_arm_holds() -> Bool { +test fn spice_inductor_projects_inductor_passive_arm_holds() -> Bool { let component = Inductor { name: ^l1, n_plus: Named { node: NamedNode { name: ^n3 } }, @@ -91,7 +89,7 @@ fn spice_inductor_projects_inductor_passive_arm_holds() -> Bool { } } -fn passive_topology_preserves_component_name_holds() -> Bool { +test fn passive_topology_preserves_component_name_holds() -> Bool { let component = Resistor { name: ^r9, n_plus: Named { node: NamedNode { name: ^n9 } }, @@ -104,7 +102,7 @@ fn passive_topology_preserves_component_name_holds() -> Bool { } } -fn named_affine_voltage_preserves_ground_reference_holds() -> Bool { +test fn named_affine_voltage_preserves_ground_reference_holds() -> Bool { let named = named_affine_voltage( reference: GroundReference, approx: timeseries_witness_spice_approx_zero @@ -115,7 +113,7 @@ fn named_affine_voltage_preserves_ground_reference_holds() -> Bool { ) } -fn absolute_potential_from_named_preserves_reference_holds() -> Bool { +test fn absolute_potential_from_named_preserves_reference_holds() -> Bool { let named = named_affine_voltage( reference: GroundReference, approx: timeseries_witness_spice_approx_zero @@ -126,48 +124,6 @@ fn absolute_potential_from_named_preserves_reference_holds() -> Bool { ) } -data claim_spice_resistor_passive_spec: TestClaim = BoolWitnessClaim { - label: "std/timeseries_signal: 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: "std/timeseries_signal: 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: "std/timeseries_signal: 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: "std/timeseries_signal: 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 } -} - -data claim_named_affine_voltage_preserves_reference: TestClaim = BoolWitnessClaim { - label: "std/timeseries_signal: named_affine_voltage preserves GroundReference", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: named_affine_voltage_preserves_ground_reference_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_absolute_potential_preserves_reference: TestClaim = BoolWitnessClaim { - label: "std/timeseries_signal: absolute_potential_from_named preserves reference", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: absolute_potential_from_named_preserves_reference_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - data claim_potential_difference_of_magnitude_structural: TestClaim = StructuralEqualsClaim { label: "std/timeseries_signal: potential_difference_of_magnitude is structural identity", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), From 89f90f40c29f4b5eb3a73f16bb6ab65f325bf18a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 15:53:57 +0000 Subject: [PATCH 2/5] Enable strict record-field typecheck: close fail-open infer_record_lit hole MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The v1-seed typechecker (infer_record_lit) was fail-OPEN on record construction — it silently ignored fields that exist on no variant of the constructed type (DESIGN.md §5: "a wrong answer is a loud error, never a warning"). That hole is what let the malformed `BoolWitness { holds }` rows typecheck green (see #5272). Closing it. Host change (src/v1/stage0/src/v1_compiler_infer.rs): - record_lit_construction_field_names: a *confident* field-name resolver that follows `type X = Y` aliases and searches the expected coproduct's arms before the global fallback (the two resolver-precision gaps the leniency was compensating for: `Set = PointwisePower` alias; variant-vs-collection name collisions like `GrammarExpr.Optional`). Returns None when not confident so anonymous/unresolved records never false-positive. - field_in_any_variant_named: an ambiguity-aware secondary scan, run only on would-be-errors, that suppresses false positives where a field is valid on a same-named variant of *another* coproduct (e.g. TextNode) while keeping teeth on truly-undefined fields. - emit CompilerDiagnostic::FieldNotFound for an unknown constructed field. Real bugs this surfaced (silently tolerated before; field name was wrong): - infer_ground_add_mvp.dag: `NodeLocus { node }` → `node_locus(node:)` (the field is `anchor`). - 3 lens/application tests: `PortLocus { port }` → `port_locus(port:)` (the field is `anchor`). Proven by execution: full claim_batch floor green (439 witnesses) with the check live; probe `BoolWitness { holds }` goes red with "field 'holds' not found in type 'BoolWitness'". Missing-required-field enforcement deferred (optional-cardinality + templating risk, unmeasured). Co-Authored-By: Claude Opus 4.8 --- src/v1/stage0/src/v1_compiler_infer.rs | 200 +++++++++++++++++- .../compiler/manual/infer_ground_add_mvp.dag | 2 +- ..._lens_introspect_rejection_is_advisory.dag | 4 +- .../enforce_rejecting_gate_fires.dag | 4 +- .../rejecting_lens_blocks_before_compile.dag | 4 +- 5 files changed, 203 insertions(+), 11 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 88f94cf7a6a..952d1c9bc5d 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -5465,6 +5465,153 @@ pub fn record_lit_alias_struct_fields( } } +// Strict record construction (§5 fail-closed): resolve the field-name set of the CONCRETE +// record a construction targets, returning `None` whenever resolution is not confident — so +// the undefined-field check stays silent rather than false-positive. Two precision rules the +// fail-open path elided: (1) a variant constructed against an expected COPRODUCT resolves to +// that arm's fields (disambiguates a constructed name that also names a top-level type, e.g. +// `GrammarExpr.Optional` vs the collection `Optional`); (2) a type ALIAS +// (`type Set = PointwisePower`) is followed to its target record. Only a Conj record +// with fields yields `Some`. +pub fn record_lit_construction_field_names( + type_name: String, + expected: Option>, + scope: Rc, +) -> Option>> { + let si = scope.type_env.clone().source_indices.clone(); + let arm_from_expected: Option> = match expected.clone() { + Some(exp) => { + let exp_resolved = resolved_type(exp.clone()); + if (exp_resolved.connective.clone() == Connective::Disj) { + { + let mut found: Option> = None; + for arm in exp_resolved.children.clone().iter().cloned() { + if (authored_name_at(si.clone(), arm.clone()).as_str() + == type_name.as_str()) + { + found = Some(arm.clone()); + } + } + found + } + } else { + None + } + } + None => None, + }; + let toplevel = lookup_type_by_name(scope.type_env.clone(), type_name.clone()); + let confident_record: Option> = match arm_from_expected.clone() { + Some(arm) => { + let e = expand_type_for_field_access( + arm.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + if ((e.connective.clone() == Connective::Conj) + && ((e.children.clone().len() as i64) > 0)) + { + Some(e.clone()) + } else { + None + } + } + None => match toplevel.clone() { + Some(decl) => { + let e = expand_type_for_field_access( + decl.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + if ((e.connective.clone() == Connective::Conj) + && ((e.children.clone().len() as i64) > 0)) + { + Some(e.clone()) + } else { + None + } + } + None => None, + }, + }; + match confident_record { + Some(rn) => Some(Rc::new({ + let mut __result = Vec::new(); + for f in rn.children.clone().iter().cloned() { + __result.push(authored_name_at(si.clone(), f.clone())); + } + __result + })), + None => { + // A variant name that is NOT a top-level type (e.g. `NodeLocus`, an arm of + // `Locus`) — resolve its fields via the variant→parent-enum path. Skipped when + // the name IS a top-level type, so a directly-constructed coproduct's arms are + // never mistaken for record fields. + match toplevel.clone() { + Some(_) => None, + None => { + let vf = + record_lit_expected_fields(Some(type_name.clone()), scope.clone()); + if ((vf.clone().len() as i64) > 0) { + Some(Rc::new({ + let mut __result = Vec::new(); + for f in vf.clone().iter().cloned() { + __result.push(authored_name_at(si.clone(), f.clone())); + } + __result + })) + } else { + None + } + } + } + } + } +} + +// Strict record construction: is `field` a member of ANY coproduct arm named `type_name` +// anywhere in the type env? A variant name can legitimately arm two different coproducts with +// different field sets (e.g. `TextNode` is `Fragment.TextNode { content }` and +// `MarkupNode.TextNode { text }`). Only a field present in NO same-named arm is genuinely +// undefined; this guards the undefined-field error against that ambiguity. Runs only on a +// would-be error (a field missing from the primary resolution), so the scan is rare. +pub fn field_in_any_variant_named( + type_name: String, + field: String, + scope: Rc, +) -> bool { + let si = scope.type_env.clone().source_indices.clone(); + let mut found = false; + for binding in v1_rt::map_values(&scope.type_env.clone().bindings.clone()) + .iter() + .cloned() + { + let node = binding.resolved.clone(); + if (node.connective.clone() == Connective::Disj) { + for arm in node.children.clone().iter().cloned() { + if (authored_name_at(si.clone(), arm.clone()).as_str() == type_name.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() + }; + for f in fields.iter().cloned() { + if (authored_name_at(si.clone(), f.clone()).as_str() == field.as_str()) { + found = true; + } + } + } + } + } + } + found +} + pub fn infer_record_lit( type_name: Option, field_inits: Rc>>, @@ -5512,6 +5659,12 @@ pub fn infer_record_lit( }, }, }; + let construction_field_names = match type_name.clone() { + Some(tn) => { + record_lit_construction_field_names(tn.clone(), expected.clone(), scope.clone()) + } + None => None, + }; let fi_infer_results = Rc::new({ let mut __result = Vec::new(); for fi in field_inits.iter().cloned() { @@ -5520,7 +5673,7 @@ pub fn infer_record_lit( fi.clone(), scope.type_env.clone().source_indices.clone(), ); - let field_expected = match Rc::new({ + let matched_sf = Rc::new({ let mut __result = Vec::new(); for sf in struct_fields.clone().iter().cloned() { if (authored_name_at( @@ -5536,8 +5689,8 @@ pub fn infer_record_lit( __result }) .first() - .cloned() - { + .cloned(); + let field_expected = match matched_sf.clone() { Some(sf) => { let ft = match sf.inferred.clone().as_deref().cloned() { Some(InferredNode::Resolved { node: rt, .. }) => rt.clone(), @@ -5553,6 +5706,42 @@ pub fn infer_record_lit( } None => None, }; + // Strict record construction (§5 fail-closed): a field that matches + // no field of a RESOLVED type is a loud, located error, not silently + // ignored. Guarded on a known `type_name` and a non-empty resolved + // field set, so an anonymous/unresolved record (empty `struct_fields`) + // never false-positives — closes the fail-open `infer_record_lit` hole. + let unknown_field_diags = match construction_field_names.clone() { + Some(names) => { + let mut present = false; + for n in names.iter().cloned() { + if (n.as_str() == fi_name.clone().as_str()) { + present = true; + } + } + if (present + || field_in_any_variant_named( + type_name.clone().unwrap_or_else(|| "".to_string()), + 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: type_name + .clone() + .unwrap_or_else(|| "".to_string()), + span: fi.span.clone(), + }), + scope.module_name.clone(), + )]) + } + } + None => Rc::new(vec![]), + }; let ar = infer_expr( field_init_node_value(fi.clone()), scope.clone(), @@ -5594,7 +5783,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(), + ), }) }); } diff --git a/src/v2/compiler/manual/infer_ground_add_mvp.dag b/src/v2/compiler/manual/infer_ground_add_mvp.dag index 4507493f0fa..581ac856f38 100644 --- a/src/v2/compiler/manual/infer_ground_add_mvp.dag +++ b/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 } } } diff --git a/src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag b/src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag index d423d677a80..9f0e0cbd004 100644 --- a/src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag +++ b/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> { 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)) ) } diff --git a/src/v2/lens/application/enforce_rejecting_gate_fires.dag b/src/v2/lens/application/enforce_rejecting_gate_fires.dag index 759beffb57b..4f5e993d458 100644 --- a/src/v2/lens/application/enforce_rejecting_gate_fires.dag +++ b/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> { 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)) ) } diff --git a/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag b/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag index 06fe3d7c6f2..91580a6d730 100644 --- a/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag +++ b/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag @@ -14,7 +14,7 @@ import v2.compiler.infer { InferredTree } import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms_empty } import v2.std.compilers.lexing { VoidLexRules } import v2.std.collection { empty_map } -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.algebra { Empty } import v2.std.node { Atom, Conj, Node, Symbol, TypeNode, SyntheticOccurrence } @@ -50,7 +50,7 @@ data rejecting_lens_authority_node: Node = Node { fn rejecting_lens_gate(_tree: InferredTree) -> Outcome> { outcome_rejected( - compile_lens_gate_rejected_diagnostic(at: PortLocus { port: ^rejecting_lens_gate_at }) + compile_lens_gate_rejected_diagnostic(at: port_locus(port: ^rejecting_lens_gate_at)) ) } From d0efa67a6e6e073a5d5d579fcc7cd489fc43d4ac Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 22:47:01 +0000 Subject: [PATCH 3/5] =?UTF-8?q?Strict=20record-field=20check:=20port=20to?= =?UTF-8?q?=20.dag=20authority=20+=20de-conflict=20TextFile=20(=C2=A73/?= =?UTF-8?q?=C2=A77)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per the §3/§7 review (cursor): the strict infer_record_lit check lived only in the generated seed .rs (a host hand-edit), not the .dag authority. Port the helpers and the infer_record_lit guard into src/v1/04_infer.dag so the seed is regenerated FROM the model: - record_lit_construction_field_names: confident field-name resolver (alias-follow + expected-coproduct-arm union), SKIPS generic/parametric types (newtype flattening makes their resolved field names non-source-faithful — the algebra-tower false positives). - field_in_any_variant_named: same-named-coproduct-arm ambiguity guard, run only on a would-be error (keeps TextNode-style constructions silent; full teeth elsewhere). - infer_record_lit emits FieldNotFound for a field on no field of a confidently-resolved non-generic record; none-result paths stay silent (no false positives). §3 de-confliction: two 'type TextFile' collided in the bootstrap's combined src/v1+dsl closure — v1 {path, content} (emit output) vs dsl/std {path, document} (markup). The name-keyed type env clobbered one, so the strict check could not resolve 'content'. Rename the dsl one to DocumentFile (it holds a Document; parallel to its sibling RenderedTextFile), the smaller + semantically-correct fix. v1 TextFile {path, content} is now the sole binding. The regenerated .rs follows (regen against current main's seed, post-merge). Co-Authored-By: Claude Opus 4.8 --- dsl/shared/dag_util.dag | 4 +- dsl/std/types.dag | 2 +- src/v1/04_infer.dag | 97 ++++++++++++++++++++++++++++++++++++++++- 3 files changed, 99 insertions(+), 4 deletions(-) diff --git a/dsl/shared/dag_util.dag b/dsl/shared/dag_util.dag index a3214713a9d..c33055db15e 100644 --- a/dsl/shared/dag_util.dag +++ b/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 } diff --git a/dsl/std/types.dag b/dsl/std/types.dag index c4a94837009..a9387887c58 100644 --- a/dsl/std/types.dag +++ b/dsl/std/types.dag @@ -566,7 +566,7 @@ type Document { trailing_newline: Bool } -type TextFile { +type DocumentFile { path: String document: Document } diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 514b4e83965..ab08f9ebacc 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2841,6 +2841,80 @@ fn record_lit_alias_struct_fields(type_name: String, scope: InferScope) -> List< } } +// The expected COPRODUCT arm whose name matches a constructed variant, if any — disambiguates +// a constructed name that also names a top-level collection (e.g. `GrammarExpr.Optional` the +// variant vs the collection `Optional`), using the import-scoped `expected` type. +fn record_lit_expected_coproduct_arm(type_name: String, expected: Node?, scope: InferScope) -> Node? { + match expected { + Present { value: exp } => + let exp_resolved = resolved_type(n: exp) + if (exp_resolved.connective == Disj) { + exp_resolved.children |> filter(arm => authored_name_at(source_indices: scope.type_env.source_indices, node: arm) == type_name) |> first + } else { none } + Absent => none + } +} + +// Strict record construction (§5 fail-closed): the source-level field-name set of the +// CONCRETE record a construction targets, or `none` whenever resolution is not confident — +// so the undefined-field check below stays silent rather than false-positive. The field set +// REUSES the already-computed `struct_fields` (§2 DRY): that set is import-scoped (derived +// from the `expected` type), so it resolves the construction's actual target rather than an +// unscoped global `lookup_type_by_name` guess. Two adjustments: (1) GENERIC/parametric +// types are SKIPPED — the resolved type env rewrites a single-field wrapper field to its +// innermost name under newtype flattening (`type Monoid { semigroup: Semigroup; ... }` +// resolves to fields `[op, identity]`: semigroup→Semigroup→magma→Magma→op), so the resolved +// set is not source-faithful and a check against it false-positives across the algebra tower; +// until generic field-name resolution is source-faithful (dissolution trigger) the check +// covers non-generic records only, which is where every real bug it found lives. (2) a variant +// constructed against an expected coproduct also admits that arm's fields, since `struct_fields` +// yields the collection's arms, not the variant's fields, for that case. +fn record_lit_construction_field_names(type_name: String, expected: Node?, struct_fields: List, scope: InferScope) -> List? { + let si = scope.type_env.source_indices + let toplevel = lookup_type_by_name(env: scope.type_env, name: type_name) + let toplevel_generic = match toplevel { + Present { value: decl } => decl.params |> count > 0 + Absent => false + } + if toplevel_generic { + none + } else { + let arm_fields = match record_lit_expected_coproduct_arm(type_name: type_name, expected: expected, scope: scope) { + Present { value: arm } => arm.children + Absent => [] + } + let combined = concat(struct_fields, arm_fields) + if combined |> count > 0 { + Present { value: combined |> map(f => authored_name_at(source_indices: si, node: f)) } + } else { 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, span: SourceSpan, name_span: SourceSpan, scope: InferScope, expected: Node?) -> InferResult { let struct_fields = match type_name { Present { value: tn } => @@ -2870,8 +2944,29 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa } } } + let construction_field_names = match type_name { + Present { value: tn } => record_lit_construction_field_names(type_name: tn, expected: expected, struct_fields: struct_fields, 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 +3003,7 @@ fn infer_record_lit(type_name: String?, field_inits: List, 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) From 9737a8772f733a653f0a85588081a9f598583837 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 00:57:37 +0000 Subject: [PATCH 4/5] =?UTF-8?q?Strict=20record-field=20check:=20tighten=20?= =?UTF-8?q?resolver=20to=20confident-only=20(=C2=A75=20no=20false=20positi?= =?UTF-8?q?ves)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The struct_fields/expected-based resolver false-positived on main's newer types where resolved field names diverge from source under newtype flattening / name collision: - `Watt = Measure` etc. — concrete aliases of the single-field generic `Measure { count: M }`; the wrapper dissolves so `count` isn't in the resolved set. - `Vendor { legal_name }` — a §3 name collision: `extdeps Vendor { legal_name }` record vs the std `Vendor = UnknownVendor | ...` enum; lookup grabs the enum. Replace it with a confident-only resolver: fire ONLY when the constructed name resolves to a plain, fully-grounded record (params == 0, connective == Conj, children > 0), reading source field names directly from its own children. Generics, concrete aliases of single-field generics, and coproduct/enum (incl. the losing side of a collision) all return none -> silent. Keeps full teeth on plain records, where every real bug lives (BoolWitness{holds}, NodeLocus{node}, PortLocus{port}). Drops the now-unused record_lit_expected_coproduct_arm. Co-Authored-By: Claude Opus 4.8 --- src/v1/04_infer.dag | 71 ++++++++++++++++----------------------------- 1 file changed, 25 insertions(+), 46 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index ab08f9ebacc..19d91715131 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2841,52 +2841,31 @@ fn record_lit_alias_struct_fields(type_name: String, scope: InferScope) -> List< } } -// The expected COPRODUCT arm whose name matches a constructed variant, if any — disambiguates -// a constructed name that also names a top-level collection (e.g. `GrammarExpr.Optional` the -// variant vs the collection `Optional`), using the import-scoped `expected` type. -fn record_lit_expected_coproduct_arm(type_name: String, expected: Node?, scope: InferScope) -> Node? { - match expected { - Present { value: exp } => - let exp_resolved = resolved_type(n: exp) - if (exp_resolved.connective == Disj) { - exp_resolved.children |> filter(arm => authored_name_at(source_indices: scope.type_env.source_indices, node: arm) == type_name) |> first - } else { none } - Absent => none - } -} - -// Strict record construction (§5 fail-closed): the source-level field-name set of the -// CONCRETE record a construction targets, or `none` whenever resolution is not confident — -// so the undefined-field check below stays silent rather than false-positive. The field set -// REUSES the already-computed `struct_fields` (§2 DRY): that set is import-scoped (derived -// from the `expected` type), so it resolves the construction's actual target rather than an -// unscoped global `lookup_type_by_name` guess. Two adjustments: (1) GENERIC/parametric -// types are SKIPPED — the resolved type env rewrites a single-field wrapper field to its -// innermost name under newtype flattening (`type Monoid { semigroup: Semigroup; ... }` -// resolves to fields `[op, identity]`: semigroup→Semigroup→magma→Magma→op), so the resolved -// set is not source-faithful and a check against it false-positives across the algebra tower; -// until generic field-name resolution is source-faithful (dissolution trigger) the check -// covers non-generic records only, which is where every real bug it found lives. (2) a variant -// constructed against an expected coproduct also admits that arm's fields, since `struct_fields` -// yields the collection's arms, not the variant's fields, for that case. -fn record_lit_construction_field_names(type_name: String, expected: Node?, struct_fields: List, 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`, `Vendor`): 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`): the wrapper +// dissolves to its `` 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` 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? { let si = scope.type_env.source_indices - let toplevel = lookup_type_by_name(env: scope.type_env, name: type_name) - let toplevel_generic = match toplevel { - Present { value: decl } => decl.params |> count > 0 - Absent => false - } - if toplevel_generic { - none - } else { - let arm_fields = match record_lit_expected_coproduct_arm(type_name: type_name, expected: expected, scope: scope) { - Present { value: arm } => arm.children - Absent => [] - } - let combined = concat(struct_fields, arm_fields) - if combined |> count > 0 { - Present { value: combined |> map(f => authored_name_at(source_indices: si, node: f)) } - } else { none } + 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 } } @@ -2945,7 +2924,7 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa } } let construction_field_names = match type_name { - Present { value: tn } => record_lit_construction_field_names(type_name: tn, expected: expected, struct_fields: struct_fields, scope: scope) + Present { value: tn } => record_lit_construction_field_names(type_name: tn, scope: scope) Absent => none } let tn_str = match type_name { From fb3a8d4f57ab309550ad36c206e16263557a7f99 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 01:45:46 +0000 Subject: [PATCH 5/5] Regenerate stage0 seed (v1_compiler_infer.rs) from 04_infer.dag MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The committed seed is the compiler's own emit of the strict 04_infer.dag authority (derived, not hand-edited) — closes the §3/§7 review: the strict infer_record_lit check now lives in the .dag model and the .rs is regenerated from it. Single-file diff (+136/-1, no new module deps): only 04_infer.dag changed, so only its emitted module changes. Proven by execution on the merged tree: - floor (claim_executor over src/v2+dsl): 0 field-not-found false positives - self-compile (src/v1+dsl via regen path): 0 field-not-found - cargo fmt --all --check + cargo clippy --all-targets -D warnings: clean - discriminating probe: `BoolWitness { holds: true }` -> loud 'field holds not found in type BoolWitness' Co-Authored-By: Claude Opus 4.8 --- src/v1/stage0/src/v1_compiler_infer.rs | 273 ++++++++++--------------- 1 file changed, 108 insertions(+), 165 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 952d1c9bc5d..ec4d51a09a6 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -5465,151 +5465,98 @@ pub fn record_lit_alias_struct_fields( } } -// Strict record construction (§5 fail-closed): resolve the field-name set of the CONCRETE -// record a construction targets, returning `None` whenever resolution is not confident — so -// the undefined-field check stays silent rather than false-positive. Two precision rules the -// fail-open path elided: (1) a variant constructed against an expected COPRODUCT resolves to -// that arm's fields (disambiguates a constructed name that also names a top-level type, e.g. -// `GrammarExpr.Optional` vs the collection `Optional`); (2) a type ALIAS -// (`type Set = PointwisePower`) is followed to its target record. Only a Conj record -// with fields yields `Some`. pub fn record_lit_construction_field_names( type_name: String, - expected: Option>, scope: Rc, ) -> Option>> { - let si = scope.type_env.clone().source_indices.clone(); - let arm_from_expected: Option> = match expected.clone() { - Some(exp) => { - let exp_resolved = resolved_type(exp.clone()); - if (exp_resolved.connective.clone() == Connective::Disj) { - { - let mut found: Option> = None; - for arm in exp_resolved.children.clone().iter().cloned() { - if (authored_name_at(si.clone(), arm.clone()).as_str() - == type_name.as_str()) - { - found = Some(arm.clone()); - } - } - found - } - } else { - None - } - } - None => None, - }; - let toplevel = lookup_type_by_name(scope.type_env.clone(), type_name.clone()); - let confident_record: Option> = match arm_from_expected.clone() { - Some(arm) => { - let e = expand_type_for_field_access( - arm.clone(), - scope.type_env.clone(), - scope.module_name.clone(), - ); - if ((e.connective.clone() == Connective::Conj) - && ((e.children.clone().len() as i64) > 0)) - { - Some(e.clone()) - } else { - None - } - } - None => match toplevel.clone() { + { + let si = scope.type_env.clone().source_indices.clone(); + match lookup_type_by_name(scope.type_env.clone(), type_name) { Some(decl) => { - let e = expand_type_for_field_access( - decl.clone(), - scope.type_env.clone(), - scope.module_name.clone(), - ); - if ((e.connective.clone() == Connective::Conj) - && ((e.children.clone().len() as i64) > 0)) + if ((((decl.params.clone().len() as i64) == 0) + && (decl.connective.clone() == Connective::Conj)) + && ((decl.children.clone().len() as i64) > 0)) { - Some(e.clone()) + 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, - }, - }; - match confident_record { - Some(rn) => Some(Rc::new({ - let mut __result = Vec::new(); - for f in rn.children.clone().iter().cloned() { - __result.push(authored_name_at(si.clone(), f.clone())); - } - __result - })), - None => { - // A variant name that is NOT a top-level type (e.g. `NodeLocus`, an arm of - // `Locus`) — resolve its fields via the variant→parent-enum path. Skipped when - // the name IS a top-level type, so a directly-constructed coproduct's arms are - // never mistaken for record fields. - match toplevel.clone() { - Some(_) => None, - None => { - let vf = - record_lit_expected_fields(Some(type_name.clone()), scope.clone()); - if ((vf.clone().len() as i64) > 0) { - Some(Rc::new({ - let mut __result = Vec::new(); - for f in vf.clone().iter().cloned() { - __result.push(authored_name_at(si.clone(), f.clone())); - } - __result - })) - } else { - None - } - } - } } } } -// Strict record construction: is `field` a member of ANY coproduct arm named `type_name` -// anywhere in the type env? A variant name can legitimately arm two different coproducts with -// different field sets (e.g. `TextNode` is `Fragment.TextNode { content }` and -// `MarkupNode.TextNode { text }`). Only a field present in NO same-named arm is genuinely -// undefined; this guards the undefined-field error against that ambiguity. Runs only on a -// would-be error (a field missing from the primary resolution), so the scan is rare. -pub fn field_in_any_variant_named( - type_name: String, - field: String, - scope: Rc, -) -> bool { - let si = scope.type_env.clone().source_indices.clone(); - let mut found = false; - for binding in v1_rt::map_values(&scope.type_env.clone().bindings.clone()) - .iter() - .cloned() +pub fn field_in_any_variant_named(type_name: String, field: String, scope: Rc) -> bool { { - let node = binding.resolved.clone(); - if (node.connective.clone() == Connective::Disj) { - for arm in node.children.clone().iter().cloned() { - if (authored_name_at(si.clone(), arm.clone()).as_str() == type_name.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() - }; - for f in fields.iter().cloned() { - if (authored_name_at(si.clone(), f.clone()).as_str() == field.as_str()) { - found = true; + 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 } } - found } pub fn infer_record_lit( @@ -5660,11 +5607,13 @@ pub fn infer_record_lit( }, }; let construction_field_names = match type_name.clone() { - Some(tn) => { - record_lit_construction_field_names(tn.clone(), expected.clone(), scope.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() { @@ -5673,7 +5622,37 @@ pub fn infer_record_lit( fi.clone(), scope.type_env.clone().source_indices.clone(), ); - let matched_sf = Rc::new({ + 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() { if (authored_name_at( @@ -5689,8 +5668,8 @@ pub fn infer_record_lit( __result }) .first() - .cloned(); - let field_expected = match matched_sf.clone() { + .cloned() + { Some(sf) => { let ft = match sf.inferred.clone().as_deref().cloned() { Some(InferredNode::Resolved { node: rt, .. }) => rt.clone(), @@ -5706,42 +5685,6 @@ pub fn infer_record_lit( } None => None, }; - // Strict record construction (§5 fail-closed): a field that matches - // no field of a RESOLVED type is a loud, located error, not silently - // ignored. Guarded on a known `type_name` and a non-empty resolved - // field set, so an anonymous/unresolved record (empty `struct_fields`) - // never false-positives — closes the fail-open `infer_record_lit` hole. - let unknown_field_diags = match construction_field_names.clone() { - Some(names) => { - let mut present = false; - for n in names.iter().cloned() { - if (n.as_str() == fi_name.clone().as_str()) { - present = true; - } - } - if (present - || field_in_any_variant_named( - type_name.clone().unwrap_or_else(|| "".to_string()), - 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: type_name - .clone() - .unwrap_or_else(|| "".to_string()), - span: fi.span.clone(), - }), - scope.module_name.clone(), - )]) - } - } - None => Rc::new(vec![]), - }; let ar = infer_expr( field_init_node_value(fi.clone()), scope.clone(),