Give asum, msum, and Product instances explicit kind signatures

This adds more explicit `Type -> Type` kind signatures to definitions that
would otherwise be kind-generalized to have overly polymorphic kinds:

* The kinds of `Asum` and `Msum` (the promoted counterparts to the term-level
  `asum` and `msum` functions, respectively).
* The helper type families generated when promoting the `Alternative` and
  `MonadPlus` instances for `Data.Functor.Product`. This sort of kind
  polymorphism isn't observable by users in today's GHC, but it will cause
  problems later in a future version of GHC that implements
  [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515). (See #601.)

(I should have added these as part of #606 or #607, but I forgot them due to an
oversight.)

singletons-base/CHANGES.md

@@ -55,6 +55,20 @@ next [????.??.??]
   `PAlternative` instances for `Compose`. The fact that these instances were so
   polymorphic to begin with was an oversight, as these instances could not be
   used when `k` was instantiated to any other kind besides `Type`.
+* The kinds of `Asum` and `Msum` are less polymorphic than they were before:
+
+  ```diff
+  -type Asum :: forall {j} {k} (t :: k    -> Type) (f :: j    -> k)    (a :: j).    t (f a) -> f a
+  +type Asum :: forall         (t :: Type -> Type) (f :: Type -> Type) (a :: Type). t (f a) -> f a
+
+  -type Msum :: forall {j} {k} (t :: k    -> Type) (m :: j    -> k)    (a :: j).    t (m a) -> m a
+  +type Msum :: forall         (t :: Type -> Type) (m :: Type -> Type) (a :: Type). t (m a) -> m a
+  ```
+
+  Similarly, the kinds of defunctionalization symbols for these definitions
+  (e.g., `AsumSym0` and `MSym0`) are less polymorphic. The fact that these were
+  kind-polymorphic to begin with was an oversight, as these definitions could
+  not be used when `j` or `k` was instantiated to any other kind besides `Type`.
 
 3.4 [2024.05.12]
 ----------------

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

@@ -581,16 +581,37 @@ $(singletonsOnly [d|
   sequence_ :: (Foldable t, Monad m) => t (m a) -> m ()
   sequence_ = foldr (>>) (return ())
 
+  -- Note that in the type signatures for `asum` and `msum` below, we explicitly
+  -- annotate `f` and `m` with the kind (Type -> Type), which is not something
+  -- that is done in the original base library. This is because when
+  -- singletons-th promotes type signatures, it omits constraints such as
+  -- `Alternative f` and `MonadPlus m`, which are essential for inferring that
+  -- `f` and `m` are of kind `Type -> Type`. Without these constraints, we may
+  -- end up with a promoted definition that looks like this:
+  --
+  --   type Asum :: t (f a) -> f a
+  --
+  -- This will result in Asum having a more polymorphic kind than intended,
+  -- since GHC will generalize Asum's kind to:
+  --
+  --   type Asum :: forall {j} {k} (t :: k -> Type) (f :: j -> k) (a :: j). t (f a) -> f a
+  --
+  -- Annotating `f :: Type -> Type` (and similarly for `m`) is a clunky but
+  -- reliable way of preventing this. See also Note [Using standalone kind
+  -- signatures not present in the base library] in
+  -- Control.Monad.Singletons.Internal for a similar situation where class
+  -- definitions can become overly polymorphic unless given an explicit kind.
+
   -- -| The sum of a collection of actions, generalizing 'concat'.
   --
   -- asum [Just "Hello", Nothing, Just "World"]
   -- Just "Hello"
-  asum :: (Foldable t, Alternative f) => t (f a) -> f a
+  asum :: forall t (f :: Type -> Type) a. (Foldable t, Alternative f) => t (f a) -> f a
   asum = foldr (<|>) empty
 
   -- -| The sum of a collection of actions, generalizing 'concat'.
   -- As of base 4.8.0.0, 'msum' is just 'asum', specialized to 'MonadPlus'.
-  msum :: (Foldable t, MonadPlus m) => t (m a) -> m a
+  msum :: forall t (m :: Type -> Type) a. (Foldable t, MonadPlus m) => t (m a) -> m a
   msum = asum
 
   -- -| The concatenation of all the elements of a container of lists.

singletons-base/src/Data/Functor/Product/Singletons.hs

@@ -102,20 +102,44 @@ $(singletonsOnly [d|
       Pair f g <*> Pair x y = Pair (f <*> x) (g <*> y)
       liftA2 f (Pair a b) (Pair x y) = Pair (liftA2 f a x) (liftA2 f b y)
 
-  instance (Alternative f, Alternative g) => Alternative (Product f g) where
-      empty = Pair empty empty
-      Pair x1 y1 <|> Pair x2 y2 = Pair (x1 <|> x2) (y1 <|> y2)
-
   instance (Monad f, Monad g) => Monad (Product f g) where
       Pair m n >>= f = Pair (m >>= fstP . f) (n >>= sndP . f)
         where
           fstP (Pair a _) = a
           sndP (Pair _ b) = b
 
-  instance (MonadPlus f, MonadPlus g) => MonadPlus (Product f g) where
-      mzero = Pair mzero mzero
-      Pair x1 y1 `mplus` Pair x2 y2 = Pair (x1 `mplus` x2) (y1 `mplus` y2)
-
   instance (MonadZip f, MonadZip g) => MonadZip (Product f g) where
       mzipWith f (Pair x1 y1) (Pair x2 y2) = Pair (mzipWith f x1 x2) (mzipWith f y1 y2)
+
+  -- Note that in the instances below, we explicitly annotate `f` with its kind
+  -- (Type -> Type), which is not something that is done in the original base
+  -- library. This is because when singletons-th promotes instance declarations,
+  -- it omits the instance contexts when generating the helper type families.
+  -- This can lead to the helper type families having overly polymorphic kinds.
+  -- For example, if the Alternative instance below lacked the explicit
+  -- (f :: Type -> Type) kind signature, the generated code would look like:
+  --
+  --   instance PAlternative (Product f g) where
+  --     type Empty = EmptyHelper
+  --     ...
+  --
+  --   type EmptyHelper :: forall f g a. Product f g a
+  --
+  -- This will result in EmptyHelper having a more polymorphic kind than
+  -- intended, since GHC will generalize EmptyHelper's kind to:
+  --
+  --   type EmptyHelper :: forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k). Product f g a
+  --
+  -- Annotating `f :: Type -> Type` is a clunky but reliable way of preventing
+  -- this. See also Note [Using standalone kind signatures not present in the
+  -- base library] in Control.Monad.Singletons.Internal for a similar situation
+  -- where class definitions can become overly polymorphic unless given an
+  -- explicit kind.
+  instance (Alternative f, Alternative g) => Alternative (Product (f :: Type -> Type) g) where
+      empty = Pair empty empty
+      Pair x1 y1 <|> Pair x2 y2 = Pair (x1 <|> x2) (y1 <|> y2)
+
+  instance (MonadPlus f, MonadPlus g) => MonadPlus (Product (f :: Type -> Type) g) where
+      mzero = Pair mzero mzero
+      Pair x1 y1 `mplus` Pair x2 y2 = Pair (x1 `mplus` x2) (y1 `mplus` y2)
   |])