Adapt to DLamCasesE in th-desugar-1.18

This patch bumps the pinned `th-desugar` commit to bring in the changes from
goldfirere/th-desugar#218, which replaces `DLamE` and
`DCaseE` in favor of `DLamCasesE`. Quite happily, this actually _simplifies_
how singling works in `singletons-th`. Previously, we went through great
efforts to annotate promoted `case` expressions with their overall return type,
as described in `Note [Annotate case return type]` and `Note [The id hack; or,
how singletons-th learned to stop worrying and avoid kind generalization]` in
`D.S.TH.Single`. After this patch, however, all `case` expressions are
desugared to `\cases` expressions, and because we already annotate singled
`\cases` expressions (by generating code like `singFun1 @LamCasesSym0 (\cases
...)`), we no longer need to use the tricks describes in those two Notes.
Hooray!

One interesting knock-on effect of these simplifications is that given code
like this:

```hs
map (\x -> ()) xs -- Note that `x` is unused
```

`singletons-th` would previously generate code that looked like this:

```hs
sMap (singFun1 @LamdaSym0 (\sX -> case sX of (_ :: Sing x) -> STuple0)) sXs
```

Unlike the original code, this singled code would compile without warnings.
This is because `sX` is "used" in the sense that it is passed to a `case`
expression. It's a very silly `case` expression, as it doesn't do anything
meaningful with `sX`, but it still technically counts as a use.

Now that `singletons-th` uses a `\cases`-based approach to singling, however,
the singled code will instead look like this:

```hs
sMap (singFun1 @LamCasesSym0 (\cases (sX :: Sing x) -> STuple0)) sXs
```

This time, GHC _does_ recognize that `sX` is unused and emits a warning. This
actually affects the way that `singletons-th` generates code for derived
`Functor` and `Foldable` instances, so I needed to generate wildcard patterns
instead of variable patterns in certain parts of
`D.S.TH.Promote.Deriving.{Functor,Foldable}`. I have also mentioned the
possibility of `singletons-th` generating more warnings in the `CHANGELOG`.

.github/workflows/haskell-ci.yml

@@ -8,9 +8,9 @@
 #
 # For more information, see https://github.com/haskell-CI/haskell-ci
 #
-# version: 0.19.20240512
+# version: 0.19.20240514
 #
-# REGENDATA ("0.19.20240512",["github","cabal.project"])
+# REGENDATA ("0.19.20240514",["github","cabal.project"])
 #
 name: Haskell-CI
 on:
@@ -121,7 +121,7 @@ jobs:
           echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV"
           echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV"
           echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV"
-          if [ $((HCNUMVER >= 91000)) -ne 0 ] ; then echo "HEADHACKAGE=true" >> "$GITHUB_ENV" ; else echo "HEADHACKAGE=false" >> "$GITHUB_ENV" ; fi
+          echo "HEADHACKAGE=false" >> "$GITHUB_ENV"
           echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV"
           echo "GHCJSARITH=0" >> "$GITHUB_ENV"
         env:
@@ -150,17 +150,6 @@ jobs:
           repository hackage.haskell.org
             url: http://hackage.haskell.org/
           EOF
-          if $HEADHACKAGE; then
-          cat >> $CABAL_CONFIG <<EOF
-          repository head.hackage.ghc.haskell.org
-             url: https://ghc.gitlab.haskell.org/head.hackage/
-             secure: True
-             root-keys: 7541f32a4ccca4f97aea3b22f5e593ba2c0267546016b992dfadcd2fe944e55d
-                        26021a13b401500c8eb2761ca95c61f2d625bfef951b939a8124ed12ecf07329
-                        f76d08be13e9a61a377a85e2fb63f4c5435d40f8feb3e12eb05905edb8cdea89
-             key-threshold: 3
-          EOF
-          fi
           cat >> $CABAL_CONFIG <<EOF
           program-default-options
             ghc-options: $GHCJOBS +RTS -M3G -RTS
@@ -226,12 +215,9 @@ jobs:
           source-repository-package
             type:     git
             location: https://github.com/goldfirere/th-desugar
-            tag:      ae6c075edb50175a99b35f0bdcf475b695a5ee78
+            tag:      60124111b9d62097202e8362885d861c4750baf3
           EOF
-          if $HEADHACKAGE; then
-          echo "allow-newer: $($HCPKG list --simple-output | sed -E 's/([a-zA-Z-]+)-[0-9.]+/*:\1,/g')" >> cabal.project
-          fi
-          $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(singletons|singletons-base|singletons-th)$/; }' >> cabal.project.local
+          $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: any.$_ installed\n" unless /^(singletons|singletons-base|singletons-th)$/; }' >> cabal.project.local
           cat cabal.project
           cat cabal.project.local
       - name: dump install plan

