Agda - Why is this case required to type check? In a simple proof that $forall m, 1 * m \equiv m$

Question

After defining the naturals, addition and multiplication as usual, I set to write a proof that 1 is a neutral element.

p : (n : ℕ) -> (1 * n) ≡ n
p zero = refl
p (suc m) = refl

Which is fine!

Since refl appears in both alternatives, I thought this should type-check:

p : (n : ℕ) -> (1 * n) ≡ n
p _ = refl

But this fails with:

1 * n != n of type ℕ
when checking that the expression refl has type (1 * n) ≡ n

What causes type to not check here?

Answer 1

It's hard to diagnose an error without a MRE, no matter how standard you think your definitions are.

Your error presumably comes from the fact _+_ and _*_ are defined like so:

0     + n = n
m     + 0 = m
suc m + n = suc (m + n)

0     * n = n
suc m * n = n + m * n

and so 1 * n = (suc 0) * n = n + 0 * n = n + 0 which is not judgmentally equal to n because _+_ is strict in its first argument and so won't evaluate until that first argument is constructor-headed.

Matching on n to expose a constructor is enough for _+_ to reduce: 0 + 0 is 0 by the first equation and suc m + 0 is suc m by the second.