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)
| ^^^^^^^^^^^^^^^
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)