> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE GADTs, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts,
>     MultiParamTypeClasses, UndecidableInstances, ScopedTypeVariables,
>     RankNTypes #-}

> module Vec where

> import Control.Applicative

> import ShePrelude

> data Nat :: * where
>   Z :: Nat
>   S :: Nat -> Nat
>   deriving (SheSingleton)

> {-
> data Down :: ({Nat} -> *) -> {Nat} -> * where
>   DNil :: Down x {Z}
>   DCons :: x {n} -> Down x {n} -> Down x {S n}
> -}

> data Vec :: {Nat} -> * -> * where
>   VNil :: Vec {Z} x
>   (:>) :: x -> Vec {n} x -> Vec {S n} x
>   deriving ()

> instance Show x => Show (Vec {n} x) where
>   show VNil       = "VNil"
>   show (x :> xs)  = show x ++ " :> " ++ show xs

> vtail :: Vec {S n} x -> Vec {n} x
> vtail (x :> xs) = xs

> type family (m :: {Nat}) :+ (n :: {Nat}) :: {Nat}
> type instance {Z} :+ n = n
> type instance {S m} :+ n = {S} (m :+ n)

> instance Functor (Vec {n}) where
>   fmap f VNil = VNil
>   fmap f (x :> xs) = f x :> fmap f xs

> vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
> vappend VNil ys = ys
> vappend (x :> xs) ys = x :> vappend xs ys

> instance {:n :: Nat:} => Applicative (Vec {n}) where
>   pure = vec {:n :: Nat:} where
>     vec :: forall x. pi (n :: Nat). x -> Vec {n} x
>     vec {Z}    x = VNil
>     vec {S n}  x = x :> vec n x
>   (<*>) = vapp where
>     vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t
>     vapp VNil VNil = VNil
>     vapp (f :> fs)  (s :> ss) = f s :> vapp fs ss

> fiveByFive :: Vec {S (S (S (S (S Z))))} Int
> fiveByFive = pure 5

> vtakePox :: forall n. Pox n ->
>             forall x. pi (m :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x
> vtakePox n {Z}   xs         = VNil
> vtakePox n {S m} (x :> xs)  = x :> vtakePox n {m} xs

> listVec :: [a] -> (pi (n :: Nat). Vec {n} a -> t) -> t
> listVec [] f = f {Z} VNil
> listVec (x : xs) f = listVec xs (\ n ys -> f {S n} (x :> ys))

> data Pox n = Pox

> pox :: forall box. (forall n. Pox n -> box n) -> (forall n. box n)
> pox f = f Pox

> newtype TakeBox n = TakeBox
>   {unboxTake :: forall x. pi (m :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x}

> -- vtake :: forall n x. pi (m :: Nat). Vec ({m} :+ {n}) x -> Vec {m} x
> vtake = unboxTake (pox (TakeBox . vtakePox))