diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml
index 0362f6b4..15b21774 100644
--- a/.github/workflows/haskell-ci.yml
+++ b/.github/workflows/haskell-ci.yml
@@ -8,9 +8,9 @@
 #
 # For more information, see https://github.com/haskell-CI/haskell-ci
 #
-# version: 0.16.3
+# version: 0.16.6
 #
-# REGENDATA ("0.16.3",["github","cabal.project"])
+# REGENDATA ("0.16.6",["github","cabal.project"])
 #
 name: Haskell-CI
 on:
@@ -245,7 +245,7 @@ jobs:
           source-repository-package
             type:     git
             location: https://github.com/goldfirere/th-desugar
-            tag:      f7db712e95a125e710cefc7cd819c6480f7e52e3
+            tag:      47f6221088ac6185566066b4d45909b0cc704855
           EOF
           $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(singletons|singletons-base|singletons-th)$/; }' >> cabal.project.local
           cat cabal.project
diff --git a/cabal.project b/cabal.project
index 942af235..00de788c 100644
--- a/cabal.project
+++ b/cabal.project
@@ -5,4 +5,4 @@ packages: ./singletons
 source-repository-package
   type: git
   location: https://github.com/goldfirere/th-desugar
-  tag: f7db712e95a125e710cefc7cd819c6480f7e52e3
+  tag: 47f6221088ac6185566066b4d45909b0cc704855
diff --git a/singletons-base/singletons-base.cabal b/singletons-base/singletons-base.cabal
index f0f3ab21..b5b22b03 100644
--- a/singletons-base/singletons-base.cabal
+++ b/singletons-base/singletons-base.cabal
@@ -78,7 +78,7 @@ library
                       singletons-th    >= 3.2  && < 3.3,
                       template-haskell >= 2.20 && < 2.21,
                       text >= 1.2,
-                      th-desugar       >= 1.15 && < 1.16
+                      th-desugar       >= 1.16 && < 1.17
   default-language:   GHC2021
   other-extensions:   TemplateHaskell
   exposed-modules:    Data.Singletons.Base.CustomStar
diff --git a/singletons-base/tests/compile-and-dump/Promote/T361.golden b/singletons-base/tests/compile-and-dump/Promote/T361.golden
index e72a8bfb..0a6c6077 100644
--- a/singletons-base/tests/compile-and-dump/Promote/T361.golden
+++ b/singletons-base/tests/compile-and-dump/Promote/T361.golden
@@ -1,8 +1,8 @@
 Promote/T361.hs:0:0:: Splicing declarations
     genDefunSymbols [''Proxy]
   ======>
-    type ProxySym0 :: forall k (t :: k). Proxy (t :: k)
-    type family ProxySym0 :: Proxy (t :: k) where
+    type ProxySym0 :: forall k (t :: k). Proxy t
+    type family ProxySym0 :: Proxy t where
       ProxySym0 = 'Proxy
 Promote/T361.hs:(0,0)-(0,0): Splicing declarations
     promote
diff --git a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden
index 86883c14..42866593 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden
@@ -60,13 +60,11 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
     type Foo3Sym1 :: forall a. a -> Foo3 a
     type family Foo3Sym1 (a0123456789876543210 :: a) :: Foo3 a where
       Foo3Sym1 a0123456789876543210 = Foo3 a0123456789876543210
-    type Foo41Sym0 :: forall (a :: Type)
-                             (b :: Type). Foo4 (a :: Type) (b :: Type)
-    type family Foo41Sym0 :: Foo4 (a :: Type) (b :: Type) where
+    type Foo41Sym0 :: forall (a :: Type) (b :: Type). Foo4 a b
+    type family Foo41Sym0 :: Foo4 a b where
       Foo41Sym0 = Foo41
-    type Foo42Sym0 :: forall (a :: Type)
-                             (b :: Type). Foo4 (a :: Type) (b :: Type)
-    type family Foo42Sym0 :: Foo4 (a :: Type) (b :: Type) where
+    type Foo42Sym0 :: forall (a :: Type) (b :: Type). Foo4 a b
+    type family Foo42Sym0 :: Foo4 a b where
       Foo42Sym0 = Foo42
     type PairSym0 :: (~>) Bool ((~>) Bool Pair)
     data PairSym0 :: (~>) Bool ((~>) Bool Pair)
@@ -199,10 +197,8 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
         = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SFoo3 c)
     data SFoo4 :: forall (a :: Type) (b :: Type). Foo4 a b -> Type
       where
-        SFoo41 :: forall (a :: Type) (b :: Type).
-                  SFoo4 (Foo41 :: Foo4 (a :: Type) (b :: Type))
-        SFoo42 :: forall (a :: Type) (b :: Type).
-                  SFoo4 (Foo42 :: Foo4 (a :: Type) (b :: Type))
+        SFoo41 :: forall (a :: Type) (b :: Type). SFoo4 (Foo41 :: Foo4 a b)
+        SFoo42 :: forall (a :: Type) (b :: Type). SFoo4 (Foo42 :: Foo4 a b)
     type instance Sing @(Foo4 a b) = SFoo4
     instance (SingKind a, SingKind b) => SingKind (Foo4 a b) where
       type Demote (Foo4 a b) = Foo4 (Demote a) (Demote b)
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T271.golden b/singletons-base/tests/compile-and-dump/Singletons/T271.golden
index 7e8c076b..7656a3c4 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T271.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T271.golden
@@ -14,8 +14,8 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations
       where Identity :: a -> Identity a
       deriving (Eq, Ord)
     type ConstantSym0 :: forall (a :: Type)
-                                (b :: Type). (~>) a (Constant (a :: Type) (b :: Type))
-    data ConstantSym0 :: (~>) a (Constant (a :: Type) (b :: Type))
+                                (b :: Type). (~>) a (Constant a b)
+    data ConstantSym0 :: (~>) a (Constant a b)
       where
         ConstantSym0KindInference :: SameKind (Apply ConstantSym0 arg) (ConstantSym1 arg) =>
                                      ConstantSym0 a0123456789876543210
@@ -23,8 +23,8 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations
     instance SuppressUnusedWarnings ConstantSym0 where
       suppressUnusedWarnings = snd ((,) ConstantSym0KindInference ())
     type ConstantSym1 :: forall (a :: Type) (b :: Type). a
-                                                         -> Constant (a :: Type) (b :: Type)
-    type family ConstantSym1 (a0123456789876543210 :: a) :: Constant (a :: Type) (b :: Type) where
+                                                         -> Constant a b
+    type family ConstantSym1 (a0123456789876543210 :: a) :: Constant a b where
       ConstantSym1 a0123456789876543210 = Constant a0123456789876543210
     type IdentitySym0 :: (~>) a (Identity a)
     data IdentitySym0 :: (~>) a (Identity a)
@@ -157,8 +157,7 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations
                       Constant a b -> Type
       where
         SConstant :: forall (a :: Type) (b :: Type) (n :: a).
-                     (Sing n) ->
-                     SConstant (Constant n :: Constant (a :: Type) (b :: Type))
+                     (Sing n) -> SConstant (Constant n :: Constant a b)
     type instance Sing @(Constant a b) = SConstant
     instance (SingKind a, SingKind b) => SingKind (Constant a b) where
       type Demote (Constant a b) = Constant (Demote a) (Demote b)
@@ -285,7 +284,7 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations
       sing = SConstant sing
     instance SingI1 Constant where
       liftSing = SConstant
-    instance SingI (ConstantSym0 :: (~>) a (Constant (a :: Type) (b :: Type))) where
+    instance SingI (ConstantSym0 :: (~>) a (Constant a b)) where
       sing = singFun1 @ConstantSym0 SConstant
     instance SingI n => SingI (Identity (n :: a)) where
       sing = SIdentity sing
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T296.golden b/singletons-base/tests/compile-and-dump/Singletons/T296.golden
index baa3bf10..a99af46d 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T296.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T296.golden
@@ -20,8 +20,8 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations
                 z = MyProxy
               in z
         in x
-    type MyProxySym0 :: forall (a :: Type). MyProxy (a :: Type)
-    type family MyProxySym0 :: MyProxy (a :: Type) where
+    type MyProxySym0 :: forall (a :: Type). MyProxy a
+    type family MyProxySym0 :: MyProxy a where
       MyProxySym0 = MyProxy
     data Let0123456789876543210ZSym0 a0123456789876543210
       where
@@ -77,8 +77,7 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations
       sing = singFun1 @FSym0 sF
     data SMyProxy :: forall (a :: Type). MyProxy a -> Type
       where
-        SMyProxy :: forall (a :: Type).
-                    SMyProxy (MyProxy :: MyProxy (a :: Type))
+        SMyProxy :: forall (a :: Type). SMyProxy (MyProxy :: MyProxy a)
     type instance Sing @(MyProxy a) = SMyProxy
     instance SingKind a => SingKind (MyProxy a) where
       type Demote (MyProxy a) = MyProxy (Demote a)
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T297.golden b/singletons-base/tests/compile-and-dump/Singletons/T297.golden
index 2c561e46..e33a7c9f 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T297.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T297.golden
@@ -18,8 +18,8 @@ Singletons/T297.hs:(0,0)-(0,0): Splicing declarations
                 z = MyProxy
               in z
         in x
