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.

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
@@ -73,7 +73,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 ())
@@ -85,15 +85,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]
@@ -104,15 +104,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

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

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 ((,) (::+@#@$$###) ())

singletons-base/tests/compile-and-dump/Promote/Newtypes.golden

@@ -14,7 +14,7 @@ Promote/Newtypes.hs:(0,0)-(0,0): Splicing declarations
       where
         FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
                                 FooSym0 a0123456789876543210
-    type instance Apply FooSym0 a0123456789876543210 = Foo a0123456789876543210
+    type instance Apply @Nat @Foo FooSym0 a0123456789876543210 = Foo a0123456789876543210
     instance SuppressUnusedWarnings FooSym0 where
       suppressUnusedWarnings = snd ((,) FooSym0KindInference ())
     type FooSym1 :: Nat -> Foo
@@ -25,7 +25,7 @@ Promote/Newtypes.hs:(0,0)-(0,0): Splicing declarations
       where
         BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
                                 BarSym0 a0123456789876543210
-    type instance Apply BarSym0 a0123456789876543210 = Bar a0123456789876543210
+    type instance Apply @Nat @Bar BarSym0 a0123456789876543210 = Bar a0123456789876543210
     instance SuppressUnusedWarnings BarSym0 where
       suppressUnusedWarnings = snd ((,) BarSym0KindInference ())
     type BarSym1 :: Nat -> Bar
@@ -36,7 +36,7 @@ Promote/Newtypes.hs:(0,0)-(0,0): Splicing declarations
       where
         UnBarSym0KindInference :: SameKind (Apply UnBarSym0 arg) (UnBarSym1 arg) =>
                                   UnBarSym0 a0123456789876543210
-    type instance Apply UnBarSym0 a0123456789876543210 = UnBar a0123456789876543210
+    type instance Apply @Bar @Nat UnBarSym0 a0123456789876543210 = UnBar a0123456789876543210
     instance SuppressUnusedWarnings UnBarSym0 where
       suppressUnusedWarnings = snd ((,) UnBarSym0KindInference ())
     type UnBarSym1 :: Bar -> Nat
@@ -53,7 +53,7 @@ Promote/Newtypes.hs:(0,0)-(0,0): Splicing declarations
       where
         TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
                                                          TFHelper_0123456789876543210Sym0 a0123456789876543210
-    type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
+    type instance Apply @Foo @((~>) Foo Bool) TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
     instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
       suppressUnusedWarnings
         = snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
@@ -62,7 +62,7 @@ Promote/Newtypes.hs:(0,0)-(0,0): Splicing declarations
       where
         TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                          TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
-    type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply @Foo @Bool (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
       suppressUnusedWarnings
         = snd ((,) TFHelper_0123456789876543210Sym1KindInference ())

singletons-base/tests/compile-and-dump/Promote/Prelude.golden

@@ -9,7 +9,7 @@ Promote/Prelude.hs:(0,0)-(0,0): Splicing declarations
       where
         OddSym0KindInference :: SameKind (Apply OddSym0 arg) (OddSym1 arg) =>
                                 OddSym0 a0123456789876543210
-    type instance Apply OddSym0 a0123456789876543210 = Odd a0123456789876543210
+    type instance Apply @Natural @Bool OddSym0 a0123456789876543210 = Odd a0123456789876543210
     instance SuppressUnusedWarnings OddSym0 where
       suppressUnusedWarnings = snd ((,) OddSym0KindInference ())
     type OddSym1 :: Natural -> Bool

singletons-base/tests/compile-and-dump/Promote/T180.golden

@@ -13,7 +13,7 @@ Promote/T180.hs:(0,0)-(0,0): Splicing declarations
       where
         X1Sym0KindInference :: SameKind (Apply X1Sym0 arg) (X1Sym1 arg) =>
                                X1Sym0 a0123456789876543210
-    type instance Apply X1Sym0 a0123456789876543210 = X1 a0123456789876543210
+    type instance Apply @Symbol @X X1Sym0 a0123456789876543210 = X1 a0123456789876543210
     instance SuppressUnusedWarnings X1Sym0 where
       suppressUnusedWarnings = snd ((,) X1Sym0KindInference ())
     type X1Sym1 :: Symbol -> X
@@ -24,7 +24,7 @@ Promote/T180.hs:(0,0)-(0,0): Splicing declarations
       where
         X2Sym0KindInference :: SameKind (Apply X2Sym0 arg) (X2Sym1 arg) =>
                                X2Sym0 a0123456789876543210
-    type instance Apply X2Sym0 a0123456789876543210 = X2 a0123456789876543210
+    type instance Apply @Symbol @X X2Sym0 a0123456789876543210 = X2 a0123456789876543210
     instance SuppressUnusedWarnings X2Sym0 where
       suppressUnusedWarnings = snd ((,) X2Sym0KindInference ())
     type X2Sym1 :: Symbol -> X
@@ -34,7 +34,7 @@ Promote/T180.hs:(0,0)-(0,0): Splicing declarations
       where
         ZSym0KindInference :: SameKind (Apply ZSym0 arg) (ZSym1 arg) =>
                               ZSym0 a0123456789876543210
-    type instance Apply ZSym0 a0123456789876543210 = Z a0123456789876543210
+    type instance Apply @_ @_ ZSym0 a0123456789876543210 = Z a0123456789876543210
     instance SuppressUnusedWarnings ZSym0 where
       suppressUnusedWarnings = snd ((,) ZSym0KindInference ())
     type family ZSym1 a0123456789876543210 where
@@ -44,7 +44,7 @@ Promote/T180.hs:(0,0)-(0,0): Splicing declarations
       where
         YSym0KindInference :: SameKind (Apply YSym0 arg) (YSym1 arg) =>
                               YSym0 a0123456789876543210
-    type instance Apply YSym0 a0123456789876543210 = Y a0123456789876543210
+    type instance Apply @X @Symbol YSym0 a0123456789876543210 = Y a0123456789876543210
     instance SuppressUnusedWarnings YSym0 where
       suppressUnusedWarnings = snd ((,) YSym0KindInference ())
     type YSym1 :: X -> Symbol