{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Handy typenat utils.

module Generic.Data.Function.Common.TypeNats where

-- natVal''
import GHC.TypeNats ( Natural, KnownNat, natVal' )
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 #-}