-    type MyProxySym0 :: forall (a :: Type). MyProxy (a :: Type)
-    type family MyProxySym0 :: MyProxy (a :: Type) where
+    type MyProxySym0 :: forall (a :: Type). MyProxy a
+    type family MyProxySym0 :: MyProxy a where
       MyProxySym0 = MyProxy
     type Let0123456789876543210ZSym0 :: MyProxy a
     type family Let0123456789876543210ZSym0 :: MyProxy a where
@@ -56,8 +56,7 @@ Singletons/T297.hs:(0,0)-(0,0): Splicing declarations
       sing = singFun1 @FSym0 sF
     data SMyProxy :: forall (a :: Type). MyProxy a -> Type
       where
-        SMyProxy :: forall (a :: Type).
-                    SMyProxy (MyProxy :: MyProxy (a :: Type))
+        SMyProxy :: forall (a :: Type). SMyProxy (MyProxy :: MyProxy a)
     type instance Sing @(MyProxy a) = SMyProxy
     instance SingKind a => SingKind (MyProxy a) where
       type Demote (MyProxy a) = MyProxy (Demote a)
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T353.golden b/singletons-base/tests/compile-and-dump/Singletons/T353.golden
index fc6f48d2..7b27978c 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T353.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T353.golden
@@ -36,10 +36,8 @@ Singletons/T353.hs:0:0:: Splicing declarations
     type MkProdSym0 :: forall k
                               (f :: k -> Type)
                               (g :: k -> Type)
-                              (p :: k). (~>) (f p) ((~>) (g p) (Prod (f :: k -> Type) (g :: k
-                                                                                            -> Type) (p :: k)))
-    data MkProdSym0 :: (~>) (f p) ((~>) (g p) (Prod (f :: k
-                                                          -> Type) (g :: k -> Type) (p :: k)))
+                              (p :: k). (~>) (f p) ((~>) (g p) (Prod f g p))
+    data MkProdSym0 :: (~>) (f p) ((~>) (g p) (Prod f g p))
       where
         MkProdSym0KindInference :: SameKind (Apply MkProdSym0 arg) (MkProdSym1 arg) =>
                                    MkProdSym0 a0123456789876543210
@@ -49,12 +47,8 @@ Singletons/T353.hs:0:0:: Splicing declarations
     type MkProdSym1 :: forall k
                               (f :: k -> Type)
                               (g :: k -> Type)
-                              (p :: k). f p
-                                        -> (~>) (g p) (Prod (f :: k -> Type) (g :: k
-                                                                                   -> Type) (p :: k))
-    data MkProdSym1 (a0123456789876543210 :: f p) :: (~>) (g p) (Prod (f :: k
-                                                                            -> Type) (g :: k
-                                                                                           -> Type) (p :: k))
+                              (p :: k). f p -> (~>) (g p) (Prod f g p)
+    data MkProdSym1 (a0123456789876543210 :: f p) :: (~>) (g p) (Prod f g p)
       where
         MkProdSym1KindInference :: SameKind (Apply (MkProdSym1 a0123456789876543210) arg) (MkProdSym2 a0123456789876543210 arg) =>
                                    MkProdSym1 a0123456789876543210 a0123456789876543210
@@ -64,11 +58,8 @@ Singletons/T353.hs:0:0:: Splicing declarations
     type MkProdSym2 :: forall k
                               (f :: k -> Type)
                               (g :: k -> Type)
-                              (p :: k). f p
-                                        -> g p -> Prod (f :: k -> Type) (g :: k -> Type) (p :: k)
-    type family MkProdSym2 (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod (f :: k
-                                                                                                     -> Type) (g :: k
-                                                                                                                    -> Type) (p :: k) where
+                              (p :: k). f p -> g p -> Prod f g p
+    type family MkProdSym2 (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod f g p where
       MkProdSym2 a0123456789876543210 a0123456789876543210 = 'MkProd a0123456789876543210 a0123456789876543210
 Singletons/T353.hs:0:0:: Splicing declarations
     genDefunSymbols [''Foo]
@@ -76,8 +67,8 @@ Singletons/T353.hs:0:0:: Splicing declarations
     type MkFooSym0 :: forall k
                              k
                              (a :: k)
-                             (b :: k). (~>) (Proxy a) ((~>) (Proxy b) (Foo (a :: k) (b :: k)))
-    data MkFooSym0 :: (~>) (Proxy a) ((~>) (Proxy b) (Foo (a :: k) (b :: k)))
+                             (b :: k). (~>) (Proxy a) ((~>) (Proxy b) (Foo a b))
+    data MkFooSym0 :: (~>) (Proxy a) ((~>) (Proxy b) (Foo a b))
       where
         MkFooSym0KindInference :: SameKind (Apply MkFooSym0 arg) (MkFooSym1 arg) =>
                                   MkFooSym0 a0123456789876543210
@@ -85,8 +76,8 @@ Singletons/T353.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings MkFooSym0 where
       suppressUnusedWarnings = snd ((,) MkFooSym0KindInference ())
     type MkFooSym1 :: forall k k (a :: k) (b :: k). Proxy a
-                                                    -> (~>) (Proxy b) (Foo (a :: k) (b :: k))
-    data MkFooSym1 (a0123456789876543210 :: Proxy a) :: (~>) (Proxy b) (Foo (a :: k) (b :: k))
+                                                    -> (~>) (Proxy b) (Foo a b)
+    data MkFooSym1 (a0123456789876543210 :: Proxy a) :: (~>) (Proxy b) (Foo a b)
       where
         MkFooSym1KindInference :: SameKind (Apply (MkFooSym1 a0123456789876543210) arg) (MkFooSym2 a0123456789876543210 arg) =>
                                   MkFooSym1 a0123456789876543210 a0123456789876543210
@@ -94,6 +85,6 @@ Singletons/T353.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings (MkFooSym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) MkFooSym1KindInference ())
     type MkFooSym2 :: forall k k (a :: k) (b :: k). Proxy a
-                                                    -> Proxy b -> Foo (a :: k) (b :: k)
-    type family MkFooSym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo (a :: k) (b :: k) where
+                                                    -> Proxy b -> Foo a b
+    type family MkFooSym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo a b where
       MkFooSym2 a0123456789876543210 a0123456789876543210 = 'MkFoo a0123456789876543210 a0123456789876543210
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T371.golden b/singletons-base/tests/compile-and-dump/Singletons/T371.golden
index deb6c788..c0799cf9 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T371.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T371.golden
@@ -13,33 +13,33 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
     data Y (a :: Type)
       = Y1 | Y2 (X a)
       deriving Show
-    type X1Sym0 :: forall (a :: Type). X (a :: Type)
-    type family X1Sym0 :: X (a :: Type) where
+    type X1Sym0 :: forall (a :: Type). X a
+    type family X1Sym0 :: X a where
       X1Sym0 = X1
-    type X2Sym0 :: forall (a :: Type). (~>) (Y a) (X (a :: Type))
-    data X2Sym0 :: (~>) (Y a) (X (a :: Type))
+    type X2Sym0 :: forall (a :: Type). (~>) (Y a) (X a)
+    data X2Sym0 :: (~>) (Y a) (X a)
       where
         X2Sym0KindInference :: SameKind (Apply X2Sym0 arg) (X2Sym1 arg) =>
                                X2Sym0 a0123456789876543210
     type instance Apply X2Sym0 a0123456789876543210 = X2 a0123456789876543210
     instance SuppressUnusedWarnings X2Sym0 where
       suppressUnusedWarnings = snd ((,) X2Sym0KindInference ())
-    type X2Sym1 :: forall (a :: Type). Y a -> X (a :: Type)
-    type family X2Sym1 (a0123456789876543210 :: Y a) :: X (a :: Type) where
+    type X2Sym1 :: forall (a :: Type). Y a -> X a
+    type family X2Sym1 (a0123456789876543210 :: Y a) :: X a where
       X2Sym1 a0123456789876543210 = X2 a0123456789876543210
-    type Y1Sym0 :: forall (a :: Type). Y (a :: Type)
-    type family Y1Sym0 :: Y (a :: Type) where
+    type Y1Sym0 :: forall (a :: Type). Y a
+    type family Y1Sym0 :: Y a where
       Y1Sym0 = Y1
-    type Y2Sym0 :: forall (a :: Type). (~>) (X a) (Y (a :: Type))
-    data Y2Sym0 :: (~>) (X a) (Y (a :: Type))
+    type Y2Sym0 :: forall (a :: Type). (~>) (X a) (Y a)
+    data Y2Sym0 :: (~>) (X a) (Y a)
       where
         Y2Sym0KindInference :: SameKind (Apply Y2Sym0 arg) (Y2Sym1 arg) =>
                                Y2Sym0 a0123456789876543210
     type instance Apply Y2Sym0 a0123456789876543210 = Y2 a0123456789876543210
     instance SuppressUnusedWarnings Y2Sym0 where
       suppressUnusedWarnings = snd ((,) Y2Sym0KindInference ())
-    type Y2Sym1 :: forall (a :: Type). X a -> Y (a :: Type)
-    type family Y2Sym1 (a0123456789876543210 :: X a) :: Y (a :: Type) where
+    type Y2Sym1 :: forall (a :: Type). X a -> Y a
+    type family Y2Sym1 (a0123456789876543210 :: X a) :: Y a where
       Y2Sym1 a0123456789876543210 = Y2 a0123456789876543210
     type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
                                           -> X a -> GHC.Types.Symbol -> GHC.Types.Symbol
@@ -123,9 +123,8 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
       type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
     data SX :: forall (a :: Type). X a -> Type
       where
-        SX1 :: forall (a :: Type). SX (X1 :: X (a :: Type))
-        SX2 :: forall (a :: Type) (n :: Y a).
-               (Sing n) -> SX (X2 n :: X (a :: Type))
+        SX1 :: forall (a :: Type). SX (X1 :: X a)
+        SX2 :: forall (a :: Type) (n :: Y a). (Sing n) -> SX (X2 n :: X a)
     type instance Sing @(X a) = SX
     instance SingKind a => SingKind (X a) where
       type Demote (X a) = X (Demote a)
@@ -136,9 +135,8 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
         = case toSing b :: SomeSing (Y a) of SomeSing c -> SomeSing (SX2 c)
     data SY :: forall (a :: Type). Y a -> Type
       where
-        SY1 :: forall (a :: Type). SY (Y1 :: Y (a :: Type))
-        SY2 :: forall (a :: Type) (n :: X a).
-               (Sing n) -> SY (Y2 n :: Y (a :: Type))
+        SY1 :: forall (a :: Type). SY (Y1 :: Y a)
+        SY2 :: forall (a :: Type) (n :: X a). (Sing n) -> SY (Y2 n :: Y a)
     type instance Sing @(Y a) = SY
     instance SingKind a => SingKind (Y a) where
       type Demote (Y a) = Y (Demote a)
@@ -235,7 +233,7 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
       sing = SX2 sing
     instance SingI1 X2 where
       liftSing = SX2
-    instance SingI (X2Sym0 :: (~>) (Y a) (X (a :: Type))) where
+    instance SingI (X2Sym0 :: (~>) (Y a) (X a)) where
       sing = singFun1 @X2Sym0 SX2
     instance SingI Y1 where
       sing = SY1
@@ -243,5 +241,5 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
       sing = SY2 sing
     instance SingI1 Y2 where
       liftSing = SY2
-    instance SingI (Y2Sym0 :: (~>) (X a) (Y (a :: Type))) where
+    instance SingI (Y2Sym0 :: (~>) (X a) (Y a)) where
       sing = singFun1 @Y2Sym0 SY2
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T412.golden b/singletons-base/tests/compile-and-dump/Singletons/T412.golden
index ac718d4c..a82f6e43 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden
@@ -288,8 +288,8 @@ Singletons/T412.hs:0:0:: Splicing declarations
       T2bSym2 a0123456789876543210 a0123456789876543210 = T2b a0123456789876543210 a0123456789876543210
     infixl 5 `T2bSym2`
     type MkD2Sym0 :: forall (a :: Type)
-                            (b :: Type). (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))
-    data MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))
+                            (b :: Type). (~>) a ((~>) b (D2 a b))
+    data MkD2Sym0 :: (~>) a ((~>) b (D2 a b))
       where
         MkD2Sym0KindInference :: SameKind (Apply MkD2Sym0 arg) (MkD2Sym1 arg) =>
                                  MkD2Sym0 a0123456789876543210
@@ -298,8 +298,8 @@ Singletons/T412.hs:0:0:: Splicing declarations
       suppressUnusedWarnings = snd ((,) MkD2Sym0KindInference ())
     infixr 5 `MkD2Sym0`
     type MkD2Sym1 :: forall (a :: Type) (b :: Type). a
-                                                     -> (~>) b (D2 (a :: Type) (b :: Type))
-    data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 (a :: Type) (b :: Type))
+                                                     -> (~>) b (D2 a b)
+    data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 a b)
       where
         MkD2Sym1KindInference :: SameKind (Apply (MkD2Sym1 a0123456789876543210) arg) (MkD2Sym2 a0123456789876543210 arg) =>
                                  MkD2Sym1 a0123456789876543210 a0123456789876543210
@@ -307,70 +307,57 @@ Singletons/T412.hs:0:0:: Splicing declarations
     instance SuppressUnusedWarnings (MkD2Sym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) MkD2Sym1KindInference ())
     infixr 5 `MkD2Sym1`
-    type MkD2Sym2 :: forall (a :: Type) (b :: Type). a
-                                                     -> b -> D2 (a :: Type) (b :: Type)
-    type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 (a :: Type) (b :: Type) where
+    type MkD2Sym2 :: forall (a :: Type) (b :: Type). a -> b -> D2 a b
+    type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 a b where
       MkD2Sym2 a0123456789876543210 a0123456789876543210 = 'MkD2 a0123456789876543210 a0123456789876543210
     infixr 5 `MkD2Sym2`
     infixr 5 `D2A`
     infixr 5 `D2B`
-    type D2BSym0 :: forall (a :: Type)
-                           (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) b
-    data D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) b
+    type D2BSym0 :: forall (a :: Type) (b :: Type). (~>) (D2 a b) b
+    data D2BSym0 :: (~>) (D2 a b) b
       where
         D2BSym0KindInference :: SameKind (Apply D2BSym0 arg) (D2BSym1 arg) =>
                                 D2BSym0 a0123456789876543210
     type instance Apply D2BSym0 a0123456789876543210 = D2B a0123456789876543210
     instance SuppressUnusedWarnings D2BSym0 where
       suppressUnusedWarnings = snd ((,) D2BSym0KindInference ())
-    type D2BSym1 :: forall (a :: Type)
-                           (b :: Type). D2 (a :: Type) (b :: Type) -> b
-    type family D2BSym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: b where
+    type D2BSym1 :: forall (a :: Type) (b :: Type). D2 a b -> b
+    type family D2BSym1 (a0123456789876543210 :: D2 a b) :: b where
       D2BSym1 a0123456789876543210 = D2B a0123456789876543210
-    type D2ASym0 :: forall (a :: Type)
-                           (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) a
-    data D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) a
+    type D2ASym0 :: forall (a :: Type) (b :: Type). (~>) (D2 a b) a
+    data D2ASym0 :: (~>) (D2 a b) a
       where
         D2ASym0KindInference :: SameKind (Apply D2ASym0 arg) (D2ASym1 arg) =>
                                 D2ASym0 a0123456789876543210
     type instance Apply D2ASym0 a0123456789876543210 = D2A a0123456789876543210
     instance SuppressUnusedWarnings D2ASym0 where
       suppressUnusedWarnings = snd ((,) D2ASym0KindInference ())
-    type D2ASym1 :: forall (a :: Type)
-                           (b :: Type). D2 (a :: Type) (b :: Type) -> a
-    type family D2ASym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: a where
+    type D2ASym1 :: forall (a :: Type) (b :: Type). D2 a b -> a
+    type family D2ASym1 (a0123456789876543210 :: D2 a b) :: a where
       D2ASym1 a0123456789876543210 = D2A a0123456789876543210
-    type D2B :: forall (a :: Type)
-                       (b :: Type). D2 (a :: Type) (b :: Type) -> b
-    type family D2B (a :: D2 (a :: Type) (b :: Type)) :: b where
-      D2B @a @b ('MkD2 _ field :: D2 (a :: Type) (b :: Type)) = field
-    type D2A :: forall (a :: Type)
-                       (b :: Type). D2 (a :: Type) (b :: Type) -> a
-    type family D2A (a :: D2 (a :: Type) (b :: Type)) :: a where
-      D2A @a @b ('MkD2 field _ :: D2 (a :: Type) (b :: Type)) = field
+    type D2B :: forall (a :: Type) (b :: Type). D2 a b -> b
+    type family D2B (a :: D2 a b) :: b where
+      D2B @a @b ('MkD2 _ field :: D2 a b) = field
+    type D2A :: forall (a :: Type) (b :: Type). D2 a b -> a
+    type family D2A (a :: D2 a b) :: a where
+      D2A @a @b ('MkD2 field _ :: D2 a b) = field
     sD2B ::
-      forall (a :: Type)
-             (b :: Type)
-             (t :: D2 (a :: Type) (b :: Type)). Sing t
-                                                -> Sing (Apply D2BSym0 t :: b)
+      forall (a :: Type) (b :: Type) (t :: D2 a b). Sing t
+                                                    -> Sing (Apply D2BSym0 t :: b)
     sD2A ::
-      forall (a :: Type)
-             (b :: Type)
-             (t :: D2 (a :: Type) (b :: Type)). Sing t
-                                                -> Sing (Apply D2ASym0 t :: a)
+      forall (a :: Type) (b :: Type) (t :: D2 a b). Sing t
+                                                    -> Sing (Apply D2ASym0 t :: a)
     sD2B (SMkD2 _ (sField :: Sing field)) = sField
     sD2A (SMkD2 (sField :: Sing field) _) = sField
-    instance SingI (D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) b) where
+    instance SingI (D2BSym0 :: (~>) (D2 a b) b) where
       sing = singFun1 @D2BSym0 sD2B
-    instance SingI (D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) a) where
+    instance SingI (D2ASym0 :: (~>) (D2 a b) a) where
       sing = singFun1 @D2ASym0 sD2A
     type SD2 :: forall (a :: Type) (b :: Type). D2 a b -> Type
     data SD2 :: forall (a :: Type) (b :: Type). D2 a b -> Type
       where
         SMkD2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b).
-                 (Sing n) ->
-                 (Sing n) ->
-                 SD2 ('MkD2 n n :: D2 (a :: Type) (b :: Type))
+                 (Sing n) -> (Sing n) -> SD2 ('MkD2 n n :: D2 a b)
     type instance Sing @(D2 a b) = SD2
     instance (SingKind a, SingKind b) => SingKind (D2 a b) where
       type Demote (D2 a b) = D2 (Demote a) (Demote b)
@@ -388,12 +375,11 @@ Singletons/T412.hs:0:0:: Splicing declarations
       liftSing = SMkD2 sing
     instance SingI2 'MkD2 where
       liftSing2 = SMkD2
-    instance SingI (MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))) where
+    instance SingI (MkD2Sym0 :: (~>) a ((~>) b (D2 a b))) where
       sing = singFun2 @MkD2Sym0 SMkD2
     instance SingI d =>
-             SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 (a :: Type) (b :: Type))) where
+             SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 a b)) where
       sing = singFun1 @(MkD2Sym1 (d :: a)) (SMkD2 (sing @d))
-    instance SingI1 (MkD2Sym1 :: a
-                                 -> (~>) b (D2 (a :: Type) (b :: Type))) where
+    instance SingI1 (MkD2Sym1 :: a -> (~>) b (D2 a b)) where
       liftSing (s :: Sing (d :: a))
         = singFun1 @(MkD2Sym1 (d :: a)) (SMkD2 s)
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T450.golden b/singletons-base/tests/compile-and-dump/Singletons/T450.golden
index 60182b9f..2d6296c4 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T450.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T450.golden
@@ -118,8 +118,8 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations
       liftSing (s :: Sing (d :: PMessage))
         = singFun1 @(AppendMessageSym1 (d :: PMessage)) (sAppendMessage s)
     type PMkFunctionSym0 :: forall (a :: Type)
-                                   (b :: Type). (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type))
-    data PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type))
+                                   (b :: Type). (~>) ((~>) a b) (PFunction a b)
+    data PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction a b)
       where
         PMkFunctionSym0KindInference :: SameKind (Apply PMkFunctionSym0 arg) (PMkFunctionSym1 arg) =>
                                         PMkFunctionSym0 a0123456789876543210
@@ -127,8 +127,8 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations
     instance SuppressUnusedWarnings PMkFunctionSym0 where
       suppressUnusedWarnings = snd ((,) PMkFunctionSym0KindInference ())
     type PMkFunctionSym1 :: forall (a :: Type) (b :: Type). (~>) a b
-                                                            -> PFunction (a :: Type) (b :: Type)
-    type family PMkFunctionSym1 (a0123456789876543210 :: (~>) a b) :: PFunction (a :: Type) (b :: Type) where
+                                                            -> PFunction a b
+    type family PMkFunctionSym1 (a0123456789876543210 :: (~>) a b) :: PFunction a b where
       PMkFunctionSym1 a0123456789876543210 = 'PMkFunction a0123456789876543210
     type SFunction :: forall (a :: Type) (b :: Type). PFunction a b
                                                       -> Type
@@ -136,8 +136,7 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations
                       PFunction a b -> Type
       where
         SMkFunction :: forall (a :: Type) (b :: Type) (n :: (~>) a b).
-                       (Sing n) ->
-                       SFunction ('PMkFunction n :: PFunction (a :: Type) (b :: Type))
+                       (Sing n) -> SFunction ('PMkFunction n :: PFunction a b)
     type instance Sing @(PFunction a b) = SFunction
     instance (SingKind a, SingKind b) => SingKind (PFunction a b) where
       type Demote (PFunction a b) = Function (Demote a) (Demote b)
@@ -149,7 +148,7 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations
       sing = SMkFunction sing
     instance SingI1 'PMkFunction where
       liftSing = SMkFunction
-    instance SingI (PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type))) where
+    instance SingI (PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction a b)) where
       sing = singFun1 @PMkFunctionSym0 SMkFunction
     composeFunction :: Function b c -> Function a b -> Function a c
     composeFunction
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T567.golden b/singletons-base/tests/compile-and-dump/Singletons/T567.golden
index 02f91f57..6e2fca69 100644
--- a/singletons-base/tests/compile-and-dump/Singletons/T567.golden
+++ b/singletons-base/tests/compile-and-dump/Singletons/T567.golden
@@ -22,16 +22,14 @@ Singletons/T567.hs:(0,0)-(0,0): Splicing declarations
     type MkD1Sym0 :: forall x p. D1 x p
     type family MkD1Sym0 :: D1 x p where
       MkD1Sym0 = MkD1
-    type MkD2Sym0 :: forall j (x :: j) p. D2 (x :: j) p
-    type family MkD2Sym0 :: D2 (x :: j) p where
+    type MkD2Sym0 :: forall j (x :: j) p. D2 x p
+    type family MkD2Sym0 :: D2 x p where
       MkD2Sym0 = MkD2
-    type MkD3Sym0 :: forall x (p :: Proxy x). D3 x (p :: Proxy x)
-    type family MkD3Sym0 :: D3 x (p :: Proxy x) where
+    type MkD3Sym0 :: forall x (p :: Proxy x). D3 x p
+    type family MkD3Sym0 :: D3 x p where
       MkD3Sym0 = MkD3
-    type MkD4Sym0 :: forall j
-                            (x :: j)
-                            (p :: Proxy x). D4 (x :: j) (p :: Proxy x)
-    type family MkD4Sym0 :: D4 (x :: j) (p :: Proxy x) where
+    type MkD4Sym0 :: forall j (x :: j) (p :: Proxy x). D4 x p
+    type family MkD4Sym0 :: D4 x p where
       MkD4Sym0 = MkD4
     type SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type
     data SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type
@@ -39,18 +37,16 @@ Singletons/T567.hs:(0,0)-(0,0): Splicing declarations
     type instance Sing @(D1 x p) = SD1
     type SD2 :: forall j (x :: j) (p :: Proxy x). D2 x p -> Type
     data SD2 :: forall j (x :: j) (p :: Proxy x). D2 x p -> Type
-      where SMkD2 :: forall j (x :: j) p. SD2 (MkD2 :: D2 (x :: j) p)
+      where SMkD2 :: forall j (x :: j) p. SD2 (MkD2 :: D2 x p)
     type instance Sing @(D2 x p) = SD2
     type SD3 :: forall k (x :: k) (p :: Proxy x). D3 x p -> Type
     data SD3 :: forall k (x :: k) (p :: Proxy x). D3 x p -> Type
-      where
-        SMkD3 :: forall x (p :: Proxy x). SD3 (MkD3 :: D3 x (p :: Proxy x))
+      where SMkD3 :: forall x (p :: Proxy x). SD3 (MkD3 :: D3 x p)
     type instance Sing @(D3 x p) = SD3
     type SD4 :: forall j (x :: j) (p :: Proxy x). D4 x p -> Type
     data SD4 :: forall j (x :: j) (p :: Proxy x). D4 x p -> Type
       where
-        SMkD4 :: forall j (x :: j) (p :: Proxy x).
-                 SD4 (MkD4 :: D4 (x :: j) (p :: Proxy x))
+        SMkD4 :: forall j (x :: j) (p :: Proxy x). SD4 (MkD4 :: D4 x p)
     type instance Sing @(D4 x p) = SD4
     instance SingI MkD1 where
       sing = SMkD1
diff --git a/singletons-th/singletons-th.cabal b/singletons-th/singletons-th.cabal
index fbfc87d3..93dab2ba 100644
--- a/singletons-th/singletons-th.cabal
+++ b/singletons-th/singletons-th.cabal
@@ -59,7 +59,7 @@ library
                       singletons       == 3.0.*,
                       syb              >= 0.4,
                       template-haskell >= 2.20 && < 2.21,
-                      th-desugar       >= 1.15 && < 1.16,
+                      th-desugar       >= 1.16 && < 1.17,
                       th-orphans       >= 0.13.11 && < 0.14,
                       transformers     >= 0.5.2
   default-language:   GHC2021
diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs
index 69d454f2..5627ada6 100644
--- a/singletons-th/src/Data/Singletons/TH/Promote.hs
+++ b/singletons-th/src/Data/Singletons/TH/Promote.hs
@@ -1087,6 +1087,8 @@ promoteExp (DSigE exp ty) = do
   ty' <- promoteType ty
   return (DSigT exp' ty', ADSigE exp' ann_exp ty')
 promoteExp e@(DStaticE _) = fail ("Static expressions cannot be promoted: " ++ show e)
+promoteExp e@(DTypedBracketE _) = fail ("Typed bracket expressions cannot be promoted: " ++ show e)
+promoteExp e@(DTypedSpliceE _) = fail ("Typed splice expressions cannot be promoted: " ++ show e)
 
 promoteLitExp :: OptionsMonad q => Lit -> q DType
 promoteLitExp (IntegerL n) = do
diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs
index e69fae8f..b7cf9994 100644
--- a/singletons-th/src/Data/Singletons/TH/Single.hs
+++ b/singletons-th/src/Data/Singletons/TH/Single.hs
@@ -994,6 +994,8 @@ isException (DCaseE e _)          = isException e
 isException (DLetE _ e)           = isException e
 isException (DSigE e _)           = isException e
 isException (DStaticE e)          = isException e
+isException (DTypedBracketE e)    = isException e
+isException (DTypedSpliceE e)     = isException e
 
 singMatch :: ADMatch -> SgM DMatch
 singMatch (ADMatch var_proms pat exp) = do