Instance Search breaks Termination Highlighting

[lawcho]

The termination checker correctly finds the bad call in the following code:

record Monad-Lite (M : Set → Set) : Set₁ where
    field _>>=_ : ∀{A B} → M A → (A → M B) → M B

instance
    Monad-id : Monad-Lite (λ x → x)
    Monad-id .Monad-Lite._>>=_ x f = f x

open Monad-Lite Monad-id

data Unit : Set where
    tt : Unit

loop : Unit
loop =
    loop >>= λ x → x

However, when I replace open Monad-Lite Monad-id with open Monad-Lite {{...}}, the highlighting disappears.

The termination checker still complains, it just doesn't say where the suspicious call is any more.

Screenshots:

Notes:

• Tested with Agda versions 2.6.2.1 and 2.6.2.2
• Tested with agda-mode plugins for both emacs and VSCode

[andreasabel]

Thanks for reporting! This used to work in Agda 2.5.2/3/4, broke in 2.6.0.

[andreasabel]

Starting bisection:

agda-bisect --with-cabal=cabal-3.2 -w ghc-8.4.4 --good v2.5.4 --bad v2.6.0 --script $PWD/issue5875.sh

Skript issue5875.sh:

$1 Issue5875b.agda | grep "(at"

The file Issue5875b.agda is the MWE from the OP.

[andreasabel]

Bisection produced this:
47358b3 is the first bad commit
Date: Thu Dec 13 13:32:18 2018 +0100
[ #3435 ] postpone instance constraints while checking applications

Let's see how helpful this information is to fix the issue...

[andreasabel]

The real culprit seems to be 2970da8 (ping @gallais) see 2970da8#r72426685:

[ warning ] Highlighting positivity issues

• killrange when solving metas
  In order to avoid positivity issues to be reported with the range of the term that made solving the meta possible rather than where the meta actually originated from. As a consequence a few golden valu[e]s are changed.