Andreas Abel

How do you envision the index to look? Some thing like: ``` [] - Data.List.List.[] - Data.List.Relation.Unary.All.All.[] - Data.Vector.Vec.[] ... ``` So this would be mapping unqualified identifiers to all...

Needs more research, on how good hasktags is in comparison with hTags.

Maybe with the new `ghc-tags` available and `hs-tags` not supporting GHC 9.2, it might be worthwhile considering a switch: - agda/hs-tags#2

Thanks for the pointers, @gallais! I think I lack imagination for the meaning of _algebra-construct-natural-choice_. Is _natural choice_ a mathematical concept around orders? Is there even a choice for min/max...

Here is my attempt: ```agda module O where open DecTotalOrder O public open import Algebra.Construct.NaturalChoice.Min totalOrder public renaming (_⊓_ to _∧_) open import Algebra.Lattice.Construct.NaturalChoice.MinOp minOperator public infimum : Infimum _≤_...

Ulf says it is cubical, not exponential. Cause: - #3358

The slowdown is not connected to instance search per se, only to the amount of unsolved meta-variables created during checking the thing subjected to generalization. We get the same slowdown...

So, in @lawcho's case there is (at least) one meta created per `Imp {_} n`, and all of these metas live under the so far unknown `genTel` generalization telescope (which...

Interesting! (Ping @jespercockx.) @UlfNorell You implemented memoization of free variable sets at some point if I remember correctly. Can this be harnessed to speed up `piSort'`?

Running a bisect...