diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,14 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.1.5.0 -- *2022 Mar 08*
+
+  * Add support for GHC 9.2.  Drop support for GHC 8.4 (or earlier).
+  * Add a `Data.Parameterized.NatRepr.leqZero :: LeqProof 0 n` function.
+    Starting with GHC 9.2, GHC is no longer able to conclude that
+    `forall (n :: Nat). 0 <= n` due to changes in how the `(<=)` type family
+    works. As a result, this fact must be asserted as an axiom, which the
+    `leqZero` function accomplishes.
+
 ## 2.1.4.0 -- *2021 Oct 1*
 
   * Added the `ifoldLM` and `fromSomeList`, `fromListWith`, and
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2013-2016 Galois Inc.
+Copyright (c) 2013-2022 Galois Inc.
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,11 +1,11 @@
 Cabal-version: 2.2
 Name:          parameterized-utils
-Version:       2.1.4.0
+Version:       2.1.5.0
 Author:        Galois Inc.
 Maintainer:    kquick@galois.com
 stability:     stable
 Build-type:    Simple
-Copyright:     ©2016-2021 Galois, Inc.
+Copyright:     ©2016-2022 Galois, Inc.
 License:       BSD-3-Clause
 License-file:  LICENSE
 category:      Data Structures, Dependent Types
@@ -19,7 +19,7 @@
 extra-source-files: Changelog.md
 homepage:      https://github.com/GaloisInc/parameterized-utils
 bug-reports:   https://github.com/GaloisInc/parameterized-utils/issues
-tested-with:   GHC==8.4.4, GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.1
+tested-with:   GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.1
 
 -- Many (but not all, sadly) uses of unsafe operations are
 -- controlled by this compile flag.  When this flag is set
@@ -59,7 +59,7 @@
                , hashable       >=1.2  && <1.4
                , hashtables     ==1.2.*
                , indexed-traversable
-               , lens           >=4.16 && <5.1
+               , lens           >=4.16 && <5.2
                , mtl
                , profunctors    >=5.6 && < 5.7
                , template-haskell
diff --git a/src/Data/Parameterized/ClassesC.hs b/src/Data/Parameterized/ClassesC.hs
--- a/src/Data/Parameterized/ClassesC.hs
+++ b/src/Data/Parameterized/ClassesC.hs
@@ -9,7 +9,7 @@
 These classes generally require type-level evidence for operations
 on their subterms, but don't actually provide it themselves (because
 their types are not themselves parameterized, unlike those in
-"Data.Parameterized.TraverableFC").
+"Data.Parameterized.TraversableFC").
 
 Note that there is still some ambiguity around naming conventions, see
 <https://github.com/GaloisInc/parameterized-utils/issues/23 issue 23>.
diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs
--- a/src/Data/Parameterized/Context/Unsafe.hs
+++ b/src/Data/Parameterized/Context/Unsafe.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE GADTs #-}
diff --git a/src/Data/Parameterized/NatRepr.hs b/src/Data/Parameterized/NatRepr.hs
--- a/src/Data/Parameterized/NatRepr.hs
+++ b/src/Data/Parameterized/NatRepr.hs
@@ -87,6 +87,7 @@
   , testStrictLeq
   , leqRefl
   , leqTrans
+  , leqZero
   , leqAdd2
   , leqSub2
   , leqMulCongr
@@ -347,7 +348,7 @@
 
 -- | @LeqProof m n@ is a type whose values are only inhabited when @m@
 -- is less than or equal to @n@.
-data LeqProof m n where
+data LeqProof (m :: Nat) (n :: Nat) where
   LeqProof :: (m <= n) => LeqProof m n
 
 -- | (<=) is a decidable relation on nats.
@@ -427,6 +428,10 @@
 leqTrans LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)
 {-# NOINLINE leqTrans #-}
 
+-- | Zero is less than or equal to any 'Nat'.
+leqZero :: LeqProof 0 n
+leqZero = unsafeCoerce (LeqProof :: LeqProof 0 0)
+
 -- | Add both sides of two inequalities
 leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
 leqAdd2 x y = seq x $ seq y $ unsafeCoerce (LeqProof :: LeqProof 0 0)
@@ -476,14 +481,14 @@
 -- | Produce proof that adding a value to the larger element in an LeqProof
 -- is larger
 leqAdd :: forall f m n p . LeqProof m n -> f p -> LeqProof m (n+p)
-leqAdd x _ = leqAdd2 x (LeqProof :: LeqProof 0 p)
+leqAdd x _ = leqAdd2 x (leqZero @p)
 
 leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)
 leqAddPos m n = leqAdd (leqProof (Proxy :: Proxy 1) m) n
 
 -- | Produce proof that subtracting a value from the smaller element is smaller.
 leqSub :: forall m n p . LeqProof m n -> LeqProof p m -> LeqProof (m-p) n
