Why this pattern matching fails in Agda?
First, let's desugar the withs.

First definition:

wa''-aux : ∀ m n -&gt; n + m ≡ m + n -&gt; wa (m + n) ≡ wa (n + m)
wa''-aux m n refl = ?  -- cannot unify n + m with m + n

wa'' : ∀ m n -&gt; wa (m + n) ≡ wa (n + m)
wa'' m n = wa''-aux m n (comm n m)


Second definition:

wa''-aux : ∀ m n w -&gt; w ≡ m + n -&gt; wa (m + n) ≡ wa w
wa''-aux m n .(m + n) refl = ?

wa'' : ∀ m n -&gt; wa (m + n) ≡ wa (n + m)
wa'' m n = wa''-aux m n (n + m) (comm n m)


When checking that refl is a valid case, we must unify the two sides of the equation it is supposed to be a proof of. Remember that refl : {x : ℕ} → x ≡ x, so we must find a single value x that is βη-equal to both the left-hand side and right-hand side.

In the first case, this means unifying n + m with m + n, and in the second case, this means unifying w with m + n. The latter is obviously possible, where we assign w ↦ m + n and note that we have done this with the dot pattern .(m + n) in w's place. The former is not obvious. How should we unify n + m with m + n? n ↦ m would be wrong: note, for example, that 2 + 3 ≡ 3 + 2, but 2 does not unify with 3.

In general, things are made difficult by the fact that Agda can't show that _+_ is injective. This is for the good reason that it isn't (as our example showed). Agda can show that constructors are injective, justified by the fact that Agda has no quotient types or the like. This is why suc m and suc n will unify. Agda does not try to show that any defined functions are injective, though it in principle could (by getting the user to supply a proof, for example).