diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,14 @@
 Changelog for the `singletons` project
 ======================================
 
+3.0.4 [2024.12.11]
+------------------
+* Define `Sing` instances such that they explicitly match on their types on the
+  left-hand sides (e.g., define `type instance Sing @(k1 ~> k2) = SLambda`
+  instead of `type instance Sing = SLambda`. Doing so will make `singletons`
+  future-proof once
+  [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515) is fixed.
+
 3.0.3 [2024.05.12]
 ------------------
 * Allow building with GHC 9.10.
diff --git a/singletons.cabal b/singletons.cabal
--- a/singletons.cabal
+++ b/singletons.cabal
@@ -1,5 +1,5 @@
 name:           singletons
-version:        3.0.3
+version:        3.0.4
 cabal-version:  1.24
 synopsis:       Basic singleton types and definitions
 homepage:       http://www.github.com/goldfirere/singletons
@@ -17,9 +17,10 @@
               , GHC == 9.0.2
               , GHC == 9.2.7
               , GHC == 9.4.8
-              , GHC == 9.6.5
+              , GHC == 9.6.6
               , GHC == 9.8.2
               , GHC == 9.10.1
+              , GHC == 9.12.1
 extra-source-files: README.md, CHANGES.md
 license:        BSD3
 license-file:   LICENSE
@@ -60,7 +61,7 @@
 
 library
   hs-source-dirs:     src
-  build-depends:      base >= 4.9 && < 4.21
+  build-depends:      base >= 4.9 && < 4.22
   default-language:   Haskell2010
   exposed-modules:    Data.Singletons
                       Data.Singletons.Decide
@@ -77,5 +78,5 @@
   other-modules:      ByHand
                       ByHand2
 
-  build-depends:      base >= 4.9 && < 4.21,
+  build-depends:      base >= 4.9 && < 4.22,
                       singletons
diff --git a/src/Data/Singletons.hs b/src/Data/Singletons.hs
--- a/src/Data/Singletons.hs
+++ b/src/Data/Singletons.hs
@@ -229,11 +229,11 @@
 -- @
 --
 -- Here, @f@ uses methods from both 'SingI' and 'SingKind'. However, the shape
--- of each constraint is rather different: using 'sing' requires a 'SingI T'
--- constraint, whereas using 'fromSing' requires a 'SingKind K' constraint.
+-- of each constraint is rather different: using 'sing' requires a @SingI T@
+-- constraint, whereas using 'fromSing' requires a @SingKind K@ constraint.
 --
 -- If you need to satisfy this constraint with an explicit singleton, please
--- see 'withSingI' or the 'Sing' pattern synonym.
+-- see 'withSingI' or the v'Sing' pattern synonym.
 #if __GLASGOW_HASKELL__ >= 900
 type SingI :: forall {k}. k -> Constraint
 #endif
@@ -405,7 +405,12 @@
 newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
   SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
                { sUnwrapSing :: Sing a } -> SWrappedSing ws
-type instance Sing = SWrappedSing
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(WrappedSing a) =
+#else
+type instance Sing =
+#endif
+  SWrappedSing
 
 #if __GLASGOW_HASKELL__ >= 810
 type UnwrapSing :: forall k (a :: k). WrappedSing a -> Sing a
@@ -591,7 +596,12 @@
 --            ( forall a. SingI a => SingI (f a)
 --            , (ApplyTyCon :: (k1 -> k2) -> (k1 ~> k2)) ~ ApplyTyConAux1
 --            ) => SingI (TyCon1 f) where
-type instance Apply (TyCon f) x = ApplyTyCon f @@ x
+#if __GLASGOW_HASKELL__ >= 808
+type instance Apply @k1 @k3 (TyCon @k1 @k2 @(k1 ~> k3) f) x =
+#else
+type instance Apply (TyCon f) x =
+#endif
+  ApplyTyCon f @@ x
 
 -- | An \"internal\" defunctionalization symbol used primarily in the
 -- definition of 'ApplyTyCon', as well as the 'SingI' instances for 'TyCon1',
@@ -730,7 +740,12 @@
 #endif
 newtype SLambda (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
-type instance Sing = SLambda
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(k1 ~> k2) =
+#else
+type instance Sing =
+#endif
+  SLambda
 
 -- | An infix synonym for `applySing`
 (@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
diff --git a/src/Data/Singletons/Sigma.hs b/src/Data/Singletons/Sigma.hs
--- a/src/Data/Singletons/Sigma.hs
+++ b/src/Data/Singletons/Sigma.hs
@@ -99,7 +99,12 @@
   (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst).
             Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd :: Sigma s t)
 infixr 4 :%&:
-type instance Sing = SSigma
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Sigma s t) =
+#else
+type instance Sing =
+#endif
+  SSigma
 
 instance forall s t (fst :: s) (a :: Sing fst) (b :: t @@ fst).
        (SingI fst, SingI b)
diff --git a/tests/ByHand.hs b/tests/ByHand.hs
--- a/tests/ByHand.hs
+++ b/tests/ByHand.hs
@@ -98,9 +98,15 @@
 data SNat :: Nat -> Type where
   SZero :: SNat Zero
   SSucc :: SNat n -> SNat (Succ n)
-type instance Sing = SNat
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Nat =
+#else
+type instance Sing =
+#endif
+  SNat
 
-#if __GLASGOW_HASKELL__ >= 810
+#if _
+_GLASGOW_HASKELL__ >= 810
 type SuccSym0 :: Nat ~> Nat
 #endif
 data SuccSym0 :: Nat ~> Nat
@@ -152,7 +158,12 @@
 data SBool :: Bool -> Type where
   SFalse :: SBool False
   STrue :: SBool True
-type instance Sing = SBool
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Bool =
+#else
+type instance Sing =
+#endif
+  SBool
 
 {-
 (&&) :: Bool -> Bool -> Bool
@@ -192,7 +203,12 @@
 data SMaybe :: forall k. Maybe k -> Type where
   SNothing :: SMaybe Nothing
   SJust :: forall k (a :: k). Sing a -> SMaybe (Just a)
-type instance Sing = SMaybe
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Maybe k) =
+#else
+type instance Sing =
+#endif
+  SMaybe
 
 #if __GLASGOW_HASKELL__ >= 810
 type EqualsMaybe :: Maybe k -> Maybe k -> Bool
@@ -242,7 +258,12 @@
 data SList :: forall k. List k -> Type where
   SNil :: SList Nil
   SCons :: forall k (h :: k) (t :: List k). Sing h -> SList t -> SList (Cons h t)
-type instance Sing = SList
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(List k) =
+#else
+type instance Sing =
+#endif
+  SList
 
 #if __GLASGOW_HASKELL__ >= 810
 type NilSym0 :: List a
@@ -315,7 +336,12 @@
 data SEither :: forall k1 k2. Either k1 k2 -> Type where
   SLeft :: forall k1 (a :: k1). Sing a -> SEither (Left a)
   SRight :: forall k2 (b :: k2). Sing b -> SEither (Right b)
-type instance Sing = SEither
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Either k1 k2) =
+#else
+type instance Sing =
+#endif
+  SEither
 
 instance (SingI a) => SingI (Left (a :: k)) where
   sing = SLeft sing