-leqSub x _ = leqSub2 x (LeqProof :: LeqProof 0 p)
+leqSub x _ = leqSub2 x (leqZero @p)
 
 addIsLeq :: f n -> g m -> LeqProof n (n + m)
 addIsLeq n m = leqAdd (leqRefl n) m
diff --git a/src/Data/Parameterized/NatRepr/Internal.hs b/src/Data/Parameterized/NatRepr/Internal.hs
--- a/src/Data/Parameterized/NatRepr/Internal.hs
+++ b/src/Data/Parameterized/NatRepr/Internal.hs
@@ -24,7 +24,7 @@
 import Data.Data
 import Data.Hashable
 import GHC.TypeNats
-import Numeric.Natural
+import qualified Numeric.Natural as Natural
 import Unsafe.Coerce
 
 import Data.Parameterized.Axiom
@@ -38,7 +38,7 @@
 --
 -- This can be used for performing dynamic checks on a type-level natural
 -- numbers.
-newtype NatRepr (n::Nat) = NatRepr { natValue :: Natural
+newtype NatRepr (n::Nat) = NatRepr { natValue :: Natural.Natural
                                      -- ^ The underlying natural value of the number.
                                    }
   deriving (Hashable, Data)
diff --git a/src/Data/Parameterized/TH/GADT.hs b/src/Data/Parameterized/TH/GADT.hs
--- a/src/Data/Parameterized/TH/GADT.hs
+++ b/src/Data/Parameterized/TH/GADT.hs
@@ -8,6 +8,7 @@
 -- This module declares template Haskell primitives so that it is easier
 -- to work with GADTs that have many constructors.
 ------------------------------------------------------------------------
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DoAndIfThenElse #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -66,7 +67,7 @@
   Q (Pat, [Name]) {- ^ pattern and bound names -}
 conPat con pre = do
   nms <- newNames pre (length (constructorFields con))
-  return (ConP (constructorName con) (VarP <$> nms), nms)
+  return (conPCompat (constructorName con) (VarP <$> nms), nms)
 
 
 -- | Return an expression corresponding to the constructor.
@@ -487,7 +488,7 @@
 showCon :: ExpQ -> Name -> Int -> MatchQ
 showCon p nm n = do
   vars <- newNames "x" n
-  let pat = ConP nm (VarP <$> vars)
+  let pat = conPCompat nm (VarP <$> vars)
   let go s e = [| $(s) . showChar ' ' . showsPrec 11 $(varE e) |]
   let ctor = [| showString $(return (LitE (StringL (nameBase nm)))) |]
   let rhs | null vars = ctor
@@ -694,6 +695,13 @@
 
 mkReprName :: Name -> Name
 mkReprName nm = mkName (nameBase nm ++ "Repr")
+
+conPCompat :: Name -> [Pat] -> Pat
+conPCompat n pats = ConP n
+#if MIN_VERSION_template_haskell(2,18,0)
+                           []
+#endif
+                           pats
 
 -- $typePatterns
 --
diff --git a/src/Data/Parameterized/Vector.hs b/src/Data/Parameterized/Vector.hs
--- a/src/Data/Parameterized/Vector.hs
+++ b/src/Data/Parameterized/Vector.hs
@@ -501,7 +501,10 @@
         snd <$> getCompose3 (natRecBounded (decNat h) (decNat h) base step)
       }
   where base :: Compose3 m ((,) b) (Vector' a) 0
-        base = Compose3 $ (\(hd, b) -> (b, MkVector' (singleton hd))) <$> gen (knownNat @0) start
+        base =
+          case leqZero @h of { LeqProof ->
+          Compose3 $ (\(hd, b) -> (b, MkVector' (singleton hd))) <$> gen (knownNat @0) start
+          }
         step :: forall p. (1 <= h, p <= h - 1)
              => NatRepr p
              -> Compose3 m ((,) b) (Vector' a) p
diff --git a/test/Test/Vector.hs b/test/Test/Vector.hs
--- a/test/Test/Vector.hs
+++ b/test/Test/Vector.hs
@@ -29,7 +29,7 @@
 import           Data.Parameterized.Some
 import           Data.Parameterized.Vector
 import           Data.Semigroup
-import           GHC.TypeLits
+import           GHC.TypeLits (KnownNat)
 import           Hedgehog
 import qualified Hedgehog.Gen as HG
 import           Hedgehog.Range