Andreas Abel

Discussed during the Agda dev meeting 2025-09-17: - @TOTBWF mentioned that in 1lab they place some indexed datatypes in `Set\omega` just to avoid the blowup caused by the left-inverse computation....

@AndrasKovacs Does this PR close this issue? - #8110

This seems to be the compromise introduced in #4065: to not print postponed type checking problems, but keep the information that there are unsolved constraints. Not happy? (Then please reopen...

2025-10-16: situation unchanged.

Doesn't come as a suprise to me. In the second case, you can eta-contract the function `a.set` to a projection, but not in the first case. Possibly related: #1581 and...

2025-11-17 still open.

> I don’t see a documented reason why fresh names shouldn’t be in scope, therefore I propose that fresh names should be in scope. The technical reason is that scope...

> Thank you. I think it would be nice to have a description of what exactly `freshName` does and what are its limitations, perhaps expanding [the comment that currently says...

> `open M using (Unit; tt; Bool) renaming (true to tt;` Indeed. But this will not be implementable at the level of concrete syntax, since there we do not know...

Agda-2.8.0 has the following timings: ``` time agda-2.8.0 Issue2528.agda --profile=internal +RTS -s Checking Issue2528 (/Users/abel/play/agda/bugs/Issue2528.agda). Total 48,423ms Miscellaneous 28ms Termination 9,749ms (28,599ms) Termination.Compare 14,548ms Termination.Graph 3,624ms Termination.RecCheck 677ms Typing 1,080ms...