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,20 @@
module gunbc.recurring_failure_mode.direct_generic_application_admits_a_distinct_phantom_argument

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

data direct_generic_application_admits_a_distinct_phantom_argument: RecurringFailureMode = RecurringFailureMode {
identity: "direct_generic_application_admits_a_distinct_phantom_argument" as NonEmptyStr,
receipts: [
"HARM: a direct call accepts a value with a different phantom type argument from its declared parameter. The runtime fields agree, but the declared type identities do not. This is the values-inhabit-declared-types floor of DESIGN section 4b. ",
"MEASUREMENT: origin/main at 03a3b91fb4c1ea7e408df2cb484f475d75080a7f, BuildBuddy invocation 5e149d38-87ae-483c-a249-b1dbb54babb1. The one-source v1-to-Rust fixture declares type First, type Second, type Record<P> { n: Int }, fn take(q: Record<First>) -> Int { q.n }, and fn probe(q: Record<Second>) -> Int { take(q: q) }. It resolves one source, emits six files, and reports zero diagnostics. ",
"SPEAKING CONTROL: on the same baseline binary, spelling the two positions through FirstRecord = Record<First> and SecondRecord = Record<Second> refuses TypeMismatch. A matching alias passed to a generic Record<P> parameter completes with zero diagnostics. The distinction is therefore enforced for these alias spellings but absent for the direct applications. ",
"MECHANISM, DISCRIMINATED: invocation 3abd8f6f-db2c-491a-9dc4-b06d8017b8df shows ResolvedFormal.declared_type and the raw actual retain First/Second; only the older conformance consumer receives Product(Record)/Product(Record). Invocation 2a450014-5839-4264-bdc8-8ded09b39871 enters the successor applied_type_argument_conflicts for both marker shapes. Adding fields to First and Second yields two DeclaredTypeNotInhabited diagnostics; the bare pair still emits zero. The existing declaration-reference lookup identifies both bare declarations exactly, but applied_type_argument_identity_known requires structure and abstains. Both instrumented builds were throwaway hand-edited-mirror probes, restored, not generated implementation artifacts. ",
"RUNG FOUND AT AND CURRENT RUNG: OutsideTheLadder. This row records an executed silent acceptance, not a completed repair. The ceiling is structural refusal derived from constructor identity and all applied arguments. ",
"NEXT-RUNG TRIGGER: the existing successor uses established declaration identity to distinguish bare markers, with declaration-bound application ownership preserved through alias routing at the direct-call declared position, with an executed negative for distinct arguments, positives for equal arguments and equivalent aliases, and a mutation that reopens the acceptance. A rendered type name or a diagnostic variant is not this evidence. ",
"CORPUS INTENT: std.measure declares PerSecond, PerMinute, PerHour, PerMonth, and Once as bare types, and states that billing unit is part of the fact. The fixture reproduces that marker shape, but a direct MoneyRate<PerMinute>/MoneyRate<PerHour> corpus-import fixture has not yet been measured; this row does not turn source similarity into execution evidence. ",
"RELATED CLASS: gunbc.recurring_failure_mode.generic_position_admits_a_foreign_constructor records a foreign owner admitted at a generic position because a generic declaration was classified as callable. This row concerns different applications of the SAME owner; repairing that guard alone leaves this specimen accepted. ",
"WHY EXISTING GREEN EVIDENCE DID NOT COVER THIS: test.claim.phantom_marker_type_argument_identity_witness tests distinct marker rendering and preservation across outer renderers. It does not ask whether a value with one argument is refused at a position declaring another. Its rendering claims remain valid and need an inhabitance sibling, not replacement. Its markers are coproduct variants; this measured fixture uses bare marker declarations, so no production-path coverage of the variant shape is claimed here. ",
],
evidence: [],
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
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. An advisory trace inside structured_application_site_type_mismatch_with_peeled on 03a3b91fb4c1 proves that the judgment runs for BOTH arms. Its type_node_is_callable guard tests parameter presence and therefore excludes the exposed generic declaration; it answers wrongly rather than lacking an incoming edge. The asymmetry is the whole class: same fault, same spelling, opposite verdicts, decided by whether the position is generic. ",
"RELATED CLASS: gunbc.recurring_failure_mode.direct_generic_application_admits_a_distinct_phantom_argument records distinct applications of the same owner accepted at a direct-call parameter. The Arrow guard alone leaves that second baseline fixture accepted. ",
"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: [],
}
1 change: 1 addition & 0 deletions dag/gunbc/stage0/stage0_crate_partition_generated.dag
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ data generated_partition_crate_rows: List<GeneratedPartitionCrateRow> = [
"std_coercion",
"extdeps_currency_currency",
"std_decl_ref",
"std_type_application",
"std_keyed_row",
"std_keyed_roster",
"std_roster_frontier",
Expand Down
30 changes: 30 additions & 0 deletions dag/std/type_application.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
module std.type_application

import std.decl_ref { DeclarationRef }
import std.types { List }

// An application is its declaring owner together with its ordered arguments.
// Arguments are a parameter because a compiler can carry substitutable syntax
// before it has ground arguments. Neither the owner alone nor the runtime
// fields identify an application: phantom arguments remain part of this fact.
// The producer establishes owner in the declaration's context. A consumer must
// not replace it with a lookup of the same spelling in the consumer's context.
// An owner with no parameters has the same representation with arguments: [].
// Consumers that require a generic application decide that from its arity.
type TypeApplication<Argument> {
owner: DeclarationRef
arguments: List<Argument>
}

// Alias-head traversal is a different relation from recursive application
// arguments. A repeated owner witnesses only a cycle along the alias-head path;
// Loop = Record<Loop> does not revisit a head on that path. Preserve the path and
// repeated declaration so consumers cannot confuse malformed traversal with an
// application that this exposure did not establish.
type TypeApplicationResolution<Argument>
= TypeApplicationResolved { application: TypeApplication<Argument> }
| TypeApplicationUnexposed
| TypeApplicationAliasHeadCycle {
path: List<DeclarationRef>
repeated_owner: DeclarationRef
}
Loading
Loading