Generate Apply instances with explicit kind arguments

After the changes in [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515) are implemented, some `Apply` instances will fail to compile due to their left-hand sides being kind-generalized to something that is more polymorphic than what their right-hand sides will allow. For example, this commonly occurs when generating `Apply` instances for lambda-lifted definitions or declarations whose kinds use visible dependent quantification. We avoid this issue by now generating `Apply` instances with explicit kind arguments (via `TypeApplications`), leveraging the fact that we know what the kinds are (most of the time) during defunctionalization. See the new section of `Note [Defunctionalization game plan], Wrinkle 2: Non-vanilla kinds` for the full details. Resolves the "Defunctionalizing declarations using visible dependent quantification" section of #601.
goldfirere · Jun 3, 2024 · ceb48a1 · ceb48a1
1 parent 7e5c92d
commit ceb48a1
Show file tree

Hide file tree

Showing 110 changed files with 987 additions and 934 deletions.
diff --git a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden
diff --git a/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden b/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden
@@ -10,7 +10,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       where
         SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                  SuccSym0 a0123456789876543210
-    type instance Apply SuccSym0 a0123456789876543210 = Succ a0123456789876543210
+    type instance Apply @Nat @Nat SuccSym0 a0123456789876543210 = Succ a0123456789876543210
     instance SuppressUnusedWarnings SuccSym0 where
       suppressUnusedWarnings = snd ((,) SuccSym0KindInference ())
     type SuccSym1 :: Nat -> Nat
@@ -65,7 +65,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       where
         Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
                                                                                 Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
-    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210
+    type instance Apply @_ @_ Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210
     instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
       suppressUnusedWarnings
         = snd
@@ -76,7 +76,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       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
+    type instance Apply @_ @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) h0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210
     instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) where
       suppressUnusedWarnings
         = snd
@@ -87,7 +87,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       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
+    type instance Apply @_ @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
     instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) where
       suppressUnusedWarnings
         = snd
@@ -106,7 +106,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       where
         InsertionSortSym0KindInference :: SameKind (Apply InsertionSortSym0 arg) (InsertionSortSym1 arg) =>
                                           InsertionSortSym0 a0123456789876543210
-    type instance Apply InsertionSortSym0 a0123456789876543210 = InsertionSort a0123456789876543210
+    type instance Apply @[Nat] @[Nat] InsertionSortSym0 a0123456789876543210 = InsertionSort a0123456789876543210
     instance SuppressUnusedWarnings InsertionSortSym0 where
       suppressUnusedWarnings
         = snd ((,) InsertionSortSym0KindInference ())
@@ -118,15 +118,15 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       where
         InsertSym0KindInference :: SameKind (Apply InsertSym0 arg) (InsertSym1 arg) =>
                                    InsertSym0 a0123456789876543210
-    type instance Apply InsertSym0 a0123456789876543210 = InsertSym1 a0123456789876543210
+    type instance Apply @Nat @((~>) [Nat] [Nat]) InsertSym0 a0123456789876543210 = InsertSym1 a0123456789876543210
     instance SuppressUnusedWarnings InsertSym0 where
       suppressUnusedWarnings = snd ((,) InsertSym0KindInference ())
     type InsertSym1 :: Nat -> (~>) [Nat] [Nat]
     data InsertSym1 (a0123456789876543210 :: Nat) :: (~>) [Nat] [Nat]
       where
         InsertSym1KindInference :: SameKind (Apply (InsertSym1 a0123456789876543210) arg) (InsertSym2 a0123456789876543210 arg) =>
                                    InsertSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (InsertSym1 a0123456789876543210) a0123456789876543210 = Insert a0123456789876543210 a0123456789876543210
+    type instance Apply @[Nat] @[Nat] (InsertSym1 a0123456789876543210) a0123456789876543210 = Insert a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (InsertSym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) InsertSym1KindInference ())
     type InsertSym2 :: Nat -> [Nat] -> [Nat]
@@ -137,15 +137,15 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
       where
         LeqSym0KindInference :: SameKind (Apply LeqSym0 arg) (LeqSym1 arg) =>
                                 LeqSym0 a0123456789876543210
-    type instance Apply LeqSym0 a0123456789876543210 = LeqSym1 a0123456789876543210
+    type instance Apply @Nat @((~>) Nat Bool) LeqSym0 a0123456789876543210 = LeqSym1 a0123456789876543210
     instance SuppressUnusedWarnings LeqSym0 where
       suppressUnusedWarnings = snd ((,) LeqSym0KindInference ())
     type LeqSym1 :: Nat -> (~>) Nat Bool
     data LeqSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool
       where
         LeqSym1KindInference :: SameKind (Apply (LeqSym1 a0123456789876543210) arg) (LeqSym2 a0123456789876543210 arg) =>
                                 LeqSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (LeqSym1 a0123456789876543210) a0123456789876543210 = Leq a0123456789876543210 a0123456789876543210
