[Agda] implicit/explicit difference in candidate

[Sergei Meshveliani]

Indeed, the candidate system allows me to remove implicits there!
Thank you.

------
Sergei


On Sat, 2018-05-26 at 01:28 -0500, Andrés Sicard-Ramírez wrote:
> 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).
>