reverse Data.HVect in Idris

reverse_hvect.idr

module reverse_hvect

import Data.HVect

reverse : HVect ts -> HVect (reverse 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:7:9:When checking right hand side of reverse_hvect.reverse with expected type
        HVect (reverse (t :: ts))

Type mismatch between
        HVect (Data.Vect.reverse, go Type k ts [] ts ++ [t]) (Type of reverse xs ++ [x])
and
        HVect (Data.Vect.reverse, go Type (S k) (t :: ts) [t] ts) (Expected type)

Specifically:
        Type mismatch between
                Data.Vect.reverse, go Type k ts [] ts ++ [t]
        and
                Data.Vect.reverse, go Type (S k) (t :: ts) [t] ts
Holes: reverse_hvect.reverse

An example how reverse should work:

myHVect : HVect [Int, String, List Nat]
myHVect = [42, "text", [1, 2, 3]]

reversedHVect : HVect [List Nat, String, Int]
reversedHVect = reverse myHVect -- should be: [[1, 2, 3], "text", 42]