Reversing Vectors... 2

{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# 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

class VecReverse n m where
    vecReverse :: Vect n -> Vect m -> Vect (Plus n m)
    
instance VecReverse Z m where
    vecReverse _ w = w

instance (VecReverse n (S m), Plus n (S m) ~ S (Plus n m)) => VecReverse (S n) m where
    vecReverse (CV x v) w = vecReverse v (CV x w)