Instantly share code, notes, and snippets.

# louisswarren/bug-2-6-1.agda

Last active Feb 24, 2020
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
Owner Author

### louisswarren commented Feb 21, 2020 • edited

 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 ``````