diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,17 @@
 Changelog for the `singletons` project
 ======================================
 
+3.0.1 [2021.10.30]
+------------------
+* Add `SingI1` and `SingI2`, higher-order versions of `SingI`, to
+  `Data.Singletons`, along with various derived functions:
+
+  * `sing{1,2}`
+  * `singByProxy{1,2}` and `singByProxy{1,2}#`
+  * `usingSing{1,2}`
+  * `withSing{1,2}`
+  * `singThat{1,2}`
+
 3.0 [2021.03.12]
 ----------------
 * The `singletons` library has been split into three libraries:
diff --git a/singletons.cabal b/singletons.cabal
--- a/singletons.cabal
+++ b/singletons.cabal
@@ -1,5 +1,5 @@
 name:           singletons
-version:        3.0
+version:        3.0.1
 cabal-version:  1.24
 synopsis:       Basic singleton types and definitions
 homepage:       http://www.github.com/goldfirere/singletons
@@ -13,8 +13,9 @@
               , GHC == 8.4.4
               , GHC == 8.6.5
               , GHC == 8.8.4
-              , GHC == 8.10.4
+              , GHC == 8.10.7
               , GHC == 9.0.1
+              , GHC == 9.2.1
               , GHCJS==8.4
 extra-source-files: README.md, CHANGES.md
 license:        BSD3
@@ -46,7 +47,7 @@
   type:     git
   location: https://github.com/goldfirere/singletons.git
   subdir:   singletons
-  tag:      v3.0
+  tag:      v3.0.1
 
 source-repository head
   type:     git
@@ -56,7 +57,7 @@
 
 library
   hs-source-dirs:     src
-  build-depends:      base >= 4.9 && < 4.16
+  build-depends:      base >= 4.9 && < 4.17
   default-language:   Haskell2010
   exposed-modules:    Data.Singletons
                       Data.Singletons.Decide
@@ -73,5 +74,5 @@
   other-modules:      ByHand
                       ByHand2
 
-  build-depends:      base >= 4.9 && < 4.16,
+  build-depends:      base >= 4.9 && < 4.17,
                       singletons
diff --git a/src/Data/Singletons.hs b/src/Data/Singletons.hs
--- a/src/Data/Singletons.hs
+++ b/src/Data/Singletons.hs
@@ -53,17 +53,23 @@
 
   Sing, SLambda(..), (@@),
 
-  SingI(..), SingKind(..),
+  SingI(..),
+  SingI1(..), sing1,
+  SingI2(..), sing2,
+  SingKind(..),
 
   -- * Working with singletons
   KindOf, SameKind,
   SingInstance(..), SomeSing(..),
   singInstance, pattern Sing, withSingI,
   withSomeSing, pattern FromSing,
-  singByProxy, demote,
+  usingSingI1, usingSingI2,
+  singByProxy, singByProxy1, singByProxy2,
+  demote, demote1, demote2,
 
-  singByProxy#,
-  withSing, singThat,
+  singByProxy#, singByProxy1#, singByProxy2#,
+  withSing, withSing1, withSing2,
+  singThat, singThat1, singThat2,
 
   -- ** @WrappedSing@
   WrappedSing(..), SWrappedSing(..), UnwrapSing,
@@ -210,6 +216,46 @@
   -- extension to use this method the way you want.
   sing :: Sing a
 
+-- | A version of the 'SingI' class lifted to unary type constructors.
+#if __GLASGOW_HASKELL__ >= 900
+type SingI1 :: forall {k1} {k2}. (k1 -> k2) -> Constraint
+#endif
+class
+#if __GLASGOW_HASKELL__ >= 806
+  (forall x. SingI x => SingI (f x)) =>
+#endif
+    SingI1 f where
+  -- | Lift an explicit singleton through a unary type constructor.
+  -- You will likely need the @ScopedTypeVariables@ extension to use this
+  -- method the way you want.
+  liftSing :: Sing x -> Sing (f x)
+
+-- | Produce a singleton explicitly using implicit 'SingI1' and 'SingI'
+-- constraints. You will likely need the @ScopedTypeVariables@ extension to use
+-- this method the way you want.
+sing1 :: (SingI1 f, SingI x) => Sing (f x)
+sing1 = liftSing sing
+
+-- | A version of the 'SingI' class lifted to binary type constructors.
+#if __GLASGOW_HASKELL__ >= 900
+type SingI2 :: forall {k1} {k2} {k3}. (k1 -> k2 -> k3) -> Constraint
+#endif
+class
+#if __GLASGOW_HASKELL__ >= 806
+  (forall x y. (SingI x, SingI y) => SingI (f x y)) =>
+#endif
+    SingI2 f where
+  -- | Lift explicit singletons through a binary type constructor.
+  -- You will likely need the @ScopedTypeVariables@ extension to use this
+  -- method the way you want.
+  liftSing2 :: Sing x -> Sing y -> Sing (f x y)
+
+-- | Produce a singleton explicitly using implicit 'SingI2' and 'SingI'
+-- constraints. You will likely need the @ScopedTypeVariables@ extension to use
+-- this method the way you want.
+sing2 :: (SingI2 f, SingI x, SingI y) => Sing (f x y)
+sing2 = liftSing2 sing sing
+
 -- | An explicitly bidirectional pattern synonym for implicit singletons.
 --
 -- As an __expression__: Constructs a singleton @Sing a@ given a
