Andreas Abel

@Bodigrim Kudos! I'll try it out next time I need to make revisions...

NB: Since this reproducer does a match of `Refl`, it should not be portable to Cubical Agda. However, I don't know enough to state this with certainty. @nad wrote: >...

Thanks, @szumixie !

> Intriguingly (to me at least), this already raises a termination error: Likely because there is a workaround in place for #1023, but it was shown to be incomplete in...

This isn't a problem with `--type-based-termination`. Proposal: disallow `--syntax-based-termination` when `--cubical` and `--safe` are on. (Or at least warn.)

@emilypi : Currently `mtl-2.3.1` is in an awkward state with a gap in the `base` versions it supports. Could we get `mtl-2.3.1.1` fixing this issue soon? It seems a fix...

@sjshuck : Noted. I don't have GHC 9.0 anymore, so I cannot easily work on this, have to leave it to others.

@UlfNorell : Do you intend to fix this for 2.7.0?

Does this mean that the following documentation is incorrect now? https://github.com/agda/agda/blob/bdcbe480c704d6c5e12f08c62cb01ab05b3199f1/doc/user-manual/tools/auto.rst?plain=1#L104-L113 We'll need an intermediate fix for the docs then.

I added a disclaminer in #7372.