{-# LANGUAGE AllowAmbiguousTypes #-} -- for my TypeApplications-based natVals
{-# LANGUAGE UndecidableInstances #-} -- for Length type family

-- | Handy typenat utils.

module Util.TypeNats where

-- natVal''
import GHC.TypeNats ( Natural, KnownNat, natVal', type (+) )
import GHC.Exts ( proxy#, Proxy# )

natVal'' :: forall n. KnownNat n => Natural
natVal'' :: forall (n :: Nat). KnownNat n => Nat
natVal'' = Proxy# n -> Nat
forall (n :: Nat). KnownNat n => Proxy# n -> Nat
natVal' (Proxy# n
forall {k} (a :: k). Proxy# a
proxy# :: Proxy# n)
{-# INLINE natVal'' #-}

natValInt :: forall n. KnownNat n => Int
natValInt :: forall (n :: Nat). KnownNat n => Int
natValInt = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
natVal'' @n
{-# INLINE natValInt #-}

-- TODO might wanna move this
-- | The length of a type-level list.
type family Length (a :: [k]) :: Natural where
    Length '[]       = 0
    Length (a ': as) = 1 + Length as