typing: defer failed-application classification (perf)#1063
Merged
Conversation
strub
force-pushed
the
fix-long-require
branch
6 times, most recently
from
04ac5ba to
54299ce
Compare
Operator selection reported every rejected candidate through EcUnify.classify_application, which peels the argument list one type at a time, head-normalising via `ty_hnorm (ty_subst (Tuni.subst (UniEnv.assubst ue)) _)` at each step. UniEnv.assubst is subst_of_uf, materialising the whole unifier by folding over UF.domain (every univar in the unienv), so each candidate cost O(arity * |unienv|) instead of the O(arity) incremental union-find of the previous single unification. Overload resolution rejects candidates constantly on the *success* path (any application of an overloaded name tries and drops the non-matching instances), so this classification ran pervasively even though the diagnostics it produces are only ever consumed when an application fails outright and an error is raised. On a large formosa-keccak module this turned a ~8s require into ~54s. Defer the classification: - EcUnify: select_outcome's KO now carries a `... Lazy.t`. select_op decides OK/KO with the cheap single `unify top texpected` and drops KO without ever forcing it; select_op_failures forces the thunks, for the error path only. classify_application is unchanged. - EcTyping.gen_select_op: the OK selection uses select_op; the failure list is a lazy closure forced only by tyerror_noop when building the UnappliedOp / UnknownVarOrOp error. select_pv likewise decides with a single unification, classifying the reason only in its failing branch. Diagnostics are byte-identical (candidate order preserved). Keccak require back to baseline; tests/op-application-errors.ec passes; unit (84/84) and stdlib (128/128) green.
Gustavo2622
approved these changes
Jul 2, 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
2 participants
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.
Operator selection reported every rejected candidate through
EcUnify.classify_application, which peels the argument list one type at a
time, head-normalising via
ty_hnorm (ty_subst (Tuni.subst (UniEnv.assubst ue)) _)at each step. UniEnv.assubst is subst_of_uf, materialising thewhole unifier by folding over UF.domain (every univar in the unienv), so
each candidate cost O(arity * |unienv|) instead of the O(arity)
incremental union-find of the previous single unification.
Overload resolution rejects candidates constantly on the success path
(any application of an overloaded name tries and drops the non-matching
instances), so this classification ran pervasively even though the
diagnostics it produces are only ever consumed when an application fails
outright and an error is raised. On a large formosa-keccak module this
turned a ~8s require into ~54s.
Defer the classification:
EcUnify: select_outcome's KO now carries a
... Lazy.t. select_opdecides OK/KO with the cheap single
unify top texpectedand drops KOwithout ever forcing it; select_op_failures forces the thunks, for the
error path only. classify_application is unchanged.
EcTyping.gen_select_op: the OK selection uses select_op; the failure
list is a lazy closure forced only by tyerror_noop when building the
UnappliedOp / UnknownVarOrOp error. select_pv likewise decides with a
single unification, classifying the reason only in its failing branch.
Diagnostics are byte-identical (candidate order preserved). Keccak
require back to baseline; tests/op-application-errors.ec passes; unit
(84/84) and stdlib (128/128) green.