Andreas Abel

> but making an inconsequential change like inserting a newline does cause the issue to surface. According to my experiments, when the change happens after the INJECTIVE_FOR_INFERENCE pragma, the issue...

Bingo! ```agda module IdentityFunction where id : {A : Set} → A → A id x = x ``` ```agda module Issue8230INLINE where open import Agda.Builtin.Nat open import IdentityFunction using...

These regressions persist in GHC 9.14 alpha2.

Comment relevant to second issue for GHC 9.14 alpha3: https://discourse.haskell.org/t/ghc-9-14-1-alpha3-is-now-available/13104 > Note that while this release makes many improvements in the specialisation optimisation, polymorphic specialisation will remain disabled by default...

> So I suppose the ShowConstraints tactic ignores the normalization parameter yet. Indeed, no `Rewrite` argument on its constructor: https://github.com/agda/agda/blob/729ad1676f6df70a4cbc0ba62b57cd74697ce0ee/src/full/Agda/Interaction/Base.hs#L145

> `C-c C-=` prints `?0 := Rel A (lzero ⊔ lzero ⊔ lzero)` This does not seem to be a regression, goes all the way back to 2.4.2.4.

> Can confirm this is an issue starting from 2.6.4.1 and is still an issue on the master branch. It seems that is already the behaviour in 2.6.2 when lossy...

AFAIK, the documentation only documents `v2` now, so this is likely a remnant that did not get cleaned up. `cabal v2-build` also silently ignores `--run-tests`. An entry `run-tests: True` in...

(Oops wrong button)

So maybe the way forward here is to have a check at the beginning of `v2-build` for options that won't be used and emit the respective warnings. I think programs...