content: {-# LANGUAGE GADTs #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE ExplicitForAll #-}
  
  import Data.Type.Equality
  
  data Nat = Z | S Nat
  
  data SNat n where
    Zero :: SNat Z
    Succ :: SNat n -> SNat (S n)
  
  data Vec :: * -> Nat -> * where
    Nil :: Vec a Z
    Cons :: a -> Vec a n -> Vec a (S n)
  
  instance Show a => Show (Vec a n) where
    show Nil         = "Nil"
    show (Cons x xs) = "Cons " ++ show x ++ " (" ++ show xs ++ ")"
  
  type family (m :: Nat) :+ (n :: Nat) :: Nat where
    Z :+ n = n
    S m :+ n = S (m :+ n)
  
  -- (a ~ b) implies (f a ~ f b)
  cong :: a :~: b -> f a :~: f b
  cong Refl = Refl
  
  -- (a ~ b) implies (f a) implies (f b)
  subst :: a :~: b -> f a -> f b
  subst Refl = id
  
  plus_zero :: forall n. SNat n -> (n :+ Z) :~: n
  plus_zero Zero = Refl
  plus_zero (Succ n) = cong (plus_zero n)
  
  plus_suc :: forall n m. SNat n -> SNat m -> (n :+ (S m)) :~: (S (n :+ m))
  plus_suc Zero m = Refl
  plus_suc (Succ n) m = cong (plus_suc n m)
  
  size :: Vec a n -> SNat n
  size Nil         = Zero
  size (Cons _ xs) = Succ $ size xs
  
  reverse :: forall n a. Vec a n -> Vec a n
  reverse xs = subst (plus_zero (size xs)) $ go Nil xs
    where
      go :: Vec a m -> Vec a k -> Vec a (k :+ m)
      go acc Nil = acc
      go acc (Cons x xs) = subst (plus_suc (size xs) (size acc)) $ go (Cons x acc) xs
  
  append :: Vec a n -> Vec a m -> Vec a (n :+ m)
  append (Cons x xs) ys = Cons x (append xs ys)
  append Nil         ys = ys
  
  vec :: Vec Int (S (S (S Z)))
  vec = 1 `Cons` (2 `Cons` (3 `Cons` Nil))
  
  test :: Vec Int (S (S (S Z)))
  test = Main.reverse vec
  