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
1 change: 1 addition & 0 deletions DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -213,6 +213,7 @@ One row per class, each carrying its recognition rule and its receipts, in [docs
- `executed_conjunct_discriminates_nothing`
- `unbacked_execution_claim`
- `mitigation_injected_where_judgment_declined`
- `one_refusal_two_destinations`

## Building & checks

Expand Down
7 changes: 7 additions & 0 deletions dag/gunbc/recurring_failure_mode.dag
Original file line number Diff line number Diff line change
Expand Up @@ -210,6 +210,12 @@ data mitigation_injected_where_judgment_declined: RecurringFailureMode = Recurri
evidence: [],
}

data one_refusal_two_destinations: RecurringFailureMode = RecurringFailureMode {
identity: "one_refusal_two_destinations" as NonEmptyStr,
authored: "**one refusal, two destinations, remedy misdirected** (a single refusal at a single source column emits two rows naming DIFFERENT expected types, because two producers resolve the same declared spelling in different environments. The reader repairs from the row that names the parameter -- and that is the row the checker did NOT refuse on. **THE SYMPTOM IS THE RECOGNITION RULE, NOT THE CAUSE**: what a debugging author encounters is one column, two rows, two expected types; the instruction that saves them is DO NOT REPAIR FROM THE INHABITANCE ROW -- the compat row is what refused. Specimen, measured 2026-09-01 on gunbc c0a378c07be by calm-boar-314 and bold-carp-449 independently, on two binaries and two phases (`gunbc compile` emit-stage refusal and `gunbc run` entry-resolve), unrepaired at authoring. A module declaring `type String = FreeMonoid<Char>` and `fn takes_bare(s: String) -> Int`, called from a foreign module that IMPORTS the function, with a deliberately wrong `Int` actual so the diagnostic must name its destination, refuses with: `type mismatch: expected 'Primitive(String)', got 'Primitive(Int)'` AND `value does not inhabit its declared type at the direct call argument for parameter 's': declared 'Node(String<Product(Char)>)', produced 'Primitive(Int)'`. THE TWO PRODUCERS, read from source rather than inferred from message shape: `v1.compiler.infer direct_call_arg_mismatch_diags` renders the compat row from the formal as the CALLER environment resolves it, and `v1.compiler.infer declared_type_obligation_diags` renders the inhabitance row from `obligation.declared` through `declared_type_inhabitance`. Both reach `type_mismatch_error` and `DeclaredTypeNotInhabited` in `v1.compiler.core`, so the rendering is shared and the DIVERGENCE IS UPSTREAM OF IT -- which is why the two rows look like one mechanism disagreeing with itself. **THE TRIGGER IS TWO COMPETING BINDINGS LIVE IN ONE RESOLVING SCOPE, NOT THE IMPORT AS SUCH**, and this row states the narrower claim deliberately: the with/without-import pair is measured, but the two AGREEING cells agree for OPPOSITE reasons -- an un-imported foreign caller agrees at `Primitive(String)` because only the kernel binding is available, and an in-module caller agrees at `Node(String<Product(Char)>)` because only the local declaration is. Phrasing the trigger as the import would make a reader conclude the class does not reproduce when some other construct puts a second binding in scope. An explicit `import <module> \{ <fn> \}` is the ONLY construct measured to create the competition; whether any other does is UNMEASURED. Crossed arm, pre-registered before its log was read: removing the import moves ONLY the inhabitance row, from `Node(String<Product(Char)>)` to `Primitive(String)`, while the compat row is `Primitive(String)` under both -- so one producer follows the import binding and the other does not, rather than the whole reading shifting. RUNG FOUND AT: 1 (mitigatable) -- the line DOES stop, and stops located, so this is not silent wrongness; what fails is that the refusal MISDIRECTS the remedy, which is DESIGN section 5's requirement that a refusal be typed AND located read one layer deeper: located at the right column while naming the wrong destination. CEILING: 3 (structurally guaranteed) -- one resolution of a callee's declared type per call site, consumed by both producers, makes two destinations unconstructible. NEXT-RUNG TRIGGER, naming the capability rather than an artifact: a single resolved-formal authority at the call site that both the compat check and the inhabitance obligation READ, sufficient that no call-site refusal can render two different expected types for one parameter. Distinct from `meaning_fork`, which is one NAME carrying two meanings across scopes -- that is the underlying condition here and is separately rostered; this row is about two PRODUCERS disagreeing inside a single refusal, which is what makes the remedy wrong rather than merely the meaning ambiguous. Distinct from `diagnostic_name_mechanism_silent`: there the diagnostic names a mechanism that never ran; here both mechanisms ran and both reported faithfully about different environments. WHAT IS NOT CLAIMED, by either measurer: which producer is correct, and why they read the binding differently. No arm on either rig touches it, and the source reading above identifies the producers without settling which environment a call-argument formal SHOULD be resolved in.)" as NonEmptyStr,
evidence: [],
}

