Bump th-desugar submodule to version 1.16

This bumps the `th-desugar` submodule to bring in all of the changes in the
upcoming `1.16` release. Aside from bumping version bounds, the only other
changes that had to be made on the `singletons` side are:

* `singletons-th` now has explicit failure cases for typed TH splices.
* Due to goldfirere/th-desugar#194, desugared data constructors now look like
  this:

  ```hs
  DataCon :: forall (a :: Type) (b :: Type). DataType a b
  ```

  Instead of this:

  ```hs
  DataCon :: forall (a :: Type) (b :: Type). DataType (a :: Type) (b :: Type)
  ```

  This causes the expected output for some test cases to change, but they are
  benign changes.

.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

cabal.project

@@ -5,4 +5,4 @@ packages: ./singletons
 source-repository-package
   type: git
   location: https://github.com/goldfirere/th-desugar
-  tag: f7db712e95a125e710cefc7cd819c6480f7e52e3
+  tag: 47f6221088ac6185566066b4d45909b0cc704855

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

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

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)

singletons-base/tests/compile-and-dump/Singletons/T271.golden

@@ -14,17 +14,17 @@ 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
     type instance Apply ConstantSym0 a0123456789876543210 = Constant a0123456789876543210
     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

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)

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)

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,36 +58,33 @@ 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]
   ======>
     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
     type instance Apply MkFooSym0 a0123456789876543210 = MkFooSym1 a0123456789876543210
     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
     type instance Apply (MkFooSym1 a0123456789876543210) a0123456789876543210 = 'MkFoo a0123456789876543210 a0123456789876543210
     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

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,13 +233,13 @@ 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
     instance SingI n => SingI (Y2 (n :: X a)) where
       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