From 5f0d4204e327767cbd8c32ef16d7ac8479e65ece Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 16 Jun 2024 11:35:55 -0400 Subject: [PATCH] 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 | 20 +++++++++++++ .../src/Control/Monad/Fail/Singletons.hs | 5 ++++ .../src/Control/Monad/Singletons/Internal.hs | 29 +++++++++++++++++++ .../src/Control/Monad/Zip/Singletons.hs | 5 ++++ .../src/Data/Foldable/Singletons.hs | 3 ++ .../src/Data/Traversable/Singletons.hs | 4 +++ 6 files changed, 66 insertions(+) diff --git a/singletons-base/CHANGES.md b/singletons-base/CHANGES.md index d250f0a0..691111f3 100644 --- a/singletons-base/CHANGES.md +++ b/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] ---------------- diff --git a/singletons-base/src/Control/Monad/Fail/Singletons.hs b/singletons-base/src/Control/Monad/Fail/Singletons.hs index f2b99b03..6a3c1899 100644 --- a/singletons-base/src/Control/Monad/Fail/Singletons.hs +++ b/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 diff --git a/singletons-base/src/Control/Monad/Singletons/Internal.hs b/singletons-base/src/Control/Monad/Singletons/Internal.hs index 67508006..dd4f0dd3 100644 --- a/singletons-base/src/Control/Monad/Singletons/Internal.hs +++ b/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. +-} diff --git a/singletons-base/src/Control/Monad/Zip/Singletons.hs b/singletons-base/src/Control/Monad/Zip/Singletons.hs index c60f53f8..21e7b809 100644 --- a/singletons-base/src/Control/Monad/Zip/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Foldable/Singletons.hs b/singletons-base/src/Data/Foldable/Singletons.hs index 9b56db26..05c665bc 100644 --- a/singletons-base/src/Data/Foldable/Singletons.hs +++ b/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 #-} diff --git a/singletons-base/src/Data/Traversable/Singletons.hs b/singletons-base/src/Data/Traversable/Singletons.hs index 49e829f7..6109600b 100644 --- a/singletons-base/src/Data/Traversable/Singletons.hs +++ b/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 #-}