Give PAlternative (and friends) the correct kinds

Previously, `singletons-th` would generalize the kinds of `PAlternative` and
related classes (e.g., `PMonadPlus`), as well of the kinds of the
defunctionalization symbols for various classes that are parameterized over a
higher-kinded type variable. As described in the "Class constraints" section of
the `README.md`, the recommended workaround for this issue is to give the
classes in question explicit kinds, so this patch does just that by giving
`Alternative`, `MonadPlus`, etc. standalone kind signatures.

This causes the code in `singletons-base` to deviate a bit from the original
code in the `base` library. I have written a new `Note [Using standalone kind
signatures not present in the base library]` and cited it in all of the places
where such a deviation occurs.

Fixes #604.

singletons-base/CHANGES.md

@@ -23,6 +23,26 @@ next [????.??.??]
   now have improve type inference and avoid the need for special casing. If you
   truly need the full polymorphism of the old type signatures, use `error`,
   `errorWithoutStackTrace`, or `undefined` instead.
+* The kinds of `PAlternative` (and other classes in `singletons-base` that are
+  parameterized over a higher-kinded type variable) are less polymorphic than
+  they were before:
+
+  ```diff
+  -type PAlternative :: (k    -> Type) -> Constraint
+  +type PAlternative :: (Type -> Type) -> Constraint
+
+  -type PMonadZip :: (k    -> Type) -> Constraint
+  +type PMonadZip :: (Type -> Type) -> Constraint
+
+  -type PMonadPlus :: (k    -> Type) -> Constraint
+  +type PMonadPlus :: (Type -> Type) -> Constraint
+  ```
+
+  Similarly, the kinds of defunctionalization symbols for these classes (e.g.,
+  `EmptySym0` and `(<|>@#@$)`) now use `Type -> Type` instead of `k -> Type`.
+  The fact that these were kind-polymorphic to begin with was an oversight, as
+  these could not be used when `k` was instantiated to any other kind besides
+  `Type`.
 
 3.4 [2024.05.12]
 ----------------

singletons-base/src/Control/Monad/Fail/Singletons.hs

@@ -25,6 +25,7 @@ module Control.Monad.Fail.Singletons (
   ) where
 
 import Control.Monad.Singletons.Internal
+import Data.Kind
 import Data.Singletons.Base.Instances
 import Data.Singletons.TH
 
@@ -49,6 +50,10 @@ $(singletonsOnly [d|
   -- @
   -- fail _ = mzero
   -- @
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type MonadFail :: (Type -> Type) -> Constraint
   class Monad m => MonadFail m where
       fail :: String -> m a
 

singletons-base/src/Control/Monad/Singletons/Internal.hs

@@ -33,6 +33,7 @@ module Control.Monad.Singletons.Internal where
 
 import Control.Applicative
 import Control.Monad
+import Data.Kind
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Singletons.Base.Instances
 import Data.Singletons.TH
@@ -51,6 +52,8 @@ $(singletonsOnly [d|
   satisfy these laws.
   -}
 
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type   Functor :: (Type -> Type) -> Constraint
   class  Functor f  where
       fmap        :: (a -> b) -> f a -> f b
 
@@ -126,6 +129,8 @@ $(singletonsOnly [d|
   --
   -- (which implies that 'pure' and '<*>' satisfy the applicative functor laws).
 
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type Applicative :: (Type -> Type) -> Constraint
   class Functor f => Applicative f where
       -- {-# MINIMAL pure, ((<*>) | liftA2) #-}
       -- -| Lift a value.
@@ -243,6 +248,9 @@ $(singletonsOnly [d|
   The instances of 'Monad' for lists, 'Data.Maybe.Maybe' and 'System.IO.IO'
   defined in the "Prelude" satisfy these laws.
   -}
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type Monad :: (Type -> Type) -> Constraint
   class Applicative m => Monad m where
       -- -| Sequentially compose two actions, passing any value produced
       -- by the first as an argument to the second.
@@ -352,6 +360,9 @@ $(singletonsOnly [d|
   -- -* @'some' v = (:) '<$>' v '<*>' 'many' v@
   --
   -- -* @'many' v = 'some' v '<|>' 'pure' []@
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type Alternative :: (Type -> Type) -> Constraint
   class Applicative f => Alternative f where
       -- -| The identity of '<|>'
       empty :: f a
@@ -386,6 +397,9 @@ $(singletonsOnly [d|
   -- The MonadPlus class definition
 
   -- -| Monads that also support choice and failure.
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  type MonadPlus :: (Type -> Type) -> Constraint
   class (Alternative m, Monad m) => MonadPlus m where
      -- -| The identity of 'mplus'.  It should also satisfy the equations
      --
@@ -479,3 +493,18 @@ $(singletonsOnly [d|
   instance MonadPlus Maybe
   instance MonadPlus []
   |])
+
+{-
+Note [Using standalone kind signatures not present in the base library]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Various type class definitions in singletons-base (Functor, Foldable,
+Alternative, etc.) are defined using standalone kind signatures. These
+standalone kind signatures are /not/ present in the original `base` library,
+however: these are specifically required by singletons-th. More precisely, all
+of these classes are parameterized by a type variable of kind `Type -> Type`,
+and we want to ensure that the promoted class (and the defunctionalization
+symbols for its class methods) all use `Type -> Type` in their kinds as well.
+For more details on why singletons-th requires this, see Note [Propagating kind
+information from class standalone kind signatures] in D.S.TH.Promote in
+singletons-th.
+-}

singletons-base/src/Control/Monad/Zip/Singletons.hs

@@ -30,6 +30,7 @@ module Control.Monad.Zip.Singletons (
 import Control.Monad.Singletons.Internal
 import Data.Functor.Identity
 import Data.Functor.Identity.Singletons
+import Data.Kind
 import Data.List.Singletons
        ( ZipSym0, ZipWithSym0, UnzipSym0
        , sZip,    sZipWith,    sUnzip )
@@ -56,6 +57,10 @@ $(singletonsOnly [d|
   --   > ==>
   --   > munzip (mzip ma mb) = (ma, mb)
   --
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type MonadZip :: (Type -> Type) -> Constraint
   class Monad m => MonadZip m where
       -- {-# MINIMAL mzip | mzipWith #-}
 

singletons-base/src/Data/Foldable/Singletons.hs

@@ -215,6 +215,9 @@ $(singletonsOnly [d|
   --
   -- > foldMap f . fmap g = foldMap (f . g)
 
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type Foldable :: (Type -> Type) -> Constraint
   class Foldable t where
       -- {-# MINIMAL foldMap | foldr #-}
 

singletons-base/src/Data/Traversable/Singletons.hs

@@ -171,6 +171,10 @@ $(singletonsOnly [d|
   --    equivalent to traversal with a constant applicative functor
   --    ('foldMapDefault').
   --
+
+  -- See Note [Using standalone kind signatures not present in the base library]
+  -- in Control.Monad.Singletons.Internal.
+  type Traversable :: (Type -> Type) -> Constraint
   class (Functor t, Foldable t) => Traversable t where
       -- {-# MINIMAL traverse | sequenceA #-}