Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions dag/extdeps/systemd/systemd.dag
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,6 @@ type SystemdUnitProperty
| SubState
| Result
| ExecMainStatus
| SubState
| ExecStartProperty
| User
| WorkingDirectoryProperty
Expand Down Expand Up @@ -103,7 +102,6 @@ fn systemd_unit_property_wire(property: SystemdUnitProperty) -> NonEmptyStr {
SubState => "SubState" as NonEmptyStr
Result => "Result" as NonEmptyStr
ExecMainStatus => "ExecMainStatus" as NonEmptyStr
SubState => "SubState" as NonEmptyStr
ExecStartProperty => "ExecStart" as NonEmptyStr
User => "User" as NonEmptyStr
WorkingDirectoryProperty => "WorkingDirectory" as NonEmptyStr
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
module gunbc.recurring_failure_mode.a_coproduct_declares_one_variant_twice

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data a_coproduct_declares_one_variant_twice: RecurringFailureMode = RecurringFailureMode {
identity: "a_coproduct_declares_one_variant_twice" as NonEmptyStr,
receipts: [
"INVALID STATE: one coproduct declaration names the same variant twice. One name, two declarations, in a single type -- the section 3 single-authority defect stated at the grain where the substrate can see it, and distinct from two variants sharing a leaf name under DIFFERENT containment, which is a namespace-identity question and not this row.",
"HARM: lookup by exact authored name takes the first match and never asks whether a second exists, so the duplicate is not merely tolerated, it is unobservable. Every consumer resolves to the first declaration and the second is dead vocabulary that still reads as declared. Nothing downstream can distinguish the two, so no consumer can report the defect either; the declaration is degenerate and the whole pipeline answers as though it were not.",
"RECEIPT, AND IT IS A LIVE ONE RATHER THAN A CONSTRUCTED SPECIMEN: extdeps.systemd SystemdUnitProperty carried two identical SubState declaration arms and two identical wire arms, on origin/main since gunbc#9761 and gunbc#10443, through every required run in that window without a single diagnostic. It was surfaced only when v1.compiler.infer_patterns find_variant_child_keyed began keying variant lookup and refusing on more than one match: both children key equal, lookup refuses, and required-witnesses-floor and heal-generated-artifacts both refused with ChangedWitnessObservationFailed naming that declaration.",
"POPULATION, BY INSTRUMENT RATHER THAN BY ASSERTION: an arm-level duplicate-leaf census over every coproduct declaration under dag/ and src/ -- splitting each type declaration right-hand side on its top-level pipe and counting duplicate leaf keys per declaration, rather than matching lines -- identifies the membership. SystemdUnitProperty was its sole member at the time of this receipt. The census is the reproduction route; a transcribed count is not the authority and would rot away from it.",
"RUNG FOUND AT: mechanically preventable, and BY ACCIDENT. The refusal that caught it is a lookup-time consequence of keying variant identity for an unrelated repair, not a wall anybody built for this class. Nothing in the parser, normalize or resolve folds refuses a duplicate variant at declaration, so on any route that does not key -- which is every route before that change -- the class remains entirely silent. Reporting this as a standing mechanical prevention would be rung inflation: the mechanism is real, executes, and is enrolled, but it guards the class only where a keyed lookup happens to reach the declaration.",
"CEILING: structurally impossible, and the argument is that the invalid state has no constructor once the declaration fold refuses it. A coproduct whose declared variant names are not distinct is not a weakly-typed program but a malformed declaration; a fold that refuses a repeated leaf at ingest leaves no accepted program in which the duplicate exists, so no validation, lookup rule or consumer discipline is needed downstream. This is a decidable, fully modeled class -- the declared children and their authored names are both in hand at the point of declaration -- so section 4b admits nothing weaker as its ceiling.",
"NEXT-RUNG TRIGGER, NAMING THE CAPABILITY AND NOT AN ARTIFACT: the declaration fold that constructs a Disj node refuses a declaration whose children do not carry pairwise distinct authored names, with a typed located diagnostic naming the type and the repeated name, executed on a paired probe -- a duplicate declaration refused, and a declaration whose variants merely share a prefix or differ only outside the leaf accepted. Owner unassigned at filing. A lookup-side refusal does NOT retire this row: it catches the class only where a keyed lookup reaches the declaration, which is what this receipt shows was true for years while the duplicate stood.",
"DISPOSITION: filed from gunbc#11301, whose subject is the one-sided coverage and lookup key in v1.compiler.infer_patterns. The SystemdUnitProperty deletion landed there as a forced consequence of that PR's refusal arm, with the population measured before the edit. The declaration-time wall is deliberately NOT that PR's scope and is left to this row's trigger, so the repair that surfaced the class is not mistaken for the wall against it.",
],
evidence: [],
}
110 changes: 110 additions & 0 deletions dag/test/claim/match_exhaustiveness_coproduct_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -295,3 +295,113 @@ test fn w_variant_named_in_type_position_is_judged_against_its_parent_roster() -
test fn w_variant_type_position_covering_the_parent_roster_is_clean() -> Bool {
non_exhaustive_blocking_count(source: variant_type_position_parent_covered_source) == 0
}

// -- ONE IDENTITY FOR THE DECLARED CONSTRUCTOR AND THE PATTERN --
//
// A coproduct arm may be authored with a DOTTED name -- `type T = a.b.Alpha | Beta` -- because
// parse_type_body_after_eq takes the first arm through parse_dotted_ident, shared with the
// type-alias lookahead. The child's authored name is then the whole dotted spelling, and two
// separate sites compared it against a pattern name that had been reduced to its leaf while the
// child had not: the coverage key in pattern_matches_constructor, which lost its declaration-side
// application in the nested-pattern matrix rewrite, and the three variant-lookup sites in
// lookup_variant_in_type, which never had one. The first reported the arm missing; the second
// refused the bare pattern with VariantNotFound. Both are the same identity applied to one side.
//
// THE REDUCTION IS THE WHOLE SOURCE, and the two class-scoped controls beneath it say which site
// closes which half -- so a repair of one alone cannot green this section and be mistaken for a
// repair of the class. Every arm is named in both directions: the negative differs from the
// positive by exactly the omitted `Beta`.

data dotted_declared_arm_source: String = "module dotted_decl_covered\ntype T = a.b.Alpha | Beta\nfn f(t: T) -> Bool {\n match t {\n Alpha => true\n Beta => false\n }\n}\n"

data dotted_declared_arm_missing_source: String = "module dotted_decl_missing\ntype T = a.b.Alpha | Beta\nfn f(t: T) -> Bool {\n match t {\n Alpha => true\n }\n}\n"

data dotted_later_arm_source: String = "module dotted_decl_later_arm\ntype T = Alpha | a.b.Beta\nfn f(t: T) -> Bool {\n match t {\n Alpha => true\n Beta => false\n }\n}\n"

fn single_source_run(path: String, source: String) -> MultiModuleCompileFixtureOutcome {
compile_fixture(MultiModuleCompileFixture {
sources: [fixture_source(path, source)],
entry: path
})
}

fn fixture_all_blocking_count(o: MultiModuleCompileFixtureOutcome) -> Int {
match o {
FixtureCompileRefused { module_count: _, diagnostics: rows, source_digest: _, compiler_digest: _ } =>
census_total_count(rows: fixture_blocking_rows(rows: rows))
FixtureCompileCompleted { module_count: _, emitted_files: _, resolved_rust_functions: _, diagnostics: rows, source_digest: _, compiler_digest: _ } =>
census_total_count(rows: fixture_blocking_rows(rows: rows))
FixtureInstrumentRefused { cause: _ } => -1
}
}

test fn w_dotted_declared_arm_covered_by_bare_patterns_compiles_clean() -> Bool {
fixture_all_blocking_count(
o: single_source_run(path: "dotted/covered.dag", source: dotted_declared_arm_source)
) == 0
}

test fn w_dotted_declared_arm_is_not_reported_missing() -> Bool {
fixture_blocking_class_count(
o: single_source_run(path: "dotted/covered.dag", source: dotted_declared_arm_source),
wanted: "NonExhaustiveMatch"
) == 0
}

test fn w_bare_pattern_resolves_against_a_dotted_declared_arm() -> Bool {
fixture_blocking_class_count(
o: single_source_run(path: "dotted/covered.dag", source: dotted_declared_arm_source),
wanted: "VariantNotFound"
) == 0
}

// THE NEGATIVE. Keying both sides must not make a real gap disappear: omitting `Beta` from the
// same declaration still refuses, and with exactly one missing arm rather than a widened roster.
test fn w_dotted_declaration_with_a_genuinely_missing_arm_still_refuses() -> Bool {
fixture_blocking_class_count(
o: single_source_run(path: "dotted/missing.dag", source: dotted_declared_arm_missing_source),
wanted: "NonExhaustiveMatch"
) == 1
}

// THE REACHABILITY BOUNDARY, recorded rather than repaired. Only the FIRST arm of the
// no-leading-pipe form reaches parse_dotted_ident; parse_more_variants_acc takes every later arm
// through expect_ident, so a dotted arm in second position refuses at parse. That refusal is a
// parser fact this change does not touch, and it is the reason the subject above is written with
// the dotted arm first. It is asserted as a REFUSAL, not as an exhaustiveness count: a parse
// refusal and a clean compile both report zero rows of any later class.
test fn w_dotted_arm_in_later_position_refuses_at_parse() -> Bool {
fixture_all_blocking_count(
o: single_source_run(path: "dotted/later.dag", source: dotted_later_arm_source)
) > 0
}

// -- A LEAF KEY THAT TWO DECLARED ARMS SHARE REFUSES, IT DOES NOT PICK ONE --
//
// Keying by leaf makes `a.b.Alpha | Alpha` possible, which exact-name matching could not produce:
// one bare `Alpha` arm now keys equal to BOTH declared children. Measured against the first-match
// revision of find_variant_child_keyed, this source compiles CLEAN -- the bare arm binds the first
// child and the match is called exhaustive while the second declared variant is unhandled. That is
// the failure arm widening instead of refusing, inside the very function whose annotation declares
// the collision unresolved. find_variant_child_keyed therefore treats more-than-one as no-match,
// which the call sites carry into the existing variant_not_found_result rather than a minted
// ambiguity spelling.
//
// THE SHAPE IS CONSTRAINED BY WHAT PARSES, and the first draft of this witness got it wrong in the
// direction that hides: `a.b.Alpha | c.d.Alpha` is green under BOTH revisions, because
// parse_more_variants_acc takes every arm after the first through expect_ident, so the second
// dotted arm refuses at parse and the collision is never reached. A witness over that source is
// permanently green and would stand as coverage for an arm it never exercises. The dotted name
// must therefore be FIRST and the colliding one bare.
//
// THIS IS THE DECLARED FRONTIER'S ARM, NOT ITS CLOSURE. Distinguishing the two variants needs the
// scope-carrying identity the namespace program is converging on; until that lands the honest
// answer is a refusal, and this witness is what keeps it a refusal.

data colliding_leaf_declaration_source: String = "module colliding_leaf_decl\ntype T = a.b.Alpha | Alpha\nfn f(t: T) -> Bool {\n match t {\n Alpha => true\n }\n}\n"

test fn w_two_declared_arms_sharing_a_leaf_key_refuse_rather_than_bind_the_first() -> Bool {
fixture_all_blocking_count(
o: single_source_run(path: "dotted/collide.dag", source: colliding_leaf_declaration_source)
) > 0
}
57 changes: 52 additions & 5 deletions src/v1/04_patterns.dag
Original file line number Diff line number Diff line change
Expand Up @@ -290,9 +290,9 @@ fn lookup_variant_in_type(scrut: PatternSubject, variant_name: String, module_na
match symbol_index_lookup(index: env.symbol_index, qualified_name: variant_name) {
Present { value: resolved } =>
if (resolved.connective == Disj) {
match find_child_named(n: resolved, name: qualified_last_segment(name: variant_name), source_indices: source_indices) {
match find_variant_child_keyed(n: resolved, variant_name: variant_name, source_indices: source_indices) {
Present { value: variant_child } =>
match find_child_named(n: expand_scrut_type_for_variant_lookup(scrut_node: scrut_node, env: env), name: qualified_last_segment(name: variant_name), source_indices: source_indices) {
match find_variant_child_keyed(n: expand_scrut_type_for_variant_lookup(scrut_node: scrut_node, env: env), variant_name: variant_name, source_indices: source_indices) {
Present { value: scrut_child } => node_lookup_resolved(node: scrut_child)
Absent => node_lookup_resolved(node: variant_child)
}
Expand Down Expand Up @@ -326,7 +326,7 @@ fn lookup_variant_in_type(scrut: PatternSubject, variant_name: String, module_na

let optional_coproduct_subject = scrut_name == "Optional"
&& (variant_name == "Present" || variant_name == "Absent")
let direct_match = find_child_named(n: scrut_node, name: variant_name, source_indices: source_indices)
let direct_match = find_variant_child_keyed(n: scrut_node, variant_name: variant_name, source_indices: source_indices)

let record_destructure = field_binding_count > 0
&& scrut_node.connective == Conj
Expand Down Expand Up @@ -366,11 +366,58 @@ fn lookup_field_in_variant(variant: PatternSubject, field_name: String, module_n
}
}

// THE KEY IS APPLIED TO BOTH SIDES OR IT IS NOT AN IDENTITY. This is the seed's incumbent
// variant-name identity -- the same bare leaf that symbol_index.global_bare is keyed on and that
// qualified_last_segment joins on throughout infer -- and it must key the DECLARED constructor
// exactly as it keys the pattern. It was authored symmetrically; the nested-pattern matrix rewrite
// kept the pattern-side application and dropped the two declaration-side ones, after which a
// declared arm carrying a dotted authored name could be covered by no pattern spelling at all and
// was reported missing under its dotted name. Every coverage comparison in the fold routes through
// pattern_matches_constructor, so keying both operands there is the whole of the matching repair;
// the absent-constructor witness cell carries the key separately because it names the gap.
//
// WHAT A LEAF-KEYED IDENTITY STILL LEAVES OPEN, so it does not stall untracked (section 4b(2)):
// two variants sharing a leaf name under different containment collide on one key. That is the
// namespace program's class, not this one's, and it is not narrowed here. Its trigger is the
// scope-carrying binding cutover answering by execution; this function is that cutover's consumer.
fn variant_pattern_coverage_key(name: String) -> String {
let segs = split(name, separator: ".")
if segs |> count == 0 { name } else { fold(segs, init: "", f: (_, seg) => seg) }
}

// VARIANT LOOKUP IS THE SAME IDENTITY QUESTION AS COVERAGE, so it is keyed by the same function on
// both sides. The three variant-lookup sites in lookup_variant_in_type each compared a name against
// a child's RAW authored name: the qualified branch reduced only the pattern, and the bare branch
// reduced neither, so a bare arm could not resolve against a child declared under a dotted authored
// name and refused with VariantNotFound -- the coverage defect one function up, one layer down.
// Unlike the coverage key that is a lost symmetry, this asymmetry is as old as the function.
//
// THIS IS DELIBERATELY NOT find_child_named. That helper also resolves FIELDS, at
// lookup_field_in_variant; keying it would make field matching leaf-keyed, which widens what a
// field name may match rather than repairing an identity, so it is left exactly as it is.
//
// AMBIGUITY REFUSES; IT DOES NOT PICK. Keying by leaf makes it possible for TWO declared children
// to key equal -- `a.b.Alpha | c.d.Alpha` -- which exact-name matching could not produce, so this
// function creates the collision and owes it an arm. Taking the first match would answer with a
// variant the source did not name, inside the very function whose annotation declares that
// collision unresolved: fail-open at the exact point the frontier is admitted. More than one match
// therefore resolves to NO match, which the three call sites already carry into
// variant_not_found_result -- a typed, located refusal in the existing vocabulary. No ambiguity
// diagnostic is minted here: the frontier is the missing scope-carrying identity, and inventing a
// spelling for it would be modeling the gap instead of refusing over it.
fn find_variant_child_keyed(n: Node, variant_name: String, source_indices: Map<String, NewlineIndex>) -> Node? {
let key = variant_pattern_coverage_key(name: variant_name)
let matches = n.children |> filter(c => variant_pattern_coverage_key(name: authored_name_at(source_indices: source_indices, node: c)) == key)
if matches |> count > 1 {
none
} else {
match matches |> first {
Present { value: ch } => Present { value: ch }
Absent => none
}
}
}

// -- NESTED PATTERN EXHAUSTIVENESS: THE COLUMNS ARE CARRIED JOINTLY --
//
// The flat fold this replaces keyed coverage on the arm HEAD alone and discarded
Expand Down Expand Up @@ -533,7 +580,7 @@ fn pattern_row_is_irrefutable(row: List<MatchPattern>) -> Bool {
fn pattern_matches_constructor(p: MatchPattern, ctor: String) -> Bool {
match p {
VariantPattern { name: n, parent_enum: _, field_bindings: _ } =>
variant_pattern_coverage_key(name: n) == ctor
variant_pattern_coverage_key(name: n) == variant_pattern_coverage_key(name: ctor)
LitPattern { value: v } =>
match v {
LitBool { value: b } => if b { ctor == "True" } else { ctor == "False" }
Expand Down Expand Up @@ -619,7 +666,7 @@ fn exhaustiveness_witnesses(rows: List<List<MatchPattern>>, columns: List<Node>,
rows: default_pattern_rows(rows: rows),
columns: rest_columns, env: env, module_name: module_name
)
absent_ctors |> flat_map(c => sub |> map(w => PatternWitnessRow { cells: concat([c], w.cells) }))
absent_ctors |> flat_map(c => sub |> map(w => PatternWitnessRow { cells: concat([variant_pattern_coverage_key(name: c)], w.cells) }))
} else {
ctors |> fold(init: [], f: (acc, c) =>
let fields = constructor_fields(type_node: head_type, ctor: c, env: env, module_name: module_name)
Expand Down
Loading
Loading