Nils Anders Danielsson

I noticed that there are CI tests for various versions of GHC, but not for GHC 9.4.2.

@jespercockx, I guess this is related to issue #6124.

> I addressed 2. by raising the error in the file with the wrong module name. The (history of the) error message for `Issue2092.agda` suggests otherwise. It starts in the...

> (If anyone decides to do something about this, please wait until after I have pushed a fix for #2473.) Done.

I think we should avoid adding more calls to `instantiateFull`. Do you have benchmarks that show that adding `instantiateFull` here is "nearly always" a good idea? I also wonder why...

> I'm not sure where else it would go: it can't be earlier since it affects the result of the unquoted action we just ran, and it can't be later...

> If you code well-founded recursion with standard recursors, you get extra function arguments (accessibility proofs) that are matched on, so you get at least different definitional equality (for open...

> If the constructor has a declared name, the `Foo.constructor` syntax is also disabled Why? The notation `record { … }` is not disabled.

> QTT is already the [core theory](https://arxiv.org/abs/2104.00480) of [Idris 2](https://github.com/idris-lang/Idris2). I assume that Idris 2 uses the three-element semiring containing "erased" (0), "linear" (1) and "unrestricted" (ω). Idris 2 accepts...

It seems to me as if Idris 2 does not implement this particular instance of QTT, but I don't know what Idris 2 actually implements. Is it a variant of...