diff --git a/README.md b/README.md
index 4a2f6820..9c6d154c 100644
--- a/README.md
+++ b/README.md
@@ -1178,32 +1178,67 @@ for the following constructs:
   yourself!
 
 * Kind signatures of promoted class methods.
-  The order of type variables will often "just work" by happy coincidence, but
-  there are some situations where this does not happen. Consider the following
-  class:
+  The order of type variables is only guaranteed to be preserved if the parent
+  class has a standalone kind signature. For example, given this class:
 
   ```haskell
-  class C (b :: Type) where
+  type C :: Type -> Constraint
+  class C b where
     m :: forall a. a -> b -> a
   ```
 
   The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds
-  `b` before `a`. This order is preserved when singling `m`, but *not* when
-  promoting `m`. This is because the `C` class is promoted as follows:
+  `b` before `a`. Because `C` has a standalone kind signature, the order of
+  type variables is preserved when promoting and singling `m`:
+
+  ```hs
+  type PC :: Type -> Constraint
+  class PC b where
+    type M @b @a (x :: a) (y :: b) :: a
+
+  type MSym0 :: forall b a. a ~> b ~> a
+  type MSym1 :: forall b a. a -> b ~> a
+
+  type SC :: Type -> Constraint
+  class SC b where
+    sM :: forall a (x :: a) (y :: b).
+          Sing x -> Sing y -> Sing (M x y)
+  ```
+
+  Note that `M`, `M`'s defunctionalization symbols, and `sM` all quantify `b`
+  before `a` in their types. The key to making this work is by using the
+  `TypeAbstractions` language extension in declaration for `M`, which is only
+  possible due to `PC` having a standalone kind signature.
+
+  If the parent class does _not_ have a standalone kind signature, then
+  `singletons-th` does not make any guarantees about the order of kind
+  variables in the promoted methods' kinds. The order will often "just work" by
+  happy coincidence, but there are some situations where this does not happen.
+  Consider the following variant of the class example above:
 
   ```haskell
-  class PC (b :: Type) where
-    type M (x :: a) (y :: b) :: a
+  -- No standalone kind signature
+  class C b where
+    m :: forall a. a -> b -> a
   ```
 
-  Due to the way GHC kind-checks associated type families, the kind of `M` is
-  `forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the
-  `StandaloneKindSignatures` extension does not provide a way to explicitly
-  declare the full kind of an associated type family, so this limitation is
-  not easy to work around.
+  Again, the full type of `m` is `forall b. C b => forall a. a -> b -> a`,
+  which binds `b` before `a`. This order is preserved when singling `m`, but
+  *not* when promoting `m`. This is because the `C` class is promoted as
+  follows:
+
+  ```haskell
+  -- No standalone kind signature
+  class PC b where
+    type M (x :: a) (y :: b) :: a
+  ```
 
-  The defunctionalization symbols for `M` will also follow a similar
-  order of type variables:
+  This time, `PC` does not have a standalone kind signature, so we cannot use
+  `TypeAbstractions` in the declaration for `M`. As such, GHC will quantify the
+  kind variables in left-to-right order, so the kind of `M` will be inferred to
+  be `forall a b. a -> b -> a`, which binds `b` *after* `a`. The
+  defunctionalization symbols for `M` will also follow a similar order of type
+  variables:
 
   ```haskell
   type MSym0 :: forall a b. a ~> b ~> a
diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs
index de0e95f2..e2d6082c 100644
--- a/singletons-base/tests/SingletonsBaseTestSuite.hs
+++ b/singletons-base/tests/SingletonsBaseTestSuite.hs
@@ -155,6 +155,7 @@ tests =
     , compileAndDumpStdTest "T581"
     , compileAndDumpStdTest "T585"
     , compileAndDumpStdTest "TypeAbstractions"
