diff --git a/singletons-base/CHANGES.md b/singletons-base/CHANGES.md index dca071eb..d3a96c95 100644 --- a/singletons-base/CHANGES.md +++ b/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] ---------------- diff --git a/singletons-base/src/Data/Foldable/Singletons.hs b/singletons-base/src/Data/Foldable/Singletons.hs index eb59ba6c..ced3236f 100644 --- a/singletons-base/src/Data/Foldable/Singletons.hs +++ b/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. diff --git a/singletons-base/src/Data/Functor/Product/Singletons.hs b/singletons-base/src/Data/Functor/Product/Singletons.hs index caf33a2b..8c056070 100644 --- a/singletons-base/src/Data/Functor/Product/Singletons.hs +++ b/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) |])