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
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
module gunbc.recurring_failure_mode.generic_position_admits_a_foreign_constructor

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

data generic_position_admits_a_foreign_constructor: RecurringFailureMode = RecurringFailureMode {
identity: "generic_position_admits_a_foreign_constructor" as NonEmptyStr,

receipts: [
"a record literal whose constructor belongs to a DIFFERENT type than the position declares is REFUSED at a non-generic position and ACCEPTED at a generic one -- the value does not inhabit its declared type, which is the ordinary compiler floor DESIGN section 4b names, so this is a below-baseline safety regression and not a missing refinement. ",
"HARM: an ill-typed program is Accepted with no diagnostic of any kind. Nothing downstream re-asks the question, so the wrong constructor travels as though it had been judged. ",
"DISTINGUISHING FACTS: the type-mismatch judgment owns this fault and fires at a non-generic position -- a coproduct arm from another type, and a product spelling too, both refused naming expected and got. That judgment does not run when the declared position is a generic application. The asymmetry is the whole class: same fault, same spelling, opposite verdicts, decided by whether the position is generic. ",
"RUNG FOUND AT: OutsideTheLadder. Silent wrongness is not the ladder's bottom rung, it is outside it, and this is silent wrongness -- the program is Accepted and nothing is reported. ",
"MEASURED ON MAIN, so it is a BASELINE FLOOR HOLE and not a regression introduced by any branch: reproduced on origin/main at a29faba47f3 with gunbc compile over a single-source probe. The generic specimen emitted zero diagnostics; the non-generic control on the same tree emitted the type mismatch. The pair differs only in whether the declared position is generic. ",
"CEILING AND REASON: a wall. Membership of a constructor in a declared coproduct is decidable and fully grounded -- the declaration enumerates its arms -- so this is a wall-after-grounding class in DESIGN section 5's sense, waiting on its single authority rather than on any undecidable property. ",
"NEXT-RUNG TRIGGER: variant-membership judgment at generic positions exists, refusing a constructor whose owner is not the declared type, with discriminating controls in both directions -- an invalid same-shape generic literal that reds, and a VALID same-shape generic constructor that stays green, so that a mechanism which merely refuses everything generic cannot satisfy it. ",
"AUTHORITY IS THAT FUTURE JUDGMENT AND NOT THE MECHANISM CURRENTLY HOLDING THE GAP. RecordLitInstantiationUndetermined's FieldTemplateSelectionFailed arm is a COMPENSATING refusal: it happens to catch this specimen because it cannot establish a field template for it, which is a different question from membership. It was not designed for this class and earns no credit for it. ",
"REMOVAL PRECONDITION, and it is the reason this row exists rather than a note: that compensating decline MUST NOT BE DELETED BEFORE THE MEMBERSHIP WALL LANDS. Routing it to NotApplicable was executed on a branch and the ill-typed specimen compiled clean -- so a later cleanup measuring zero corpus firings and no reachable correct code would delete it and fail open on exactly this class, justified by reasoning that is otherwise sound. Once the membership wall independently refuses the wrong-owner fixture, rerun that deletion mutation; only if the specimen STAYS RED may the compensation be removed. AND ONE SPECIMEN IS NOT THE WHOLE BAR, so the population is enumerated here rather than described. The compensating arm is reached, with the declaration in hand, by exactly two conditions: a constructor named at the position that no candidate domain carries, and the many-owner case. The deletion must discharge EACH of those, showing it is covered by the new wall, independently refused, or unreachable -- not rerun the single fixture that happened to expose the hole. A third condition appearing later is then visibly a new member rather than a reinterpretation of this sentence. The discharge may well be small: the many-owner case has no established production reachability at all, and of the not-carried names, one whose spelling exists nowhere is already refused by the unresolved-name authority, leaving the foreign-owner case that the wall itself is built to refuse. That is the expected SHAPE of the discharge and not a prediction of its result. THE REMOVAL IS A DELETION, NOT A REROUTE. When the compensation goes, FieldTemplateSelectionFailed goes with it, along with any producer, message or consumer surface left orphaned -- leaving the cause standing in RecordLitUnavailableCause, or mapping it to a quieter fallback to preserve the shape, discharges the bar by making the arm silent rather than by making it unnecessary. AmbiguousVariantOwners may survive that deletion independently, because the selector's many-arm control still requires it; its survival is not an incomplete deletion. AND THIS ROW IS UPDATED WHEN THE WALL LANDS, NOT ERASED. A resolved failure mode is the record of a climb: the rung moves off OutsideTheLadder to whatever the membership judgment's executed evidence earns, and the deletion change records both that the compensation is gone and that the original specimen is still refused without it. Deleting the row would erase the only account of why the compensation existed. ",
],

evidence: [],
}
2 changes: 2 additions & 0 deletions dag/gunbc/recurring_failure_mode/roster.dag
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import std.types { List }
import gunbc.recurring_failure_mode { RecurringFailureMode }
import gunbc.recurring_failure_mode.a_type_name_asserts_an_algebra_the_arithmetic_does_not_carry { a_type_name_asserts_an_algebra_the_arithmetic_does_not_carry }
import gunbc.recurring_failure_mode.censored_estimator_drops_its_own_tail { censored_estimator_drops_its_own_tail }
import gunbc.recurring_failure_mode.generic_position_admits_a_foreign_constructor { generic_position_admits_a_foreign_constructor }
import gunbc.recurring_failure_mode.selection_view_read_as_population { selection_view_read_as_population }
import gunbc.recurring_failure_mode.unlanded_citation_indistinguishable_at_the_citing_end { unlanded_citation_indistinguishable_at_the_citing_end }
import gunbc.recurring_failure_mode.hollow_alias { hollow_alias }
Expand Down Expand Up @@ -153,6 +154,7 @@ import gunbc.recurring_failure_mode.one_disposition_defined_jointly_by_independe
data recurring_failure_mode_roster: List<RecurringFailureMode> = [
a_type_name_asserts_an_algebra_the_arithmetic_does_not_carry,
censored_estimator_drops_its_own_tail,
generic_position_admits_a_foreign_constructor,
selection_view_read_as_population,
unlanded_citation_indistinguishable_at_the_citing_end,
hollow_alias,
Expand Down
4 changes: 4 additions & 0 deletions src/v1/00_core.dag
Original file line number Diff line number Diff line change
Expand Up @@ -303,6 +303,7 @@ type CompilerDiagnostic
| MethodNotFound { method: String, receiver_type: String, span: SourceSpan }
| MethodExistenceUndecided { method: String, receiver_type: String, span: SourceSpan }
| MethodExistenceFrontierAdmitted { method: String, receiver_type: String, trigger: String, span: SourceSpan }
| RecordLitInstantiationUndetermined { declared: String, cause: String, span: SourceSpan }
| ReceiverTypeUnestablished { method: String, span: SourceSpan }
| FrontierOccurrenceBudgetExceeded { method: String, receiver_type: String, declared: Int, observed: Int, span: SourceSpan }
| MissingField { field: String, type_name: String, span: SourceSpan }
Expand Down Expand Up @@ -520,6 +521,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan {
MethodNotFound { method: _, receiver_type: _, span: s } => s
MethodExistenceUndecided { method: _, receiver_type: _, span: s } => s
MethodExistenceFrontierAdmitted { method: _, receiver_type: _, trigger: _, span: s } => s
RecordLitInstantiationUndetermined { declared: _, cause: _, span: s } => s
ReceiverTypeUnestablished { method: _, span: s } => s
FrontierOccurrenceBudgetExceeded { method: _, receiver_type: _, declared: _, observed: _, span: s } => s
MissingField { field: _, type_name: _, span: s } => s
Expand Down Expand Up @@ -591,6 +593,7 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
MethodNotFound { method: m, receiver_type: t, span: _ } => concat("method '", m, "' not found on receiver type '", t, "'")
MethodExistenceUndecided { method: m, receiver_type: t, span: _ } => concat("method '", m, "' cannot be resolved: receiver type '", t, "' establishes no method surface, so the method's existence is not established and no declared frontier row admits it")
MethodExistenceFrontierAdmitted { method: m, receiver_type: t, trigger: tr, span: _ } => concat("method '", m, "' on receiver type '", t, "' is admitted by a declared unresolved-method frontier row; dissolves on: ", tr)
RecordLitInstantiationUndetermined { declared: d, cause: c, span: _ } => concat(concat(concat("cannot select the field template for this record literal: the position is rendered '", d), concat("'. The fields are NOT judged here, because judging them would mean comparing values against a template that was never established -- so this says nothing about whether the fields are correct. It does NOT clear the literal: a constructor belonging to a different type than the position expects arrives here too, and at a generic position no other check judges it. Cause: ", c)), "")
ReceiverTypeUnestablished { method: _, span: _ } => "the receiver's own type was never established, so nothing is known about the method's existence here; this is an upstream type-propagation deficit, not a fact about the method"
FrontierOccurrenceBudgetExceeded { method: m, receiver_type: t, declared: _, observed: _, span: _ } =>
concat(concat(concat("the declared frontier row for '", m), concat("' on receiver type '", t)), "' no longer matches what this module contains: its declared occurrence count and the count observed here differ, and both numbers are carried on this diagnostic. If MORE were observed, a new unresolved call has appeared and the receiver's type should be established rather than the count raised. If FEWER were observed, the deficit has partly dissolved and the row must be lowered or deleted so the ratchet keeps its new ground. The count is an equality, not a ceiling, in both directions.")
Expand Down Expand Up @@ -792,6 +795,7 @@ fn diagnostic_disposition(d: CompilerDiagnostic) -> DiagnosticDisposition {
EqualityMemberUnjudgeable { type_name: _, member: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
TypeArgumentArityMismatch { type_name: _, supplied: _, declared: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
OccurrenceTransportViolation { refusal: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
RecordLitInstantiationUndetermined { declared: _, cause: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
ContainerSpellingUnrecognized { name: _, container_leaf: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
ServiceConfigReferenceJudgmentDeferred { field: _, referenced_name: _, trigger: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateAdvisoryTypecheck }
TransportEmissionNotModeled { transport_kind: _, service: _, operation: _, declaring_module: _, target: _, missing_realization_fact: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
Expand Down
Loading