aliao/killargs-perf into main Addresses a performance issue with long telescopes that @totbwf minimized out of investigating !133. It does not address the actual issue described there, only this tangential minimization.
The code was already using forceNotFree to try removing the offending
variables if necessary, so all that was needed to actually get it
working was a minor adjustment to the ForceNotFree instances to make
sure they actually reach everywhere that a MaybeFree variable might be
hiding.
Fixes a pretty bad case of quadratic type-checking time for long
telescopes, see test/Succeed/OccursCheckInstantiate, where the issue was
instantiateFull quadratically re-traversing the prefix of the telescope
up to the meta to decide how to prune f out of the metavariable standing
for its type: in each argument we had
A(7 + n) : ∀ a b c d e (f : ?0) → _≡_ {?1 f} f (A6 a b c d e)
?1 f := ?0
except the meta ?1 from which we were trying to kill f was also applied
to the entirety of An telescope up to A(7 + n), and the sorts of those
variables were *also* metas, and instantiateFull wanted to traverse
*all* of these sorts. However Occurs was basically already using the
rapier approach to free variable handling so we just had to remove the
quadratic sledgehammer.
Testing performance regressions is kinda difficult, though, and I can
only hope that 64M is enough heap to pass in CI!
1a2bac6cfb
b168a06b76
No due date set.
No dependencies set.
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?