[Agda] "unsolved metas" in candidate

[Sergei Meshveliani]

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

[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

Post by Sergei Meshveliani
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
------------------------------------------------
_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 α=
/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
https://lists.chalmers.se/mailman/listinfo/agda