{-# LANGUAGE EmptyDataDecls           #-}
{-# LANGUAGE KindSignatures           #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE DeriveDataTypeable       #-}

module MIR.HarmGram.TypeLevel (
      Su, Ze 
    , T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10
    , ToNat(..)
  ) where

import Data.Typeable


-- Type level peano naturals
data Su :: * -> *  deriving Typeable
data Ze :: *       deriving Typeable

-- Some shorthands
type T0 = Ze
type T1 = Su T0
type T2 = Su T1
type T3 = Su T2
type T4 = Su T3
type T5 = Su T4
type T6 = Su T5
type T7 = Su T6
type T8 = Su T7
type T9 = Su T8
type T10 = Su T9

class ToNat n where
  toNat :: n -> Int

instance ToNat Ze where toNat _ = 0
instance (ToNat n) => ToNat (Su n) where toNat _ = 1 + toNat (undefined :: n)