Nils Anders Danielsson

I ran some experiments for a larger project with Agda compiled using GHC 9.4.2 with `-foptimise-heavily` on and the run-time options `+RTS -M4G -s`. Unfortunately you can get rather different...

> I saw some similar errors, like the not in scope error when `C-c C-n` `∷`: In this case I assume that `∷` is not in scope, as opposed to...

For the common case of universe levels I think it makes sense to be as general as possible.

Is the idea that inductive families would not be allowed unless this flag is used, or would the flag only affect the extra clauses? In the former case the flag...

I currently use `--cubical`/`--erased-cubical` when I use cubical features, and otherwise mostly `--without-K`, and I can use both variants in a single development. With the suggested setup, if I work...

The option `--cubical-compatible` has to be used in all imported modules. I think we should encourage people writing reusable libraries to use this option.

If @plt-amy's new modality check (#6236) is integrated, then I think the only difference between `--without-K` and `--cubical-compatible` is that the extra clauses related to inductive families are not generated...

Erasure is also always enabled, and one cannot avoid erasure if one uses data or record types with parameters. However, if a program with erasure annotations is accepted, then the...

> I type-checked the standard library once with `--cubical-compatible`, and once with `--without-K` (without the checks from @plt-amy's pull request), and obtained the following figures: Now I also included `--profile=internal`...

> `--without-K` should also avoid generating `hcomp`/`transp` helpers for data types/records and the `transpX` constructors themselves. Will you implement this?