Skip redundant unifyTypes in entailment solver (-15% full build)#14
Merged
kozak merged 4 commits intorestaumaticfrom Apr 21, 2026
Merged
Skip redundant unifyTypes in entailment solver (-15% full build)#14kozak merged 4 commits intorestaumaticfrom
kozak merged 4 commits intorestaumaticfrom
Conversation
When the entailment solver enforces functional dependencies after matching an instance, it unifies each inferred type with the corresponding constraint type. For constraints on wide row types (e.g. HasField on a 667-field record), this triggers O(n) row alignment via alignRowsWith — even when both sides are structurally identical (the inferred type IS the constraint type after variable substitution). Add an eqType guard before unifyTypes to skip the unification when the inferred type already equals the target type. eqType is a simple structural equality check (O(n) but no sorting, no recursive unification, no cache insertion) compared to the full unifyRows path (rowToSortedList O(n log n) + alignment O(n) + recursive unifications). Measured on pr-admin (1758 modules, optimised -O2 build): full build: 74s -> 63s (-15%) no-change: 1.2s (unchanged) prelude-edit:5.3s (unchanged) leaf-edit: 2.0s (unchanged) All 1340 tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
zyla
approved these changes
Apr 20, 2026
Collaborator
zyla
left a comment
There was a problem hiding this comment.
Great stuff.
One thing I'd suggest: add a comment why the eqType special case is there (i.e. for performance) - otherwise looks odd.
BTW, we should fix CI on the fork - currently it fails to build deps so doesn't even run tests
The build step uses --haddock --no-haddock-deps, which affects the install-path hash. Downstream steps (glob-test, build-package-set, libtinfo check) called stack exec/path without those flags, resolving to a different install hash and failing to find the purs binary. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
stack path --local-doc-root doesn't inherit flags from the outer stack exec invocation, so it resolved to a different install hash than the build artifacts. Since stack exec already puts the binary on PATH, use command -v / which instead. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.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
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.
Summary
unifyTypescalls during entailment functional dependency enforcement when the inferred type is structurally equal to the target typeHasFieldon a 667-fieldTranslationsrecord), this avoids O(n log n) row sorting + O(n) alignment that produces no new informationEntailment.hs— addsunless (eqType inferredType t2)guard before the existingunifyTypescallBackground
The entailment solver's
Solvedbranch (Entailment.hs:295-298) enforces functional dependencies by calling:When the instance types are
TypeVars (common — e.g.HasField label (Record row) ty), the substitution maps them back to the original constraint types. SoinferredTypeis often structurally identical tot2.For small types this is harmless —
unifyTypeson identical small types is fast. But for wide row types like a 667-fieldTranslationsrecord,unifyTypesdispatches tounifyRowswhich callsalignRowsWith, which:rowToSortedListtwice — O(n log n) eachAll for a no-op result (identical types always unify successfully with no new bindings).
The
eqTypeguard does a simple O(n) structural comparison that short-circuits on the first mismatch — much cheaper than the full unification path, and free for the common case where types differ (different constructors → O(1) False).Measurements
Measured on pr-admin (1758 modules, -O2 optimised build, median of 3 runs):
Test plan
stack test --fast)🤖 Generated with Claude Code