Skip to content

IType: cache free type variables on interned nodes; prune tSubst#1055

Open
nanavati wants to merge 23 commits into
B-Lang-org:mainfrom
nanavati:itype-ftv-cache
Open

IType: cache free type variables on interned nodes; prune tSubst#1055
nanavati wants to merge 23 commits into
B-Lang-org:mainfrom
nanavati:itype-ftv-cache

Conversation

@nanavati

Copy link
Copy Markdown
Collaborator

Stacks on #1048 (IType interning); #925 (lift-dictionaries) stacks on this.

What

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. The intern table is immortal, so the field
is 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. fTVars becomes a field read.

tSubstWith now prunes: at each interior node, if the cached free variables are
disjoint from the substitution domain (ctxAvoids), the subtree returns Unchanged
without traversal. The ITForAll case additionally requires the binder not collide with
the 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 in
one binary: nodes store a single shared empty set (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, 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 stays
exact either way.

Validation

  • The flag gating was audited to be total: every consumer of the cached sets is behind
    it, and the disabled path is the pre-cache code, not an approximation of it.
  • The two flag states produce fully compatible output. The cached sets themselves never
    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.)
  • No benchmarks have been run. The flag exists precisely so the optimization can be
    measured A/B on real workloads with a single binary; measurements on more real-world
    examples are of interest.

nanavati and others added 23 commits July 15, 2026 02:56
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant