Roundtrip a String through Vect and back

roundtrip.idr

module Main

import Data.Vect

listToVect : List a -> (n ** Vect n a)
listToVect [] = (0 ** [])
listToVect (a :: as) with (listToVect as)
  | (n ** as') = (1 + n ** a :: as')

stringToVect : String -> (n ** Vect n Char)
stringToVect = listToVect . unpack

vectToList : Vect n a -> List a
vectToList [] = []
vectToList (a :: as) = a :: vectToList as

vectToString : Vect n Char -> String
vectToString = pack . vectToList

roundtrip : String -> String
roundtrip s with (stringToVect s)
  | (_ ** s') = vectToString s'