[Agda] strangely cannot reproduce a report

[mechvel at scico.botik.ru]

People,

Several times I observed a very strange effect.

This time the code is

-----------------------------------------
foo {pairsₛ} {pairsₛ'} pairsₛ∣pl≡-pairsₛ' {p} {e} p,e∈pairs =
   let
     pairs = map fromNZ-inFirst pairsₛ;   pairs' = map fromNZ-inFirst 
pairsₛ'

     ((P , e') , P,e'∈pairsₛ , p,e=ₚfrom-P,e') =
                                         ∈-map⁻ setoidₚₛ setoid-CN 
p,e∈pairs
     -- debug : Nonzero   -- (1)
     -- debug = P

     p' = fromNZ P;   (p≈p' , e≡e') = p,e=ₚfrom-P,e'

     (Q , Q,e'∈pairsₛ' , P~Q) =  pairsₛ∣pl≡-pairsₛ' P,e'∈pairsₛ           
    -- (2)
                                 -- pairsₛ∣pl≡-pairsₛ' {P} {e'} 
P,e'∈pairsₛ  -- (3)
     ...
    ...
-------------------------------------------

Agda 2.6.1 (under emacs) (ghc 8.8.3) reports

_snd_2297
   : Subsetoid.Member (Submagma.subsetoid nzSubmagma)
     (proj₁ (proj₁ (proj₁(Membership.find setoidₚₛ
         (Data.List.Relation.Unary.Any.Properties.map⁻ p,e∈pairs)))))
[ at 
/home/mechvel/inAgda/doconA/3.0/source/CancellativeSemiring-II.agda:675,33-51 
]

for the line of (2).
I guess that this is due to implicit arguments being not resolved for 
the
function  pairsₛ∣pl≡-pairsₛ'  in the line (2)

(BTW: why Agda does not put any explaining humanly words to such 
reports?).


All right, I insert there the implicits {P} {e'}, as in the line (3).

Now it reports that  P  in the line (3) has a wrong type.  ** A critical 
point.

I am surprised, and insert the two debug lines (1), to check the 
resolved type of P.

Now there start adventures.
The whole file is type-checked!
Then, remove the "debug" lines - and it again is type-checked!

Then I return to the variant of the line (2), obtain the unsolved-like 
report,
insert there implicit arguments, as in the line (3).
And now it is type checked!

I fail to reproduce the report of a wrong type of P.
I delete  Foo.agdai,  and repeat the whole session without emacs,
by calling
             > agda $agdaLibOpt Foo.agda

And I fail to reproduce the report about P.

This effect is not for the first time.
The impression is that Agda learns something from previous sessions. A 
smart girl!

Earlier I thought that this was because I forget about some typos made, 
so that I fail
to really reproduce a session. But this time it looks more clear, I did 
things attentively.

May be this is due to that  emacs  sets something invisible for me when 
I edit Foo.agda?
For example, I wrote "{P}", and occasionally pressed some key, and 
something invisible
has been inserted there?

If it was a system or a hardware corruption, then I probably would not 
be able
to sensibly type-check, compile and run the tests in a large project, as 
I did.

Has people met with such effects?

Thanks,

------
Sergei