data instrument_output_read_as_subject_content: RecurringFailureMode = RecurringFailureMode {
identity: "instrument_output_read_as_subject_content" as NonEmptyStr,
authored: "**instrument output read as subject content** (a consumer derives a SET from a report whose completeness is a property of the REPORTING TOOL rather than of the subject. **The boundary against `execution_provenance_loss` is the whole justification for a separate row, because the two look identical at the call site and have opposite repairs**: there a value is consumed as though an observation produced it while nothing proves the observation path RAN, and the fix is to bind an execution receipt; here the observation ran and reported FAITHFULLY — the instrument answered its own question correctly — and what is wrong is that its output was complete for the REPORTER s purpose and was read as complete for the CONSUMER s. Provenance is intact; the SUBJECT is substituted, so no receipt binding can detect it and the repair is instead to derive the set from the subject itself. Distinct from `total_at_the_level_examined_blind`, which is a judgment shape (a match total over the type it examines, blind inside an arm), and from `reachability_read_as_occupancy`, which asks whether a quiet guard should exist; this is neither a match nor a guard. Specimen with a receipt, repaired on main by gunbc#9829: the required floor asked `extdeps.git` `git.Core.DiffUnified0` (`git diff -U0 <range>`) which lines a change touched, and `floor_diff_edits_from_line_ranges` attributed those lines to enclosing declarations to decide which witness identities the change established. Git prints only the hunks that DIFFER, so on a rename it prints the module line and whatever else moved — while every identity at the destination is a newly qualified `module.function` that has never executed under that spelling, because the authored module name moved with the file. **THE REASON IT SURVIVED IS THAT THE TWO ANSWERS COINCIDE BY ACCIDENT IN THE COMMON CASE**: for a wholly-added file every line is a `+` line, so line attribution reaches every declaration and the defect is invisible; it appears only when the instrument gets TERSE, which rename detection is. Measured over the window reachable in a shallow session clone — a floor on the population, not the population, since older renames are unmeasured — 8 of 8 rename-destination `.dag` files carrying test decls were under-enrolled and at least 87 of their 103 identities were never selected; a PURE MOVE with no content edit enrolled NOTHING. It was not merely a reporting gap: changed-witness membership is what OVERRIDES the cost-debt withhold and the outside-gate suppression, so the same miss on a rostered identity is a silent decline of a witness whose author is present, which is the state `v2.workflow.floor_changed_witness` `changed_witness_execution_standing` exists to red. The repair derives the set from the subject: a path `parse_unified_diff_added_paths` already rules new-at-path contributes the declarations THE FILE ITSELF PARSES TO, bounded to that file s own decl list and never the corpus, so it is the precise answer rather than an absorbing widen. Its discriminating red is `rename_destination_enrolls_every_test_decl_not_only_the_diff_touched_one`, which feeds the specimen s verbatim diff and FAILS when the rule is disabled, paired with `in_place_modify_enrolls_only_the_touched_test_decl`, which passes under both states so the first cannot be satisfied by widening. **Recognition rule, and it predicts well beyond git**: whenever a set is read out of a tool s output, ask whether that tool promised completeness over YOUR question or over its own — `--stat`, any de-duplicating or truncating reporter, and any porcelain that elides for human brevity all report faithfully and none of them promise the consumer s set. **Its near twin is `executed_conjunct_discriminates_nothing`, approached from the other side**: there the satisfied signal is EXECUTION -- the conjunct genuinely runs and is genuinely gated on -- while here it is COMPLETENESS RELATIVE TO THE REPORTER, which is why this class is not a reachability problem and looking for an unexecuted path finds everything healthy. In both, the axis the diligent reader checks already reads green, and checking it harder returns the same green.)",
Expand Down Expand Up @@ -259,4 +265,5 @@ data recurring_failure_mode_roster: List<RecurringFailureMode> = [
executed_conjunct_discriminates_nothing,
unbacked_execution_claim,
mitigation_injected_where_judgment_declined,
one_refusal_two_destinations,
]
Loading