Partially revert TypeAbstractions-related changes in #596

The changes in #596 cause `singletons-th` to use `TypeAbstractions` to
explicitly quantify the kind variables of promoted class methods whenever the
parent class has a standalone kind signature, thereby ensuring that the order
of kind variables matches the order in which the user wrote them. At least,
that was the intention. Unfortunately, as #605 reveals, this approach sometimes
causes `singletons-th` to generate ill-kinded code for promoted class methods,
and there isn't an obvious way to work around this limitation.

As such, this patch reverts the `TypeAbstractions`-related changes from #596.
Once again, `singletons-th` now does not make any guarantees about the order of
kind variables for promoted class methods or their defunctionalization symbols.

On the other hand, this patch _does_ keep the changes from #596 that cause
`singletons-th` to propagate kind information from the parent class's
standalone kind signature through to the promoted class methods'
defunctionalization symbols, as this feature is useful independent of the
`TypeAbstractions`-related changes. I have taken the opportunity to document
why we do this in the new `Note [Propagating kind information from class
standalone kind signatures]` in `D.S.TH.Promote`.

I've removed the `T589` test case, as the functionality it was testing no
longer exists after reverting the `TypeAbstractions`-related changes. I have
also added a new `T605` test case that ensures that the regression from #605
stays fixed. In a subsequent commit, I will add another test case that
demonstrates that the kind propagation works as intended.

Fixes #605.

README.md

@@ -1179,72 +1179,34 @@ for the following constructs:
   yourself!
 
 * Kind signatures of promoted class methods.
-  The order of type variables is only guaranteed to be preserved if the parent
-  class has a standalone kind signature. For example, given this class:
+  The order of type variables will often "just work" by happy coincidence, but
+  there are some situations where this does not happen. Consider the following
+  class:
 
   ```haskell
-  type C :: Type -> Constraint
-  class C b where
+  class C (b :: Type) where
     m :: forall a. a -> b -> a
   ```
 
   The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds
-  `b` before `a`. Because `C` has a standalone kind signature, the order of
-  type variables is preserved when promoting and singling `m`:
-
-  ```hs
-  type PC :: Type -> Constraint
-  class PC b where
-    type M @b @a (x :: a) (y :: b) :: a
-
-  type MSym0 :: forall b a. a ~> b ~> a
-  type MSym1 :: forall b a. a -> b ~> a
-
-  type SC :: Type -> Constraint
-  class SC b where
-    sM :: forall a (x :: a) (y :: b).
-          Sing x -> Sing y -> Sing (M x y)
-  ```
-
-  Note that `M`, `M`'s defunctionalization symbols, and `sM` all quantify `b`
-  before `a` in their types. The key to making this work is by using the
-  `TypeAbstractions` language extension in declaration for `M`, which is only
-  possible due to `PC` having a standalone kind signature.
-
-  If the parent class does _not_ have a standalone kind signature, then
-  `singletons-th` does not make any guarantees about the order of kind
-  variables in the promoted methods' kinds. The order will often "just work" by
-  happy coincidence, but there are some situations where this does not happen.
-  Consider the following variant of the class example above:
+  `b` before `a`. This order is preserved when singling `m`, but *not* when
+  promoting `m`. This is because the `C` class is promoted as follows:
 
   ```haskell
-  -- No standalone kind signature
-  class C b where
-    m :: forall a. a -> b -> a
-  ```
-
-  Again, the full type of `m` is `forall b. C b => forall a. a -> b -> a`,
-  which binds `b` before `a`. This order is preserved when singling `m`, but
-  *not* when promoting `m`. This is because the `C` class is promoted as
-  follows:
-
-  ```haskell
-  -- No standalone kind signature
-  class PC b where
+  class PC (b :: Type) where
     type M (x :: a) (y :: b) :: a
   ```
 
-  This time, `PC` does not have a standalone kind signature, so we cannot use
-  `TypeAbstractions` in the declaration for `M`. As such, GHC will quantify the
-  kind variables in left-to-right order, so the kind of `M` will be inferred to
-  be `forall a b. a -> b -> a`, which binds `b` *after* `a`. The
-  defunctionalization symbols for `M` will also follow a similar order of type
-  variables:
+  Due to the way GHC kind-checks associated type families, the kind of `M` is
+  `forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the
+  `StandaloneKindSignatures` extension does not provide a way to explicitly
+  declare the full kind of an associated type family, so this limitation is
+  not easy to work around.
 
-  ```haskell
-  type MSym0 :: forall a b. a ~> b ~> a
-  type MSym1 :: forall a b. a -> b ~> a
-  ```
+  As a result, one should not depend on the order of kind variables for promoted
+  class methods like `M`. The order of kind variables in defunctionalization
+  symbols for promoted class methods (e.g. `MSym0` and `MSym1`) is similarly
+  unspecified.
 
 ### Wildcard types
 

singletons-base/tests/SingletonsBaseTestSuite.hs

@@ -156,7 +156,6 @@ tests =
     , compileAndDumpStdTest "T582"
     , compileAndDumpStdTest "T585"
     , compileAndDumpStdTest "TypeAbstractions"
-    , compileAndDumpStdTest "T589"
     ],
     testCompileAndDumpGroup "Promote"
     [ compileAndDumpStdTest "Constructors"
@@ -167,6 +166,7 @@ tests =
     , compileAndDumpStdTest "Prelude"
     , compileAndDumpStdTest "T180"
     , compileAndDumpStdTest "T361"
+    , compileAndDumpStdTest "T605"
     ],
     testGroup "Database client"
     [ compileAndDumpTest "GradingClient/Database" ghcOpts

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

@@ -0,0 +1,39 @@
+Promote/T605.hs:(0,0)-(0,0): Splicing declarations
+    promoteOnly
+      [d| type Traversable' :: (Type -> Type) -> Constraint
+
+          class (Functor t, Foldable t) => Traversable' t where
+            traverse' :: Applicative f => (a -> f b) -> t a -> t (f b) |]
+  ======>
+    type Traverse'Sym0 :: forall (t :: Type -> Type)
+                                 a
+                                 f
+                                 b. (~>) ((~>) a (f b)) ((~>) (t a) (t (f b)))
+    data Traverse'Sym0 :: (~>) ((~>) a (f b)) ((~>) (t a) (t (f b)))
+      where
+        Traverse'Sym0KindInference :: SameKind (Apply Traverse'Sym0 arg) (Traverse'Sym1 arg) =>
+                                      Traverse'Sym0 a0123456789876543210
+    type instance Apply Traverse'Sym0 a0123456789876543210 = Traverse'Sym1 a0123456789876543210
+    instance SuppressUnusedWarnings Traverse'Sym0 where
+      suppressUnusedWarnings = snd ((,) Traverse'Sym0KindInference ())
+    type Traverse'Sym1 :: forall (t :: Type -> Type)
+                                 a
+                                 f
+                                 b. (~>) a (f b) -> (~>) (t a) (t (f b))
+    data Traverse'Sym1 (a0123456789876543210 :: (~>) a (f b)) :: (~>) (t a) (t (f b))
+      where
+        Traverse'Sym1KindInference :: SameKind (Apply (Traverse'Sym1 a0123456789876543210) arg) (Traverse'Sym2 a0123456789876543210 arg) =>
+                                      Traverse'Sym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (Traverse'Sym1 a0123456789876543210) a0123456789876543210 = Traverse' a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (Traverse'Sym1 a0123456789876543210) where
+      suppressUnusedWarnings = snd ((,) Traverse'Sym1KindInference ())
+    type Traverse'Sym2 :: forall (t :: Type -> Type)
+                                 a
+                                 f
+                                 b. (~>) a (f b) -> t a -> t (f b)
+    type family Traverse'Sym2 @(t :: Type
+                                     -> Type) @a @f @b (a0123456789876543210 :: (~>) a (f b)) (a0123456789876543210 :: t a) :: t (f b) where
+      Traverse'Sym2 a0123456789876543210 a0123456789876543210 = Traverse' a0123456789876543210 a0123456789876543210
+    type PTraversable' :: (Type -> Type) -> Constraint
+    class PTraversable' t where
+      type family Traverse' (arg :: (~>) a (f b)) (arg :: t a) :: t (f b)

singletons-base/tests/compile-and-dump/Promote/T605.hs

@@ -0,0 +1,11 @@
+module T605 where
+
+import Data.Kind
+import Data.Singletons.Base.TH
+import Prelude.Singletons
+
+$(promoteOnly [d|
+  type Traversable' :: (Type -> Type) -> Constraint
+  class (Functor t, Foldable t) => Traversable' t where
+    traverse' :: Applicative f => (a -> f b) -> t a -> t (f b)
+  |])

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

@@ -25,7 +25,7 @@ Singletons/T326.hs:0:0:: Splicing declarations
     infixl 9 <%>@#@$$$
     type PC1 :: Type -> Constraint
     class PC1 (a :: Type) where
-      type family (<%>) @(a :: Type) (arg :: a) (arg :: a) :: a
+      type family (<%>) (arg :: a) (arg :: a) :: a
     infixl 9 <%>
 Singletons/T326.hs:0:0:: Splicing declarations
     genSingletons [''C2]
@@ -54,7 +54,7 @@ Singletons/T326.hs:0:0:: Splicing declarations
     infixl 9 <%%>@#@$$$
     type PC2 :: Type -> Constraint
     class PC2 (a :: Type) where
-      type family (<%%>) @(a :: Type) (arg :: a) (arg :: a) :: a
+      type family (<%%>) (arg :: a) (arg :: a) :: a
     infixl 9 <%%>
     class SC2 (a :: Type) where
       (%<%%>) ::

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

@@ -74,7 +74,7 @@ Singletons/T378b.hs:(0,0)-(0,0): Splicing declarations
     type family F @b @a (a :: a) (a :: b) :: () where
       F @b @a (_ :: a) (_ :: b) = Tuple0Sym0
     type PC :: forall b a. a -> b -> Constraint
-    class PC @b @a (x :: a) (y :: b)
+    class PC x y
     sNatMinus ::
       (forall (t :: Nat) (t :: Nat).
        Sing t

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

@@ -225,7 +225,7 @@ Singletons/T412.hs:0:0:: Splicing declarations
     infix 6 `M2Sym2`
     type PC2 :: Type -> Type -> Constraint
     class PC2 (a :: Type) (b :: Type) where
-      type family M2 @(a :: Type) @(b :: Type) (arg :: a) (arg :: b) :: Bool
+      type family M2 (arg :: a) (arg :: b) :: Bool
     infix 5 `PC2`
     infix 6 `M2`
     class SC2 (a :: Type) (b :: Type) where

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

@@ -70,7 +70,7 @@ Singletons/T414.hs:(0,0)-(0,0): Splicing declarations
     type family T3Sym2 (a0123456789876543210 :: Bool) (a0123456789876543210 :: Type) :: Type where
       T3Sym2 a0123456789876543210 a0123456789876543210 = T3 a0123456789876543210 a0123456789876543210
     type PC3 :: Bool -> Constraint
-    class PC3 (a :: Bool)
+    class PC3 a
     class SC1 (a :: Bool)
     class SC2 a
     class SC3 a