Vector map in Haskell

VectMap.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

module VectMap where

import GHC.TypeLits

data Vect (n :: Nat) a where
  Nil  ::                  Vect 0 a
  Cons :: a -> Vect n a -> Vect (1 + n) a


vMap :: (a -> b) -> Vect n a -> Vect n b
vMap _ Nil         = Nil
vMap f (Cons a as) = f a `Cons` vMap f as