@@ -361,7 +387,12 @@
 #endif
 data SComposite :: forall k1 k2. Composite k1 k2 -> Type where
   SMkComp :: forall k1 k2 (a :: Either (Maybe k1) k2). SEither a -> SComposite (MkComp a)
-type instance Sing = SComposite
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(Composite k1 k2) =
+#else
+type instance Sing =
+#endif
+  SComposite
 
 instance SingI a => SingI (MkComp (a :: Either (Maybe k1) k2)) where
   sing = SMkComp sing
@@ -393,7 +424,12 @@
 #endif
 data SEmpty :: Empty -> Type
 
-type instance Sing = SEmpty
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Empty =
+#else
+type instance Sing =
+#endif
+  SEmpty
 instance SingKind Empty where
   type Demote Empty = Empty
   fromSing = \case
@@ -420,7 +456,12 @@
   SNat :: SRep Nat
   SMaybe :: SRep a -> SRep (Maybe a)
   SVec :: SRep a -> SNat n -> SRep (Vec a n)
-type instance Sing = SRep
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Type =
+#else
+type instance Sing =
+#endif
+  SRep
 
 instance SingI Nat where
   sing = SNat
@@ -1039,4 +1080,9 @@
 #endif
 data SG :: forall a. G a -> Type where
   SMkG :: SG MkG
-type instance Sing = SG
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @(G a) =
+#else
+type instance Sing =
+#endif
+  SG
diff --git a/tests/ByHand2.hs b/tests/ByHand2.hs
--- a/tests/ByHand2.hs
+++ b/tests/ByHand2.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators,
              DefaultSignatures, ScopedTypeVariables, InstanceSigs,
              MultiParamTypeClasses, FunctionalDependencies,
-             UndecidableInstances, CPP #-}
+             UndecidableInstances, CPP, TypeApplications #-}
 {-# OPTIONS_GHC -Wno-missing-signatures -Wno-orphans #-}
 
 #if __GLASGOW_HASKELL__ < 806
@@ -27,7 +27,12 @@
 data SNat :: Nat -> Type where
   SZero :: SNat 'Zero
   SSucc :: SNat n -> SNat ('Succ n)
-type instance Sing = SNat
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Nat =
+#else
+type instance Sing =
+#endif
+  SNat
 
 {-
 type Bool :: Type
@@ -40,7 +45,12 @@
 data SBool :: Bool -> Type where
   SFalse :: SBool 'False
   STrue  :: SBool 'True
-type instance Sing = SBool
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Bool =
+#else
+type instance Sing =
+#endif
+  SBool
 
 {-
 type Ordering :: Type
@@ -54,7 +64,12 @@
   SLT :: SOrdering 'LT
   SEQ :: SOrdering 'EQ
   SGT :: SOrdering 'GT
-type instance Sing = SOrdering
+#if __GLASGOW_HASKELL__ >= 808
+type instance Sing @Ordering =
+#else
+type instance Sing =
+#endif
+  SOrdering
 
 {-
 not :: Bool -> Bool