search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

Re. #7196: Only prune instances in serialised iface #7197

Closed plt-amy closed 3 months ago

plt-amy commented 3 months ago

Removing "temporary" instances (= with visible arguments, declared in a section) from the TC state makes them disappear for interactive development, too. Removing them just before serialization has the intended benefits and doesn't cause this. Fixes #7196

andreasabel commented 3 months ago

Just to make sure: these instances remain in the state longer now, can they interfere with other instances during instance search?

plt-amy commented 3 months ago

At worst they'll make instance search performance slightly worse during interactive use/subsequent definitions (in that module). They can't actually fire because they're out of scope/have visible arguments, which is why I was getting rid of them in the first place.

(* Slightly worse because they'd be quickly ruled out since noticing that a neutral Def can't be a Pi and that things are out of scope is extremely fast when compared to actually comparing full instance heads)