+    type instance Apply @Nat @Bool (LeqSym1 a0123456789876543210) a0123456789876543210 = Leq a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (LeqSym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) LeqSym1KindInference ())
     type LeqSym2 :: Nat -> Nat -> Bool

diff --git a/singletons-base/tests/compile-and-dump/Promote/Constructors.golden b/singletons-base/tests/compile-and-dump/Promote/Constructors.golden
@@ -13,15 +13,15 @@ Promote/Constructors.hs:(0,0)-(0,0): Splicing declarations
       where
         (::+@#@$###) :: SameKind (Apply (:+@#@$) arg) ((:+@#@$$) arg) =>
                         (:+@#@$) a0123456789876543210
-    type instance Apply (:+@#@$) a0123456789876543210 = (:+@#@$$) a0123456789876543210
+    type instance Apply @Foo @((~>) Foo Foo) (:+@#@$) a0123456789876543210 = (:+@#@$$) a0123456789876543210
     instance SuppressUnusedWarnings (:+@#@$) where
       suppressUnusedWarnings = snd ((,) (::+@#@$###) ())
     type (:+@#@$$) :: Foo -> (~>) Foo Foo
     data (:+@#@$$) (a0123456789876543210 :: Foo) :: (~>) Foo Foo
       where
         (::+@#@$$###) :: SameKind (Apply ((:+@#@$$) a0123456789876543210) arg) ((:+@#@$$$) a0123456789876543210 arg) =>
                          (:+@#@$$) a0123456789876543210 a0123456789876543210
-    type instance Apply ((:+@#@$$) a0123456789876543210) a0123456789876543210 = (:+) a0123456789876543210 a0123456789876543210
+    type instance Apply @Foo @Foo ((:+@#@$$) a0123456789876543210) a0123456789876543210 = (:+) a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings ((:+@#@$$) a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) (::+@#@$$###) ())
     type (:+@#@$$$) :: Foo -> Foo -> Foo
@@ -32,7 +32,7 @@ Promote/Constructors.hs:(0,0)-(0,0): Splicing declarations
       where
         BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
                                 BarSym0 a0123456789876543210
-    type instance Apply BarSym0 a0123456789876543210 = BarSym1 a0123456789876543210
+    type instance Apply @Bar @((~>) Bar ((~>) Bar ((~>) Bar ((~>) Foo Bar)))) BarSym0 a0123456789876543210 = BarSym1 a0123456789876543210
     instance SuppressUnusedWarnings BarSym0 where
       suppressUnusedWarnings = snd ((,) BarSym0KindInference ())
     type BarSym1 :: Bar
@@ -41,31 +41,31 @@ Promote/Constructors.hs:(0,0)-(0,0): Splicing declarations
       where
         BarSym1KindInference :: SameKind (Apply (BarSym1 a0123456789876543210) arg) (BarSym2 a0123456789876543210 arg) =>
                                 BarSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (BarSym1 a0123456789876543210) a0123456789876543210 = BarSym2 a0123456789876543210 a0123456789876543210
+    type instance Apply @Bar @((~>) Bar ((~>) Bar ((~>) Foo Bar))) (BarSym1 a0123456789876543210) a0123456789876543210 = BarSym2 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (BarSym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) BarSym1KindInference ())
     type BarSym2 :: Bar -> Bar -> (~>) Bar ((~>) Bar ((~>) Foo Bar))
     data BarSym2 (a0123456789876543210 :: Bar) (a0123456789876543210 :: Bar) :: (~>) Bar ((~>) Bar ((~>) Foo Bar))
       where
         BarSym2KindInference :: SameKind (Apply (BarSym2 a0123456789876543210 a0123456789876543210) arg) (BarSym3 a0123456789876543210 a0123456789876543210 arg) =>
                                 BarSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
-    type instance Apply (BarSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = BarSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply @Bar @((~>) Bar ((~>) Foo Bar)) (BarSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = BarSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (BarSym2 a0123456789876543210 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) BarSym2KindInference ())
     type BarSym3 :: Bar -> Bar -> Bar -> (~>) Bar ((~>) Foo Bar)
     data BarSym3 (a0123456789876543210 :: Bar) (a0123456789876543210 :: Bar) (a0123456789876543210 :: Bar) :: (~>) Bar ((~>) Foo Bar)
       where
         BarSym3KindInference :: SameKind (Apply (BarSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) =>
                                 BarSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
-    type instance Apply (BarSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply @Bar @((~>) Foo Bar) (BarSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (BarSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) BarSym3KindInference ())
     type BarSym4 :: Bar -> Bar -> Bar -> Bar -> (~>) Foo Bar
     data BarSym4 (a0123456789876543210 :: Bar) (a0123456789876543210 :: Bar) (a0123456789876543210 :: Bar) (a0123456789876543210 :: Bar) :: (~>) Foo Bar
       where
         BarSym4KindInference :: SameKind (Apply (BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210) arg) (BarSym5 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 arg) =>
                                 BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
-    type instance Apply (BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply @Foo @Bar (BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210) a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (BarSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) BarSym4KindInference ())
     type BarSym5 :: Bar -> Bar -> Bar -> Bar -> Foo -> Bar

diff --git a/singletons-base/tests/compile-and-dump/Promote/GenDefunSymbols.golden b/singletons-base/tests/compile-and-dump/Promote/GenDefunSymbols.golden
@@ -7,7 +7,7 @@ Promote/GenDefunSymbols.hs:0:0:: Splicing declarations
       where
         LiftMaybeSym0KindInference :: Data.Singletons.SameKind (Apply LiftMaybeSym0 arg) (LiftMaybeSym1 arg) =>
                                       LiftMaybeSym0 a0123456789876543210
-    type instance Apply LiftMaybeSym0 a0123456789876543210 = LiftMaybeSym1 a0123456789876543210
+    type instance Apply @((~>) a b) @((~>) (Maybe a) (Maybe b)) LiftMaybeSym0 a0123456789876543210 = LiftMaybeSym1 a0123456789876543210
     instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings LiftMaybeSym0 where
       Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
         = snd ((,) LiftMaybeSym0KindInference ())
@@ -17,7 +17,7 @@ Promote/GenDefunSymbols.hs:0:0:: Splicing declarations
       where
         LiftMaybeSym1KindInference :: Data.Singletons.SameKind (Apply (LiftMaybeSym1 a0123456789876543210) arg) (LiftMaybeSym2 a0123456789876543210 arg) =>
                                       LiftMaybeSym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (LiftMaybeSym1 a0123456789876543210) a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
+    type instance Apply @(Maybe a) @(Maybe b) (LiftMaybeSym1 a0123456789876543210) a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210
     instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings (LiftMaybeSym1 a0123456789876543210) where
       Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
         = snd ((,) LiftMaybeSym1KindInference ())
@@ -33,7 +33,7 @@ Promote/GenDefunSymbols.hs:0:0:: Splicing declarations
       where
         SuccSym0KindInference :: Data.Singletons.SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                  SuccSym0 a0123456789876543210
-    type instance Apply SuccSym0 a0123456789876543210 = 'Succ a0123456789876543210
+    type instance Apply @NatT @NatT SuccSym0 a0123456789876543210 = 'Succ a0123456789876543210
     instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings SuccSym0 where
       Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
         = snd ((,) SuccSym0KindInference ())
@@ -45,7 +45,7 @@ Promote/GenDefunSymbols.hs:0:0:: Splicing declarations
       where
         (::+@#@$###) :: Data.Singletons.SameKind (Apply (:+@#@$) arg) ((:+@#@$$) arg) =>
                         (:+@#@$) a0123456789876543210
-    type instance Apply (:+@#@$) a0123456789876543210 = (:+@#@$$) a0123456789876543210
+    type instance Apply @Natural @((~>) Natural Natural) (:+@#@$) a0123456789876543210 = (:+@#@$$) a0123456789876543210
     instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings (:+@#@$) where
       Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
         = snd ((,) (::+@#@$###) ())
@@ -54,7 +54,7 @@ Promote/GenDefunSymbols.hs:0:0:: Splicing declarations
       where
         (::+@#@$$###) :: Data.Singletons.SameKind (Apply ((:+@#@$$) a0123456789876543210) arg) ((:+@#@$$$) a0123456789876543210 arg) =>
                          (:+@#@$$) a0123456789876543210 a0123456789876543210
-    type instance Apply ((:+@#@$$) a0123456789876543210) a0123456789876543210 = (:+) a0123456789876543210 a0123456789876543210
+    type instance Apply @Natural @Natural ((:+@#@$$) a0123456789876543210) a0123456789876543210 = (:+) a0123456789876543210 a0123456789876543210
     instance Data.Singletons.TH.SuppressUnusedWarnings.SuppressUnusedWarnings ((:+@#@$$) a0123456789876543210) where
       Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings
         = snd ((,) (::+@#@$$###) ())