{-# Language DataKinds #-}
{-# Language GADTs #-}
{-# Language KindSignatures #-}
{-# Language NoImplicitPrelude #-}
{-# Language StandaloneDeriving #-}
{-# Language TypeFamilies #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Vect where

import Prelude (Show)
import GHC.Types (Type)

data Nat where
  Z :: Nat
  S :: Nat -> Nat
  deriving Show

data Vect (n :: Nat) (a :: Type) where
  Nil  :: Vect Z a
  Cons :: a -> Vect n a -> Vect (S n) a

deriving instance Show a => Show (Vect n a)

head :: Vect (S n) a -> a
head (Cons x _) = x

tail :: Vect (S n) a -> Vect n a
tail (Cons _ xs) = xs

type family Add (n :: Nat) (m :: Nat) :: Nat where
  Add Z m = m
  Add (S n) m = S (Add n m)

(++) :: Vect n a -> Vect m a -> Vect (Add n m) a
Nil ++ ys = ys
(Cons x xs) ++ ys = Cons x (xs ++ ys)

data Fin (n :: Nat) where
  FZ :: Fin (S k)
  FS :: Fin k -> Fin (S k)

deriving instance Show (Fin n)

index :: Vect n a -> Fin n -> a
index (Cons x xs) FZ = x
index (Cons x xs) (FS n) = index xs n