IType: cache free type variables on interned nodes; prune tSubst#1055
Open
nanavati wants to merge 23 commits into
Open
IType: cache free type variables on interned nodes; prune tSubst#1055nanavati wants to merge 23 commits into
nanavati wants to merge 23 commits into
Conversation
ISyntaxCheck.atfEqsFromDict built associated-type-function tycons from raw getAllTypes enumeration keys. The symtab type map holds one entry per visible alias of a type -- for the current package's own decls both the qualified name and the bare one, sharing a single TypeInfo -- so each dict addition also manufactured a duplicate equivalence keyed by an unqualified ATF tycon (first seen: Rep alongside Prelude.Rep, during the Prelude's own compile). Every other ITCon producer feeds from CTypes canonicalized by MakeSymTab.trCType', which substitutes the qualified ti_qual_id, so real ATF applications always carry qualified tycon Ids. The unqualified duplicates could never match them in eqType: they sat in the equivalence classes as silently inert entries. Build the ATF tycon from ti_qual_id and keep one entry per ATF by matching only the canonical alias (atfId == qatfId). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
ISyntaxUtil.itListCons hand-builds the type of the Cons constructor's internal struct (Prelude::List_$Cons with fields _1, _2) for iMkCons/iMkList -- the path IPrims takes to materialize a List result (PrimRealToDigits and friends, reached from realToDigits and from Real formatting in Printf/$format). It rebuilt the tycon from struct shape alone, tagging it (TIstruct SStruct [_1,_2]). The frontend records a positional data constructor's struct as TIstruct (SDataCon parent False) fields (CParser), and that is what the List_$Cons tycon built from the Prelude's own source carries. So evaluated designs mix two distinct ISyntax nodes for the same tycon: the frontend's correct form, and this hand-built one whose metadata is factually wrong (an SStruct claim for what is a data constructor's struct). ITCon equality compares only the Id, so the disagreement is latent today -- but anything that inspects the sort, or ever wants to share type nodes, would see the two forms differ. iMkCons is the only handwritten multi-arg constructor (the other iMk* constructors are single-arg and need no internal struct), so this is the lone site of its class. Thread the true SDataCon identity. Validated: full build, plus bsc.real/evaluator and bsc.lib/Printf localchecks, green with no regolds. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
The Prelude's port-name checks (checkPortNames and the excess-arg_names case of methodArgBaseNames) report primError at getEvalPosition of a (_ :: m) type proxy, and that position is only ever recovered from Ids embedded in the proxy's TYPE -- the method type's tycons. So S0015 pointed at a type mentioned in the field's signature (e.g. Foo at 17:12), not at the field the user declared. Report a term-side position instead. GenWrap already passes each WrapField call a StrArg name proxy; build that proxy as a raw undefined stamped with the interface field's decl-side position (mkStrArgProxyExpr) instead of a plain don't-care, whose class-dispatched undefined construction rebuilds the nullary StrArg constructor and loses the position. The Prelude's WrapField instance takes getEvalPosition of that proxy and threads a Position__ through the WrapMethod port-check methods (methodArgBaseNames, inputPortNames, outputPortNames, saveMethodPortTypes) into checkPortNames and the excess-arg_names primError. The noinline path (fromWrapNoInline) uses the position of its name string literal, which GenFuncWrap stamps with the function's def position. The errors now point at the interface field being checked (its decl Id): BadSplitInst_TooManyPortNames.bs 17:2 (was the type use at 17:12) and TooManyArgNames.bs 27:2 (was 27:29). Regold the two expected files accordingly. Validated: build green; bsc.verilog/splitports localcheck fully green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
…independent A class exported without (..) appears in its package's signature as CIclass, which carried no member names. An importing package's MakeSymTab.getTI therefore rebuilt the class tycon's TIstruct SClass sort from the superclass preds alone -- an impoverished payload, divergent from the defining compile's (field names ++ superclass ids). Abstract structs never had this problem: their signature form keeps the fields, merely invisible. For abstract classes, SymTab.addTypes has papered over the divergence forever via pickBetter's "abstract typeclasses have hidden methods" length comparison, so the impoverished form was tolerated -- but the sort payload of the same qualified tycon differed between the defining compile and its importers, depending on which package's view you happened to hold. Thread the defining package's sort member list (field names ++ superclass ids, exactly as getTI computes it for Cclass) through CIclass: GenSign records it both when exporting a class abstractly (genDefSign) and when embedding a used-but-unexported class (classToIClass, from the symtab's own TypeInfo), and the importer's getTI/getCls use it verbatim for the TypeInfo sort and the Class tyConOf. The fields themselves stay hidden: nothing new enters the field table, and TypeAnalysis's typeclass analysis now skips sort members without a FieldInfo instead of internal-erroring on them. CIclass gains a field, so the .bo signature encoding changes: bump the .bo header tag to bsc-bo-20260715-3 (and the .ba tag in lockstep to bsc-ba-20260715-3). Validated: full install-src build, plus green localchecks in bsc.typechecker/dontcare, bsc.typechecker/typeclasses, and bsc.bluetcl/commands. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
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
Heap-ref (IRefT) types are no longer restamped with positions by updateIExprPosition/updateIExprPosition2: the poss field added in 7e17339 collects the stamped positions out of band, and once ITypes are hash-consed (next change) a restamping rebuild would re-canonicalize to the original node and drop the stamps anyway. The retirement alone moves no output. The position readers (getIExprPosition, getIExprPositionCross) now prefer the stamped positions on the heap ref, falling back to the type's own positions, so the poss field is no longer write-only. Reading poss regolds five tests: * bsc.evaluator/fileIO SetBufferingAfterClose: an outright improvement -- the S0085 file-handle error now blames the user's call site (SetBufferingAfterClose.bsv:10:21) instead of Prelude.bs internals. * bsc.misc/lambda_calculus lc-sysMethods/lc-sysStructs and bsc.misc/sal CTX_sysMethods/CTX_sysStructs: not position diffs but let-binding ordering flips -- these backends order parallel bindings by a position-influenced key, so the changed heap-ref positions flip the order of two bindings. Both orders are semantically equivalent and the new order is deterministic; the ordering's sensitivity to positions is a pre-existing fragility, not addressed here. Since the readers force poss, eqPtrs' redirected-ref rebuild now uses S.empty for that field instead of an internalError placeholder (the ref payload, which really is never touched, keeps its error). The five bsc.mcd ClockCheck outputs (GitHub issue B-Lang-org#863, pinned as .bad-expected) are byte-identical before and after this change: the evaluator-side position stamping was disconnected when -cross-info was removed in 2a0f45d, so those heap refs carry no useful poss entries yet. Restoring the desired use-site positions there is future work: re-enable stamping into poss at the evaluator sites; the readers here are ready to consume it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Hash-cons IType: ITForAll and ITAp become private constructors (ITForAll_, ITAp_) carrying an intern unique, and bidirectional pattern synonyms keep every construction and match site in the compiler textually unchanged. The four leaf constructors stay raw. A global intern table (Data.Map keyed on exact structural NodeKeys, behind an IORef in the SpeedyString style, with a read fast path and an atomic lookup-or-insert on misses) canonicalizes interior nodes. Keys compare at full serialization granularity, via hand-written exact comparators: leaf Ids contribute base, qual, position and props; ITCon contributes its complete (kind, sort) payload including the Ids embedded in sorts and the CTypes inside type synonyms; the ITForAll key includes the binder kind even though cmpT skips it. Interning must never change anything observable, byte-for-byte: since it substitutes the first-constructed representative for every key-equal request, any key coarser than the serialized content changes .bo bytes. Two measured incidents during development: keying Ids without positions/props conflated position-variant types and shrank every library .bo; keying ITCon by Id alone (sound at Id granularity, per the tconcheck-verified one-tycon-per-qualified-name invariant) leaked import-qualification variants of sort-payload Ids into the .bo. A deliberate relaxation to coarser keys (more sharing) remains possible later, with its own golden accounting. The uniques are arrival-order identifiers and never observable: Show, PPrint, Ord and serialization print and compare exactly what they did before; cmpT only uses equal uniques as a fast EQ path. With the syb traversals gone from ISyntax, IType no longer derives or defines Data/Typeable at all: nothing in the compiler requires a Data IType instance, so generic code can neither observe the private constructors nor forge interior nodes with stale uniques. Setting BSC_INTERN_SANITY in the environment makes every intern hit verify full structural equality of the requested children against the canonical node's children. ISyntax re-exports the six names through the same explicit list; the real constructors do not escape IType. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Move the built-in type-function reduction (TAdd/TSub/TMul/TDiv/TLog/ TExp/TMax/TMin on ITNums, TStrCat on ITStrs, TNumToStr, Id__) from ISyntax.normITAp into IType.mkITAp, the smart constructor behind the ITAp pattern synonym. Every ITAp construction now normalizes, so a reducible application like TAdd#(2,3) can no longer be built at all; the former normITAp call sites (IConv.iConvT', ISyntaxSubst.tSubstWith, IExpandUtils.fullTypeNormalizer) just say ITAp now. mkNumConT moves along with the reduction (ISyntax still re-exports it). The raw-construction sites that did not call normITAp were audited: all of them build applications with heads that no reduction rule can fire on (itArrow, itBit, itPrimArray, idPrimPair, idList, idMaybe, struct/ATF tycons), so this changes no behavior there. The only sites that can now reduce where they previously built unreduced applications are ISyntaxCheck.addDict's equivalence-class seeds (ITAp iTAdd/iTLog/... over dictionary argument types); reduction there only folds numeric-literal applications that every other path (iConvT, substitution, .bo reads) already folds, so the checker's equivalences are unchanged in effect. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Ids embedded in ITypes are about to be normalized on entry to the intern layer (no props, no positions), so the commutativity hack must not read an IdProp off an ITCon head. The five commutative numeric tycons are a fixed prelude set; test membership by name. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
Env vars are a redundant control channel: hidden trace flags already reach every bsc invocation via BSC_OPTIONS, including library builds. Replace BSC_INTERN_SANITY with the -trace-itype-intern trace flag. Intended use: the library build and a dedicated checked testsuite leg while the intern key is under change. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
… ITypeKey The .bo writer detects repeated ITypes with a cache keyed by ITypeKey, a full structural mirror of the type (built because Eq/Ord IType are deliberately loose). Since ITAp/ITForAll nodes are now hash-consed at exact serialization granularity, the intern unique IS an interior node's structural identity: key interior nodes by their unique and keep the exact leaf keys. This removes a deep structural walk per written type that re-walked shared subtrees once per path -- exponential on DAG-shaped types (a self-nested typedef tower now writes its .bo in milliseconds instead of dominating the compile). The unique never enters the byte stream: it only keys the writer-local map, and the emitted bytes remain structure plus first-occurrence LOCAL indices, fully content-determined and hermetic. Verified by byte-identity: all 128 library .bo files, both library .ba files, and assorted test packages (including the DAG-shaped tower) are byte-identical before and after this change. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Ids embedded in ITypes are identity, not provenance. The ITVar/ITCon leaves join ITAp/ITForAll behind normalizing smart constructors and pattern synonyms: positions and props are stripped on entry, payload entity Ids (constructors, fields, wrapper names) canonicalize to the owning tycon's qualification, and qualified tycons are interned by name -- the one-tycon-per-qualified-name invariant (tconcheck-verified, -trace-itype-intern-checked) lets a by-name hit skip the payload walk. Key-equal is now byte-equal by construction: representative choice cannot drift .bo output, and the serialized form loses the position and prop payload of every type-embedded Id. Fresh format tags. Unqualified tycons (package-local associated type functions like Rep during their defining compile -- a longstanding form, first observed by the checked build) are normalized but not name-interned: an empty-qual key would collide across packages. The checked library build (-trace-itype-intern) caught both design refinements on its first runs: PrimPair payload qualification variance between handwritten constants and compiled source, then unqualified Rep. Consumer audit and rulings: ITYPE-INTERNING-DESIGN.md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
ISyntaxCheck.atfEqsFromDict built associated-type-function tycons from raw symtab enumeration keys. The symtab type map holds one entry per visible alias of a type -- for the current package's own decls both the qualified name and the bare one, sharing a single TypeInfo -- so each dict addition also produced an equivalence keyed by an unqualified ATF tycon (first seen: Rep of Prelude's Generic, during the Prelude's own compile). Every other ITCon producer feeds from CTypes canonicalized by MakeSymTab.trCType', which substitutes the qualified ti_qual_id; this was the one site synthesizing tycons outside that layer. Build the ATF tycon from ti_qual_id and keep one entry per ATF by matching only the canonical alias. With the origin fixed, retire mkITCon's normalize-but-don't-intern bypass for unqualified tycons (now a hard internalError naming the invariant) and ownedId's empty-qualifier tolerance with it. Validated: BSC_OPTIONS=-trace-itype-intern checked library build is green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
The .bo writer re-keying pull-down brought tests that exercise lifted dictionaries, which live in the lifting PR above this one; on this branch the feature does not exist and the tests fail. They return with the lifting stack. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
…tions/props
Regold the testsuite fallout from stripping positions and props off Ids
embedded in ITypes (e5dfc4f7 + 3771bcac). Every regolded difference is
one of these classes, verified line-by-line against the actual-vs-
expected diffs:
- bluetcl browser: X(IfcPosition) fields disappear (the interface
type's position is no longer real, so the field is omitted), and the
X(...) key column narrows by one space where IfcPosition was the
widest key. X(position) values for type-derived node names move to
a different (filtered) library source line.
- bluetcl browser: sibling order of vector elements changes
(_element_0 now lists after _element_1/_element_2). The sort
tiebreak cmpSuffixedIdByName keys off the suffix-count IdProp;
type-derived name Ids lost that prop, so _element_0 compares as an
unsuffixed full name. Pure reordering: subtrees move intact, with
identical content (verified by multiset comparison), and the order
is deterministic.
- evaluator dynamic errors (G0067/G0068/G0069/G0070/G0094): the error
column moves within the same line, from the position of the
declaration's type-embedded Id to the array-size expression in the
declarator. Same error code, message, and line.
- b381: internal-error dump no longer prints [IdP_bad_name] props on
type-embedded Ids (_v101[IdP_bad_name] -> _v101); the version banner
line is refreshed as a side effect of regolding the raw output.
- dontcare: restore DummyInDeflQual.bs.bsc-out.{0,1}.expected, which
commit 5e98be0e deleted while leaving the test in dontcare.exp. The
current output is byte-identical to the old option-0 expected file.
NOT regolded (left failing, needs a compiler-side fix): the two
bsc.verilog/splitports S0015 tests, where a real file:line:col
degraded to "Unknown position" -- a diagnostics regression.
Per-directory localcheck is green for all six regolded directories.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
Exact-comparison intern keys are now redundant: every Id embedded in an IType is normalized on entry (positions and props stripped -- qual+base is all that remains), ITCon leaves are interned by qualified name under the one-tycon-per-qualified-name invariant (tconcheck-guarded), and post-strip a leaf's name IS its serialized bytes. So TKey's leaf constructors become plain names and values (TKCon qual base, TKVar base, TKNum, TKStr) with derived Eq/Ord, and NodeKey derives its instances too -- built-in Id Eq/Ord is base+qual, which is full granularity on normalized binders. NodeKey keeps the ITForAll binder kind: it is semantic (cmpT skips it), so the key must not. Delete the now-unreferenced exact comparison family (exactCmpLeaf, exactCmpSort, exactCmpSST, exactCmpCT, exactCmpTyCon, exactCmpIfcP, exactCmpMaybe, exactCmpList, exactCmpIdProp, exactCmpId, thenCmp) and rewrite the intern-table comment block for the new invariant: normalization makes key-equal byte-equal; leaf keys are names/values; payload exactness is established once at first intern and guarded by tconcheck plus -trace-itype-intern. The -trace-itype-intern checker keeps its verification strength: structEqT's leaf case now compares the normalized fields directly with built-in (==) (equivalent on normalized values), and mkITCon's checkHit still verifies kind + sort on every hit -- built-in (==) on normalized sorts is exactly serialization granularity. Validated with a checked library build (BSC_OPTIONS= -trace-itype-intern make install-src) and checked localcheck runs of bsc.typechecker/dontcare, bsc.verilog/splitports, bsc.real/evaluator and bsc.bluetcl/commands. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
The intern-table hit verification (internSanityOn / structEqT / the checkHit paths in internAp, mkITForAll, mkITCon) and its hidden -trace-itype-intern flag were scaffolding for validating the name/value intern keys; with the checked library build and testsuite legs clean, hits now return the canonical node directly. mkITCon keeps a comment naming the one-tycon-per-qualified-name invariant, tconcheck as its static guard, and the re-instrumentation recipe (a structural verify on hit plus a trace flag; this commit has the deleted scaffolding). Ids embedded in ITypes are stripped to noPosition on entry (the IType normalization), so the type-position readers became constant: delete ISyntax.getITypePosition and getITypePositionCrossInternal, drop the type-fallback arms of getIExprPosition / getIExprPositionCross (ILam, IAps, IRefT), and return noPosition directly for type arguments in IExpand.getArgPosition. PreIds stops attaching IdPCommutativeTCon to idAdd/idMax/idMin/idMul/ idNumEq: since e6e333b4 (commutative tycons identified by name) the prop has no readers. The IdProp constructor stays for BinData tag stability, marked write-only/historical. The iExpandIface position overwrite of ICTuple field ids is kept: those ids are term-side (built by IConv from CStructT field names) and still carry real positions, so the overwrite is load-bearing for error messages, not a normalization leftover. Validated: make install-src green; localcheck green in bsc.options, bsc.options/messages, bsc.typechecker/dontcare, bsc.real/evaluator, bsc.bluetcl/commands (no goldens embed the removed trace flag). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
Interior interned nodes gain a strict VarSet field holding their free type variables, computed at construction: an ITAp's set is the union of its children's, an ITForAll's is its body's minus the binder. Since the intern table is immortal a lazy field would be a permanent thunk, and the eager cost is near zero: set union and delete return an existing set by pointer when one side is empty or the element absent, and ground types all share one empty set. The field is metadata only -- it never serializes, prints, or participates in comparison or intern keys. fTVars moves to IType and becomes a field read; aTVars keeps walking (rare, alpha-conversion paths only). tSubstWith now prunes: at each interior node, if the cached free variables are disjoint from the substitution domain (the new ctxAvoids method), the subtree is returned Unchanged without traversal. The ITForAll case also requires that the binder not collide with the payloads' free variables (ctxContainsVar, now a cached-set membership): the original code alpha-converts in that case even when the body contains no domain variable, and that rename is observable, so it falls through to the original logic there. The set representation is kept behind a small VarSet API (vsEmpty, vsUnion, vsDelete, ...) so it can be specialized in one place; the substitution contexts store VarSet and the lazily-consumed alpha-conversion avoid-lists keep their Set Id form. Reworked in the cherry-pick onto the name/value-keyed interning lineage (validation scaffolding since removed): the fvs field and its construction-time computation are re-applied onto the reworked IType.hs -- the interior constructors become 5-field, iTypeNodeId/tKey and the pattern synonyms update arity, tKey keeps the reworked branch's sealed name-keyed leaves (ITVar_/ITCon_), and mkITForAll computes the set by deleting the tidied binder (ti) it already stores. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
…ack-no-itype-ftv-cache) The hidden command-line flag -hack-no-itype-ftv-cache disables both the cached free-variable metadata and the tSubst pruning that consumes it, in one binary: interned nodes store a single shared empty set in the field (so the flag also measures the field's own residency cost), fTVarSet walks instead of reading the field, and the substitution machinery takes the exact pre-cache code paths -- full free-variable walks and the original alpha-conversion behavior, including the gratuitous binder renames the pruning otherwise skips. Without the flag the cache stays enabled (the default, unchanged behavior). The flag uses the progArgs idiom of the other hidden flags -- consumed via IOUtil.progArgs (which also reads BSC_OPTIONS), registered in FlagsDecode.traceflags so the command-line parser accepts it -- since Flags does not reach IType/ISyntaxSubst. The pruning guards are gated on the flag itself, never on the cached sets: a dummy empty set consulted by a guard would prune everything. Context free-variable bookkeeping goes through fTVarSet, which walks in disabled mode, so ctxContainsVar (capture detection) stays exact either way. The switch lets the optimization be measured A/B on any workload with a single binary and doubles as a diagnostic chicken switch; measurements on more real-world examples are of interest. Reworked in the cherry-pick onto the name/value-keyed interning lineage: the gated set computations land on the simplified intern constructors (hit verification since removed), mkITForAll uses the tidied binder (ti) it already stores, and the progArgs import returns to IType.hs (the scaffolding removal had dropped its last use). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
Canonicalize the VarSets stored on interned nodes through a global
content-keyed table, in the same posture as the node intern table.
The node table is immortal, so it amplifies every duplicate set:
polymorphic types otherwise retain one copy of each tiny set (like
{e,m}) per node that carries it. Only freshly built sets consult the
table -- the empty-side union arms and the absent-element delete arm
return existing (already canonical) sets lookup-free, and those are
the hot ground-type paths. With -hack-no-itype-ftv-cache the fields
hold the shared dummy and no canonicalization happens at all.
Set content is unchanged, sets never serialize, and the pruning
behavior is unaffected, so compiler output is byte-identical.
Reworked in the cherry-pick onto the name/value-keyed interning
lineage: mkITForAll's vsDeleteCanon takes the tidied binder (ti) it
already stores, matching the previous commits' resolution.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Claude-Session: https://claude.ai/code/session_01Vjo7EmAfHvZTWPDJ923FVz
This was referenced Jul 15, 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
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.
Stacks on #1048 (IType interning); #925 (lift-dictionaries) stacks on this.
What
Interior interned nodes gain a strict
VarSetfield holding their free type variables,computed at construction: an
ITAp's set is the union of its children's, anITForAll's is its body's minus the binder. The intern table is immortal, so the fieldis eager (a lazy field would be a permanent thunk) and cheap: union/delete return an
existing set by pointer when one side is empty or the element absent, ground types share
one empty set, and the sets themselves are canonicalized through a content-keyed table
in the same posture as the node table. The field is metadata only — it never serializes,
prints, or participates in comparison or intern keys.
fTVarsbecomes a field read.tSubstWithnow prunes: at each interior node, if the cached free variables aredisjoint from the substitution domain (
ctxAvoids), the subtree returnsUnchangedwithout traversal. The
ITForAllcase additionally requires the binder not collide withthe payloads' free variables — the original code alpha-converts there even when the body
contains no domain variable, and that rename is observable, so it falls through to the
original logic.
The chicken switch
One hidden flag,
-hack-no-itype-ftv-cache, disables both the cache and the pruning inone binary: nodes store a single shared empty set (so the flag also measures the field's
own residency cost),
fTVarSetwalks instead of reading the field, and the substitutionmachinery takes the exact pre-cache code paths, including the gratuitous binder renames
the pruning otherwise skips. The pruning guards are gated on the flag itself, never on
the cached sets (a dummy empty set consulted by a guard would prune everything), and
capture detection goes through
fTVarSet, which walks in disabled mode — so it staysexact either way.
Validation
it, and the disabled path is the pre-cache code, not an approximation of it.
serialize; the only output difference is alpha-naming of forall binders inside
serialized types (the pruning skips the pre-cache walk's gratuitous renames of
binders in subtrees a substitution cannot change). That naming is semantically
neutral — every compiler dump is byte-identical between the states, and binders are
freshly instantiated at every use — so .bo files from either state are valid and
mutually readable. (Mixing states across packages can at worst miss a
sharing/dedup opportunity, since type comparison is nominal on binder names; it can
never produce a wrong result.)
measured A/B on real workloads with a single binary; measurements on more real-world
examples are of interest.