{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

data Z
data S n

type family Pred n
type instance Pred (S n) = n

newtype Vec n a = Vec {
    foldV' :: forall u. forall b.
      u Z b ->
        (forall k. a ->
          u k b ->
          u (S k) b) ->
        u n b
  }

newtype Const n a = C { unC :: a }

c2 = C . C
unC2 = unC . unC

foldCV z c = unC . foldV (C z) (\x (C xs) -> C $ c x xs)

foldV ::
  u Z b ->
    (forall k. a ->
      u k b ->
      u (S k) b) ->
    Vec n a -> u n b
foldV z c v = foldV' v z c

nilV = Vec $ \z c -> z

consV :: a -> Vec n a -> Vec (S n) a
consV a v = Vec $ \z c -> c a (foldV z c v)

(@:) = consV

infixr @:

newtype TailV n a = TailV { unwrapTV :: (Vec (Pred n) a, Vec n a) }

tailV :: Vec (S n) a -> Vec n a
tailV = fst . unwrapTV . foldV (TailV (undefined, nilV)) step
  where
    step :: a -> TailV k a -> TailV (S k) a
    step x (TailV (_, xs)) = TailV (xs, x `consV` xs)

headV :: Vec (S n) a -> a
headV = foldCV undefined const

unconsV v = (headV v, tailV v)

instance Show a => Show (Vec n a) where
  show = unC2 . foldV (c2 "nilV") (\x xs -> c2 $ show x ++ " @: " ++ unC2 xs)

main :: IO ()
main = putStrLn . show . unconsV $ 1 @: 2 @: 3 @: 4 @: nilV