@@ -783,6 +829,20 @@
   case toSing x of
     SomeSing x' -> f x'
 
+-- | Convert a group of 'SingI1' and 'SingI' constraints (representing a
+-- function to apply and its argument, respectively) into a single 'SingI'
+-- constraint representing the application. You will likely need the
+-- @ScopedTypeVariables@ extension to use this method the way you want.
+usingSingI1 :: forall f x r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r
+usingSingI1 k = withSingI (sing1 @f @x) k
+
+-- | Convert a group of 'SingI2' and 'SingI' constraints (representing a
+-- function to apply and its arguments, respectively) into a single 'SingI'
+-- constraint representing the application. You will likely need the
+-- @ScopedTypeVariables@ extension to use this method the way you want.
+usingSingI2 :: forall f x y r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => r) -> r
+usingSingI2 k = withSingI (sing2 @f @x @y) k
+
 -- | A convenience function useful when we need to name a singleton value
 -- multiple times. Without this function, each use of 'sing' could potentially
 -- refer to a different singleton, and one has to use type signatures (often
@@ -790,6 +850,22 @@
 withSing :: SingI a => (Sing a -> b) -> b
 withSing f = f sing
 
+-- | A convenience function useful when we need to name a singleton value for a
+-- unary type constructor multiple times. Without this function, each use of
+-- 'sing1' could potentially refer to a different singleton, and one has to use
+-- type signatures (often with @ScopedTypeVariables@) to ensure that they are
+-- the same.
+withSing1 :: (SingI1 f, SingI x) => (Sing (f x) -> b) -> b
+withSing1 f = f sing1
+
+-- | A convenience function useful when we need to name a singleton value for a
+-- binary type constructor multiple times. Without this function, each use of
+-- 'sing1' could potentially refer to a different singleton, and one has to use
+-- type signatures (often with @ScopedTypeVariables@) to ensure that they are
+-- the same.
+withSing2 :: (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> b) -> b
+withSing2 f = f sing2
+
 -- | A convenience function that names a singleton satisfying a certain
 -- property.  If the singleton does not satisfy the property, then the function
 -- returns 'Nothing'. The property is expressed in terms of the underlying
@@ -798,14 +874,52 @@
          => (Demote k -> Bool) -> Maybe (Sing a)
 singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing
 
+-- | A convenience function that names a singleton for a unary type constructor
+-- satisfying a certain property.  If the singleton does not satisfy the
+-- property, then the function returns 'Nothing'. The property is expressed in
+-- terms of the underlying representation of the singleton.
+singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1).
+             (SingKind k2, SingI1 f, SingI x)
+          => (Demote k2 -> Bool) -> Maybe (Sing (f x))
+singThat1 p = withSing1 $ \x -> if p (fromSing x) then Just x else Nothing
+
+-- | A convenience function that names a singleton for a binary type constructor
+-- satisfying a certain property.  If the singleton does not satisfy the
+-- property, then the function returns 'Nothing'. The property is expressed in
+-- terms of the underlying representation of the singleton.
+singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).
+             (SingKind k3, SingI2 f, SingI x, SingI y)
+          => (Demote k3 -> Bool) -> Maybe (Sing (f x y))
+singThat2 p = withSing2 $ \x -> if p (fromSing x) then Just x else Nothing
+
 -- | Allows creation of a singleton when a proxy is at hand.
 singByProxy :: SingI a => proxy a -> Sing a
 singByProxy _ = sing
 
+-- | Allows creation of a singleton for a unary type constructor when a proxy
+-- is at hand.
+singByProxy1 :: (SingI1 f, SingI x) => proxy (f x) -> Sing (f x)
+singByProxy1 _ = sing1
+
+-- | Allows creation of a singleton for a binary type constructor when a proxy
+-- is at hand.
+singByProxy2 :: (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y)
+singByProxy2 _ = sing2
+
 -- | Allows creation of a singleton when a @proxy#@ is at hand.
 singByProxy# :: SingI a => Proxy# a -> Sing a
 singByProxy# _ = sing
 
+-- | Allows creation of a singleton for a unary type constructor when a
+-- @proxy#@ is at hand.
+singByProxy1# :: (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)
+singByProxy1# _ = sing1
+
+-- | Allows creation of a singleton for a binary type constructor when a
+-- @proxy#@ is at hand.
+singByProxy2# :: (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y)
+singByProxy2# _ = sing2
+
 -- | A convenience function that takes a type as input and demotes it to its
 -- value-level counterpart as output. This uses 'SingKind' and 'SingI' behind
 -- the scenes, so @'demote' = 'fromSing' 'sing'@.
@@ -817,6 +931,12 @@
 --
 -- >>> demote @(Nothing :: Maybe Ordering)
 -- Nothing
