Much faster type checker#3305
Draft
konnov wants to merge 20 commits into
Draft
Conversation
The type checker was spending ~12 min / ~1 GB RAM on large specs. JFR profiling identified three dominant allocation sources: #2 BitmapIndexedMapNode (20 690 samples) — varToClass HashMap rebuilt per unify() call by copying all EqClass objects O(k·n) #6 EqClass (983 samples) — fresh copy per class per call #7 UID (975 samples) — one UID per EqClass copy This commit replaces the EqClass object graph with a union-find over flat int arrays (parent[], rank[]) inside TypeUnifier: - find() uses iterative path compression - mergeReprs() always makes the smallest-index variable the representative (preserving the existing invariant relied on by callers) - unifyImpl() resets only the activeVars set instead of allocating a new HashMap per call; snapshot/restore is a single array clone Additional changes bundled in this commit: - Substitution: key type changed from Map[EqClass, TlaType1] to Map[Int, TlaType1] (representative var index as key); varToClassMap accessor added for TypeUnifier; fromEqClasses() compatibility factory retained for tests - VarT1: intern first 1024 instances to eliminate 886 allocation samples from mkCanonicalSub - ConstraintSolver: boundVars rebuilt via solution.allVarNums (O(1)) instead of flatMap over EqClass.typeVars - EtcTypeChecker, ToEtcExpr, Inliner: removed EqClass(v) wrappers; Inliner composition fixed to resolve callee vars through unifierSub before composing (required by the new flat Int-key mapping) - TypeCheckerProfiler: new lightweight profiling object, auto-enabled via -Dapalache.typechecker.profile=true All 765 tests in tlair/tla_typechecker/tla_pp pass. Benchmark on MC3_system.tla (1962 lines): 12 min → 11 min 11 sec (~7%). Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This reverts commit 6609e49.
Fix several correctness gaps in EtcTypeCheckerFast compared to the legacy ETC solver: speculative overload probes no longer mutate live inference state, LET-local overload resolution only fails ambiguities created inside the LET, and record/sparse tuple unification now follows legacy structural behavior. Add regression coverage for record joins, sparse tuple bounds, speculative overload leakage, and enclosing-context overload resolution. Co-authored-by: Codex <codex@openai.com>
Add a researcher-oriented internal note on EtcTypeCheckerFast, covering the live inference graph, unification, LET polymorphism, delayed overload resolution, export compatibility, and expected regression coverage. Co-authored-by: Codex <codex@openai.com>
Add a researcher-oriented internal note on EtcTypeCheckerFast, covering the live inference graph, unification, LET polymorphism, delayed overload resolution, export compatibility, and expected regression coverage. Co-authored-by: Codex <codex@openai.com>
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.
Our current type checker
EtcTypeCheckeris known to be slow on large specifications. I've hit a brick wall on a 2300 LOC spec. The type checker was taking 12 minutes.The first contribution of this PR is a performance improvement by Claude + Sonnet 4.6. It cut the running times of the type checker on the large benchmark to about 6 minutes. However, we needed a more systematic rewrite.
The second contribution of this PR is a new implementation
EtcTypeCheckerFastby Codex + GPT 5.4 medium. With this type checker, it finishes on our large benchmark in 12-13 seconds. It took Codex 7-8 iterations, since we have a large test suite.Leaving this PR in the draft mode for now. It needs a careful review. For now, we can experiment with this new type checker on this branch.
make fmt-fix(or had formatting run automatically on all files edited)./unreleased/for any new functionality