{-# LANGUAGE TypeFamilies, EmptyDataDecls, GADTs #-}
{-# OPTIONS -fallow-undecidable-instances #-}
module Main where

-- peano number basics & addition type family
data Zero
data Succ a
type family Add n m

-- type family instances
type instance Add Zero     n = n
type instance Add (Succ n) m = Succ (Add n m)

data Vec e len where
    Nil  :: Vec e Zero
    Cons :: e -> Vec e len -> Vec e (Succ len)

-- basic show instances
instance (Show e) => Show (Vec e len) where
    show Nil         = "Nil"
    show (Cons x xs) = "Cons "++ (show x) ++ " ("++(show xs)++")"

instance (Eq e) => Eq (Vec e len) where
    Nil         == Nil      = True
    (Cons x xs) == (Cons x' xs') = x == x' && xs == xs'

-- append two vec's
vappend :: Vec e n -> Vec e m -> Vec e (Add n m)
vappend Nil          l = l
vappend (Cons x xs) ys = Cons x (vappend xs ys)

-- create a singleton vector
vsingleton :: e -> Vec e (Succ Zero)
vsingleton x = Cons x Nil

main = print $ Cons 1 (Cons 2 Nil) == vappend (vsingleton 1) (vsingleton 2)
{- type err if:
       print $ Cons 2 Nil == vappend (vsingleton 1) (vsingleton 2)
-}