Tracking: explicit universes can improve performance substantially
Opened this issue · 0 comments
mattrobball commented
For AlgebraicGeometry.Scheme and similar bundled categories, elaboration seems to inject level metavariables resulting more steps in unification. Providing explicit universe annotations, Scheme.{u}, prevents this.
It would nice to understand what is happening.