Idris "did not change type" for rewrite with exact same type

Context I'm trying to write a version of ++ for Vect where the compiler can infer the resulting Vect has the expected contents.

Detail I'm struggling to see why this second rewrite isn't working

import Data.Vect
import Data.Nat

infixl 9 ++:

public export
(++:) : {0 r, r' : Nat} -> Vect r Nat -> Vect r' Nat -> Vect (r' + r) Nat
(++:) [] y = rewrite plusZeroRightNeutral r' in y
(++:) {r = S rr} (x :: xs) y = rewrite plusSuccRightSucc r' rr in x :: (xs ++: y)

I've intentionally added the vector lengths in the signature in the reverse order to make the API easier to use. I'm seeing

"tmp.idr" 8L, 254C written
Error: While processing right hand side of ++:. Rewriting by S (r' + rr) = r' + S rr did not change type Vect (r' + S rr) Nat.

/src/tmp.idr:8:32--8:82
   |
 8 | (++:) {r = S rr} (x :: xs) y = rewrite plusSuccRightSucc r' rr in x :: (xs ++: y)

I don't get why a proof that r' + S rr is equal to S (r' + rr) doesn't rewrite r' + S rr. Here's the error when I don't have the rewrite

"tmp.idr" 8L, 219C written
Error: While processing right hand side of ++:. Can't solve constraint between: S (plus r' rr) and plus r' (S rr).

/src/tmp.idr:8:32--8:47
   |
 8 | (++:) {r = S rr} (x :: xs) y = x :: (xs ++: y)
   |                                ^^^^^^^^^^^^^^^

Solution

It's simple because rewrite works in the reverse order. So if the goal is goal but you have a, you need a proof goal = a, not a = goal. (I found this always very confusing, as the replace in the background takes a = goal, but I guess it is because rewrite rewrites the goal term.) So with sym this should work:

(++:) {r = S rr} (x :: xs) y = rewrite sym $ plusSuccRightSucc r' rr in x :: (xs ++: y)