Monads indexed by categories (updated version after discussion at https://stackoverflow.com/questions/57040321/type-level-monoid-like-operations-for-generalizing-indexed-monads/57046042?noredirect=1#comment100643986_57046042)

CatMonad.hs

{-# LANGUAGE GADTs, FunctionalDependencies, FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}

module CatMonad where

import Control.Category as C
import Data.Kind

class CatMonad (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) | c -> m where
  type Id c :: c x x
  type Cat c (f :: c x y) (g :: c y z) :: c x z

  xpure :: a -> m (Id c) a

  xbind :: m f a -> (a -> m g b) -> m (Cat c f g) b

data Edge (cat :: k -> k -> Type) (x :: k) (y :: k) = E

-- newtype IWriter (cat :: k -> k -> Type) (i :: k) (j :: k) (q :: Edge cat i j) (a :: Type)
--   = IWriter { runWriter :: (a, cat i j) }

newtype IWriter (cat :: k -> k -> Type) :: forall (i :: k) (j :: k). Edge cat i j -> Type -> Type where
  IWriter :: { runWriter :: (a, cat i j) } -> IWriter cat (e :: Edge cat i j) a

instance Category cat => CatMonad (Edge cat) (IWriter cat) where
  type Id  (Edge cat) = E
  type Cat (Edge cat) _ _ = E

  xpure a = IWriter (a, C.id)
  xbind (IWriter (a, f)) k =
    let IWriter (b, g) = k a in
    IWriter (b, f C.>>> g)

hello :: IWriter (->) (E :: Edge (->) Bool Bool) String
hello = xpure "hello"