+--
+-- >>> demote @(Just EQ)
+-- Just EQ
+--
+-- >>> demote @'(True,EQ)
+-- (True,EQ)
 demote ::
 #if __GLASGOW_HASKELL__ >= 900
   forall {k} (a :: k). (SingKind k, SingI a) => Demote k
@@ -824,6 +944,51 @@
   forall a. (SingKind (KindOf a), SingI a) => Demote (KindOf a)
 #endif
 demote = fromSing (sing @a)
+
+-- | A convenience function that takes a unary type constructor and its
+-- argument as input, applies them, and demotes the result to its
+-- value-level counterpart as output. This uses 'SingKind', 'SingI1', and
+-- 'SingI' behind the scenes, so @'demote1' = 'fromSing' 'sing1'@.
+--
+-- This function is intended to be used with @TypeApplications@. For example:
+--
+-- >>> demote1 @Just @EQ
+-- Just EQ
+--
+-- >>> demote1 @('(,) True) @EQ
+-- (True,EQ)
+demote1 ::
+#if __GLASGOW_HASKELL__ >= 900
+  forall {k1} {k2} (f :: k1 -> k2) (x :: k1).
+  (SingKind k2, SingI1 f, SingI x) =>
+  Demote k2
+#else
+  forall f x.
+  (SingKind (KindOf (f x)), SingI1 f, SingI x) =>
+  Demote (KindOf (f x))
+#endif
+demote1 = fromSing (sing1 @f @x)
+
+-- | A convenience function that takes a binary type constructor and its
+-- arguments as input, applies them, and demotes the result to its
+-- value-level counterpart as output. This uses 'SingKind', 'SingI2', and
+-- 'SingI' behind the scenes, so @'demote2' = 'fromSing' 'sing2'@.
+--
+-- This function is intended to be used with @TypeApplications@. For example:
+--
+-- >>> demote2 @'(,) @True @EQ
+-- (True,EQ)
+demote2 ::
+#if __GLASGOW_HASKELL__ >= 900
+  forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).
+  (SingKind k3, SingI2 f, SingI x, SingI y) =>
+  Demote k3
+#else
+  forall f x y.
+  (SingKind (KindOf (f x y)), SingI2 f, SingI x, SingI y) =>
+  Demote (KindOf (f x y))
+#endif
+demote2 = fromSing (sing2 @f @x @y)
 
 ----------------------------------------------------------------------
 ---- SingI TyCon{N} instances ----------------------------------------
diff --git a/tests/ByHand.hs b/tests/ByHand.hs
--- a/tests/ByHand.hs
+++ b/tests/ByHand.hs
@@ -135,6 +135,8 @@
   sing = SZero
 instance SingI n => SingI (Succ n) where
   sing = SSucc sing
+instance SingI1 Succ where
+  liftSing = SSucc
 instance SingKind Nat where
   type Demote Nat = Nat
   fromSing SZero = Zero
@@ -221,6 +223,8 @@
   sing = SNothing
 instance SingI a => SingI (Just (a :: k)) where
   sing = SJust sing
+instance SingI1 Just where
+  liftSing = SJust
 instance SingKind k => SingKind (Maybe k) where
   type Demote (Maybe k) = Maybe (Demote k)
   fromSing SNothing = Nothing
@@ -289,6 +293,10 @@
 instance (SingI h, SingI t) =>
            SingI (Cons (h :: k) (t :: List k)) where
   sing = SCons sing sing
+instance SingI h => SingI1 (Cons (h :: k)) where
+  liftSing = SCons sing
+instance SingI2 Cons where
+  liftSing2 = SCons
 instance SingKind k => SingKind (List k) where
   type Demote (List k) = List (Demote k)
   fromSing SNil = Nil
@@ -311,8 +319,12 @@
 
 instance (SingI a) => SingI (Left (a :: k)) where
   sing = SLeft sing
+instance SingI1 Left where
+  liftSing = SLeft
 instance (SingI b) => SingI (Right (b :: k)) where
   sing = SRight sing
+instance SingI1 Right where
+  liftSing = SRight
 instance (SingKind k1, SingKind k2) => SingKind (Either k1 k2) where
   type Demote (Either k1 k2) = Either (Demote k1) (Demote k2)
   fromSing (SLeft x) = Left (fromSing x)
@@ -353,6 +365,8 @@
 
 instance SingI a => SingI (MkComp (a :: Either (Maybe k1) k2)) where
   sing = SMkComp sing
+instance SingI1 MkComp where
+  liftSing = SMkComp
 instance (SingKind k1, SingKind k2) => SingKind (Composite k1 k2) where
   type Demote (Composite k1 k2) =
     Composite (Demote k1) (Demote k2)
@@ -412,8 +426,14 @@
   sing = SNat
 instance SingI a => SingI (Maybe a) where
   sing = SMaybe sing
+instance SingI1 Maybe where
+  liftSing = SMaybe
 instance (SingI a, SingI n) => SingI (Vec a n) where
   sing = SVec sing sing
+instance SingI a => SingI1 (Vec a) where
+  liftSing = SVec sing
+instance SingI2 Vec where
+  liftSing2 = SVec
 
 instance SingKind Type where
   type Demote Type = Rep