Bug in Agda version 2.6.0.1.20191219

bug-2-6-1.agda

-- Agda version 2.6.0.1.20191219

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma

ℕ×ℕ : Set
ℕ×ℕ = Σ ℕ λ _ → ℕ

record Cont : Set where
  constructor cont
  field
    value : ℕ×ℕ

-- Define decidability
data ⊥ : Set where

data Dec (A : Set) : Set where
  yes : A       → Dec A
  no  : (A → ⊥) → Dec A

-- Equality is decidable for natural numbers
natEq : (n m : ℕ) → Dec (n ≡ m)
natEq zero    zero    = yes refl
natEq zero    (suc m) = no λ ()
natEq (suc n) zero    = no λ ()
natEq (suc n) (suc m) with natEq n m
...                   | yes refl = yes refl
...                   | no  n≢m  = no  λ { refl → n≢m refl }

-- ... and so for pairs of natural numbers
pairEq : (a b : ℕ×ℕ) → Dec (a ≡ b)
pairEq (n , i) (m , j) with natEq n m | natEq i j
...                    | yes refl     | yes refl = yes refl
...                    | _            | no  i≢j  = no λ { refl → i≢j refl }
...                    | no  n≢m      | _        = no λ { refl → n≢m refl }

-- ... and so for Cont.
contEq₁ : (x y : Cont) → Dec (x ≡ y)
contEq₁ (cont a) (cont b) with pairEq a b
...                       | yes refl = yes refl
...                       | no  a≢b  = no λ { refl → a≢b refl }

-- We could of course prove this without the result for pairs.
contEq₂ : (x y : Cont) → Dec (x ≡ y)
contEq₂ (cont a) (cont b)
    with natEq (fst a) (fst b) | natEq (snd a) (snd b)
... | yes refl                 | yes refl  = yes refl
... | _                        | no  a₁≢b₁ = no λ { refl → a₁≢b₁ refl }
... | no  a₀≢b₀                | yes refl  = no λ ()

-- What happens if we mix those two?
contEq₃ : (x y : Cont) → Dec (x ≡ y)
contEq₃ (cont a) (cont b)
    with natEq (fst a) (fst b) | pairEq a b
... | yes refl                 | yes ()  -- Huh?
... | _                        | no  a≢b = no λ { refl → a≢b refl }
... | no a₀≢b₀                 | _       = no λ { refl → a₀≢b₀ refl }
-- There is no case where they are equal

-- The same happens if the two with-abstractions are separate.
contEq₄ : (x y : Cont) → Dec (x ≡ y)
contEq₄ (cont a) (cont b) with natEq (fst a) (fst b)
...                       | no  a₀≢b₀ = no λ { refl → a₀≢b₀ refl }
...                       | yes refl  with pairEq a b
...                                   | no a≢b = no λ ()

-- What value does contEq₃ compute?
c00 = cont (0 , 0)

c00≟c00 : Dec (c00 ≡ c00)
c00≟c00 = contEq₃ c00 c00
-- Normalises to
-- contEq₃ (cont (0 , 0)) (cont (0 , 0)) | yes refl | yes refl

compiled.agda

open import IO
open import Agda.Builtin.Unit

open import bug-2-6-1

yesOrNo : {A : Set} → Dec A → IO ⊤
yesOrNo (yes _) = putStrLn "Result was yes"
yesOrNo (no  _) = putStrLn "Result was no"

main = run (yesOrNo c00≟c00)

issue.agda

-- Agda version 2.6.0.1.20191219

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma

ℕ×ℕ : Set
ℕ×ℕ = Σ ℕ λ _ → ℕ

record Cont : Set where
  constructor cont
  field
    value : ℕ×ℕ

data ⊥ : Set where

data Dec (A : Set) : Set where
  yes : A       → Dec A
  no  : (A → ⊥) → Dec A

natEq : (n m : ℕ) → Dec (n ≡ m)
natEq zero    zero    = yes refl
natEq zero    (suc m) = no λ ()
natEq (suc n) zero    = no λ ()
natEq (suc n) (suc m) with natEq n m
...                   | yes refl = yes refl
...                   | no  n≢m  = no  λ { refl → n≢m refl }

pairEq : (a b : ℕ×ℕ) → Dec (a ≡ b)
pairEq (n , i) (m , j) with natEq n m | natEq i j
...                    | yes refl     | yes refl = yes refl
...                    | _            | no  i≢j  = no λ { refl → i≢j refl }
...                    | no  n≢m      | _        = no λ { refl → n≢m refl }


contEq : (x y : Cont) → Dec (x ≡ y)
contEq (cont a) (cont b)
    with natEq (fst a) (fst b) | pairEq a b
... | yes refl                 | yes ()  -- Huh?
... | _                        | no  a≢b = no λ { refl → a≢b refl }
... | no a₀≢b₀                 | _       = no λ { refl → a₀≢b₀ refl }

output.txt

Result was no

If you try to add a case for yes refl, you get:

The case for the constructor refl is impossible
because unification ended with a cyclic equation
  b ≟ fst b , snd₁
Possible solution: remove the clause, or use an absurd pattern ().
when checking that the pattern refl has type (fst b , snd₁) ≡ b