Repository navigation
RFM: ground-scalar specimen for generic_formal_unjudged_against_a_sibling_bound_argument (conflicting actuals, advisory-mitigated) - #13348
Conversation
…d actuals (silent acceptance, measured at main ed68b55) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
LAND. This row isolates a real, silently accepted class at the exact producer: unify_generics inserts the first binding and its Present arm returns acc without judging the later actual. The two opposite-order specimens establish the first-write behavior rather than merely one bad return inference.
The ground-scalar boundary is useful and honest. String versus Int is decidable without the declaration-identity carrier needed by the bare-marker and unit-variant populations, so this row can carry a concrete structurally-guaranteed ceiling and a narrower trigger without claiming those siblings repaired. It also states #13330 as unmerged and explicitly records that its repair neither causes nor closes this class.
The next-rung evidence is properly discriminating: both mismatched orderings refuse at the second argument, while pick(a: 1, b: 2) remains accepted. No code repair or enrolled wall is claimed by this filing.
…al_unjudged_against_a_sibling_bound_argument; drop the duplicate row (it is advisory-mitigated, not silent) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Reworked: this PR's first version claimed silent acceptance, and a diagnostic census at main ed68b55 shows each conflicting argument draws the UndecidableGenericFormal advisory. So it duplicated — sent from jolly-pike-330 |
briansrls
left a comment
There was a problem hiding this comment.
LAND at this head. The prior approval’s separate-class verdict is superseded by the diagnostic census: the conflicting ground actual is not silent; it reaches the existing typed, located DeclaredTypeInhabitanceUndecided / UndecidableGenericFormal population. Deleting generic_parameter_keeps_the_first_of_conflicting_actuals and adding the ground-scalar occurrence to generic_formal_unjudged_against_a_sibling_bound_argument restores one authority for the class instead of keeping two rows distinguished only by an incorrect rung.
The specimen belongs in the existing class: the first actual fixes T, the later incompatible actual is nevertheless admitted at the same raw generic formal, and the advisory makes the path mitigatable under direct_call_unbound_carried_generic_compat. Ground String-vs-Int remains a useful narrower fact because its conflict is decidable without nominal declaration identity, but that supports an earlier repair subset, not a separate failure class.
The current PR diff contains only the addition to the established row; the duplicate row is absent. Queue only after this exact head's required witnesses complete successfully.
Updates the existing row
generic_formal_unjudged_against_a_sibling_bound_argumentwith a ground-scalar specimen. No code changes.Correction. This PR first filed a new row (
generic_parameter_keeps_the_first_of_conflicting_actuals) claiming that conflicting actuals are accepted silently. A diagnostic census at mained68b5573b(gunbc compile --entry) shows that is wrong:take_s(s: pick(a: 'x', b: 2))andpick(a: 1, b: 's')each drawDeclaredTypeInhabitanceUndecided(UndecidableGenericFormal) ataandb. That is exactly this existing class, which is mitigatable undergunbc.rung_drop.direct_call_unbound_carried_generic_compat.What this head (
bc4e34d1d6) does:The PR was dequeued for this change and needs a fresh review.
🤖 Generated with Claude Code