Andreas Abel

Maybe not surprising that the OP can happen, given that the highlighting is independent from the printing of warnings: https://github.com/agda/agda/blob/1ca774278a208761a92325720057ea34ee2a41b7/src/full/Agda/TypeChecking/Warnings.hs#L71-L74 Maybe not a good API design: https://github.com/agda/agda/commit/bb680eb7e0dd2606289d8bdc33ca916b1bde1a2f However, I fixed...

> In the following code the warning `NotAffectedByOpaque` is turned off, and Agda does not print any warning, but the definition of `R` is still highlighted with `agda2-highlight-deadcode-face`: `R` is...

This happens with all benign warnings, has nothing to do with `opaque`.

MWE: ```agda {-# OPTIONS -WnoEmptyPrivate #-} private ``` This has no deadcode highlighting with 2.5.4.2, it starts to appear with 2.6.0. 2.6.0 was released on 12 April 2019 so my...

This issue is after all easy to fix by calling `highlightWarning` only for enabled warnings: https://github.com/agda/agda/blob/49a12eab7f68fade557b72a811504be52475105f/src/full/Agda/TypeChecking/Warnings.hs#L76-L79 However, since `-WCoverageNoExactSplit` aka `--exact-split` is usually not enabled, this will make the white...

> Until we have such an alternative, perhaps having a hack in place is not the worst thing in the world. Ok, I refine the PR to include a hardwired...

This issue is fixed on master, I supplied a testcase in #8209. @plt-amy Did you fix this?

Maybe related: - #5948

> We can give the solution `refl` in the second hole and it is accepted by Agda without any constraints. However, when we reload the file we do get the...

We are not systematically reducing with non-recursive clauses: ```agda open import Agda.Builtin.Nat record R : Set where field fun : Nat → Nat val : Nat open R r :...