Perché questa corrispondenza del modello fallisce in AGDA?

Question

Considera la funzione wa'' (Hai bisogno di definizione del numero naturale, in stdlib o 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

Il modello che corrisponde comm n m insieme a refl non riesce. Ma se aggiungo un'altra partita:

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

Questo codice funziona. Esiste una differenza a livello di semantica tra questi due frammenti di codice?