[Agda] type-checking x=x

[mechvel at scico.botik.ru]

Probably this has been discussed earlier, but for any occasion:
I see that
     begin ...
           p ∙ (q ∙ (p' ∙ (b ∙ q'a)))
     ∎
     where  pp' = p ∙ p';  qq' = q ∙ q';  q'a = q'a

is not type-checked in Agda 2.6.1 in a reasonable time.
Needs it to report something like
"Cycle in assignments: q'a = q'a "
?

Regards,

------
Sergei