-------------------------------------------------------------
-- |
-- Module      : Data.Nat
-- Copyright   : (C) 2015, Yu Fukuzawa
-- License     : BSD3
-- Maintainer  : minpou.primer@email.com
-- Stability   : experimental
-- Portability : portable
--
-----------------------------------------------------------

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

module Data.Nat where

data Nat = Z | S Nat

data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

class SingNat (n :: Nat) where
  singNat :: SNat n

instance SingNat Z where
  singNat = SZ
  {-# INLINE singNat #-}

instance SingNat n => SingNat (S n) where
  singNat = SS singNat
  {-# INLINE singNat #-}

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

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

class (:<=) (n :: Nat) (m :: Nat) where
instance (:<=) Z n
instance (n :<= m) => (:<=) (S n) (S m)