Minimal reification example extracted from https://blog.jle.im/entry/fixed-length-vector-types-in-haskell.html

MinimalReificationExample.hs

#!/usr/bin/env stack
-- stack --resolver nightly-2017-09-13 --install-ghc exec ghci --package vector

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import Data.Type.Equality ((:~:)(Refl))
import Data.Proxy (Proxy(..))
import Data.Vector (Vector)
import qualified Data.Vector as Vector
import GHC.TypeNats (KnownNat, Nat)
import qualified GHC.TypeNats as TypeNats

data Vec (n :: Nat) a = UnsafeMkVec { getVector :: Vector a }
  deriving Show

-- Reification is taking a "value-level runtime property (the length) and bringing
-- it up to the type-level".  See the 'withVec' function.
exactLength :: forall n m a. (KnownNat n, KnownNat m) => Vec n a -> Maybe (Vec m a)
exactLength v = case TypeNats.sameNat (Proxy @n) (Proxy @m) of
  Just Refl -> Just v
  Nothing -> Nothing

zipSame :: forall a b. Vector a -> Vector b -> Maybe (Vector (a, b))
zipSame v1 v2 = withVec v1 $ \(v1' :: Vec n a) ->
                withVec v2 $ \(v2' :: Vec m b) ->
                case exactLength v1' of
                  Just v1Same -> Just $ getVector (zipVec v1Same v2')
                  Nothing -> Nothing

withVec :: Vector a -> (forall n. KnownNat n => Vec n a -> r) -> r
withVec v f = case TypeNats.someNatVal (fromIntegral (Vector.length v)) of
  TypeNats.SomeNat (Proxy :: Proxy m) -> f (UnsafeMkVec @m v)

zipVec :: Vec n a -> Vec n b -> Vec n (a, b)
zipVec (UnsafeMkVec xs) (UnsafeMkVec ys) = UnsafeMkVec (Vector.zip xs ys)