[Agda] implicit lambda in Development Sep.16

[Sergei Meshveliani]

On Sun, 2016-09-18 at 21:47 +0200, Ulf Norell wrote:
> It's the change to eagerly insert trailing implicit argument in
> left-hand sides.
> See https://github.com/agda/agda/blob/stable-2.5/doc/release-notes/2-5-2.txt#L301 and
> https://github.com/agda/agda/issues/2001.
> 
> 
> The fix is simply to move the bindings of p a b to the left-hand side:
> 
> 
> prime∣split-nz {p} {a} {b} = impl prime∣split {p} {a} {b}
> 

Indeed, it works! Thank you.

------
Sergei




> 
> On Sun, Sep 18, 2016 at 9:30 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Dear Agda developers,
>         
>         The fragment
>         
>           Prime∣split :  Set (α= ⊔ α)
>           Prime∣split =  ∀ {p a b} → IsPrime p → p ∣ (a ∙ b) → p ∣ a ⊎
>         p ∣ b
>         
>           ...
>         
>           prime∣split-nz :  NZPack0.Prime∣split
>           prime∣split-nz =  \ {p a b} → impl prime∣split {p} {a} {b}
>         -- *
>                             where
>                             impl :  Prime∣split → NZPack0.Prime∣split
>                             impl =  proj₁ Prime∣split←→Prime∣split-nz
>         
>         
>         is type-checked in Agda-2.5.1.1,
>         
>         and Development Agda of September 16, 2016 reports
>         
>         -----------
>         Found an implicit lambda where an explicit lambda was expected
>         when checking that the expression
>         λ {p} {a} {b} → impl prime∣split {p} {a} {b} has type
>         NZPack0.IsPrime .p →
>         (UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p)
>         ((*upCMon-NZ UpCommutativeMonoid.∙ .a) .b) →
>         (UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p) .a ⊎
>         (UpCommutativeMonoid.upMonoid *upCMon-NZ UpMonoid.∣ .p) .b
>         -----------
>         
>         If you can guess of what is this effect, then, please, inform
>         me
>         (because I wonder, how to fix this).
>         
>         Thanks,
>         
>         ------
>         Sergei
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>