reverse Data.HVect in Idris

reverse_hvect.idr

module reverse_hvect

import Data.Vect
import Data.HVect

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

reverse : HVect ts -> HVect (myReverse ts)
reverse [] = []
reverse (x::xs) = (reverse xs) ++ [x]

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

Type checking .\reverse_hvect.idr
reverse_hvect.idr:12:9:When checking right hand side of reverse_hvect.reverse with expected type
        HVect (myReverse (t :: ts))

Type mismatch between
        HVect (myReverse ts ++ [t]) (Type of reverse xs ++ [x])
and
        HVect (replace (sym (replace (sym (replace (sym (plusZeroRightNeutral k)) Refl)) (replace (sym (plusSuccRightSucc k 0)) Refl))) (myReverse ts ++ [t])) (Expected type)

Specifically:
        Type mismatch between
                myReverse ts ++ [t]
        and
                replace (sym (replace (sym (replace (sym (plusZeroRightNeutral k)) Refl)) (replace (sym (plusSuccRightSucc k 0)) Refl))) (myReverse ts ++ [t])
Holes: reverse_hvect.reverse