Векторы фиксированной на уровне типа длины

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE KindSignatures      #-}
 
data Peano = Z | S Peano deriving Show
data Vec (n :: Peano) a where VNil :: Vec 'Z a
                                VCons :: a -> Vec n a -> Vec ('S n) a
infixr 5 `VCons`
deriving instance Show a => Show (Vec n a)

{-# LANGUAGE Haskell2010         #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE KindSignatures      #-}
 
import Data.Proxy
import GHC.TypeLits
 
data Peano = Z | S Peano deriving Show
data Vec (n :: Peano) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a
infixr 5 `VCons`
deriving instance Show a => Show (Vec n a)
 
class ListToVec (n :: Peano) where
  listToVec :: [a] -> Maybe (Vec n a)
 
instance ListToVec Z where
  listToVec [] = Just VNil
  listToVec (x:xs) = Nothing
 
instance ListToVec n => ListToVec (S n) where
  listToVec [] = Nothing
  listToVec (x:xs) = VCons x <$> listToVec xs
 
main :: IO ()
main = do
  print $ (listToVec []      :: Maybe (Vec Z Int))             -- Just VNil
  print $ (listToVec [1,2,3] :: Maybe (Vec (S (S (S Z))) Int)) -- Just (VCons 1 (VCons 2 (VCons 3 VNil)))
  print $ (listToVec [1,2]   :: Maybe (Vec (S (S (S Z))) Int)) -- Nothing
  print $ (listToVec [1,2,3] :: Maybe (Vec (S (S Z)) Int))     -- Nothing