Pin the conflicted type names by identity, not by count - #2798
Merged
Conversation
`tri types dup` found 79 type names with more than one definition and reported
them. Nothing held the line.
tri types ratchet --bless # writes docs/reports/type_conflicts.json
tri types ratchet # a NEW conflict fails; a RESOLVED one fails too
IDENTITY, NOT A COUNT, and the difference is the whole point. A count cannot see
a SWAP: one name resolved while another appears leaves the total at 79 and the
ledger wrong. Seen failing on purpose, three ways:
- Lexer removed from the ledger -> "+ Lexer NEW conflict", exit 1
- a name added to the ledger -> "- ZZZGone resolved", exit 1
- one swapped for another at 79 -> BOTH lines, exit 1
The third is the one a count misses.
A RESOLVED name fails too, on purpose -- the same rule this repository already
applies to an unexpected PASS in the corpus ratchet. An entry that has stopped
being true and stays in the ledger is slack the next conflict hides in.
And absence is not amnesty (T31): with no ledger the command exits 1 and says to
bless once and commit the file, rather than passing quietly over an empty oracle.
Eleven tests. The three new ones cover the swap at a constant count, a resolved
name, and agreement being silence; `drift` is a pure function so they test the
production comparison rather than a re-implementation of it.
WHY THESE NAMES MATTER. A quantifier's domain size is computed from declared
types. For a conflicted name the answer is "unbounded" -- not because the type is
infinite but because WHICH type is undetermined. Any enumerating lowering of
`forall` hits the same wall, so this set has to stop growing before that decision
is worth making. See #2774.
Refs #2774
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 10:53:42 UTC
Summary
Seal Status
|
This was referenced Aug 29, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
feat(tri): pin the conflicted type names by identity, not by count
tri types dupfound 79 type names with more than one definition and reportedthem. Nothing held the line.
IDENTITY, NOT A COUNT, and the difference is the whole point. A count cannot see
a SWAP: one name resolved while another appears leaves the total at 79 and the
ledger wrong. Seen failing on purpose, three ways:
The third is the one a count misses.
A RESOLVED name fails too, on purpose -- the same rule this repository already
applies to an unexpected PASS in the corpus ratchet. An entry that has stopped
being true and stays in the ledger is slack the next conflict hides in.
And absence is not amnesty (T31): with no ledger the command exits 1 and says to
bless once and commit the file, rather than passing quietly over an empty oracle.
Eleven tests. The three new ones cover the swap at a constant count, a resolved
name, and agreement being silence;
driftis a pure function so they test theproduction comparison rather than a re-implementation of it.
WHY THESE NAMES MATTER. A quantifier's domain size is computed from declared
types. For a conflicted name the answer is "unbounded" -- not because the type is
infinite but because WHICH type is undetermined. Any enumerating lowering of
forallhits the same wall, so this set has to stop growing before that decisionis worth making. See #2774.
Refs #2774
Co-Authored-By: Claude Opus 5 noreply@anthropic.com