Repository navigation
record-literal constructor domains: candidates with routes, not one canonical node - #10473
gunbai-bot[bot] wants to merge 15 commits into
Conversation
The child was branched from the parent, so it carried 54 of the parent's files and could not be reviewed or landed independently of it. This reconstructs the cut from origin/main and keeps only its own material. Its one real dependency on the parent was borrowing OptionalNarrowingUndetermined to report the decline. #10187's own body argues that borrowing is wrong -- ONE VARIANT MAY NOT ANSWER FOR TWO CAUSES -- so the dependency is discharged by construction rather than by sequencing: RecordLitInstantiationUndetermined is declared here, and it names the check's own deficit rather than a defect at the position. Pre-rebuild head is c85792a045950d5ae0ad59b25837ad9f10b70ed0, retained as tag child-pre-rebuild. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
gunbai-bot
Bot
changed the title
…ompile_clean The build lane refused c3b17e9 for generated surface drift over five mirrors (compiler_tests.rs, std_measure.rs, v1_compiler_compiler_tests_rust.rs, v1_compiler_infer.rs, v1_std_core.rs) -- the carriers had moved and the projections had not. Declaring RecordLitInstantiationUndetermined also obliges its total consumers. compile_clean's histogram matches over CompilerDiagnostic are deliberately total ("no silent widening"), so each gets an explicit arm rather than a catch-all; the histogram name is the `declared` type, which is the position's identity. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
… and dedup owners by declaration
Two repairs in the record-literal instantiation authority, both on the axis this
PR is about.
1. The arity guard compared decl.params against exp.children. That is right when
exp is an APPLIED type node, whose children are the supplied type arguments.
It is wrong once a route has resolved exp to the owner's coproduct body, where
children are the VARIANTS -- so `Cons { head: prefix, tail: Empty {} }` at a
List<String> position was refused because FreeMonoid declares 1 parameter and
has 2 variants. 122 corpus sites refused with nothing wrong with any of them.
The comparison is inherited from the pre-split cascade, where it returned a
bare `none` that the legacy path absorbed silently; typing the result is what
made it visible. The answer is NotApplicable, not Unavailable: no application
happened at that position, so instantiation does not ARISE there.
It also closes a silent wrong answer no count would have shown: where a type's
parameter count HAPPENED to equal its variant count, the old code proceeded and
substituted a variant node in for the type parameter. Green, for the wrong
reason.
unique decline sites 122 -> 10
unique blocking sites 194 -> 80
genuine arity error still refused upstream (TypeArgumentArityMismatch)
unresolved-name literal still declines
2. expected_domain_push's comment claimed deduplication by owner IDENTITY while
the predicate compared owner_name, a String. Two distinct owners sharing an
authored name collapsed before the many-owner fold could see them -- deciding
the ambiguity the fold exists to refuse. Identity is now the declaration's
source span; owner_name survives as the reporting label only.
GenericArityDisagreement is kept rather than deleted, with its disposition
recorded at the declaration: it has no observed population, an authored arity
error never reaches it, and the cause carries no rung of its own.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
# Conflicts: # src/v1/stage0/src/compiler_tests.rs # src/v1/stage0/src/v1_compiler_infer.rs
…sified tests The floor lane refused on ChangedWitnessObservationFailed: one decline at src/v2/compiler/body_producer_forward.dag:34:3 broke changed-witness attribution. There is no threshold there -- one hard diagnostic is fatal -- so the remaining declines had to go to zero or become declared drops. Enumerated, all ten were the same shape: `Cons`/`Empty` at a List<X> position, rendered 'Coproduct(FreeMonoid)', every one correct code that main compiles cleanly. Instrumenting the selector showed why: at such a position the routes produce exactly ONE candidate, the element type, and no FreeMonoid candidate at all. The selection could not find the constructor and reported that miss as though the declaration were unlookupable. So VariantNotFound is NotApplicable, not Unavailable. The routes not reaching an owner is a fact about this authority, not about the program, and withholding the legacy fallback there turned a blind spot into a blocking accusation. The refusal for an unknown name stays where it belongs, at UnresolvedType -- verified by execution, not assumed. DeclarationLookupUnavailable had no remaining raise site and is deleted. unique decline sites 122 -> 0 unique blocking sites 194 -> 75 Two tests are retired because this measurement FALSIFIED them, not because they became inconvenient: the both-owner cell asserted the List<Colour> shape emits one ambiguity and its prose called that state authorable. The instrumented candidate list shows one candidate, so the assertion could never hold and the prose was false. the outer-only cell asserted only that zero ambiguities appear -- satisfied by a completely dead route, so it could not fail for the reason it existed. What replaces them asserts a discriminating PAIR: the element route selects, and a source differing by one identifier is refused, so neither arm can go vacuous alone. The dedup comment's own example is corrected in place and marked as having been false: it claimed a List<T> position reaches FreeMonoid by two routes. It does not. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
Three remaining producers of InstantiationUnavailable, three verdicts, each from
a measurement rather than from the shape of the code.
FieldTemplateSelectionFailed -- KEPT, it is production-authorable. Ordinary
authored source reaches it through the real inference seam:
type Out<T> = | Acc { value: T } | Rej
type Other = | Zed { q: Int }
type Holder { r: Out<Int> }
fn probe() -> Holder { Holder { r: Zed { q: 1 } } } -> declines, this cause
with a control differing by ONE identifier -- `Acc` for `Zed` -- that stays
silent, so neither half passes vacuously. Enrolled as
a_field_template_that_cannot_be_selected_declines_from_authored_source. This is
what keeps the typed decline a refusal a user can actually see rather than a
diagnostic surface nothing reaches.
GenericArityDisagreement -- DELETED, along with the comment defending it. A real
arity error never arrives at that comparison: TypeArgumentArityMismatch refuses
it upstream and names both counts. I had kept it in case that wall were later
narrowed; that is a second authority over one fault, insured against a
hypothetical, and if the upstream wall narrows it is that wall's own controls
that must red. An unreachable check is deleted, not insured.
AmbiguousVariantOwners -- kept as the selector's forced >1 residue. A fold over
a carrier admitting many candidates must answer for many, and refusing is the
only non-fabricating answer. It earns no production-coverage credit.
The manually-constructed unavailable test is annotated as UNIT EVIDENCE ONLY: it
proves the consumer refuses the fallback for a constructed Unavailable, and says
nothing about production reach. It now names the cell that does carry that reach.
corpus after: 0 declines, 75 blocking sites -- unchanged by the deletion
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
…e message clearing the literal Routing FieldTemplateSelectionFailed aside and recompiling turned up something worse than the wording bug it was meant to check: 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 Measured on origin/main at a29faba, with the non-generic control refused on that same tree -- so it is a BASELINE FLOOR HOLE, not anything this branch caused, and the control is what makes the zero readable rather than merely absent. A value that does not inhabit its declared type is the ordinary compiler floor, so the rung is OutsideTheLadder: the program is Accepted and nothing is reported. Filed as gunbc.recurring_failure_mode.generic_position_admits_a_foreign_constructor, whose authority is the FUTURE generic-position variant-membership judgment. This PR's decline is recorded as the compensating mechanism that happens to hold the gap and earns no credit for it. The row exists mostly for its removal precondition. This decline is now load-bearing for a class it was not designed for, so a later cleanup measuring "zero corpus firings, unreachable by correct code" would delete it and fail open -- justified by reasoning that is otherwise sound, and with nothing left to object. The wall must land first, and the deletion mutation must be rerun against the specimen, which must stay red. The diagnostic no longer asserts the condition is "NOT a defect in the code at this position". That was true of every decline measured before -- the ten List<X> cases were correct code and the disclaimer protected them -- and false for this one. It now says the fields are not judged, that this says nothing about whether they are correct, and that it does NOT clear the literal. 7' lands with it: the selector's 0/1/many decision is extracted as a pure helper so the control feeds the fold directly rather than manufacturing source. Both mutations were RUN, not argued -- many->first and many->last each red it independently, because the assertion names both owners rather than counting them. It carries no production-coverage credit and says so. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
The compensating arm is reached whenever a template cannot be selected WITH the declaration in hand -- a constructor no candidate carries, and the many-owner case both land there. My earlier note routed the not-found case to NotApplicable only on the path where the declaration could not be looked up, so the cause retains jobs beyond the floor class this row is about. A future deletion must therefore enumerate that population and show each member still refused. Rerunning the single fixture that exposed the hole would clear the bar while leaving the rest of what the arm quietly does uncovered. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
A phrase is arguable; a list is checkable. With the declaration in hand the compensating arm is reached by exactly two conditions -- a constructor no candidate domain carries, and the many-owner case -- so the row names both, and a third appearing later is visibly a new member rather than a rereading of the sentence. The bar is also stated as a discharge rather than as research: each member covered by the new wall, independently refused, or unreachable. The likely shape is recorded without pre-deciding it -- the many-owner case has no established production reachability, and a name that exists nowhere is already refused by the unresolved-name authority. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
Two ways the removal bar could be discharged without being met: leaving FieldTemplateSelectionFailed standing as a dead cause, or mapping it to a quieter fallback to preserve the shape. Both make the arm silent rather than unnecessary, which is the disposition refused earlier when GenericArityDisagreement was deleted with its defending comment rather than kept inert. The row now says the cause is deleted along with whatever surface is orphaned, and names AmbiguousVariantOwners as legitimately surviving so its survival is not read as a half-deletion. It also says the row is UPDATED when the wall lands rather than removed as resolved. A resolved failure mode is the record of a climb, and deleting it would erase the only account of why the compensation existed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
…orrection of it The comment claimed a List<T> position reaches FreeMonoid by two routes. I replaced that with the flat claim that no route produces a FreeMonoid candidate at all, and the replacement was wrong in the more dangerous direction: deleting the AliasTarget push declines nine production positions that compile today. I had measured the flat claim on a probe whose element type carried the constructor, where the element route supplies a match and AliasTarget is never needed. The candidate list showed one entry and I read a property of that position as a property of the routes. Both the original error and my correction of it are kept in the comment rather than the file being quietly flipped back. What stays genuinely open is the original's other half -- whether two routes ever reach ONE owner at a single position, which is what the dedup exists to collapse. Nine sites prove AliasTarget supplies an owner ALONE; none shows a second route reaching the same one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
Adding the row module declares the row; it does not enrol it. The rostered-row-join phase refused with RecurringFailureModeRows declared=135 against rostered_names=137, which is that phase doing exactly its job: a failure-mode row no roster ranges over is a row no wall will ever see. Enrolled in both places the roster carries a row -- the import block and the all-rows list -- and docs/design-failure-modes.md regenerated through generated_artifact_gate main_wet rather than hand-edited. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES on exact head ec1a9e1. CI is green on this head; 7' is CLOSED by source inspection. Remaining bar:
-
R1 — THE TYPED MANY-OWNER RESULT IS COLLAPSED AGAIN DOWNSTREAM.
record_lit_variant_selectioncorrectly returnsVariantAmbiguous { owners }, butrecord_lit_instantiation_template_fieldsprojects bothVariantNotFoundandVariantAmbiguous { owners: _ }to the samenone. Its caller then maps thatnonetoInstantiationUnavailable { cause: FieldTemplateSelectionFailed }. Thus if the >1 state ever becomes production-reachable through a resolved generic application, the owner census is lost and the typed ambiguity becomes the generic template-selection failure. That is the same optional-as-verdict/state-space-conflation class this PR is repairing, one seam later. Preserve the distinction through template selection — e.g. a typed template-selection result — so ambiguity reachesAmbiguousVariantOwners { owners }. Unit evidence is sufficient at the current honest reachability rung; do not claim production coverage. -
R2 — ROUTE ATTRIBUTION IS NOT YET COMPLETE/CONSISTENT WITH THE BODY. The live body still says
WholeExpectedTypeis unestablished, while the newer deletion measurement reports removing it produces 30 declines. Update the body and retain that route if that measurement is the accepted result. Complete the single-route deletion mutations forNominalOptionalWrapperandCardinalityOptionalWrapper. Do not derive either population by 45-30. If both single-route mutations are zero, the covering-pair mutation withoutWholeExpectedTypeis the right next discriminator. A zero diagnostic delta is only 'not solely load-bearing'; check selector/owner standing so 0->0 cannot hide a changed answer. -
R3 — THE SIX ORIGINAL GENERIC VARIANT SITES STILL NEED SUBJECT ATTRIBUTION. For the six
Accepted { value: optional_present(...) }positions that inverted the landing order, establish by exact site identity whether #10473's expected-constructor-domain authority supplies the instantiated field template or whether the legacy fallback still does. A blocking-count delta is not this receipt. This is the causal edge that makes #10473 a prerequisite of #10187, so it needs to be observed rather than inferred from the combined green. -
R4 — RE-RUN THE BASE/HEAD SITE-IDENTITY JOIN ON THE CURRENT BASE. With declines now zero, the remaining comparison is weaker but still needed: no unrelated blocking population was introduced while the intended population moved. Record introduced/removed identities rather than only aggregate 194/75-style counts.
-
R5 — CLEAN THE STALE COVERAGE PROSE.
ct_record_lit_domain_selection_testsstill carries the old comment that the fixture 'AUTHORS the both-owner case'. The current 7' correctly uses a synthetic unit shape and explicitly carries no production-coverage credit. Make the surrounding source comment say the same thing; otherwise the source still claims the rung the test deliberately refuses to claim.
No objection to the baseline floor-hole row or its compensation/removal precondition on this head. No merge authorization is implied by this review.
…ot collapse
record_lit_instantiation_template_fields returned List<Node>?, so VariantNotFound and
VariantAmbiguous { owners } both became `none`, and the caller mapped that common `none`
to FieldTemplateSelectionFailed. The owner census this authority exists to produce died
one seam after it was built.
Repaired by construction rather than by a check: TemplateFieldSelection has no arm both
causes can occupy, so the collapse is unwritable rather than validated. The consumer maps
TemplateFieldsUnavailable { cause: c } -> InstantiationUnavailable { cause: c }.
Also corrects a comment that claimed the source-level fixture AUTHORS the both-owner case.
It does not reach the many-owner arm -- that was measured -- and the comment now says the
synthetic cell is where the arm is covered and that authored-source reach is unestablished.
Regen fixed point at gen 3, 0 declines, RC=0. Seed unit tests 774 passed / 0 failed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
# Conflicts: # docs/design-failure-modes.md # src/v1/stage0/src/compiler_tests.rs # src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs # src/v1/stage0/src/v1_std_core.rs
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 91a0965cc7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| run_fixture_closure_discrimination, run_function_value_adapter_discrimination, | ||
| run_nested_refinement_cast_discrimination, run_phantom_marker_identity_discrimination, | ||
| FixtureClosureOutcome, | ||
| run_nested_refinement_cast_discrimination, FixtureClosureOutcome, |
There was a problem hiding this comment.
Any library test build now fails before running tests: compiler_tests.rs still calls crate::cli_run::run_phantom_marker_identity_discrimination, but this hunk removes that helper from the test-only re-export and the commit also deletes its implementation. I confirmed this with cargo test -p v1-compiler --lib --no-run, which reports E0425 at compiler_tests.rs:799; restore the helper or remove/update the generated test that calls it.
Useful? React with 👍 / 👎.
| let mut names: Vec<String> = entries | ||
| .filter_map(|e| e.ok()) | ||
| .filter_map(|e| e.file_name().into_string().ok()) | ||
| .collect(); |
There was a problem hiding this comment.
When ReadDir fails while advancing, an entry name is not UTF-8, or a name contains the newline delimiter, these filter_map calls either silently discard the entry/error or encode one filename as multiple listing rows, yet the operation returns success: true. Consumers use non-membership in this listing to establish filesystem absence, so a partial enumeration can produce false absences, while a newline-bearing filename can fabricate a presence; retain the fail-closed collection path rather than dropping these cases.
Useful? React with 👍 / 👎.
| } | ||
|
|
||
| // THE DECLARED-VERSUS-ROSTERED IDENTITY JOIN RIDES THE SAME INGESTION, for | ||
| // the same reason the two joins above do: the roster half is a membership | ||
| // fact readable only from the parse this phase has already performed, and a | ||
| // corpus-wide job per question is what DESIGN §6 refuses. The declared half | ||
| // is read through the `data_decl_type_facts` producer — the same walk the | ||
| // `v2.std.decl_index` builtin marshals, not a second derivation of it. | ||
| // | ||
| // IT LIVES IN THE LANE THE PARSE PHASE LIVES IN, whichever that is: it is a | ||
| // rider, not a phase, so `RequiredCiPhase::Parse`'s lane ownership answers for | ||
| // it and no second routing fact exists to drift. No job is added; the roster of | ||
| // required jobs is closed to growth, and this check belongs to a phase that | ||
| // already exists. | ||
| match v1_compiler::cli_run::rostered_row_join::run_rostered_row_join( | ||
| &sweep.index, | ||
| ) { | ||
| Ok(report) => { | ||
| // A GREEN NAMES ITS DENOMINATORS, per row type: declared, rostered | ||
| // and CHECKED, so a subject that narrowed is legible from the log | ||
| // rather than only from the verdict. | ||
| eprintln!( | ||
| "required-ci: rostered-row-join sources_accounted={} controls_fired={}", | ||
| report.sources_accounted, | ||
| report.control_findings.len() | ||
| ); | ||
| for counts in &report.counts { | ||
| eprintln!( | ||
| "required-ci: rostered-row-join {} population_of_type={} excluded_other_carrier={} declared={} rostered_names={} checked={} fixture_home={}", | ||
| counts.row_type, | ||
| counts.population_of_type, | ||
| counts.excluded_other_carrier, | ||
| counts.declared, | ||
| counts.rostered, | ||
| counts.checked, | ||
| counts.fixture_home, | ||
| ); | ||
| } | ||
| for finding in &report.control_findings { | ||
| eprintln!( | ||
| "required-ci: rostered-row-join CONTROL {}", | ||
| finding.rendered() | ||
| ); | ||
| } | ||
| for finding in &report.findings { | ||
| eprintln!( | ||
| "required-ci: rostered-row-join FAIL {}", | ||
| finding.rendered() | ||
| ); | ||
| } | ||
| if !report.findings.is_empty() { | ||
| phase_failures.push(format!( | ||
| "rostered-row-join ({} finding(s))", | ||
| report.findings.len() | ||
| )); | ||
| } | ||
| } | ||
| // NO VERDICT IS NOT A GREEN. The declared population being unobtainable | ||
| // stops the line under its own name rather than being reported as a | ||
| // clean join over nothing. | ||
| Err(e) => { | ||
| eprintln!("required-ci: rostered-row-join NOT EVALUATED — {e}"); | ||
| phase_failures.push( | ||
| "rostered-row-join (declared population unobtainable)".to_string(), | ||
| ); | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
When a new top-level data row is omitted from its corresponding roster, the parse phase now ends without invoking run_rostered_row_join, and this commit also stops compiling the otherwise still-present cli_run/rostered_row_join.rs module. Consequently required CI reports no failure for unrostered declarations, silently removing the enforcement that prevents newly added failure-mode and guarantee rows from disappearing from their projections.
Useful? React with 👍 / 👎.
| CompilerDiagnostic::WhereRefinementUnenforced { | ||
| predicate, reason, .. | ||
| } => format!("{predicate}: {reason}"), | ||
| CompilerDiagnostic::WhereRefinementUnenforced { predicate, .. } => predicate.clone(), |
There was a problem hiding this comment.
When the same refinement predicate is deferred for different reasons, keying only on predicate merges those distinct failure classes into one compile-clean histogram bucket. Fixing one evaluator gap can therefore leave the aggregate row looking unchanged or partially improved without revealing which reason remains, corrupting the burn-down measurement; keep the reason in the key as the parent implementation did.
Useful? React with 👍 / 👎.
1 participant
Record-literal instantiation: what this PR actually establishes
This started as a candidates-and-routes authority for selecting the field template of a
record literal. Measuring it changed what it claims. Two of its original claims did not
survive their own evidence and are withdrawn below rather than defended.
What it repairs, measured
The arity misfire. The guard compared a declaration's parameter count against
exp.children. That is correct whenexpis an applied type node, whose children are thesupplied type arguments — and wrong once a route has resolved
expto the owner's coproductbody, where children are the variants. So
Cons { head: prefix, tail: Empty {} }at aList<String>position was refused becauseFreeMonoiddeclares 1 parameter and has 2variants. 122 sites refused with nothing wrong with any of them.
The comparison was inherited from the pre-split cascade, where it returned a bare
nonethat the legacy path absorbed silently. Typing the result is what made it visible.
It also closed a silent wrong answer no count would have shown: where a type's parameter
count happened to equal its variant count, the old code proceeded and substituted a
variant node in for the type parameter — green, for the wrong reason.
Positions these routes cannot reach are no longer accused. All ten survivors were one
family:
Cons/EmptyatList<X>positions, every one correct code.VariantNotFoundisnow
NotApplicable— the routes failing to reach an owner is a fact about this authority,not about the program. The refusal for an unknown name stays at
UnresolvedType, verifiedby execution.
Dedup compares declarations, not spellings. The comment claimed owner identity while the
predicate compared
owner_name, aString, so two distinct owners sharing a name collapsedbefore the many-owner fold could see them — deciding the exact question the fold exists to
refuse. Identity is now the declaration's source span.
One cause no longer stands for two.
RecordLitInstantiationUndeterminedis this PR'sown diagnostic rather than a borrowed one. Its message states that the fields are not
judged and that this says nothing about whether they are correct — it deliberately does
not clear the literal, because a constructor belonging to a different type arrives here
too. An earlier wording claimed the condition was the check's own deficit and "not a defect
in the code at this position"; that was measured false for one cause and is gone.
A baseline floor hole this PR did not cause, and now compensates
Routing the decline aside and recompiling showed something worse than a wording bug:
type mismatch: expected 'Coproduct(A1)', got 'Coproduct(B1)'Reproduced on
origin/mainata29faba47f3, so it is a baseline floor hole, not aregression from this branch. A value that does not inhabit its declared type is the ordinary
compiler floor, so this sits outside the guarantee ladder — silent wrongness — and is filed
as
gunbc.recurring_failure_mode.generic_position_admits_a_foreign_constructor.FieldTemplateSelectionFailedcurrently catches that specimen by accident — it cannotestablish a field template, which is a different question from membership. That makes this
branch strictly safer than main on the measured specimen, and it makes the decline
load-bearing for a class it was not designed for:
Corrected, on measurement
The outer-constructor claim stands, and is now demonstrated by deletion. It was
withdrawn earlier in this PR's history on a probe whose element type happened to carry the
constructor; that withdrawal was wrong and the correction is recorded here rather than
quietly reverted. Removing the
AliasTargetpush and recompiling the corpus:AliasTargetremovedCoproduct(FreeMonoid), nine distinct positionsAll nine are in
dag/extdeps/languages/rust/capabilities.dag, of the shapewhere
ConsisFreeMonoid's constructor reached throughList's alias and the elementtype does not carry it.
AliasTargetis the unique route that can supply the owner, so theroute is load-bearing and its population is demonstrated rather than asserted.
The other three routes are not established.
WholeExpectedType,NominalOptionalWrapperandCardinalityOptionalWrapperhave no such demonstration, and adeletion mutation per route is the way to settle each.
The typed decline, scoped honestly
InstantiationUnavailableis fail-closed when produced, and the current corpus produceszero such declines. That is a capability statement, not a corpus repair, and it is only
worth making because one ordinary cause is genuinely reachable from authored source:
FieldTemplateSelectionFailed— kept, and the honest reason is narrower than"production-authorable": ordinary correct code does not reach it, which is why the corpus
count is zero. A defective program reaches it, and nothing else refuses that program.
Carried by a paired control whose two sources differ by one identifier and land on opposite
sides — the valid same-shape generic constructor is the adversarial arm, so a mutation that
simply refused every generic position could not satisfy it.
GenericArityDisagreement— deleted. A real arity error is refused upstream byTypeArgumentArityMismatch; keeping this was a second authority over one fault, insuredagainst a hypothetical narrowing. If that wall narrows, its own controls must red.
AmbiguousVariantOwners— the selector's forced>1residue. A fold over a carrieradmitting many candidates must answer for many, and refusing is the only non-fabricating
answer. It earns no production-coverage credit; no source program has been found that
presents two matching candidate domains, and no wall is credited for that absence.
Evidence
the_element_route_selects_and_a_name_no_route_reaches_declines— a discriminating pair.a_field_template_that_cannot_be_selected_declines_from_authored_source— the productionreach of the decline arm.
an_unavailable_instantiation_refuses_the_legacy_fallback_and_is_judged— unit evidenceonly, annotated as such: it proves the consumer handles a constructed value, not that
production can produce one.
Two earlier tests were retired because measurement falsified them: one asserted an
ambiguity its own source cannot express, the other asserted only an absence and would have
been satisfied by a completely dead route.
Ordering
Supersedes #10442, rebuilt on
main(pre-rebuild headc85792a045950d5ae0ad59b25837ad9f10b70ed0,tag
child-pre-rebuild). It carries none of #10187's hunks and borrows none of itsvocabulary. #10473 lands before #10187.
🤖 Generated with Claude Code
https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23