diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,7 @@
+0.13.1 [2021.10.31]
+-------------------
+* Allow building with GHC 9.2.
+
 0.13 [2021.02.17]
 -----------------
 * `Data.Constraint.Symbol` now reexports the `GHC.TypeLits.AppendSymbol` type
diff --git a/constraints.cabal b/constraints.cabal
--- a/constraints.cabal
+++ b/constraints.cabal
@@ -1,6 +1,6 @@
 name:          constraints
 category:      Constraints
-version:       0.13
+version:       0.13.1
 license:       BSD2
 cabal-version: >= 1.10
 license-file:  LICENSE
@@ -23,8 +23,10 @@
              , GHC == 8.2.2
              , GHC == 8.4.4
              , GHC == 8.6.5
-             , GHC == 8.8.3
-             , GHC == 8.10.1
+             , GHC == 8.8.4
+             , GHC == 8.10.7
+             , GHC == 9.0.1
+             , GHC == 9.2.1
 extra-source-files: README.markdown
                   , CHANGELOG.markdown
 
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
@@ -77,10 +77,10 @@
 axiom :: forall a b. Dict (a ~ b)
 axiom = unsafeCoerce (Dict :: Dict (a ~ a))
 
-axiomLe :: forall a b. Dict (a <= b)
+axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)
 axiomLe = axiom
 
-eqLe :: (a ~ b) :- (a <= b)
+eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)
 eqLe = Sub Dict
 
 dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
@@ -150,10 +150,18 @@
 timesOne = Dict
 
 minZero :: forall n. Dict (Min n 0 ~ 0)
+#if MIN_VERSION_base(4,16,0)
+minZero = axiom
+#else
 minZero = Dict
+#endif
 
 maxZero :: forall n. Dict (Max n 0 ~ n)
+#if MIN_VERSION_base(4,16,0)
+maxZero = axiom
+#else
 maxZero = Dict
+#endif
 
 powZero :: forall n. Dict ((n ^ 0) ~ 1)
 powZero = Dict
@@ -161,8 +169,12 @@
 leZero :: forall a. (a <= 0) :- (a ~ 0)
 leZero = Sub axiom
 
-zeroLe :: forall a. Dict (0 <= a)
+zeroLe :: forall (a :: Nat). Dict (0 <= a)
+#if MIN_VERSION_base(4,16,0)
+zeroLe = axiom
+#else
 zeroLe = Dict
+#endif
 
 plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)
 plusMinusInverse1 = axiom
@@ -346,11 +358,11 @@
 
 -- (<=) is an internal category in the category of constraints.
 
-leId :: forall a. Dict (a <= a)
+leId :: forall (a :: Nat). Dict (a <= a)
 leId = Dict
 
-leEq :: forall a b. (a <= b, b <= a) :- (a ~ b)
+leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)
 leEq = Sub axiom
 
-leTrans :: forall a b c. (b <= c, a <= b) :- (a <= c)
+leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c)
 leTrans = Sub (axiomLe @a @c)