Verify handwritten tycon constants against the Prelude (tconcheck); qualification-scoped tycon comparison#1046
Open
nanavati wants to merge 4 commits into
Open
Verify handwritten tycon constants against the Prelude (tconcheck); qualification-scoped tycon comparison#1046nanavati wants to merge 4 commits into
nanavati wants to merge 4 commits into
Conversation
Generic.everywhere rebuilds every node of the IModule whether changed or not; the transformation only rewrites ICon identifiers. An explicit traversal covers the same reachable ICon sites (heap references are leaves either way, since the cells sit behind IORefs), preserves untouched subtrees instead of reallocating them, and answers the old XXX about IAps recursion explicitly. bluetcl's find_vmodinfo becomes a direct query (ICVerilog is the only VModInfo carrier reachable in an IPackage), and with the last generic traversals gone, the Data/Typeable derivings on ISyntax and HeapData are removed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012KHVhEzJpur1ZRjNjpzBVj
BSC's front end enforces one type constructor per qualified name, so a
qualified Id determines its (kind, sort) payload. Shipped comparison
code already relies on this invariant (TyCon Eq ignores the sort; ITCon
comparison is by Id alone), but nothing checked the compiler's
handwritten copies of Prelude tycon payloads against the Prelude truth.
Add a tconcheck utility that obtains a Prelude symbol table the
production way (BinUtil.readImports on an in-memory probe package, the
full all-defs signatures via BinUtil.replaceImportedSignatures exactly
as bsc's module-generation symtab does, then MakeSymTab.mkSymTab) and
verifies, entry by entry:
* every registered Type.hs TCon constant (new registry
Type.handwrittenTCons, 40 entries): Maybe Kind and TISort
* every registered ISyntaxUtil/IType ITCon constant (new registry
ISyntaxUtil.handwrittenITCons, 32 entries): IKind via IConv.iConvK
(newly exported) and TISort
* every StdPrel.preTypes row against the symbol table
* every StdPrel.preClasses tyConOf payload, both against the symbol
table and against its preTypes twin row (these are seeded through
independent paths in MakeSymTab with nothing else enforcing
agreement)
The check runs as part of the build (src/Libraries/Makefile), pointed
at the just-built libraries, so a Prelude edit that changes a payload
fails the build instead of silently drifting; tconcheck is built and
installed with the standard comp install for that purpose. A thin
testsuite wrapper (testsuite/bsc.misc/tcon_drift) re-checks the
installed tools.
The checker found nine pre-existing drifts, masked until now by the
payload-ignoring comparisons; they are documented and waived (loudly)
in tconcheck.knownDrift pending direction, e.g. Type.hs still calls
Int/UInt/File abstract although the Prelude declares them as data
types, ISyntaxUtil.itInout has kind # -> * although Inout is * -> *,
and itPrimPair's kind is left-nested because IKFun has no fixity
declaration.
In lifting the inline ITCon literals out of itPair/itList/itMaybe so
they could be registered (itPrimPair, itListCon, itMaybeCon), the
expressions are kept verbatim; no behavior change.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
BSC's front end enforces one type constructor per qualified name, so a
qualified Id determines its (kind, sort) payload. This invariant was
already load-bearing in comparison code -- TyCon Eq ignored the sort,
and ITCon comparison in IType.cmpT is by Id alone -- but unstated, and
the TyCon instances mixed regimes: Eq compared kinds even for pairs
where the invariant makes that a dead tail, while remaining
kind-sensitive for the unqualified names where the invariant is
undefined.
Scope the TyCon comparisons by qualification:
* Eq: both-qualified pairs compare by Id (qualEq); the kind hedge is
kept only when either side is unqualified (resolution-era fuzz).
* Ord: lexicographic on (base, qual); within a (base, qual) bucket,
both-qualified ties are EQ without consulting the kinds, and the
unqualified bucket keeps the kind comparison. This remains a
lawful total order.
Document at the instances: the invariant and its qualified-only domain,
the deliberate non-transitivity of Eq via qualEq (pre-existing), the
Eq/Ord disagreement (pre-existing; containers key on Ord), and the
pointer to the tconcheck build step that verifies the handwritten
payload copies the by-Id comparisons rely on. Also upgrade the cmpT
comment in IType.hs: ITCon by-Id comparison is justified by the same
invariant (all ITCon Ids are qualified, since IType is born
post-resolution at IConv); the ITForAll binder-kind skip is a separate,
alpha-structural assumption, unchanged.
The only behavior delta is a both-qualified pair with the same name and
differing Maybe Kind fields. An audit of the pipeline found no
comparison site where a qualified Nothing-kinded TyCon (parse-era
trees, cTCon-built compiler-generated code) can meet its Just-kinded
twin (symtab/convCQType-era types): type-level Eq/Ord is only exercised
within a single kind regime, cross-regime checks use kind-agnostic
helpers (leftCon, mkInstId, Id comparisons), and no container is keyed
on Type/CType where mixed twins could coexist. The full testsuite and
a rebuild of all libraries with the changed compiler back this
empirically.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Bring all nine drifted constants in line with the Prelude-derived truth
(the checker's DRIFT output was used as the spec), and empty the
tconcheck knownDrift waiver list; the waiver mechanism remains for
future incidents but ships empty.
* Type.hs tInt/tUInt: TIabstract -> TIdata (Prelude declares
'data Int n = Int (Bit n)' and likewise UInt)
* Type.hs tPrimPair (and StdPrel tiPair, used by itPrimPair):
SStruct -> SInterface [] (PrimPair is declared as an interface)
* Type.hs tActionValue: old struct sort -> TIdata [ActionValue]
('data ActionValue a = ActionValue ...')
* Type.hs tActionValue_: field names __value/__action ->
avValue_/avAction_ (new PreIds position variants added)
* Type.hs tFile: TIabstract -> TIdata [InvalidFile, MCD, FD]
(new PreStrings/PreIds constructor ids added)
* ISyntaxUtil itInout: kind # -> * (apparently copied from itInout_)
corrected to * -> *
* ISyntaxUtil itPrimPair: kind was left-nested, (* -> *) -> *,
because IKFun had no fixity declaration and defaulted to infixl 9;
IType.hs now declares infixr 8 `IKFun` (matching Kind's right-nested
Kfun and IConv.iConvK). Census of every backticked IKFun chain in
the tree: itPrimPair was the only unparenthesized multi-arrow chain;
all others are single-arrow or already explicitly parenthesized, so
the fixity change reparses nothing else.
* StdPrel tiBufferMode (used by itBufferMode): tiEnum -> tiData
(BlockBuffering carries a Maybe Integer argument, so BufferMode is
not an enum)
The corresponding position-parameterized variants (tIntAt,
tActionValueAt, tActionValue_At) are fixed to the same payloads.
A consumer audit found no reader of these payloads out of the constants
themselves: comparison sites use Eq/Ord (which compare by qualified Id)
or wildcard the payload fields in patterns; the payloads only travel
into generated ISyntax via iConvT, where they now agree with what
symtab-derived types already carried.
tconcheck now reports all 94 entries OK with zero waived.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
nanavati
force-pushed
the
tycon-drift-check
branch
from
July 14, 2026 18:15
8e40aae to
1122268
Compare
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.
Adds a build-time checker for an invariant the compiler already relies on, and aligns the tycon comparison instances with it.
The invariant
The front end enforces one type constructor per qualified name, so a qualified Id determines its (kind, sort) payload. This is already load-bearing in shipped comparison code:
IType.cmpTcomparesITConby Id only (kind and sort ignored), andCType'sEq TyConignores the sort. But the compiler also carries handwritten copies of tycon payloads (Type.hsconstants,ISyntaxUtilITConliterals, StdPrel's seeded rows andtyConOffields) with nothing keeping them in agreement with the Prelude — drift is silent precisely because the comparisons ignore the payload.tconcheck
A new checker executable (built with the other utility exes) that obtains a Prelude symbol table through the production path —
BinUtil.readImportson an in-memory probe package,replaceImportedSignaturesfor full-defs signatures (needed:Pred__/SchedPragmaare declared but not exported),MakeSymTab.mkSymTab— and verifies 94 entries across three registries:Type.handwrittenTCons(40),ISyntaxUtil.handwrittenITCons(32), and StdPrel'spreTypesrows andpreClasses'tyConOftwins (22). Registries are co-located beneath the constants they cover.It is wired as a build step:
make install-srcruns it right after the libraries build and fails on any unwaived drift (drift produces a compiler whose type comparisons are silently wrong — the artifact should not be produced). A thin testsuite wrapper (bsc.misc/tcon_drift) additionally checks installed artifacts for self-coherence.What it found on its first run
Nine real drifts, all masked today by the payload-ignoring comparisons: six stale sorts in
Type.hs(Int/UIntclaimTIabstractvs Prelude'sTIdata;PrimPairclaimsSStructvsSInterface;ActionValueclaims a struct sort vsTIdata;ActionValue_has stale field names;FileclaimsTIabstract), and three on the ISyntax side including two kind bugs:itInouthas kind# -> *(the realInoutis* -> *), anditPrimPair's kind is left-nested becauseIKFunhas no fixity declaration (Haskell defaults toinfixl 9, so backticked kind chains parse backwards). A follow-up commit on this branch fixes all nine and declares the fixity, shrinking the waiver list to empty.Comparison alignment
Eq/Ord TyConbecome qualification-scoped: when both Ids are qualified (the invariant's domain), comparison is by Id; when either is unqualified — where an Id is a scope query, not a name, and the invariant is undefined — the existing kind hedge is kept. The instances now document the semantics that were previously implicit:Eq TyConis deliberately non-transitive viaqualEq(scope-resolution fuzz),EqandOrddisagree (containers key on the lawfulOrd), andcmpT's by-IdITConcomparison is justified by the invariant (allITConIds are qualified — IType is born post-resolution at IConv) rather than by an unstated assumption. An audit found no comparison site that mixes kind-resolved and unresolved tycons of the same qualified name (qualification and kind-filling happen together inMakeSymTab.convCQType; boundary code uses kind-agnostic helpers).Validation
Full testsuite: 19046 PASS / 0 FAIL / 129 XFAIL / 0 XPASS. The build gate demonstrably works (it failed the build on the nine drifts before they were waived/fixed). The checker result is identical against pre-change and post-change compilers and freshly rebuilt libraries.
This also prepares the ground for hash-consing IType (planned follow-up): interning wants Id-determines-payload to be a checked invariant rather than folklore.
🤖 Generated with Claude Code
https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK