[Agda] "bug" on x = x

[mechvel at scico.botik.ru]

I have a certain fragment

...    | _ | no x≉0 =  aux (r ≟ 0#)
   where
   pair = divRem y x x≉0
   q    = proj₁ pair
   -q   = -q
   ...

Probably the type checker (Agda 2.6.1) needs to report about a loop in  
"-q = -q".
But it does not terminate (in 20 minutes).

I recall the effect is known. I write now about it, for any occasion.

Regards,

------
Sergei