{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}

-- | Inductive type-level natural numbers
module Debug.RecoverRTTI.Nat (
    -- * Type-level natural numbers
    Nat(..)
  , SNat(..)
  , KnownNat(..)
  , natVal
    -- * Type level functions computing natural numbers
  , Length
  ) where

{-------------------------------------------------------------------------------
  Natural numbers
-------------------------------------------------------------------------------}

-- | Natural numbers
--
-- Intended to be used lifted to the type level; unlike @ghc@'s type level
-- natural numbers, these are inductive.
data Nat = Z | S Nat

-- | Singleton for 'Nat'
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

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

instance               KnownNat 'Z     where singNat :: SNat 'Z
singNat = SNat 'Z
SZ
instance KnownNat n => KnownNat ('S n) where singNat :: SNat ('S n)
singNat = SNat n -> SNat ('S n)
forall (n :: Nat). SNat n -> SNat ('S n)
SS SNat n
forall (n :: Nat). KnownNat n => SNat n
singNat

natVal :: forall n proxy. KnownNat n => proxy n -> Int
natVal :: proxy n -> Int
natVal proxy n
_ = SNat n -> Int
forall (m :: Nat). SNat m -> Int
go (SNat n
forall (n :: Nat). KnownNat n => SNat n
singNat :: SNat n)
  where
    go :: forall m. SNat m -> Int
    go :: SNat m -> Int
go SNat m
SZ     = Int
0
    go (SS SNat n
n) = SNat n -> Int
forall (m :: Nat). SNat m -> Int
go SNat n
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

{-------------------------------------------------------------------------------
  Type-level functions computing natural numbers
-------------------------------------------------------------------------------}

type family Length (xs :: [k]) :: Nat where
  Length '[]       = 'Z
  Length (_ ': xs) = 'S (Length xs)