diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,11 @@
 
 ## UNRELEASED
 
+## 3.0.3 - 2023-04-18
+
+* Added `hasNoVariablesQ` and `forAllNonVariableDL` functions to help make
+  quantification require less boilerplate in `DL` properties.
+
 ## 3.0.2 - 2023-02-17
 
 * Added instances of `HasVariables` for Word types
diff --git a/quickcheck-dynamic.cabal b/quickcheck-dynamic.cabal
--- a/quickcheck-dynamic.cabal
+++ b/quickcheck-dynamic.cabal
@@ -1,6 +1,6 @@
 cabal-version:   2.2
 name:            quickcheck-dynamic
-version:         3.0.2
+version:         3.0.3
 license:         Apache-2.0
 license-files:
   LICENSE
diff --git a/src/Test/QuickCheck/DynamicLogic.hs b/src/Test/QuickCheck/DynamicLogic.hs
--- a/src/Test/QuickCheck/DynamicLogic.hs
+++ b/src/Test/QuickCheck/DynamicLogic.hs
@@ -22,6 +22,7 @@
   assertModel,
   monitorDL,
   forAllQ,
+  forAllNonVariableQ,
   forAllDL,
   forAllMappedDL,
   forAllUniqueDL,
@@ -119,6 +120,11 @@
 --   Generated values will only shrink to smaller values that could also have been generated.
 forAllQ :: Quantifiable q => q -> DL s (Quantifies q)
 forAllQ q = DL $ \s k -> DL.forAllQ q $ \x -> k x s
+
+-- | Generate a random value using the given `Quantification` (or list/tuple of quantifications).
+--   Generated values will only shrink to smaller values that could also have been generated.
+forAllNonVariableQ :: QuantifyConstraints (HasNoVariables a) => Quantification a -> DL s a
+forAllNonVariableQ q = DL $ \s k -> DL.forAllQ (hasNoVariablesQ q) $ \(HasNoVariables x) -> k x s
 
 runDL :: Annotated s -> DL s () -> DL.DynFormula s
 runDL s dl = unDL dl s $ \_ _ -> DL.passTest
diff --git a/src/Test/QuickCheck/DynamicLogic/Quantify.hs b/src/Test/QuickCheck/DynamicLogic/Quantify.hs
--- a/src/Test/QuickCheck/DynamicLogic/Quantify.hs
+++ b/src/Test/QuickCheck/DynamicLogic/Quantify.hs
@@ -18,11 +18,13 @@
   whereQ,
   chooseQ,
   withGenQ,
+  hasNoVariablesQ,
   validQuantification,
   Quantifiable (..),
 ) where
 
 import Control.Monad
+import Data.Coerce
 import Data.Maybe
 import Data.Typeable
 import System.Random
@@ -144,6 +146,14 @@
     (liftM2 (,) <$> genQ q <*> genQ q')
     (\(a, a') -> isaQ q a && isaQ q' a')
     (\(a, a') -> map (,a') (shrQ q a) ++ map (a,) (shrQ q' a'))
+
+-- | Wrap a Quantification in `HasNoVariables` to indicate that you know
+-- what you're doing and there are no symbolic variables in the thing you
+-- are quantifying over. WARNING: use this function carefully as there is
+-- no guarantee that you won't get bitten by very strange failures if you
+-- were in fact not honest about the lack of variables.
+hasNoVariablesQ :: Quantification a -> Quantification (HasNoVariables a)
+hasNoVariablesQ = coerce
 
 type QuantifyConstraints a = (Eq a, Show a, Typeable a, HasVariables a)
 
diff --git a/src/Test/QuickCheck/StateModel/Variables.hs b/src/Test/QuickCheck/StateModel/Variables.hs
--- a/src/Test/QuickCheck/StateModel/Variables.hs
+++ b/src/Test/QuickCheck/StateModel/Variables.hs
@@ -16,7 +16,7 @@
   isWellTyped,
   allVariables,
   unsafeCoerceVar,
-  unsafeNextVarIndex
+  unsafeNextVarIndex,
 ) where
 
 import Data.Data
@@ -61,6 +61,9 @@
 
 newtype HasNoVariables a = HasNoVariables a
 
+deriving via a instance Show a => Show (HasNoVariables a)
+deriving via a instance Eq a => Eq (HasNoVariables a)
+
 instance HasVariables (HasNoVariables a) where
   getAllVariables _ = mempty
 
@@ -127,7 +130,7 @@
 unsafeCoerceVar (Var i) = Var i
 
 unsafeNextVarIndex :: VarContext -> Int
-unsafeNextVarIndex (VarCtx vs) = 1 + maximum (0 : [ i | Some (Var i) <- Set.toList vs ])
+unsafeNextVarIndex (VarCtx vs) = 1 + maximum (0 : [i | Some (Var i) <- Set.toList vs])
 
 instance {-# OVERLAPPABLE #-} (Generic a, GenericHasVariables (Rep a)) => HasVariables a