From e328357b99de91443edb50cd77623eae86b93d22 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 18 Jun 2024 07:35:42 -0400 Subject: [PATCH] Give Compose's instances explicit kind signatures Previously, the promoted versions of certain `Compose` instances (`Functor`, `Foldable`, etc.) would be overly general due to the fact that `singletons-th` omits instance contexts during promotion. For example, the promoted `Functor` instance for `Compose` was: ```hs instance PFunctor (Compose (f :: k -> Type) (g :: Type -> k)) where ... ``` But this was too general, as `f` and `g` should both be of kind `Type -> Type` instead. The defunctionalization symbols associated with the instances also had a similar problem. This patch annotates each instance with an explicit kind (e.g., `Functor (Compose (f :: Type -> Type) g)` to ensure that the promoted instances also have the intended kind. This is very much in the same spirit as the situation described in `Note [Using standalone kind signatures not present in the base library]` in `Control.Monad.Singletons.Internal`, but for instance declarations instead of class declarations. Resolves the "Overly polymorphic instance methods" section of #601. --- .../src/Data/Functor/Compose/Singletons.hs | 25 +++++++++++++++---- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/singletons-base/src/Data/Functor/Compose/Singletons.hs b/singletons-base/src/Data/Functor/Compose/Singletons.hs index 056971fc..37884974 100644 --- a/singletons-base/src/Data/Functor/Compose/Singletons.hs +++ b/singletons-base/src/Data/Functor/Compose/Singletons.hs @@ -78,23 +78,38 @@ $(singletonsOnly [d| deriving instance Eq (f (g a)) => Eq (Compose f g a) deriving instance Ord (f (g a)) => Ord (Compose f g a) - instance (Functor f, Functor g) => Functor (Compose f g) where + -- 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. As such, the instance declarations (as well + -- as the associated defunctionalization symbols) would be given overly + -- polymorphic kinds due to kind generalization, e.g., + -- + -- instance PFunctor (Compose (f :: k -> Type) (g :: Type -> k)) where ... + -- + -- 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 (Functor f, Functor g) => Functor (Compose (f :: Type -> Type) g) where fmap f (Compose x) = Compose (fmap (fmap f) x) a <$ (Compose x) = Compose (fmap (a <$) x) - instance (Foldable f, Foldable g) => Foldable (Compose f g) where + instance (Foldable f, Foldable g) => Foldable (Compose (f :: Type -> Type) g) where foldMap f (Compose t) = foldMap (foldMap f) t - instance (Traversable f, Traversable g) => Traversable (Compose f g) where + instance (Traversable f, Traversable g) => Traversable (Compose (f :: Type -> Type) g) where traverse f (Compose t) = Compose <$> traverse (traverse f) t - instance (Applicative f, Applicative g) => Applicative (Compose f g) where + instance (Applicative f, Applicative g) => Applicative (Compose (f :: Type -> Type) g) where pure x = Compose (pure (pure x)) Compose f <*> Compose x = Compose (liftA2 (<*>) f x) liftA2 f (Compose x) (Compose y) = Compose (liftA2 (liftA2 f) x y) - instance (Alternative f, Applicative g) => Alternative (Compose f g) where + instance (Alternative f, Applicative g) => Alternative (Compose (f :: Type -> Type) g) where empty = Compose empty Compose x <|> Compose y = Compose (x <|> y) |])