[Agda] implicit/explicit difference in candidate

[Andrés Sicard-Ramírez]

On 25 May 2018 at 14:44, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 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')
> -----------------------------------------------------------------

It seems you can remove all the implicit arguments when using
`AllProp.gmap` (based on
https://github.com/agda/agda-stdlib/commit/33b88cfe66d909d8519823c0174b1e7b233f8b59).


-- 
Andrés