Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Bug in Agda version 2.6.0.1.20191219
-- 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
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)
-- 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 }
Result was no
@louisswarren

This comment has been minimized.

Copy link
Owner Author

louisswarren commented Feb 21, 2020

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.