Reverse Vec in Haskell without theorem proving

ReverseVec.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module ReverseVec where

data Nat = Z | S Nat

data Vec a (n :: Nat) where
  Nil  :: Vec a Z
  Cons :: a -> Vec a n -> Vec a (S n)

newtype Bump (p :: Nat -> *) (n :: Nat) = Bump { lower :: p (S n) }

foldlVec :: forall p a m.
            (forall n. a -> p n -> p (S n)) ->
            p Z ->
            Vec a m -> p m
foldlVec pS pZ Nil         = pZ
foldlVec pS pZ (Cons x xs) = lower $ foldlVec pSS pSZ xs
  where
    pSS :: forall n. a -> Bump p n -> Bump p (S n)
    pSS = \ a -> Bump . pS a . lower
    pSZ = Bump $ pS x pZ

reverse :: Vec a n -> Vec a n
reverse = foldlVec Cons Nil

instance Show a => Show (Vec a n) where
  show Nil         = "[]"
  show (Cons x xs) = show x ++ " : " ++ show xs