Nils Anders Danielsson

> Instead of depending on it, we could simply merge it wholesale into `Agda.Utils` and use it when compiling to WASM. That package does not have the same licence as...

> * Remove `hcomp` as a universe constructor and instead push it down through type formers, If I'm not mistaken the current implementation of `--erased-cubical` relies on `hcomp` being a...

> This would create a situation where `--cubical-without-glue` would have an `hcomp` operation which specializes to a constructor `HCompU` in `--cubical-erased` and `--cubical`, but to a reducing thing in `--cubical-with-uip`....

If you want to use `unfolding`, then you should use `opaque`.

This feature request was discussed during a recent developer meeting. Someone (@jespercockx?) suggested that there should also be non-pragma syntax corresponding to `--opaque`, and @plt-amy suggested that one could use...

Agda rejects the following code: ```agda {-# OPTIONS --safe --cubical-compatible --erasure #-} data _≡_ {@0 a} {@0 A : Set a} (@0 x : A) : A → Set a...

> One can perhaps fix this problem temporarily by making the `UnsupportedIndexedMatch` warning incompatible with `--safe`, and also incompatible with compilation. However, note that this warning is not raised when...

I found three more examples: https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/api/Issue1168.hs#L14-L21 https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/api/PrettyInterface.hs#L17-L29 https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/api/ScopeFromInterface.hs#L27-L41 When I run `make api-test` I get the following output: ``` ====================================================================== ========== Successful tests using Agda as a Haskell library ==========...

The API test cases could perhaps be integrated into the `agda-tests` program.

Another broken test case: ``` $ make size-solver-test ====================================================================== ================= Installing the size-solver program ================= ====================================================================== make[1]: Entering directory '[…]/src/size-solver' cabal v1-install --enable-tests --builddir=./dist-2.6.3-ghc-9.0.2 -fenable-cluster-counting --ghc-options="+RTS -M6G -RTS" Resolving dependencies......