{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Safe #-}
{-# OPTIONS_GHC -Wno-unused-top-binds -fexpose-all-unfoldings #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module GHC.TypeLits.KnownNat () where
import Data.Bits (shiftL)
import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownNat, Nat, type (+), type (*), type (^), natVal)
newtype SNatKn (n :: Nat) = SNatKn Integer
class KnownNatAdd (a :: Nat) (b :: Nat) where
natSingAdd :: SNatKn (a + b)
instance (KnownNat a, KnownNat b) => KnownNatAdd a b where
natSingAdd = SNatKn (natVal (Proxy @ a) + natVal (Proxy @ b))
{-# INLINE natSingAdd #-}
class KnownNatMul (a :: Nat) (b :: Nat) where
natSingMul :: SNatKn (a * b)
instance (KnownNat a, KnownNat b) => KnownNatMul a b where
natSingMul = SNatKn (natVal (Proxy @ a) * natVal (Proxy @ b))
{-# INLINE natSingMul #-}
class KnownNatExp (a :: Nat) (b :: Nat) where
natSingExp :: SNatKn (a ^ b)
instance (KnownNat a, KnownNat b) => KnownNatExp a b where
natSingExp = let x = natVal (Proxy @ a)
y = natVal (Proxy @ b)
z = case x of
2 -> shiftL 1 (fromInteger y)
_ -> x ^ y
in SNatKn z
{-# INLINE natSingExp #-}