cabal.project

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

singletons-base/singletons-base.cabal

@@ -78,7 +78,7 @@ library
                       singletons-th    >= 3.4  && < 3.5,
                       template-haskell >= 2.22 && < 2.23,
                       text >= 1.2,
-                      th-desugar       >= 1.17 && < 1.18
+                      th-desugar       >= 1.18 && < 1.19
   default-language:   GHC2021
   other-extensions:   TemplateHaskell
   exposed-modules:    Data.Singletons.Base.CustomStar

singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden

@@ -27,7 +27,8 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       fromSing (SSucc b) = Succ (fromSing b)
       toSing Zero = SomeSing SZero
       toSing (Succ (b :: Demote Nat))
-        = case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c)
+        = (\cases (SomeSing c) -> SomeSing (SSucc c))
+            (toSing b :: SomeSing Nat)
     instance SingI Zero where
       sing = SZero
     instance SingI n => SingI (Succ (n :: Nat)) where
@@ -61,46 +62,43 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     insertionSort :: [Nat] -> [Nat]
     insertionSort [] = []
     insertionSort (h : t) = insert h (insertionSort t)
-    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
+    type family LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_0123456789876543210 where
+      LamCases_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
+      LamCases_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
+    data LamCases_0123456789876543210Sym0 n0123456789876543210
       where
-        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
-                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
-    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210
-    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
+        LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply LamCases_0123456789876543210Sym0 arg) (LamCases_0123456789876543210Sym1 arg) =>
+                                                         LamCases_0123456789876543210Sym0 n0123456789876543210
+    type instance Apply LamCases_0123456789876543210Sym0 n0123456789876543210 = LamCases_0123456789876543210Sym1 n0123456789876543210
+    instance SuppressUnusedWarnings LamCases_0123456789876543210Sym0 where
       suppressUnusedWarnings
-        = snd
-            ((,)
-               Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
-               ())
-    data Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
+        = snd ((,) LamCases_0123456789876543210Sym0KindInference ())
+    data LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
       where
-        Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 arg) =>
-                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
-    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) h0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210
-    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) where
+        LamCases_0123456789876543210Sym1KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym1 n0123456789876543210) arg) (LamCases_0123456789876543210Sym2 n0123456789876543210 arg) =>
+                                                         LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
+    type instance Apply (LamCases_0123456789876543210Sym1 n0123456789876543210) h0123456789876543210 = LamCases_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210
+    instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym1 n0123456789876543210) where
       suppressUnusedWarnings
-        = snd
-            ((,)
-               Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference
-               ())
-    data Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
+        = snd ((,) LamCases_0123456789876543210Sym1KindInference ())
+    data LamCases_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
       where
-        Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 arg) =>
-                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
-    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
-    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) where
+        LamCases_0123456789876543210Sym2KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) arg) (LamCases_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 arg) =>
+                                                         LamCases_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
+    type instance Apply (LamCases_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) t0123456789876543210 = LamCases_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210
+    instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) where
       suppressUnusedWarnings
-        = snd
-            ((,)
-               Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference
-               ())
-    type family Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
-      Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
-    type family Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
-      Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h
-    type family Case_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 t where
-      Case_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
-      Case_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
+        = snd ((,) LamCases_0123456789876543210Sym2KindInference ())
+    data LamCases_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
+      where
+        LamCases_0123456789876543210Sym3KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210) arg) (LamCases_0123456789876543210Sym4 n0123456789876543210 h0123456789876543210 t0123456789876543210 arg) =>
+                                                         LamCases_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
+    type instance Apply (LamCases_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
+    instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210) where
+      suppressUnusedWarnings
+        = snd ((,) LamCases_0123456789876543210Sym3KindInference ())
+    type family LamCases_0123456789876543210Sym4 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 where
+      LamCases_0123456789876543210Sym4 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
     type InsertionSortSym0 :: (~>) [Nat] [Nat]
     data InsertionSortSym0 :: (~>) [Nat] [Nat]
       where
@@ -158,7 +156,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     type Insert :: Nat -> [Nat] -> [Nat]
     type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
       Insert n '[] = Apply (Apply (:@#@$) n) NilSym0
