Pourquoi cette correspondance de modèle échoue dans Agda?

Question

Considérez la fonction wa'' (Besoin de définition du nombre naturel, soit en stdlib, soit 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

Le motif correspondant sur comm n m avec refl échoue. Mais si j'ajoute un match de plus:

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

Ce code fonctionne. Y a-t-il une différence au niveau de la sémantique entre ces deux extraits de code?