How to rewrite: Vect (S (S (n + m))) a -> Vect (S (plus n (S m))) a

Question

I am stuck with Idris (again, sigh). I am doing an exercise on merge sort from the type driven development with Idris book on chapter 10. I have this:

import Data.Vect
import Data.Vect.Views

sort2 : Ord a => (l: a) -> (r: a) -> (a, a)
sort2 l r = if l <= r then (l, r) else (r, l)

needHelp :  Vect (S (S (n + m))) a -> Vect (S (plus n (S m))) a
needHelp {n=(S n)} {m=(S m)} (x :: xs) = ?help

vectMerge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
vectMerge [] ys = ys
vectMerge {n} xs [] = rewrite plusZeroRightNeutral n in xs
vectMerge {n=(S n)} {m=(S m)} (x :: xs) (y :: ys) =
  let (f, s) = sort2 x y in
  needHelp (f :: s :: (vectMerge xs ys))

I have isolated the needHelp function so you can see the rewrite that I want to achieve. I tried this:

vectMerge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
vectMerge [] ys = ys
vectMerge {n} xs [] = rewrite plusZeroRightNeutral n in xs
vectMerge {n=(S n)} {m=(S m)} (x :: xs) (y :: ys) =
  let (f, s) = sort2 x y in
  let tail = (rewrite plusSuccRightSucc n m in s :: vectMerge xs ys) in
  f :: tail

But Idris complains:

When checking right hand side of Main.case block in vectMerge with expected type
        Vect (S (plus n (S m))) a

rewriting S (plus n m) to plus n (S m) did not change type letty

I don't understand why this doesn't work. Help much appreciated.

Answer 1

rewrite works with respect to your current goal, not wrt to the term you are trying to use to solve the goal (I tried to illustrate it in this answer).

So, here is a possible solution:

import Data.Vect

sort2 : Ord a => (l: a) -> (r: a) -> (a, a)
sort2 l r = if l <= r then (l, r) else (r, l)

vectMerge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a
vectMerge [] ys = ys
vectMerge {n} xs [] = rewrite plusZeroRightNeutral n in xs
vectMerge {n=(S n)} {m=(S m)} (x :: xs) (y :: ys) =
  let (f, s) = sort2 x y in
  rewrite sym $ plusSuccRightSucc n m in
  (f :: s :: (vectMerge xs ys))

sym in sym $ plusSuccRightSucc n m reverses the direction of rewrite.