-      Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
+      Insert n ('(:) h t) = Apply (Apply (Apply (Apply LamCases_0123456789876543210Sym0 n) h) t) (Apply (Apply LeqSym0 n) h)
     type Leq :: Nat -> Nat -> Bool
     type family Leq (a :: Nat) (a :: Nat) :: Bool where
       Leq 'Zero _ = TrueSym0
@@ -183,23 +181,19 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     sInsert (sN :: Sing n) SNil
       = applySing (applySing (singFun2 @(:@#@$) SCons) sN) SNil
     sInsert (sN :: Sing n) (SCons (sH :: Sing h) (sT :: Sing t))
-      = let
-          sScrutinee_0123456789876543210 ::
-            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
-          sScrutinee_0123456789876543210
-            = applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH
-        in
-          id
-            @(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)))
-            (case sScrutinee_0123456789876543210 of
-               STrue
-                 -> applySing
-                      (applySing (singFun2 @(:@#@$) SCons) sN)
-                      (applySing (applySing (singFun2 @(:@#@$) SCons) sH) sT)
-               SFalse
-                 -> applySing
-                      (applySing (singFun2 @(:@#@$) SCons) sH)
-                      (applySing (applySing (singFun2 @InsertSym0 sInsert) sN) sT))
+      = applySing
+          (singFun1
+             @(Apply (Apply (Apply LamCases_0123456789876543210Sym0 n) h) t)
+             (\cases
+                STrue
+                  -> applySing
+                       (applySing (singFun2 @(:@#@$) SCons) sN)
+                       (applySing (applySing (singFun2 @(:@#@$) SCons) sH) sT)
+                SFalse
+                  -> applySing
+                       (applySing (singFun2 @(:@#@$) SCons) sH)
+                       (applySing (applySing (singFun2 @InsertSym0 sInsert) sN) sT)))
+          (applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH)
     sLeq SZero _ = STrue
     sLeq (SSucc _) SZero = SFalse
     sLeq (SSucc (sA :: Sing a)) (SSucc (sB :: Sing b))

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

@@ -368,13 +368,10 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
       type Demote Baz = Baz
       fromSing (SBaz b b b) = Baz (fromSing b) (fromSing b) (fromSing b)
       toSing (Baz (b :: Demote Nat) (b :: Demote Nat) (b :: Demote Nat))
-        = case
-              (,,)
-                (toSing b :: SomeSing Nat) (toSing b :: SomeSing Nat)
-                (toSing b :: SomeSing Nat)
-          of
-            (,,) (SomeSing c) (SomeSing c) (SomeSing c)
-              -> SomeSing (SBaz c c c)
+        = (\cases
+             (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SBaz c c c))
+            (toSing b :: SomeSing Nat) (toSing b :: SomeSing Nat)
+            (toSing b :: SomeSing Nat)
     instance (SingI n, SingI n, SingI n) =>
              SingI (Baz (n :: Nat) (n :: Nat) (n :: Nat)) where
       sing = SBaz sing sing sing

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

@@ -194,7 +194,8 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
       type Demote (Foo3 a) = Foo3 (Demote a)
       fromSing (SFoo3 b) = Foo3 (fromSing b)
       toSing (Foo3 (b :: Demote a))
-        = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SFoo3 c)
+        = (\cases (SomeSing c) -> SomeSing (SFoo3 c))
+            (toSing b :: SomeSing a)
     data SFoo4 :: forall (a :: Type) (b :: Type). Foo4 a b -> Type
       where
         SFoo41 :: forall (a :: Type) (b :: Type). SFoo4 (Foo41 :: Foo4 a b)
@@ -215,10 +216,8 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
       type Demote Pair = Pair
       fromSing (SPair b b) = Pair (fromSing b) (fromSing b)
       toSing (Pair (b :: Demote Bool) (b :: Demote Bool))
-        = case
-              (,) (toSing b :: SomeSing Bool) (toSing b :: SomeSing Bool)
-          of
-            (,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c)
+        = (\cases (SomeSing c) (SomeSing c) -> SomeSing (SPair c c))
+            (toSing b :: SomeSing Bool) (toSing b :: SomeSing Bool)
     instance SBounded Foo1 where
       sMinBound :: Sing (MinBoundSym0 :: Foo1)
       sMaxBound :: Sing (MaxBoundSym0 :: Foo1)

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

@@ -47,7 +47,8 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations
       type Demote (Box a) = Box (Demote a)
       fromSing (SFBox b) = FBox (fromSing b)
       toSing (FBox (b :: Demote a))
-        = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SFBox c)
+        = (\cases (SomeSing c) -> SomeSing (SFBox c))
+            (toSing b :: SomeSing a)
     instance SingI n => SingI (FBox (n :: a)) where
       sing = SFBox sing
     instance SingI1 FBox where