Nils Anders Danielsson

> However, the generation of the extra clauses can make Agda quite a bit slower. I think we should mention this in the changelog and the user manual. I've written...

I accidentally closed the issue.

> Will you implement this? @jespercockx stated that he had already implemented it.

What about other sorts? https://github.com/agda/agda/blob/27ea7f2207c25d6f68387c264aaed9ffc1a733e8/src/full/Agda/Syntax/Internal.hs#L296-L309

When I made all those sorts rigid some error messages changed. Here is one example, for `test/Fail/Issue821.agda`: * Before: ``` Issue821.agda:26,9-10 x != (f _ x) of type (D A)...

I read the text as "the inferred type of `Set` is not `Set₁`", but I guess it should be read as "the inferred type, `Set`, is not `Set₁`".

> * What can be done about `telViewUpTo n t0'`? Perhaps it would make sense to replace the `t0` argument of `checkArgumentsE'` with a `TelView`, and work with that instead...

Some other parts of the code might also be problematic: https://github.com/agda/agda/blob/982e18cdcbb2355d571bc05a8a98811fe6b48525/src/full/Agda/Syntax/Concrete/Operators.hs#L184 https://github.com/agda/agda/blob/982e18cdcbb2355d571bc05a8a98811fe6b48525/src/full/Agda/Syntax/Concrete/Operators.hs#L278-L295 An operator grammar is built for each expression, and as an optimisation this is done based on the...

The code is accepted by Agda 2.3.2 if every occurrence of the `OPTIONS` pragma except for the first one is removed. I got the following timings for 10 and 20...

What do you mean? I could add the information that Agda 2.6.3-2976b59 is, in both cases, a little faster.