Draft: Adapt to DLamCasesE in th-desugar-1.18

This patch bumps the pinned `th-desugar` commit to bring in the changes from
TODO RGS, which replace `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!

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/src/Data/List/NonEmpty/Singletons.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoNamedWildCards #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeFamilies #-}

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