Andreas Abel

Thanks @Bodigrim ! Looks like `cabal-add` is missing from Stackage nightly. (It is also missing from older LTSs, but I guess nothing can done about that but adding it as...

> but I suppose there is a bigger issue: are we happy to drop GHC < 9.2? Yes, that should be fine. `hackage-cli` is mostly an executable, and there is...

Turns out that many tests are already disabled...

> The cabal-plan tool can help with that, but this tool only handles Cabal packages (and the rts package seems to be excluded from the generated listing). See #5134 for...

@L-TChen > 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the...

I suppose dropping GHC 8.4 would be ok nowadays. Even ubuntu-20.04 (which had its EOL) ships a more recent GHC.

Good point. Yet the current implementation does unbounded eta-record "splitting": https://github.com/agda/agda/blob/26ef5bcba940898ca861ea7a46304e3a30dea77b/src/full/Agda/TypeChecking/Empty.hs#L70-L75 https://github.com/agda/agda/blob/26ef5bcba940898ca861ea7a46304e3a30dea77b/src/full/Agda/TypeChecking/Empty.hs#L101-L115 Indeed, I can exploit this to make Agda loop: ```agda data ⊥ : Set where record R :...

> My suggestion is to not expand recursive records (eta or no) in the emptiness check That sounds too drastic, e.g. the following is perfectly fine: ```agda open import Agda.Builtin.Maybe...

We can extend the check to all guarded record types without much change, only have to record whether a record type is guarded in the signature. However, we already have...

Great! Indeed, this is all that is required. I added you on Hackage and invited you to the repo, and asked to pass Stackage maintainership to you: https://github.com/commercialhaskell/stackage/pull/7845/commits/14e11b82548a61714d805ba54bc0b2124ef36a87