diff --git a/modular-arithmetic.cabal b/modular-arithmetic.cabal
--- a/modular-arithmetic.cabal
+++ b/modular-arithmetic.cabal
@@ -1,6 +1,6 @@
 cabal-version:       2.2
 name:                modular-arithmetic
-version:             2.0.0.1
+version:             2.0.0.2
 synopsis:            A type for integers modulo some constant.
 
 description:         A convenient type for working with integers modulo some constant. It saves you from manually wrapping numeric operations all over the place and prevents a range of simple mistakes. @Integer `Mod` 7@ is the type of integers (mod 7) backed by @Integer@.
@@ -28,7 +28,8 @@
   default-language:    Haskell2010
   exposed-modules:     Data.Modular
   build-depends:       base >4.9 && <5
-                     , typelits-witnesses <0.5
+  if impl(ghc < 9.2.1)
+    build-depends:     typelits-witnesses <0.5
 
 test-suite examples
   hs-source-dirs:      test-suite, src
@@ -37,4 +38,5 @@
   type:                exitcode-stdio-1.0
   build-depends:       base >4.9 && <5
                      , doctest >= 0.9
-                     , typelits-witnesses <0.5
+  if impl(ghc < 9.2.1)
+    build-depends:     typelits-witnesses <0.5
diff --git a/src/Data/Modular.hs b/src/Data/Modular.hs
--- a/src/Data/Modular.hs
+++ b/src/Data/Modular.hs
@@ -29,7 +29,6 @@
 
 import           Data.Proxy    (Proxy (..))
 import           Data.Ratio    ((%), denominator, numerator)
-import           Data.Type.Equality     ((:~:)(..))
 
 import           Text.Printf   (printf)
 
@@ -39,8 +38,12 @@
 import           GHC.TypeLits
 #endif
 
+#if !MIN_VERSION_base(4,16,0)
+import           Data.Type.Equality     ((:~:)(..))
+
 import           GHC.TypeLits.Compare   ((%<=?), (:<=?)(LE, NLE))
 import           GHC.TypeLits.Witnesses (SNat (SNat))
+#endif
 
 -- $setup
 --
@@ -294,6 +297,13 @@
            -> Maybe (SomeMod i)
 someModVal i n = do
   SomeNat (_ :: Proxy n) <- someNatVal n
+#if MIN_VERSION_base(4,16,0)
+  case Proxy @1 `cmpNat` Proxy @n of
+    LTI -> pure $ SomeMod $ toMod @n i
+    EQI -> pure $ SomeMod $ toMod @n i
+    GTI -> Nothing
+#else
   case SNat @1 %<=? SNat @n of
     LE Refl -> pure $ SomeMod $ toMod @n i
     NLE _ _ -> Nothing
+#endif