+    , compileAndDumpStdTest "T589"
     ],
     testCompileAndDumpGroup "Promote"
     [ compileAndDumpStdTest "Constructors"
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T326.golden b/singletons-base/tests/compile-and-dump/Singletons/T326.golden
index 4a9a89e3..fb6f759a 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T326.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T326.golden
@@ -1,7 +1,7 @@
 Singletons/T326.hs:0:0:: Splicing declarations
     genPromotions [''C1]
   ======>
-    type (<%>@#@$) :: forall a. (~>) a ((~>) a a)
+    type (<%>@#@$) :: forall (a :: Type). (~>) a ((~>) a a)
     data (<%>@#@$) :: (~>) a ((~>) a a)
       where
         (:<%>@#@$###) :: SameKind (Apply (<%>@#@$) arg) ((<%>@#@$$) arg) =>
@@ -10,7 +10,7 @@ Singletons/T326.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings (<%>@#@$) where
       suppressUnusedWarnings = snd ((,) (:<%>@#@$###) ())
     infixl 9 <%>@#@$
-    type (<%>@#@$$) :: forall a. a -> (~>) a a
+    type (<%>@#@$$) :: forall (a :: Type). a -> (~>) a a
     data (<%>@#@$$) (a0123456789876543210 :: a) :: (~>) a a
       where
         (:<%>@#@$$###) :: SameKind (Apply ((<%>@#@$$) a0123456789876543210) arg) ((<%>@#@$$$) a0123456789876543210 arg) =>
@@ -19,18 +19,18 @@ Singletons/T326.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings ((<%>@#@$$) a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) (:<%>@#@$$###) ())
     infixl 9 <%>@#@$$
-    type (<%>@#@$$$) :: forall a. a -> a -> a
-    type family (<%>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
+    type (<%>@#@$$$) :: forall (a :: Type). a -> a -> a
+    type family (<%>@#@$$$) @(a :: Type) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
       (<%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%>) a0123456789876543210 a0123456789876543210
     infixl 9 <%>@#@$$$
     type PC1 :: Type -> Constraint
     class PC1 (a :: Type) where
-      type family (<%>) (arg :: a) (arg :: a) :: a
+      type family (<%>) @(a :: Type) (arg :: a) (arg :: a) :: a
     infixl 9 <%>
 Singletons/T326.hs:0:0:: Splicing declarations
     genSingletons [''C2]
   ======>
-    type (<%%>@#@$) :: forall a. (~>) a ((~>) a a)
+    type (<%%>@#@$) :: forall (a :: Type). (~>) a ((~>) a a)
     data (<%%>@#@$) :: (~>) a ((~>) a a)
       where
         (:<%%>@#@$###) :: SameKind (Apply (<%%>@#@$) arg) ((<%%>@#@$$) arg) =>
@@ -39,7 +39,7 @@ Singletons/T326.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings (<%%>@#@$) where
       suppressUnusedWarnings = snd ((,) (:<%%>@#@$###) ())
     infixl 9 <%%>@#@$
-    type (<%%>@#@$$) :: forall a. a -> (~>) a a
+    type (<%%>@#@$$) :: forall (a :: Type). a -> (~>) a a
     data (<%%>@#@$$) (a0123456789876543210 :: a) :: (~>) a a
       where
         (:<%%>@#@$$###) :: SameKind (Apply ((<%%>@#@$$) a0123456789876543210) arg) ((<%%>@#@$$$) a0123456789876543210 arg) =>
@@ -48,13 +48,13 @@ Singletons/T326.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings ((<%%>@#@$$) a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) (:<%%>@#@$$###) ())
     infixl 9 <%%>@#@$$
-    type (<%%>@#@$$$) :: forall a. a -> a -> a
-    type family (<%%>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
+    type (<%%>@#@$$$) :: forall (a :: Type). a -> a -> a
+    type family (<%%>@#@$$$) @(a :: Type) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where
       (<%%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%%>) a0123456789876543210 a0123456789876543210
     infixl 9 <%%>@#@$$$
     type PC2 :: Type -> Constraint
     class PC2 (a :: Type) where
-      type family (<%%>) (arg :: a) (arg :: a) :: a
+      type family (<%%>) @(a :: Type) (arg :: a) (arg :: a) :: a
     infixl 9 <%%>
     class SC2 (a :: Type) where
       (%<%%>) ::
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden
index 81b3db76..cc31d5ae 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden
@@ -74,7 +74,7 @@ Singletons/T378b.hs:(0,0)-(0,0): Splicing declarations
     type family F @b @a (a :: a) (a :: b) :: () where
       F @b @a (_ :: a) (_ :: b) = Tuple0Sym0
     type PC :: forall b a. a -> b -> Constraint
-    class PC x y
+    class PC @b @a (x :: a) (y :: b)
     sNatMinus ::
       (forall (t :: Nat) (t :: Nat).
        Sing t
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T412.golden b/singletons-base/tests/compile-and-dump/Singletons/T412.golden
index b757f4e1..dc1e31a3 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden
@@ -201,7 +201,7 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations
 Singletons/T412.hs:0:0:: Splicing declarations
     genSingletons [''C2, ''T2a, ''T2b, ''D2]
   ======>
-    type M2Sym0 :: forall a b. (~>) a ((~>) b Bool)
+    type M2Sym0 :: forall (a :: Type) (b :: Type). (~>) a ((~>) b Bool)
     data M2Sym0 :: (~>) a ((~>) b Bool)
       where
         M2Sym0KindInference :: SameKind (Apply M2Sym0 arg) (M2Sym1 arg) =>
@@ -210,7 +210,7 @@ Singletons/T412.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings M2Sym0 where
       suppressUnusedWarnings = snd ((,) M2Sym0KindInference ())
     infix 6 `M2Sym0`
-    type M2Sym1 :: forall a b. a -> (~>) b Bool
+    type M2Sym1 :: forall (a :: Type) (b :: Type). a -> (~>) b Bool
     data M2Sym1 (a0123456789876543210 :: a) :: (~>) b Bool
       where
         M2Sym1KindInference :: SameKind (Apply (M2Sym1 a0123456789876543210) arg) (M2Sym2 a0123456789876543210 arg) =>
@@ -219,13 +219,13 @@ Singletons/T412.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings (M2Sym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) M2Sym1KindInference ())
     infix 6 `M2Sym1`
-    type M2Sym2 :: forall a b. a -> b -> Bool
-    type family M2Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where
+    type M2Sym2 :: forall (a :: Type) (b :: Type). a -> b -> Bool
+    type family M2Sym2 @(a :: Type) @(b :: Type) (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where
       M2Sym2 a0123456789876543210 a0123456789876543210 = M2 a0123456789876543210 a0123456789876543210
     infix 6 `M2Sym2`
     type PC2 :: Type -> Type -> Constraint
     class PC2 (a :: Type) (b :: Type) where
-      type family M2 (arg :: a) (arg :: b) :: Bool
+      type family M2 @(a :: Type) @(b :: Type) (arg :: a) (arg :: b) :: Bool
     infix 5 `PC2`
     infix 6 `M2`
     class SC2 (a :: Type) (b :: Type) where
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T414.golden b/singletons-base/tests/compile-and-dump/Singletons/T414.golden
index a317c607..0d97f536 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T414.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T414.golden
@@ -70,7 +70,7 @@ Singletons/T414.hs:(0,0)-(0,0): Splicing declarations
     type family T3Sym2 (a0123456789876543210 :: Bool) (a0123456789876543210 :: Type) :: Type where
       T3Sym2 a0123456789876543210 a0123456789876543210 = T3 a0123456789876543210 a0123456789876543210
     type PC3 :: Bool -> Constraint
-    class PC3 a
+    class PC3 (a :: Bool)
     class SC1 (a :: Bool)
     class SC2 a
     class SC3 a
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T589.golden b/singletons-base/tests/compile-and-dump/Singletons/T589.golden
new file mode 100644
index 00000000..1cea4900
--- /dev/null
+++ b/singletons-base/tests/compile-and-dump/Singletons/T589.golden
@@ -0,0 +1,127 @@
+Singletons/T589.hs:(0,0)-(0,0): Splicing declarations
+    singletons
+      [d| type C1 :: Type -> Constraint
+          type C2 :: k -> Constraint
+          
+          class C1 b where
+            m1 :: forall a. a -> b -> a
+          class C2 b where
+            m2 :: a -> Proxy b
+          
+          instance C1 Ordering where
+            m1 x _ = x
+          instance C2 Ordering where
+            m2 _ = Proxy |]
+  ======>
+    type C1 :: Type -> Constraint
+    class C1 b where
+      m1 :: forall a. a -> b -> a
+    instance C1 Ordering where
+      m1 x _ = x
+    type C2 :: k -> Constraint
+    class C2 b where
+      m2 :: a -> Proxy b
+    instance C2 Ordering where
+      m2 _ = Proxy
+    type M1Sym0 :: forall (b :: Type) a. (~>) a ((~>) b a)
+    data M1Sym0 :: (~>) a ((~>) b a)
+      where
+        M1Sym0KindInference :: SameKind (Apply M1Sym0 arg) (M1Sym1 arg) =>
+                               M1Sym0 a0123456789876543210
+    type instance Apply M1Sym0 a0123456789876543210 = M1Sym1 a0123456789876543210
+    instance SuppressUnusedWarnings M1Sym0 where
+      suppressUnusedWarnings = snd ((,) M1Sym0KindInference ())
+    type M1Sym1 :: forall (b :: Type) a. a -> (~>) b a
+    data M1Sym1 (a0123456789876543210 :: a) :: (~>) b a
+      where
+        M1Sym1KindInference :: SameKind (Apply (M1Sym1 a0123456789876543210) arg) (M1Sym2 a0123456789876543210 arg) =>
+                               M1Sym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (M1Sym1 a0123456789876543210) a0123456789876543210 = M1 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (M1Sym1 a0123456789876543210) where
+      suppressUnusedWarnings = snd ((,) M1Sym1KindInference ())
+    type M1Sym2 :: forall (b :: Type) a. a -> b -> a
+    type family M1Sym2 @(b :: Type) @a (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where
+      M1Sym2 a0123456789876543210 a0123456789876543210 = M1 a0123456789876543210 a0123456789876543210
+    type PC1 :: Type -> Constraint
+    class PC1 (b :: Type) where
+      type family M1 @(b :: Type) @a (arg :: a) (arg :: b) :: a
+    type M2Sym0 :: forall k (b :: k) a. (~>) a (Proxy b)
+    data M2Sym0 :: (~>) a (Proxy b)
+      where
+        M2Sym0KindInference :: SameKind (Apply M2Sym0 arg) (M2Sym1 arg) =>
+                               M2Sym0 a0123456789876543210
+    type instance Apply M2Sym0 a0123456789876543210 = M2 a0123456789876543210
+    instance SuppressUnusedWarnings M2Sym0 where
+      suppressUnusedWarnings = snd ((,) M2Sym0KindInference ())
+    type M2Sym1 :: forall k (b :: k) a. a -> Proxy b
+    type family M2Sym1 @k @(b :: k) @a (a0123456789876543210 :: a) :: Proxy b where
+      M2Sym1 a0123456789876543210 = M2 a0123456789876543210
+    type PC2 :: k -> Constraint
+    class PC2 @k (b :: k) where
+      type family M2 @k @(b :: k) @a (arg :: a) :: Proxy b
+    type M1_0123456789876543210 :: forall a. a -> Ordering -> a
+    type family M1_0123456789876543210 @a (a :: a) (a :: Ordering) :: a where
+      M1_0123456789876543210 @a x _ = x
+    type M1_0123456789876543210Sym0 :: forall a. (~>) a ((~>) Ordering a)
+    data M1_0123456789876543210Sym0 :: (~>) a ((~>) Ordering a)
+      where
+        M1_0123456789876543210Sym0KindInference :: SameKind (Apply M1_0123456789876543210Sym0 arg) (M1_0123456789876543210Sym1 arg) =>
+                                                   M1_0123456789876543210Sym0 a0123456789876543210
+    type instance Apply M1_0123456789876543210Sym0 a0123456789876543210 = M1_0123456789876543210Sym1 a0123456789876543210
+    instance SuppressUnusedWarnings M1_0123456789876543210Sym0 where
+      suppressUnusedWarnings
+        = snd ((,) M1_0123456789876543210Sym0KindInference ())
+    type M1_0123456789876543210Sym1 :: forall a. a -> (~>) Ordering a
+    data M1_0123456789876543210Sym1 (a0123456789876543210 :: a) :: (~>) Ordering a
+      where
+        M1_0123456789876543210Sym1KindInference :: SameKind (Apply (M1_0123456789876543210Sym1 a0123456789876543210) arg) (M1_0123456789876543210Sym2 a0123456789876543210 arg) =>
+                                                   M1_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (M1_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = M1_0123456789876543210 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (M1_0123456789876543210Sym1 a0123456789876543210) where
+      suppressUnusedWarnings
+        = snd ((,) M1_0123456789876543210Sym1KindInference ())
+    type M1_0123456789876543210Sym2 :: forall a. a -> Ordering -> a
+    type family M1_0123456789876543210Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Ordering) :: a where
+      M1_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = M1_0123456789876543210 a0123456789876543210 a0123456789876543210
+    instance PC1 Ordering where
+      type M1 a a = Apply (Apply M1_0123456789876543210Sym0 a) a
+    type M2_0123456789876543210 :: forall a. a -> Proxy Ordering
+    type family M2_0123456789876543210 @a (a :: a) :: Proxy Ordering where
+      M2_0123456789876543210 @a _ = ProxySym0
+    type M2_0123456789876543210Sym0 :: forall a. (~>) a (Proxy Ordering)
+    data M2_0123456789876543210Sym0 :: (~>) a (Proxy Ordering)
+      where
+        M2_0123456789876543210Sym0KindInference :: SameKind (Apply M2_0123456789876543210Sym0 arg) (M2_0123456789876543210Sym1 arg) =>
+                                                   M2_0123456789876543210Sym0 a0123456789876543210
+    type instance Apply M2_0123456789876543210Sym0 a0123456789876543210 = M2_0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings M2_0123456789876543210Sym0 where
+      suppressUnusedWarnings
+        = snd ((,) M2_0123456789876543210Sym0KindInference ())
+    type M2_0123456789876543210Sym1 :: forall a. a -> Proxy Ordering
+    type family M2_0123456789876543210Sym1 @a (a0123456789876543210 :: a) :: Proxy Ordering where
+      M2_0123456789876543210Sym1 a0123456789876543210 = M2_0123456789876543210 a0123456789876543210
+    instance PC2 Ordering where
+      type M2 a = Apply M2_0123456789876543210Sym0 a
+    class SC1 b where
+      sM1 ::
+        forall a (t :: a) (t :: b). Sing t
+                                    -> Sing t -> Sing (Apply (Apply M1Sym0 t) t :: a)
+    class SC2 b where
+      sM2 ::
+        (forall (t :: a).
+         Sing t -> Sing (Apply M2Sym0 t :: Proxy b) :: Type)
+    instance SC1 Ordering where
+      sM1 (sX :: Sing x) _ = sX
+    instance SC2 Ordering where
+      sM2 _ = SProxy
+    type SC1 :: Type -> Constraint
+    instance SC1 b => SingI (M1Sym0 :: (~>) a ((~>) b a)) where
+      sing = singFun2 @M1Sym0 sM1
+    instance (SC1 b, SingI d) =>
+             SingI (M1Sym1 (d :: a) :: (~>) b a) where
+      sing = singFun1 @(M1Sym1 (d :: a)) (sM1 (sing @d))
+    instance SC1 b => SingI1 (M1Sym1 :: a -> (~>) b a) where
+      liftSing (s :: Sing (d :: a)) = singFun1 @(M1Sym1 (d :: a)) (sM1 s)
+    type SC2 :: k -> Constraint
+    instance SC2 b => SingI (M2Sym0 :: (~>) a (Proxy b)) where
+      sing = singFun1 @M2Sym0 sM2
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T589.hs b/singletons-base/tests/compile-and-dump/Singletons/T589.hs
new file mode 100644
index 00000000..6a9278b8
--- /dev/null
+++ b/singletons-base/tests/compile-and-dump/Singletons/T589.hs
@@ -0,0 +1,59 @@
+module T589 where
+
+import Data.Kind
+import Data.Proxy
+import Data.Proxy.Singletons
+import Data.Singletons.Base.TH
+import Prelude.Singletons
+
+$(singletons [d|
+  type C1 :: Type -> Constraint
+  class C1 b where
+    m1 :: forall a. a -> b -> a
+
+  instance C1 Ordering where
+    m1 x _ = x
+
+  type C2 :: k -> Constraint
+  class C2 b where
+    m2 :: a -> Proxy b
+
+  instance C2 Ordering where
+    m2 _ = Proxy
+  |])
+
+-- Test some type variable orderings
+m1Ex :: Bool -> Ordering -> Bool
+m1Ex = m1 @Ordering @Bool
+
+type M1Ex :: Bool
+type M1Ex = M1 @Ordering @Bool True EQ
+
+type M1Ex0 :: Bool ~> Ordering ~> Bool
+type M1Ex0 = M1Sym0 @Ordering @Bool
+
+type M1Ex1 :: Bool -> Ordering ~> Bool
+type M1Ex1 = M1Sym1 @Ordering @Bool
+
+type M1Ex2 :: Bool
+type M1Ex2 = M1Sym2 @Ordering @Bool True EQ
+
+sM1Ex :: forall (x :: Bool) (y :: Ordering).
+         Sing x -> Sing y -> Sing (M1 @Ordering @Bool x y)
+sM1Ex = sM1 @Ordering @Bool
+
+m2Ex :: Bool -> Proxy Ordering
+m2Ex = m2 @Type @Ordering @Bool
+
+type M2Ex :: Proxy Ordering
+type M2Ex = M2 @Type @Ordering @Bool True
+
+type M2Ex0 :: Bool ~> Proxy Ordering
+type M2Ex0 = M2Sym0 @Type @Ordering @Bool
+
+type M2Ex1 :: Proxy Ordering
+type M2Ex1 = M2Sym1 @Type @Ordering @Bool True
+
+sM2Ex :: forall (x :: Bool).
+         Sing x -> Sing (M2 @Type @Ordering @Bool x)
+sM2Ex = sM2 @Type @Ordering @Bool
diff --git a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden
index 6e390106..a52c42dd 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden
@@ -168,7 +168,10 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations
     type MkD4Sym1 :: forall a. a -> D4 @a
     type family MkD4Sym1 @a (a0123456789876543210 :: a) :: D4 @a where
       MkD4Sym1 a0123456789876543210 = MkD4 a0123456789876543210
-    type Meth1Sym0 :: forall a b. (~>) (Proxy a) (Proxy b)
+    type Meth1Sym0 :: forall j
+                             k
+                             (a :: j)
+                             (b :: k). (~>) (Proxy a) (Proxy b)
     data Meth1Sym0 :: (~>) (Proxy a) (Proxy b)
       where
         Meth1Sym0KindInference :: SameKind (Apply Meth1Sym0 arg) (Meth1Sym1 arg) =>
@@ -176,13 +179,16 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations
     type instance Apply Meth1Sym0 a0123456789876543210 = Meth1 a0123456789876543210
     instance SuppressUnusedWarnings Meth1Sym0 where
       suppressUnusedWarnings = snd ((,) Meth1Sym0KindInference ())
-    type Meth1Sym1 :: forall a b. Proxy a -> Proxy b
-    type family Meth1Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where
+    type Meth1Sym1 :: forall j k (a :: j) (b :: k). Proxy a -> Proxy b
+    type family Meth1Sym1 @j @k @(a :: j) @(b :: k) (a0123456789876543210 :: Proxy a) :: Proxy b where
       Meth1Sym1 a0123456789876543210 = Meth1 a0123456789876543210
     type PC1 :: forall j k. j -> k -> Constraint
     class PC1 @j @k (a :: j) (b :: k) where
-      type family Meth1 (arg :: Proxy a) :: Proxy b
-    type Meth2Sym0 :: forall a b. (~>) (Proxy a) (Proxy b)
+      type family Meth1 @j @k @(a :: j) @(b :: k) (arg :: Proxy a) :: Proxy b
+    type Meth2Sym0 :: forall x
+                             y
+                             (a :: x)
+                             (b :: y). (~>) (Proxy a) (Proxy b)
     data Meth2Sym0 :: (~>) (Proxy a) (Proxy b)
       where
         Meth2Sym0KindInference :: SameKind (Apply Meth2Sym0 arg) (Meth2Sym1 arg) =>
@@ -190,13 +196,16 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations
     type instance Apply Meth2Sym0 a0123456789876543210 = Meth2 a0123456789876543210
     instance SuppressUnusedWarnings Meth2Sym0 where
       suppressUnusedWarnings = snd ((,) Meth2Sym0KindInference ())
-    type Meth2Sym1 :: forall a b. Proxy a -> Proxy b
-    type family Meth2Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where
+    type Meth2Sym1 :: forall x y (a :: x) (b :: y). Proxy a -> Proxy b
+    type family Meth2Sym1 @x @y @(a :: x) @(b :: y) (a0123456789876543210 :: Proxy a) :: Proxy b where
       Meth2Sym1 a0123456789876543210 = Meth2 a0123456789876543210
     type PC2 :: forall j k. j -> k -> Constraint
     class PC2 @x @y (a :: x) (b :: y) where
-      type family Meth2 (arg :: Proxy a) :: Proxy b
-    type Meth3Sym0 :: forall a b. (~>) (Proxy a) (Proxy b)
+      type family Meth2 @x @y @(a :: x) @(b :: y) (arg :: Proxy a) :: Proxy b
+    type Meth3Sym0 :: forall j
+                             (a :: j)
+                             k
+                             (b :: k). (~>) (Proxy a) (Proxy b)
     data Meth3Sym0 :: (~>) (Proxy a) (Proxy b)
       where
         Meth3Sym0KindInference :: SameKind (Apply Meth3Sym0 arg) (Meth3Sym1 arg) =>
@@ -204,18 +213,18 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations
     type instance Apply Meth3Sym0 a0123456789876543210 = Meth3 a0123456789876543210
     instance SuppressUnusedWarnings Meth3Sym0 where
       suppressUnusedWarnings = snd ((,) Meth3Sym0KindInference ())
-    type Meth3Sym1 :: forall a b. Proxy a -> Proxy b
-    type family Meth3Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where
+    type Meth3Sym1 :: forall j (a :: j) k (b :: k). Proxy a -> Proxy b
+    type family Meth3Sym1 @j @(a :: j) @k @(b :: k) (a0123456789876543210 :: Proxy a) :: Proxy b where
       Meth3Sym1 a0123456789876543210 = Meth3 a0123456789876543210
     type PC3 :: forall j. j -> forall k. k -> Constraint
     class PC3 @j (a :: j) @k (b :: k) where
-      type family Meth3 (arg :: Proxy a) :: Proxy b
-    type Meth4Sym0 :: forall a. a
-    type family Meth4Sym0 @a :: a where
+      type family Meth3 @j @(a :: j) @k @(b :: k) (arg :: Proxy a) :: Proxy b
+    type Meth4Sym0 :: forall (a :: Type). a
+    type family Meth4Sym0 @(a :: Type) :: a where
       Meth4Sym0 = Meth4
     type PC4 :: forall (a :: Type). Constraint
-    class PC4 @a where
-      type family Meth4 :: a
+    class PC4 @(a :: Type) where
+      type family Meth4 @(a :: Type) :: a
     type SD1 :: forall j k (a :: j) (b :: k). D1 @j @k a b -> Type
     data SD1 :: forall j k (a :: j) (b :: k). D1 @j @k a b -> Type
       where
diff --git a/singletons-th/CHANGES.md b/singletons-th/CHANGES.md
index 29cb7000..386e415a 100644
--- a/singletons-th/CHANGES.md
+++ b/singletons-th/CHANGES.md
@@ -5,6 +5,10 @@ next [????.??.??]
 -----------------
 * Add support for promoting and singling type variables that scope over the
   bodies of class method defaults and instance methods.
+* When promoting a class with a standalone kind signature, `singletons-th` will
+  now guarantee that the promoted class methods will quantify their kind
+  variables in the exact same order as the type variables in the original class
+  methods' types.
 
 3.4 [2024.05.12]
 ----------------
diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs
index c25659dd..f1f603c5 100644
--- a/singletons-th/src/Data/Singletons/TH/Promote.hs
+++ b/singletons-th/src/Data/Singletons/TH/Promote.hs
@@ -36,7 +36,8 @@ import Control.Arrow (second)
 import Control.Monad
 import Control.Monad.Trans.Maybe
 import Control.Monad.Writer
-import Data.List (nub)
+import Data.Function (on)
+import Data.List (deleteFirstsBy, nub)
 import qualified Data.Map.Strict as Map
 import Data.Map.Strict ( Map )
 import Data.Maybe
@@ -257,7 +258,7 @@ promoteDataDec (DataDecl _ _ _ ctors) = do
 
 promoteClassDec :: UClassDecl -> PrM AClassDecl
 promoteClassDec decl@(ClassDecl { cd_name = cls_name
-                                , cd_tvbs = cls_tvbs
+                                , cd_tvbs = orig_cls_tvbs
                                 , cd_fds  = fundeps
                                 , cd_atfs = atfs
                                 , cd_lde  = lde@LetDecEnv
@@ -270,19 +271,34 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name
       meth_names     = map fst meth_sigs_list
       defaults_list  = OMap.assocs defaults
       defaults_names = map fst defaults_list
-      cls_tvb_names  = map extractTvbName cls_tvbs
+      cls_tvb_names  = map extractTvbName orig_cls_tvbs
   mb_cls_sak <- dsReifyType cls_name
-  sig_decs <- mapM (uncurry promote_sig) meth_sigs_list
+
+  -- If the class has a standalone kind signature, we take the original,
+  -- user-written class binders (`orig_cls_tvbs`) and fill them out using
+  -- `matchUpSAKWithDecl` to produce the "full" binders, as described in
+  -- Note [Promoted class methods and kind variable ordering] (Case 1:
+  -- Parent class with standalone kind signature).
+  mb_full_cls_tvbs <-
+    traverse (\cls_sak -> matchUpSAKWithDecl cls_sak orig_cls_tvbs) mb_cls_sak
+  -- Compute the DTyVarBndrVis binders to use in the promoted class declaration.
+  -- If the class has a standalone kind signature, these will be the full
+  -- binders (see `mb_full_cls_tvbs above`). Otherwise, these will be the
+  -- original binders (`orig_cls_tvbs`).
+  let pro_cls_tvbs_vis =
+        maybe orig_cls_tvbs tvbForAllTyFlagsToBndrVis mb_full_cls_tvbs
+
+  sig_decs <- mapM (uncurry (promote_sig mb_full_cls_tvbs)) meth_sigs_list
   (default_decs, ann_rhss, prom_rhss)
     <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs cls_tvb_names) defaults_list
-  defunAssociatedTypeFamilies cls_tvbs atfs
+  defunAssociatedTypeFamilies orig_cls_tvbs atfs
 
   infix_decls' <- mapMaybeM (uncurry (promoteInfixDecl Nothing)) $
                   OMap.assocs infix_decls
   cls_infix_decls <- promoteReifiedInfixDecls $ cls_name:meth_names
 
   -- no need to do anything to the fundeps. They work as is!
-  let pro_cls_dec = DClassD [] pClsName cls_tvbs fundeps
+  let pro_cls_dec = DClassD [] pClsName pro_cls_tvbs_vis fundeps
                             (sig_decs ++ default_decs ++ infix_decls')
       mb_pro_cls_sak = fmap (DKiSigD pClsName) mb_cls_sak
   emitDecs $ maybeToList mb_pro_cls_sak ++ pro_cls_dec:cls_infix_decls
@@ -291,57 +307,245 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name
   return (decl { cd_lde = lde { lde_defns = OMap.fromList defaults_list'
                               , lde_proms = OMap.fromList proms } })
   where
-    promote_sig :: Name -> DType -> PrM DDec
-    promote_sig name ty = do
+    -- Promote a class method's type signature to an associated type family.
+    promote_sig ::
+         Maybe [DTyVarBndr ForAllTyFlag]
+         -- ^ If the parent class has a standalone kind signature, then this
+         -- will be @'Just' full_bndrs@, where @full_bndrs@ are the full type
+         -- variable binders described in
+         -- @Note [Promoted class methods and kind variable ordering]@ (Case 1:
+         -- Parent class with standalone kind signature). Otherwise, this will
+         -- be 'Nothing'.
+      -> Name
+         -- ^ The class method's name.
+      -> DType
+         -- ^ The class method's type.
+      -> PrM DDec
+         -- ^ The associated type family for the promoted class method.
+    promote_sig mb_full_cls_tvbs name meth_ty = do
       opts <- getOptions
       let proName = promotedTopLevelValueName opts name
-      -- When computing the kind to use for the defunctionalization symbols,
-      -- /don't/ use the type variable binders from the method's type...
-      (_, argKs, resK) <- promoteUnraveled ty
-      args <- mapM (const $ qNewName "arg") argKs
-      let proTvbs = zipWith (`DKindedTV` BndrReq) args argKs
-      -- ...instead, compute the type variable binders in a left-to-right order,
-      -- since that is the same order that the promoted method's kind will use.
-      -- See Note [Promoted class methods and kind variable ordering]
-          meth_sak_tvbs = changeDTVFlags SpecifiedSpec $
-                          toposortTyVarsOf $ argKs ++ [resK]
-          meth_sak      = ravelVanillaDType meth_sak_tvbs [] argKs resK
+      (meth_expl_tvbs, meth_arg_kis, meth_res_ki) <- promoteUnraveled meth_ty
+      args <- mapM (const $ qNewName "arg") meth_arg_kis
+      let pro_meth_args = zipWith (`DKindedTV` BndrReq) args meth_arg_kis
+          -- Compute the type variables to use in the invisible `forall`s in the
+          -- defunctionalization symbols' standalone kind signatures.
+          meth_sak_tvbs =
+            case tvbForAllTyFlagsToSpecs <$> mb_full_cls_tvbs of
+              -- If the parent class has a standalone kind signature, then make
+              -- sure that the order of type variables in the `forall`s matches
+              -- the order in the method's original type signature. As described
+              -- in Note [Promoted class methods and kind variable ordering]
+              -- (Case 1: Parent class with standalone kind signature), this
+              -- consists of the class variables (`full_cls_tvbs_spec`) followed
+              -- by the method variables (see `meth_tvbs` below).
+              Just full_cls_tvbs_spec ->
+                -- Compute the type variabes that the method's type signature
+                -- quantifies.
+                let meth_tvbs
+                      -- If the method's type signature lacks an explicit
+                      -- `forall`, then we infer the order in which the method
+                      -- implicitly quantifies its type variables using
+                      -- `toposortTyVarsOf`. Make sure to exclude the type
+                      -- variables already bound by the class header, as we
+                      -- don't want to re-quantify them.
+                      | null meth_expl_tvbs
+                      = deleteFirstsBy
+                          ((==) `on` extractTvbName)
+                          (changeDTVFlags SpecifiedSpec
+                             (toposortTyVarsOf (meth_arg_kis ++ [meth_res_ki])))
+                          full_cls_tvbs_spec
+                      -- If the method's type signature has an explicit
+                      -- `forall`,then just use the type variables quantified by
+                      -- that `forall`.
+                      | otherwise
+                      = meth_expl_tvbs in
+                full_cls_tvbs_spec ++ meth_tvbs
+              -- If the parent class lacks a standalone kind signature, then we
+              -- cannot make any guarantees about the order in which the type
+              -- variables appear. Still, we should at least pick /some/ order
+              -- for the type variables. We compute the type variable binders in
+              -- a left-to-right order, since that is the same order that the
+              -- promoted method's kind will use. See
+              -- Note [Promoted class methods and kind variable ordering]
+              -- (Case 2: Parent class without standalone kind signature).
+              Nothing ->
+                changeDTVFlags SpecifiedSpec $
+                toposortTyVarsOf $ meth_arg_kis ++ [meth_res_ki]
+          meth_sak = ravelVanillaDType meth_sak_tvbs [] meth_arg_kis meth_res_ki
+          -- All of the type variable binders to use in the promoted method
+          -- declaration. If the parent class has a standalone kind signature,
+          -- these will include both invisible binders (`meth_sak_tvbs`) and
+          -- visible binders (`pro_meth_args`). Otherwise, this will only
+          -- include visible binders (`pro_meth_args`).
+          all_meth_tvbs
+            | isJust mb_full_cls_tvbs
+            = tvbSpecsToBndrVis meth_sak_tvbs ++ pro_meth_args
+            | otherwise
+            = pro_meth_args
       m_fixity <- reifyFixityWithLocals name
       emitDecsM $ defunctionalize proName m_fixity $ DefunSAK meth_sak
 
       return $ DOpenTypeFamilyD (DTypeFamilyHead proName
-                                                 proTvbs
-                                                 (DKindSig resK)
+                                                 all_meth_tvbs
+                                                 (DKindSig meth_res_ki)
                                                  Nothing)
 
 {-
 Note [Promoted class methods and kind variable ordering]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In general, we make an effort to preserve the order of type variables when
-promoting type signatures, but there is an annoying corner case where this is
-difficult: class methods. When promoting class methods, the order of kind
-variables in their kinds will often "just work" by happy coincidence, but
-there are some situations where this does not happen. Consider the following
-class:
+promoting type signatures, but there is a corner case where this is difficult:
+class methods.
+
+Specifically, we are able only able to preserve the order of type variables in
+class method types when the parent class has a standalone kind signature. This
+is because we use the TypeAbstractions language extension to explicitly bind
+the promoted classes' kind variables in the intended order, and one can only
+use TypeAbstractions in associated type families when the parent class has a
+standalone kind signature. (Let's call this Case 1.)
+
+The flip side is that when the parent class lacks a standalone kind signature,
+we cannot use TypeAbstractions in the promoted classes. In such cases, we
+cannot make any guarantees about the order of kind variables for promoted
+classes. (Let's call this Case 2.)
+
+-----
+-- Case 1: Parent class with standalone kind signature
+-----
 
-  class C (b :: Type) where
+As an example, consider:
+
+  type C :: Type -> Constraint
+  class C b where
+    m :: forall a. a -> b -> a
+
+The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds
+`b` before `a`. Because `C` has a standalone kind signature, the order of
+type variables is preserved when promoting `m`:
+
+  type PC :: Type -> Constraint
+  class PC b where
+    type M @b @a (x :: a) (y :: b) :: a
+
+Here, we use TypeAbstractions to explicitly bind `b` before `a` in the
+declaration for `M`, thus ensuring that `M :: forall b a. a -> b -> a`. We
+preserve this order of kind variables in `M`'s defunctionalization symbols as
+well:
+
+  type MSym0 :: forall b a. a ~> b ~> a
+  type MSym1 :: forall b a. a -> b ~> a
+
+Therefore, the trick is to figure out what variables to bind with
+TypeAbstractions in the promoted class declarations. Roughly speaking, we have
+the following formula:
+
+  type M @<class variables> ... @<method variables> ... <method arguments> ... :: <method result>
+
+In the example above:
+
+* The class variables are: @b
+* The method variables are: @a
+* The method arguments are: (x :: a) (y :: b)
+* The method result is: a
+
+The hardest part of this formula to get right are the class variables. Here is
+a slightly more interesting example which illustrates the challenges:
+
+  type C :: k -> Constraint
+  class C b where
+    m :: forall a. a -> Proxy b
+
+A naïve attempt at promoting `C` would be:
+
+  type PC :: k -> Constraint
+  class PC b where
+    type M @b @a (x :: a) :: Proxy b
+
+However, this is not quite right. This is because `k` is specified in the type
+of `m`:
+
+  m :: forall k (b :: k). C b => forall a. a -> Proxy b
+
+But `k` is /inferred/ in the kind of `M`:
+
+  M :: forall {k} (b :: k) a. a -> Proxy b
+
+The reason this happens is because GHC determines the visibilities of kind
+variables for associated type families independently of the parent class's
+standalone kind signature. That is, it only considers `type M @b @a (x :: a) ::
+Proxy b` in isolation, and since we didn't write out `k` explicitly in this
+declaration, GHC considers `k` to be inferred.
+
+In order to make `k` specified in `M`'s kind, we need to instead promote `C` to
+something that looks closer to this:
+
+  type PC :: k -> Constraint
+  class PC @k (b :: k) where
+    type M @k @(b :: k) @a (x :: a) :: Proxy b
+    -- Because we wrote out `k`, we now have:
+    -- M :: forall {k} (b :: k) a. a -> Proxy b
+
+In the declaration for `M`, we have:
+
+* The class variables are: @k @(b :: k)
+* The method variables are: @a
+* The method arguments are: (x :: a)
+* The method result is: Proxy b
+
+Note that we now have `class PC @k (b :: k)` instead of simply `class PC b`.
+This is a slight departure from what the user originally wrote (without any @
+binders), but it is a necessary departure, as `k` would not be in scope over
+the definition of `M` otherwise.
+
+As such, we need a way to go from `class PC b` (which lacks the `k` from the
+standalone kind signature) to `class PC @k (b :: k)` (which does include `k`).
+Let's call the former's type variable binders the /original/ binders, and let's
+call the latter's type variable binders the /full/ binders. (They are "full" in
+the sense that we have filled them out using type variable binders from the
+standalone kind signature.)
+
+We use the `matchUpSAKWithDecl` function to take the original binders (plus the
+parent class's standalone kind signature) as input and produce the full binders
+as output. With the full binders in hand, we can complete the rest of the
+promoted class declaration:
+
+* We can produce the `@k (b :: k)` part of `class PC @k (b :: k)` by calling
+  `tvbForAllTyFlagsToVis` on the full binders.
+* For each promoted method `M`, we can produce the <class variables> in
+  `type M @<class variables> ...` by calling
+  `tvbSpecsToBndrVis . tvbForAllTyFlagsToSpecs` on the full binders. Note that
+  this is /not/ the same thing as calling `tvbForAllTyFlagsToVis`, as we want
+  all of the <class variables> to be invisible, which `tvbSpecsToBndrVis`
+  accomplishes.
+
+-----
+-- Case 2: Parent class without standalone kind signature
+-----
+
+If the parent class does /not/ have a standalone kind signature, then we do not
+make any guarantees about the order of kind variables in the promoted methods'
+kinds. The order will often "just work" by happy coincidence, but there are
+some situations where this does not happen. Consider the following class:
+
+  -- No standalone kind signature
+  class C b where
     m :: forall a. a -> b -> a
 
 The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds
 `b` before `a`. This order is preserved when singling `m`, but *not* when
 promoting `m`. This is because the `C` class is promoted as follows:
 
-  class PC (b :: Type) where
+  -- No standalone kind signature
+  class PC b where
     type M (x :: a) (y :: b) :: a
 
-Due to the way GHC kind-checks associated type families, the kind of `M` is
-`forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the
-`StandaloneKindSignatures` extension does not provide a way to explicitly
-declare the full kind of an associated type family, so this limitation is
-not easy to work around.
-
-The defunctionalization symbols for `M` will also follow a similar
-order of type variables:
+Because `PC` does not have a standalone kind signature, we cannot use
+`TypeAbstractions` in the declaration for `M`. As such, GHC will quantify the
+kind variables in left-to-right order, so the kind of `M` will be inferred to
+be `forall a b. a -> b -> a`, which binds `b` *after* `a`. The
+defunctionalization symbols for `M` will also follow a similar order of type
+variables:
 
   type MSym0 :: forall a b. a ~> b ~> a
   type MSym1 :: forall a b. a -> b ~> a
@@ -349,7 +553,7 @@ order of type variables:
 There is one potential hack we could use to rectify this:
 
   type FlipConst x y = y
-  class PC (b :: Type) where
+  class PC b where
     type M (x :: FlipConst '(b, a) a) (y :: b) :: a
 
 Using `FlipConst` would cause `b` to be mentioned before `a`, which would give
diff --git a/singletons-th/src/Data/Singletons/TH/Single/Data.hs b/singletons-th/src/Data/Singletons/TH/Single/Data.hs
index 27932aa5..7817dc85 100644
--- a/singletons-th/src/Data/Singletons/TH/Single/Data.hs
+++ b/singletons-th/src/Data/Singletons/TH/Single/Data.hs
@@ -13,9 +13,7 @@ module Data.Singletons.TH.Single.Data
 
 import Language.Haskell.TH.Desugar as Desugar
 import Language.Haskell.TH.Syntax
-import qualified Data.Map.Strict as Map
 import Data.Maybe
-import Data.Traversable (mapAccumL)
 import Data.Singletons.TH.Names
 import Data.Singletons.TH.Options
 import Data.Singletons.TH.Promote.Type
@@ -269,26 +267,12 @@ singCtor dataName (DCon con_tvbs cxt name fields rty)
 -- type SD :: forall j l (a :: l) (b :: j). D @j @l (a :: l) b -> Type
 -- @
 --
--- Note that:
+-- Note that the order of the invisible quantifiers is preserved, so both
+-- @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would
+-- expect it to.
 --
--- * This function has a precondition that the length of @data_bndrs@ must
---   always be equal to the number of visible quantifiers (i.e., the number of
---   function arrows plus the number of visible @forall@–bound variables) in
---   @sak@. @singletons-th@ maintains this invariant when constructing a
---   'DataDecl' (see the 'buildDataDTvbs' function).
---
--- * The order of the invisible quantifiers is preserved, so both
---   @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would
---   expect it to.
---
--- * Whenever possible, this function reuses type variable names from the data
---   type's user-written binders. This is why the standalone kind signature uses
---   @forall j l@ instead of @forall j k@, since the @(a :: l)@ binder uses @l@
---   instead of @k@. We could have just as well chose the other way around, but
---   we chose to pick variable names from the data type binders since they scope
---   over other parts of the data type declaration (e.g., in @deriving@
---   clauses), so keeping these names avoids having to perform some
---   alpha-renaming.
+-- See also the comments on the 'matchUpSAKWithDecl' function (in
+-- "Data.Singletons.TH.Util"), which also apply here.
 singDataSAK ::
      MonadFail q
   => DKind
@@ -300,58 +284,10 @@ singDataSAK ::
   -> q DKind
      -- ^ The standalone kind signature for the singled data type
 singDataSAK data_sak data_bndrs data_k = do
-  -- (1) First, explicitly quantify any free kind variables in `data_sak` using
-  -- an invisible @forall@. This is done to ensure that precondition (2) in
-  -- `matchUpSigWithDecl` is upheld. (See the Haddocks for that function).
-  let data_sak_free_tvbs =
-        changeDTVFlags SpecifiedSpec $ toposortTyVarsOf [data_sak]
-      data_sak' = DForallT (DForallInvis data_sak_free_tvbs) data_sak
-
-  -- (2) Next, compute type variable binders for the singled data type's
-  -- standalone kind signature using `matchUpSigWithDecl`. Note that these can
-  -- be biased towards type variable names mention in `data_sak` over names
-  -- mentioned in `data_bndrs`, but we will fix that up in the next step.
-  let (data_sak_args, _) = unravelDType data_sak'
-  sing_sak_tvbs <- matchUpSigWithDecl data_sak_args data_bndrs
-
-  -- (3) Swizzle the type variable names so that names in `data_bndrs` are
-  -- preferred over names in `data_sak`.
-  --
-  -- This is heavily inspired by similar code in GHC:
-  -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616
-  let invis_data_sak_args = filterInvisTvbArgs data_sak_args
-      invis_data_sak_arg_nms = map extractTvbName invis_data_sak_args
-
-      invis_data_bndrs = toposortKindVarsOfTvbs data_bndrs
-      invis_data_bndr_nms = map extractTvbName invis_data_bndrs
-
-      swizzle_env =
-        Map.fromList $ zip invis_data_sak_arg_nms invis_data_bndr_nms
-      (_, swizzled_sing_sak_tvbs) =
-        mapAccumL (swizzleTvb swizzle_env) Map.empty sing_sak_tvbs
-      swizzled_sing_sak_tvbs' =
-        map (fmap mk_data_sak_spec) swizzled_sing_sak_tvbs
-
-  -- (4) Finally, construct the kind of the singled data type.
-  pure $ DForallT (DForallInvis swizzled_sing_sak_tvbs')
+  sing_sak_tvbs <- matchUpSAKWithDecl data_sak data_bndrs
+  let sing_sak_tvbs' = tvbForAllTyFlagsToSpecs sing_sak_tvbs
+  pure $ DForallT (DForallInvis sing_sak_tvbs')
        $ DArrowT `DAppT` data_k `DAppT` DConT typeKindName
-  where
-    -- Convert a ForAllTyFlag value to a Specificity value, i.e., a binder
-    -- suitable for use in an invisible `forall`. We convert Required values
-    -- to SpecifiedSpec values because all of the binders in the `forall` are
-    -- invisible. For instance, we would single this data type:
-    --
-    --   type T :: forall k -> k -> Type
-    --   data T k (a :: k) where ...
-    --
-    -- Like so:
-    --
-    --   -- Note: the `k` is invisible, not visible
-    --   type ST :: forall k (a :: k). T k a -> Type
-    --   data ST z where ...
-    mk_data_sak_spec :: ForAllTyFlag -> Specificity
-    mk_data_sak_spec (Invisible spec) = spec
-    mk_data_sak_spec Required         = SpecifiedSpec
 
 {-
 Note [singletons-th and record selectors]
diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs
index 6bbf8504..1e9a37ea 100644
--- a/singletons-th/src/Data/Singletons/TH/Util.hs
+++ b/singletons-th/src/Data/Singletons/TH/Util.hs
@@ -267,6 +267,14 @@ maybeSigT ty (Just ki) = ty `DSigT` ki
 -- @
 --
 -- Note that note of @b@, @d@, or @e@ appear in the list.
+--
+-- See also 'tvbForAllTyFlagsToBndrVis', which takes a list of @'DTyVarBndr'
+-- 'ForAllTyFlag'@ as arguments instead of a list of 'DTyVarBndrSpec's. Note
+-- that @'tvbSpecsToBndrVis' . 'tvbForAllTyFlagsToSpecs'@ is /not/ the same
+-- thing as 'tvbForAllTyFlagsToBndrVis'. This is because 'tvbSpecsToBndrVis'
+-- only produces 'BndrInvis' binders as output, whereas
+-- 'tvbForAllTyFlagsToBndrVis' can produce both 'BndrReq' and 'BndrInvis'
+-- binders.
 tvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis]
 tvbSpecsToBndrVis = mapMaybe (traverse specificityToBndrVis)
   where
@@ -720,6 +728,96 @@ mapAndUnzip3M f (x:xs) = do
 isHsLetter :: Char -> Bool
 isHsLetter c = isLetter c || c == '_'
 
+-- @'matchUpSAKWithDecl' decl_sak decl_bndrs@ produces @'DTyVarBndr'
+-- 'ForAllTyFlag'@s for a declaration, using the original declaration's
+-- standalone kind signature (@decl_sak@) and its user-written binders
+-- (@decl_bndrs@) as a template. For this example:
+--
+-- @
+-- type D :: forall j k. k -> j -> Type
+-- data D \@j \@l (a :: l) b = ...
+-- @
+--
+-- We would produce the following @'DTyVarBndr' 'ForAllTyFlag'@s:
+--
+-- @
+-- \@j \@l (a :: l) (b :: j)
+-- @
+--
+-- From here, these @'DTyVarBndr' 'ForAllTyFlag'@s can be converted into other
+-- forms of 'DTyVarBndr's:
+--
+-- * They can be converted to 'DTyVarBndrSpec's using 'tvbForAllTyFlagsToSpecs'.
+--   (See, for example, 'singDataSAK' in "Data.Singletons.TH.Single.Data", which
+--   does this to construct the invisible @forall@s in the standalone kind
+--   signature for a singled @data@ declaration.)
+--
+-- * They can be converted to 'DTyVarBndrVis'es using 'tvbForAllTyFlagsToVis'.
+--   (See, for example, 'promoteClassDec' in "Data.Singletons.TH.Promote", which
+--   does this to compute the \"full\" user-written binders for a promoted class
+--   declaration, as described in @Note [Promoted class methods and kind variable
+--   ordering] (Case 1: Case 1: Parent class with standalone kind signature).)
+--
+-- Note that:
+--
+-- * This function has a precondition that the length of @decl_bndrs@ must
+--   always be equal to the number of visible quantifiers (i.e., the number of
+--   function arrows plus the number of visible @forall@–bound variables) in
+--   @decl_sak@.
+--
+-- * Whenever possible, this function reuses type variable names from the
+--   declaration's user-written binders. This is why the @'DTyVarBndr'
+--   'ForAllTyFlag'@ use @\@j \@l@ instead of @\@j \@k@, since the @(a :: l)@
+--   binder uses @l@ instead of @k@. We could have just as well chose the other
+--   way around, but we chose to pick variable names from the user-written
+--   binders since they scope over other parts of the declaration. (For example,
+--   the user-written binders of a @data@ declaration scope over the type
+--   variables mentioned in a @deriving@ clause.) As such, keeping these names
+--   avoids having to perform some alpha-renaming.
+--
+-- This function's implementation was heavily inspired by parts of GHC's
+-- kcCheckDeclHeader_sig function:
+-- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2524-2643
+matchUpSAKWithDecl ::
+     forall q.
+     MonadFail q
+  => DKind
+     -- ^ The declaration's standalone kind signature
+  -> [DTyVarBndrVis]
+     -- ^ The user-written binders in the declaration
+  -> q [DTyVarBndr ForAllTyFlag]
+matchUpSAKWithDecl decl_sak decl_bndrs = do
+  -- (1) First, explicitly quantify any free kind variables in `decl_sak` using
+  -- an invisible @forall@. This is done to ensure that precondition (2) in
+  -- `matchUpSigWithDecl` is upheld. (See the Haddocks for that function).
+  let decl_sak_free_tvbs =
+        changeDTVFlags SpecifiedSpec $ toposortTyVarsOf [decl_sak]
+      decl_sak' = DForallT (DForallInvis decl_sak_free_tvbs) decl_sak
+
+  -- (2) Next, compute type variable binders using `matchUpSigWithDecl`. Note
+  -- that these can be biased towards type variable names mention in `decl_sak`
+  -- over names mentioned in `decl_bndrs`, but we will fix that up in the next
+  -- step.
+  let (decl_sak_args, _) = unravelDType decl_sak'
+  sing_sak_tvbs <- matchUpSigWithDecl decl_sak_args decl_bndrs
+
+  -- (3) Finally, swizzle the type variable names so that names in `decl_bndrs`
+  -- are preferred over names in `decl_sak`.
+  --
+  -- This is heavily inspired by similar code in GHC:
+  -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616
+  let invis_decl_sak_args = filterInvisTvbArgs decl_sak_args
+      invis_decl_sak_arg_nms = map extractTvbName invis_decl_sak_args
+
+      invis_decl_bndrs = toposortKindVarsOfTvbs decl_bndrs
+      invis_decl_bndr_nms = map extractTvbName invis_decl_bndrs
+
+      swizzle_env =
+        Map.fromList $ zip invis_decl_sak_arg_nms invis_decl_bndr_nms
+      (_, swizzled_sing_sak_tvbs) =
+        mapAccumL (swizzleTvb swizzle_env) Map.empty sing_sak_tvbs
+  pure swizzled_sing_sak_tvbs
+
 -- Match the quantifiers in a type-level declaration's standalone kind signature
 -- with the user-written binders in the declaration. This function assumes the
 -- following preconditions:
@@ -896,7 +994,67 @@ swizzleTvb swizzle_env subst tvb =
 data ForAllTyFlag
   = Invisible !Specificity
     -- ^ If the 'Specificity' value is 'SpecifiedSpec', then the binder is
-    -- permitted by request. If the 'Specificity' value is 'InferredSpec', then
-    -- the binder is prohibited from appearing in source Haskell.
+    -- permitted by request (e.g., @\@a@). If the 'Specificity' value is
+    -- 'InferredSpec', then the binder is prohibited from appearing in source
+    -- Haskell (e.g., @\@{a}@).
   | Required
-    -- ^ The binder is required to appear in source Haskell
+    -- ^ The binder is required to appear in source Haskell (e.g., @a@).
+
+-- | Convert a list of @'DTyVarBndr' 'ForAllTyFlag'@s to a list of
+-- 'DTyVarBndrSpec's, which is suitable for use in an invisible @forall@.
+-- Specifically:
+--
+-- * Variable binders that use @'Invisible' spec@ are converted to @spec@.
+--
+-- * Variable binders that are 'Required' are converted to 'SpecifiedSpec',
+--   as all of the 'DTyVarBndrSpec's are invisible. As an example of how this
+--   is used, consider what would happen when singling this data type:
+--
+--   @
+--   type T :: forall k -> k -> Type
+--   data T k (a :: k) where ...
+--   @
+--
+--   Here, the @k@ binder is 'Required'. When we produce the standalone kind
+--   signature for the singled data type, we use 'tvbForAllTyFlagsToSpecs' to
+--   produce the type variable binders in the outermost @forall@:
+--
+--   @
+--   type ST :: forall k (a :: k). T k a -> Type
+--   data ST z where ...
+--   @
+--
+--   Note that the @k@ is bound visibily (i.e., using 'SpecifiedSpec') in the
+--   outermost, invisible @forall@.
+tvbForAllTyFlagsToSpecs :: [DTyVarBndr ForAllTyFlag] -> [DTyVarBndrSpec]
+tvbForAllTyFlagsToSpecs = map (fmap to_spec)
+  where
+   to_spec :: ForAllTyFlag -> Specificity
+   to_spec (Invisible spec) = spec
+   to_spec Required         = SpecifiedSpec
+
+-- | Convert a list of @'DTyVarBndr' 'ForAllTyFlag'@s to a list of
+-- 'DTyVarBndrVis'es, which is suitable for use in a type-level declaration
+-- (e.g., the @var_1 ... var_n@ in @class C var_1 ... var_n@). Specifically:
+--
+-- * Variable binders that use @'Invisible' 'InferredSpec'@ are dropped
+--   entirely. Such binders cannot be represented in source Haskell.
+--
+-- * Variable binders that use @'Invisible' 'SpecifiedSpec'@ are converted to
+--   'BndrInvis'.
+--
+-- * Variable binders that are 'Required' are converted to 'BndrReq'.
+--
+-- See also 'tvbSpecsToBndrVis', which takes a list of 'DTyVarBndrSpec's as
+-- arguments instead of a list of @'DTyVarBndr' 'ForAllTyFlag'@s. Note that
+-- @'tvbSpecsToBndrVis' . 'tvbForAllTyFlagsToSpecs'@ is /not/ the same thing as
+-- 'tvbForAllTyFlagsToBndrVis'. This is because 'tvbSpecsToBndrVis' only
+-- produces 'BndrInvis' binders as output, whereas 'tvbForAllTyFlagsToBndrVis'
+-- can produce both 'BndrReq' and 'BndrInvis' binders.
+tvbForAllTyFlagsToBndrVis :: [DTyVarBndr ForAllTyFlag] -> [DTyVarBndrVis]
+tvbForAllTyFlagsToBndrVis = catMaybes . map (traverse to_spec_maybe)
+  where
+    to_spec_maybe :: ForAllTyFlag -> Maybe BndrVis
+    to_spec_maybe (Invisible InferredSpec) = Nothing
+    to_spec_maybe (Invisible SpecifiedSpec) = Just BndrInvis
+    to_spec_maybe Required = Just BndrReq