Andreas Abel

> Could we rename the flag to "--lossy-unification" I think that would be fine. `--lossy-unification` already shows a red flag, not need to double this up with `experimental`.

~~Alternatives: ~~`--optimistic-unification`~~, `--speculative-unification`.~~

I had this for the terms produced by unification, only that it uncovered the hack where level variables were abused as sort variables. Since you (presumably) cleaned this up, we...

Maybe a way to go is to ignore certain problems (like wrong sorts) at first to catch more important problems, such as #2797. Once we caught the most harmful bugs,...

De Bruijn bug fixed by @jespercockx in 0f67eb82365ef4d767bbc7216473744668c752a5

> Would it be helpful in fixing this if I were able to make the test case smaller? Yes, this always helps, because focusing the trigger will usually give some...

> Are they fundamentally harder than constructor pattern synonyms? I don't think so.

Actually also failing locally on my machine (I am using GHC-9.0.1). Could be a `.ghc.environment` thing? (Wild guess.) Libraries are not installed globally anymore...

> nuking all environment files Are you installing everything with `v1`-cabal? Otherwise, can you still use `ghci` then? It doesn't pick up packages otherwise, it seems. So far, `write-ghc-environment-files: always`...

On my machine, the problem seems to be this: - I do a `cabal v2-build` which creates a `.ghc.environment` file - after a while, I do `make install-bin` which installs...