Reversable Vect

{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types                #-}
{-# LANGUAGE TypeFamilies              #-}

data Z
data S n

type family Plus m n where
    Plus Z m = m
    Plus (S n) m = S (Plus n m)

data Vect n where
    ZV :: Vect Z
    CV :: Int -> Vect n -> Vect (S n)

instance Show (Vect n) where
    show ZV = "Nil"
    show (CV x v) = show x ++ " : " ++ show v

vecReverse :: Vect n -> Vect m -> Vect (Plus n m)
vecReverse ZV w = w
vecReverse (CV x v) w = vecReverse v (CV x w)