How to get superclass Category (Kleisli m) to entail Monad m
Summary
The constraint FunctorOf dom cod f
implies Category dom
and Category cod
. Since Category (Kleisli m)
implies a Monad m
constraint I would like to get a Monad constraint from FunctorOf (Kleisli m) (->) f
.
instance Monad m => Category (Kleisli m)
Steps to reproduce
The following program
{-# Language ConstraintKinds #-}
{-# Language FlexibleInstances #-}
{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language MultiParamTypeClasses #-}
{-# Language RankNTypes #-}
{-# Language TypeOperators #-}
import Control.Arrow
import Control.Category
import Data.Kind
import Data.Maybe
import Prelude hiding (fmap)
-- type FunctorOf :: Cat d -> Cat c -> Object (d->c)
class (Category dom, Category cod) => FunctorOf dom cod f where
fmap :: dom a a' -> cod (f a) (f a')
instance FunctorOf (Kleisli Maybe) (->) [] where
fmap :: Kleisli Maybe a a' -> ([a] -> [a'])
fmap (Kleisli f) = mapMaybe f
-- from Data.Constraint
-- Dict :: Constraint -> Type
data Dict cls where
Dict :: cls => Dict cls
-- (:-) :: Cat Constraint
newtype a :- b where
Sub :: (a => Dict b) -> (a :- b)
-- a functor from `Kleisli m' entails that Kleisli m is a Category.
foo :: FunctorOf (Kleisli m) (->) f :- Category (Kleisli m)
foo = Sub Dict
-- • Could not deduce (Monad m) arising from a use of ‘Dict’
-- from the context: FunctorOf (Kleisli m) (->) f
-- baz :: FunctorOf (Kleisli m) (->) f :- Monad m
-- baz = Sub Dict
Expected behavior
I was hoping the functor constraint in baz
would entail a monad constraint.
Is this Bidirectional Type Class Instances? https://arxiv.org/pdf/1906.12242.pdf, it's possible this shouldn't work at all since Category (Kleisli m)
doesn't carry around a Monad m
dictionary. This is exactly what I need at the moment though!
Environment
- GHC version used: 8.10.0.20191123