[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