Nils Anders Danielsson

> The only solution I've found is to use the `--experimental-lossy-unification` flag (which I believe was implemented by @Saizan). Note that Agda is not really designed for the use of...

> Right, but what we noticed (especially when working on the Z-cohomology stuff) is that it's pretty much impossible to do anything without the `--experimental-lossy-unification` flag as Agda gets so...

> I would expect that in most cases if a variable gets solved with an unexpected term you'll realize when you try to prove something about the affected definition. Perhaps...

> Right, but what we noticed (especially when working on the Z-cohomology stuff) is that it's pretty much impossible to do anything without the `--experimental-lossy-unification` flag as Agda gets so...

> Was there any file that was particularly problematic? The first module that I encountered problems in was `Cubical.ZCohomology.RingStructure.RingLaws` (see the local definition `finalTransp`). > I actually don't think `Kn→ΩKn+1...

Could you use something like `cabal exec /bin/sh -- -c 'cd DIR && agda […]'` instead of `cabal run agda -- --cwd DIR […]`?

``` $ which agda […]/bin/agda $ cabal exec /bin/sh -- -c 'which agda' […]/dist-newstyle/build/x86_64-linux/ghc-9.0.2/Agda-2.6.3/build/agda/agda $ cabal exec -- which agda […]/dist-newstyle/build/x86_64-linux/ghc-9.0.2/Agda-2.6.3/build/agda/agda ``` From `cabal exec --help`: "The PATH is modified...

If you look at a file with `--safe` at the top in Emacs, load the file, and then read "Checked" in the mode line, then you can be fairly certain...

> One could also relax the semantics of `--safe` to mean _safe if no open goals_. In that case, how do you find out if you have open goals? Currently...

> E.g. if I say `--allow-unsolved-metas` on the command line, this should have the highest authority, overruling any complains by `--safe` modules. I [disagree](https://github.com/agda/agda/issues/5265#issuecomment-865685563): > I don't think it should...