[Agda] implicit/explicit difference in candidate

[Sergei Meshveliani]

Dear Agda developers,

the fragment

  allPrime-fromAsd-ks' : All IsPrime (map fromAsd ks')
  allPrime-fromAsd-ks' =
     AllProp.gmap {A = Associated} {B = C} {P = Asd.IsPrime}
        {Q = IsPrime} {f = fromAsd}
        (\ {p'} → proj₂ $ IsPrime←→IsPrime-asd $ fromAsd p') 
        all-prime-ks'

in DoCon-A-2.02 (FactorizationMon/FtMonoid1.agda) 
is type-checked in Agda 2.5.3  
and is not type-checked in Agda 2.5.3.20180519 :

------------------------------------------------------------------
Found an implicit application where an explicit application was
expected
when checking that {f = fromAsd}
(λ {p'} → proj₂ $ IsPrime←→IsPrime-asd $ fromAsd p') all-prime-ks'
are valid arguments to a function of type
Asd.IsPrime Relation.Unary.⊆
(λ {.x} → IsPrime) ∘
_f_422 cMon∣? cancel a M' all-prime-ks' [a]='value-M' →
All Asd.IsPrime Relation.Unary.⊆
(λ {.x} → All IsPrime) ∘
map (_f_422 cMon∣? cancel a M' all-prime-ks' [a]='value-M')
-----------------------------------------------------------------


The test is a very large program.
I start to reduce it.
Meanwhile, if you guess, what is the nature of the effect, then please
inform me.

------
Sergei