Adapt to DLamCasesE in th-desugar-1.18

.github/workflows/haskell-ci.yml

@@ -215,7 +215,7 @@ jobs:
           source-repository-package
             type:     git
             location: https://github.com/goldfirere/th-desugar
-            tag:      ae6c075edb50175a99b35f0bdcf475b695a5ee78
+            tag:      1d17abf8add216424790f10bbb3e4c33d2d736f5
           EOF
           $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: any.$_ installed\n" unless /^(Cabal|Cabal-syntax|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: ae6c075edb50175a99b35f0bdcf475b695a5ee78
+  tag: 1d17abf8add216424790f10bbb3e4c33d2d736f5

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,13 +62,19 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
     insertionSort :: [Nat] -> [Nat]
     insertionSort [] = []
     insertionSort (h : t) = insert h (insertionSort t)
-    type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
-      Let0123456789876543210Scrutinee_0123456789876543210Sym0 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)
+    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 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
+      where
+        LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) arg) (LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 arg) =>
+                                                         LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
+    type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
+    instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) where
+      suppressUnusedWarnings
+        = snd ((,) LamCases_0123456789876543210Sym0KindInference ())
+    type family LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 where
+      LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
     type InsertionSortSym0 :: (~>) [Nat] [Nat]
     data InsertionSortSym0 :: (~>) [Nat] [Nat]
       where
@@ -125,7 +132,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_0123456789876543210Sym0 n h t)
+      Insert n ('(:) h t) = 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
@@ -148,23 +155,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_0123456789876543210 n h t)
-          sScrutinee_0123456789876543210
-            = applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH
-        in
-          id
-            @(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym0 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
+             @(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

@@ -286,13 +286,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

@@ -164,7 +164,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)
@@ -185,10 +186,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 = SFoo1
       sMaxBound = SFoo1

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

@@ -46,7 +46,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