{-# LANGUAGE EmptyDataDecls,
             Rank2Types,
             TypeFamilies,
             TypeOperators,
             ScopedTypeVariables,
             UndecidableInstances #-}

module TypeNat (Z, S,
                (:+:), (:*:), (:^:),
                TypeNat, reflectTypeNat, 
                Zero, Succ, One, Two, Three, Four) where

infixl 6 :+:
infixl 7 :*:
infixr 8 :^:


data Z
data S a


type family a :+: b
type instance Z :+: a = a
type instance S a :+: b = S (a :+: b)

type family a :*: b
type instance Z :*: a = Z
type instance S a :*: b = a :*: b :+: b

type family a :^: b
type instance a :^: Z = S Z
type instance a :^: S b = a :^: b :*: a


class TypeNat a where
  reflectTypeNat :: (Num b) => a -> b

instance TypeNat Z where
  reflectTypeNat _ = 0
instance (TypeNat a) => TypeNat (S a) where
  reflectTypeNat _ = reflectTypeNat (undefined :: a) + 1


reifyTypeNat :: (Num a, Ord a) => a -> (forall b . (TypeNat b) => b -> c) -> c
reifyTypeNat 0 k = k (undefined :: Z)
reifyTypeNat a k | a > 0 = reifyTypeNat (a - 1) (\(_ :: b) -> k (undefined :: S b))
                 | a < 0 = undefined