Why does Agda require pattern matching here

Question

I have the following:

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

_×_ : {n m : Level} (A : Set n) (B : Set m) → Set (n ⊔ m)
X × Y = Σ X (λ _ → Y)

ℕ² : Set
ℕ² = ℕ × ℕ 

canonical : ℕ² → ℕ²
canonical (x , 0) = (x , 0)
canonical (0 , y) = (0 , y)
canonical (suc x , suc y) = canonical (x , y)

p1 : (a : ℕ) → (a , 0) ≡ canonical (a , 0) -- works
p1 a = refl

p2 : (a : ℕ) → (0 , a) ≡ canonical (0 , a) -- doesn't work
p2 a = refl

p3 : (a : ℕ) → (0 , a) ≡ canonical (0 , a) -- works
p3 0 = refl
p3 (suc a) = refl

When I try to typecheck it agda responds with an error in p2

zero != fst (canonical (0 , a)) of type ℕ
when checking that the expression refl has type
(0 , a) ≡ canonical (0 , a)

Why does Agda require me to do pattern matching for the second element of a pair, as in p3? Why does p1 typecheck but not p2?

Jesper Jesper · Accepted Answer · 2021-10-20T14:08:27

Agda compiles all definitions by pattern matching to a case tree, as described in the user manual page on function definitions. In your case, the case tree looks as follows:

canonical xy = case xy of
  (x , y) -> case y of
    zero -> (x , 0)
    suc y -> case x of
      zero -> (0 , suc y)
      suc x -> canonical (x , y)

In particular, the function will only compute when the second argument is known to be either zero or suc. Agda provides a gentle warning when this happens by giving a light grey background to the second clause. You can also make this into an error by turning on the --exact-split flag (with a {-# OPTIONS --exact-split #-} pragma at the top of your file.

If you want to know more about the translation to a case tree, I recommend our paper on elaboration of dependent pattern matching. You might also be interested in a possible solution to this problem (which sadly did not make it into the main version of Agda) or the --rewriting flag which allows you to add the computation rule canonical (0 , y) = (0 , y) by first proving it and then registering it as a rewrite rule.

Why does Agda require pattern matching here

1 Answers