Why this pattern matching fails in Agda?

Question

Consider function wa'' (need natural number definition, either in stdlib or Agda.Builtin.Nat):

postulate comm : ∀ m n -> m + n ≡ n + m

wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m)
wa'' m n with comm n m
...        | refl = { }0

The pattern matching on comm n m with refl fails. But if I add one more match:

wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m)
wa'' m n with (n + m) | comm n m
...        | .(m + n) | refl = { }0

This code works. Is there any semantics-level difference between these two code snippets?