"Panic: uncaught pattern violation" while trying to eliminate uses of `inspect`

[jamesmckinna]

While trying to eliminate uses of inspect (issue agda/agda-stdlib#1580) in Data.Fin.Properties

combine-surjective : ∀ {m} {n} (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i
combine-surjective {m = m} {n = n} i with remQuot {m} n i in eq
... | p = {!begin
  combine j k                       ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩
  uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩
  i                                 ∎!}
  where open ≡-Reasoning

causes the following error: "Panic: uncaught pattern violation"
(inessential variations on this theme seem also to be a problem)

Not clear what is responsible for raising the bug.

But the original

combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i
combine-surjective {m} {n} i with remQuot {m} n i | P.inspect (remQuot {m} n) i
... | j , k | P.[ eq ] = j , k , (begin
  combine j k                       ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩
  uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩
  i                                 ∎)
  where open ≡-Reasoning

seems to be OK?

[gallais]

This is an upstream issue, shall I transfer it to the agda repo?
(We had a bunch of similar issues in agda/agda-stdlib#1630)

[jamesmckinna]

Ah... interesting. ;-)

You could do, but I had wondered if the combination of two things:

• surjective pairing
• flipping a (non-dependent) pair (remQuot vs. quotRem)

was responsible for this, and hence whether it might be avoidable even without fixing an evident agda bug...

... but you're right, any such thing should get fixed.

[andreasabel]

I think for debugging this we need some more information:

• Agda version used
• At least a commit hash of a version of the agda-stdlib we can check out to reproduce the error
• Ideal would be a MWE

[jamesmckinna]

• Agda version: 2.6.2
• Stdlib commit hash: efc0230019937a694c87db0e3b49e45cc56a238d looks as though it's what you want (base of the current PR #1930)
• MWE: can't easily provide one, but I have found a workaround, albeit an incomprehensible one:
  stdlib commit b4a665e07b2f46d15293f4e5507cac48cec441ae on branch jamesmckinna:inspect

[andreasabel]

Thanks, James!
I checked out the commit efc02300 and then replaced combine-surjective by the code in the OP. Latest Agda responds:

?0
  : Data.Product.Σ (Fin m)
    (λ a → Data.Product.Σ (Fin n) (λ k → combine a k ≡ i))
_a_2416 : Level  [ at /Users/abel/project/open-source/agda-stdlib/src/Data/Fin/Properties.agda:682,1-687,25 ]
_A_2417 : Set _a_2416  [ at /Users/abel/project/open-source/agda-stdlib/src/Data/Fin/Properties.agda:682,1-687,25 ]
Sort _2418  [ at /Users/abel/project/open-source/agda-stdlib/src/Data/Fin/Properties.agda:682,1-687,25 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  {m n : ℕ} (i : Fin (m ℕ.* n))
  (w : Data.Product.Σ (Fin m) (λ x → Fin n)) →
  (proj₂ (quotRem n i) , proj₁ (quotRem n i)) ≡ w →
  Data.Product.Σ (Fin m)
  (λ a →
     Data.Product.Σ (Fin n)
     (λ k → combine a k ≡ i)) is a well-formed type
    (blocked on _A_2417)
  (proj₂ (quotRem n i) , proj₁ (quotRem n i)) ≡
  w is a well-formed type
    (blocked on _A_2417)

This looks fine, a priori.

Could you please check if the problem persists in latest Agda (2.6.3)?

[jamesmckinna]

Thank Andreas, I will do, but I now have a heavy teaching spell, so it might take a few days... after this recent spell of furious stdlib-hacking.

[jamesmckinna]

Not an MWE, but a smaller working example: three variants at the end, the last of which is the failing case (so, if nothing else, a workaround is possible). I'll push as Data.Fin.MWE to the branch. Testing with 2.6.3 still to come...

[gallais]

I think the above comment was meant to link to https://github.com/agda/agda-stdlib/blob/7e6a2478aa23287be516dd04c8cac45270c2aa8c/src/Data/Fin/MWE.agda

[jamesmckinna]

UPDATE: it would appear to be fixed already by 2.6.2.2, as per @andreasabel 's comment on earlier versions of the associated PRs.
Apologies for any wasted effort!

[andreasabel]

@jamesmckinna wrote

Apologies for any wasted effort!

To prevent bug reports for "old" Agda versions I set up an issue template that asks the reporter to check the problem on the latest release or master.
But I can see how transferring this issue from https://github.com/agda/agda-stdlib via github magic bypassed my security measurements... ;-)