diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,8 @@
+0.14.2 [2024.05.12]
+-------------------
+* Re-export `Log2` from `Data.Constraint.Nat`.
+* Add `log2Nat` and `log2Pow` to `Data.Constraint.Nat`.
+
 0.14.1 [2024.04.29]
 -------------------
 * Remove an unused dependency on the `type-equality` library.
diff --git a/constraints.cabal b/constraints.cabal
--- a/constraints.cabal
+++ b/constraints.cabal
@@ -1,7 +1,7 @@
 cabal-version: 2.4
 name:          constraints
 category:      Constraints
-version:       0.14.1
+version:       0.14.2
 license:       BSD-2-Clause
 license-file:  LICENSE
 author:        Edward A. Kmett
@@ -60,6 +60,9 @@
     , hashable       >= 1.2   && < 1.5
     , mtl            >= 2.2   && < 2.4
     , transformers   >= 0.5   && < 0.7
+  if !impl(ghc >= 9.0)
+    build-depends:
+      integer-gmp
 
   exposed-modules:
     Data.Constraint
diff --git a/src/Data/Constraint/Nat.hs b/src/Data/Constraint/Nat.hs
--- a/src/Data/Constraint/Nat.hs
+++ b/src/Data/Constraint/Nat.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -15,8 +16,8 @@
 --
 -- This module is only available on GHC 8.0 or later.
 module Data.Constraint.Nat
-  ( Min, Max, Lcm, Gcd, Divides, Div, Mod
-  , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat
+  ( Min, Max, Lcm, Gcd, Divides, Div, Mod, Log2
+  , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat, log2Nat
   , plusZero, minusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne
   , plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates
   , plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes
@@ -36,6 +37,7 @@
   , euclideanNat
   , plusMod, timesMod
   , modBound
+  , log2Pow
   , dividesDef
   , timesDiv
   , eqLe, leEq, leId, leTrans
@@ -47,10 +49,17 @@
 import Data.Constraint.Unsafe
 import Data.Proxy
 import Data.Type.Bool
-import GHC.TypeLits
-#if MIN_VERSION_base(4,18,0)
-import qualified GHC.TypeNats as TN
+import GHC.TypeNats
+import qualified Numeric.Natural as Nat
+
+#if MIN_VERSION_base(4,15,0)
+import GHC.Num.Natural (naturalLog2)
 #else
+import GHC.Exts (Int(..))
+import GHC.Integer.Logarithms (integerLog2#)
+#endif
+
+#if !MIN_VERSION_base(4,18,0)
 import Unsafe.Coerce
 #endif
 
@@ -69,13 +78,20 @@
 newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))
 #endif
 
-magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
+magicNNN :: forall n m o. (Nat.Natural -> Nat.Natural -> Nat.Natural) -> (KnownNat n, KnownNat m) :- KnownNat o
 #if MIN_VERSION_base(4,18,0)
-magic f = Sub $ TN.withKnownNat @o (unsafeSNat (fromInteger (natVal (Proxy @n) `f` natVal (Proxy @m)))) Dict
+magicNNN f = Sub $ withKnownNat @o (unsafeSNat (natVal (Proxy @n) `f` natVal (Proxy @m))) Dict
 #else
-magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))
+magicNNN f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy @n) `f` natVal (Proxy @m))
 #endif
 
+magicNN :: forall n m. (Nat.Natural -> Nat.Natural) -> KnownNat n :- KnownNat m
+#if MIN_VERSION_base(4,18,0)
+magicNN f = Sub $ withKnownNat @m (unsafeSNat (f (natVal (Proxy @n)))) Dict
+#else
+magicNN f = Sub $ unsafeCoerce (Magic Dict) (f (natVal (Proxy :: Proxy n)))
+#endif
+
 axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)
 axiomLe = unsafeAxiom
 
@@ -107,35 +123,45 @@
 lcmOne = unsafeAxiom
 
 gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
-gcdNat = magic gcd
+gcdNat = magicNNN gcd
 
 lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
-lcmNat = magic lcm
+lcmNat = magicNNN lcm
 
 plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
-plusNat = magic (+)
+plusNat = magicNNN (+)
 
 minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
-minusNat = Sub $ case magic @n @m (-) of Sub r -> r
+minusNat = Sub $ case magicNNN @n @m (-) of Sub r -> r
 
 minNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)
-minNat = magic min
+minNat = magicNNN min
 
 maxNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)
-maxNat = magic max
+maxNat = magicNNN max
 
 timesNat  :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)
-timesNat = magic (*)
+timesNat = magicNNN (*)
 
 powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
-powNat = magic (^)
+powNat = magicNNN (^)
 
 divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
-divNat = Sub $ case magic @n @m div of Sub r -> r
+divNat = Sub $ case magicNNN @n @m div of Sub r -> r
 
 modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
-modNat = Sub $ case magic @n @m mod of Sub r -> r
+modNat = Sub $ case magicNNN @n @m mod of Sub r -> r
 
+log2Nat :: forall n. (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
+log2Nat = Sub $ case magicNN @n log2 of Sub r -> r
+  where
+    log2 :: Nat.Natural -> Nat.Natural
+#if MIN_VERSION_base(4,15,0)
+    log2 n = fromIntegral (naturalLog2 n)
+#else
+    log2 n = fromIntegral (I# (integerLog2# (toInteger n)))
+#endif
+
 plusZero :: forall n. Dict ((n + 0) ~ n)
 plusZero = Dict
 
@@ -231,6 +257,9 @@
 
 modBound :: forall m n. (1 <= n) :- (Mod m n <= n)
 modBound = Sub unsafeAxiom
+
+log2Pow :: forall n. Dict (Log2 (2 ^ n) ~ n)
+log2Pow = unsafeAxiom
 
 euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))
 euclideanNat = Sub unsafeAxiom
diff --git a/src/Data/Constraint/Symbol.hs b/src/Data/Constraint/Symbol.hs
--- a/src/Data/Constraint/Symbol.hs
+++ b/src/Data/Constraint/Symbol.hs
@@ -64,21 +64,21 @@
 #if MIN_VERSION_base(4,18,0)
 magicNSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))) Dict
 #else
-magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy :: Proxy n)) `f` symbolVal (Proxy :: Proxy m))
+magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))
 #endif
 
 magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o
 #if MIN_VERSION_base(4,18,0)
 magicSSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))) Dict
 #else
-magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy :: Proxy n) `f` symbolVal (Proxy :: Proxy m))
+magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))
 #endif
 
 magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n
 #if MIN_VERSION_base(4,18,0)
 magicSN f = Sub $ TN.withKnownNat (unsafeSNat @n (fromIntegral (f (symbolVal (Proxy :: Proxy a))))) Dict
 #else
-magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy :: Proxy a))))
+magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy @a))))
 #endif
 
 -- operations