reverse_vect.idr

module reverse_vect

import Data.Vect

myReverse : Vect n a -> Vect n a
myReverse [] = []
myReverse (x::xs) = (myReverse xs) ++ [x]

I try to reverse a Data.Vect but my code results in an error:

Type checking .\reverse_vect.idr
reverse_vect.idr:16:11:When checking right hand side of myReverse with expected type
        Vect (S k) a

Type mismatch between
        Vect (k + 1) a (Type of myReverse xs ++ [x])
and
        Vect (S k) a (Expected type)

Specifically:
        Type mismatch between
                plus k 1
        and
                S k
Holes: reverse_vect.myReverse

How can I fix it?

Hi, it should be:

module reverse_vect

import Data.Vect

myReverse : Vect n a -> Vect n a
myReverse [] = []
myReverse {n = S k} (x::xs) = rewrite plusCommutative 1 k in (myReverse xs) ++ [x]

The reason that k + 1 is not S k is that + is defined to recurse on the left argument in Nat. So k + 1 would not reduce any further since k is unknown rewriting with plusCommutative ensures that the arguments are flipped so that k + 1 becomes 1 + k which can reduce to S k. The reason that the type of myReverse xs ++ [x] is k + 1 is because of the definition of ++ which adds the length of the given arguments in the resulting Vect 😄