[Agda] "unsolved metas" in candidate

[Sergei Meshveliani]

But find it now.
Agda-2.5.3 allows 
           case ((a ≟ 0#) , (b ≟ 0#))
below,
and  Agda 2.5.3.20180519  requires  _,′_  there.

------
Sergei



On Fri, 2018-05-25 at 21:49 +0300, Sergei Meshveliani wrote:
> Dear Agda developers,
> 
> DoCon-A-2.02 has a fragment
> 
>     from :  NZPack0.Prime∣split → Prime∣split
>     from prime∣split-nz {p} {a} {b} prime-p (c , pc≈ab) =
>          case
>              ((a ≟ 0#) , (b ≟ 0#))
>          of \
>          { (yes a≈0 , _      ) →  let p*0≈a =  ≈trans (*0 p) (≈sym a≈0)
>                                   in  inj₁ (0# , p*0≈a)
>          ; _ → anything
>          }
> 
> which is type-checked in Agda-2.5.3 and is not type-checked in 
> Agda 2.5.3.20180519: 
> 
> ------------------------------------------------
> Failed to solve the following constraints:
>   _635
>     := λ {α} {α=} iR∣? prime∣split-nz {p} {a} {b} prime-p c pc≈ab →
>          (iR IntegralRing.≟ b)
>          (.Structures2.Ringoid.0#
>           (.Structures2.Ring.ringoid
>            (.Structures3.RingWithOne.ring
>             (.Structures3.CommutativeRing.ringWithOne
>              (IntegralRing.commutativeRing iR)))))
>     [blocked on problem 1866]
>   [1866] Dec (b ≈ 0#) =< _B_634 iR∣? (a ≟ 0#) : Set α=
> Unsolved metas at the following locations:
>   /home/mechvel/doconA/2.02.1/source/Structures6.agda:302,24-25
>   /home/mechvel/doconA/2.02.1/source/Structures6.agda:302,27-33
> -----------------------------------------------
> 
> The current test is a very large program.
> I am going to reduce the test.
> Meanwhile: if you guess about the nature of the effect, then, please
> inform me.
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda