<div dir="ltr">It&#39;s the change to eagerly insert trailing implicit argument in left-hand sides. See <a href="https://github.com/agda/agda/blob/stable-2.5/doc/release-notes/2-5-2.txt#L301">https://github.com/agda/agda/blob/stable-2.5/doc/release-notes/2-5-2.txt#L301</a> and<div><a href="https://github.com/agda/agda/issues/2001">https://github.com/agda/agda/issues/2001</a>.<br><div><br></div><div>The fix is simply to move the bindings of p a b to the left-hand side:</div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">prime∣split-nz {p} {a} {b} = impl prime∣split {p} {a} {b}</span><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">/ Ulf</span></div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Sep 18, 2016 at 9:30 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda developers,<br>
<br>
The fragment<br>
<br>
  Prime∣split :  Set (α= ⊔ α)<br>
  Prime∣split =  ∀ {p a b} → IsPrime p → p ∣ (a ∙ b) → p ∣ a ⊎ p ∣ b<br>
<br>
  ...<br>
<br>
  prime∣split-nz :  NZPack0.Prime∣split<br>
  prime∣split-nz =  \ {p a b} → impl prime∣split {p} {a} {b}      -- *<br>
                    where<br>
                    impl :  Prime∣split → NZPack0.Prime∣split<br>
                    impl =  proj₁ Prime∣split←→Prime∣split-nz<br>
<br>
<br>
is type-checked in Agda-2.5.1.1,<br>
<br>
and Development Agda of September 16, 2016 reports<br>
<br>
-----------<br>
Found an implicit lambda where an explicit lambda was expected<br>
when checking that the expression<br>
λ {p} {a} {b} → impl prime∣split {p} {a} {b} has type<br>
NZPack0.IsPrime .p →<br>
(UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p)<br>
((*upCMon-NZ UpCommutativeMonoid.∙ .a) .b) →<br>
(UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p) .a ⊎<br>
(UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p) .b<br>
-----------<br>
<br>
If you can guess of what is this effect, then, please, inform me<br>
(because I wonder, how to fix this).<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>