[Agda] termination checking loop

[mechvel at scico.botik.ru]

Dear Agda developers,

I have a module Foo.agda in which the last line for `foo' is erroneously 
set of kind  x = x.

foo mon {f} nn =
   begin-p
     f *pm mon                       =ₚ[ =ₚsym .. (*mp-comm mon f) ]
     mon *mp f                       =ₚ[ ... ]
     (mon *ₘ lmF) +mp (mon *mp fₜ)   =ₚ[ ... ]
     (lmF *ₘ mon) +mp (fₜ *pm mon)
   ∎p
   where
   lmF = lm f nn;   fₜ = tailPol f nn
   ...
   fₜ*m = fₜ*m    -- **

And the type checker of  Agda 2.6.0.1  seems to loop infinitely (> 30 
minutes, for large memory space).

1) If I replace this marked clause with the needed one, then Foo.agda is 
type-checked fast.
2) I tried to set a clause of kind  x = x  in several previous and 
similar places in Foo.agda,
    after `where` in "begin-p ... ∎p where".
    And it type-checks fast, reporting "Termination checking failed for 
the following functions: ...".

What might this mean?
As I recall, when the type checker loops infinitely, it is considered as 
a bug.

Regards,

------
Sergei