Nils Anders Danielsson

Agda seemed to have gotten stuck in an infinite loop.

I updated the script above: ``` mkdir fresh cd fresh git clone https://github.com/agda/agda-stdlib (cd agda-stdlib && git checkout b0505d661fbbfecf7ffeae20cc4b48c8ef41e078) git clone https://github.com/graded-type-theory/graded-type-theory cd graded-type-theory git checkout 5a4d9eaf5af978f97142801da220373b78ab572d printf '../agda-stdlib/standard-library.agda-lib\ngraded-type-theory.agda-lib' >...

Sorry, I have pushed the missing commit now. @jespercockx, I think it would be good if you could take a look at this before the release.

> In this light it makes sense that the directly recursive definition is rejected but the one with the indirection is accepted: in the latter case, the clause has not...

See also #7847.

I guess the flag should be infective. Cubical Agda uses irrelevance in some way, right? Would `--cubical-compatible` have to imply this flag? In that case the flag might not be...

> To the first point: there are eg some very old usages come from [@nad](https://github.com/nad) who maintains a lot of legacy code for both teaching and research. I've no wish...

> As originally written, the DSL is not extractable to Haskell because it uses the `Path` type in several of its primitive constructions. There are no limitations on the use...

> I forgot to mention that I also use`transport` in something that is necessary at runtime, which I need to replace with `Data.Equality.transport` or something similar to compile There is...

> There are several ways I can augment my codebase or the Cubical standard library to mitigate these issues, but to me it seems the simplest and most generalizable solution...