{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Zero
data Succ n

data Vec a n where
    Nil :: Vec a Zero
    Cons :: a -> Vec a n -> Vec a (Succ n)

headSafe :: Vec a (Succ n) -> a
headSafe (Cons x _) = x 
-- headSafe Nil = error "bad, bad boy"

tailSafe :: Vec a (Succ n) -> Vec a n
tailSafe (Cons _ xs ) = xs

-- xxx = headSafe Nil -- does not typecheck!
-- yyy = headSafe (Cons 'a' Nil :: Vec Char (Succ Zero))

mapSafe :: (a -> b) -> Vec a n -> Vec b n
mapSafe _ Nil = Nil
mapSafe f (Cons x xs) = Cons (f x) (mapSafe f xs) 

zipWithSafe :: (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n  -- necessary, cannot be deduced!
zipWithSafe f Nil Nil = Nil
zipWithSafe f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWithSafe f xs ys)

snoc :: Vec a n -> a -> Vec a (Succ n) -- necessary, cannot be deduced!
snoc Nil         y = Cons y Nil
snoc (Cons x xs) y = Cons x (snoc xs y)

reverseSafe :: Vec a n -> Vec a n -- necessary, cannot be deduced!
reverseSafe Nil = Nil
reverseSafe (Cons x xs) = snoc xs x

-- vector join, using GADTs only

data Sum m n s where
   SumZero :: Sum Zero n n
   SumSucc :: Sum m n s -> Sum (Succ m) n (Succ s)

append :: Sum m n s -> Vec a m -> Vec a n -> Vec a s
append SumZero Nil ys = ys
append (SumSucc p) (Cons x xs) ys = Cons x (append p xs ys)

-- append (SumSucc(SumSucc SumZero)) (Cons 'a' (Cons 'b' Nil)) (Cons 'c' Nil)

-- vector join, using GADTs + Type Families

type family SSum m n :: * 
type instance SSum Zero n = n
type instance SSum (Succ m) n = Succ (SSum m n)

append2 :: Vec a m -> Vec a n -> Vec a (SSum m n)
append2 Nil ys = ys
append2 (Cons x xs) ys = Cons x (append2 xs ys)

-- append2 (Cons 'a' (Cons 'b' Nil)) (Cons 'c' Nil)

instance (Show a) => Show (Vec a n) where
  show Nil = ""
  show (Cons a b) = show a ++ show b