[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

[Andrés Sicard-Ramírez]

Post by 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
------------------------------------------------------------------
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).

[Sergei Meshveliani]

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

------
Sergei

Post by Andrés Sicard-Ramírez

Post by 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
------------------------------------------------------------------
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).