Nat as a type-level category, to be used as the index of a category-indexed monad

CatMonadCounter.hs

-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971

{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE TypeApplications, TypeOperators, GADTs #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Kind
import GHC.TypeLits

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

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

data Edge (x :: ()) (y :: ()) where
    E :: Nat -> Edge '() '()

type family EPlus (n :: Edge x y) (m :: Edge y z) :: Edge x z where
    EPlus (E n) (E m) = E (n + m)

newtype Counter (i :: ()) (j :: ()) (q :: Edge i j) a = Counter { runCounter :: a }

instance CatMonad Counter where
    type Id Counter = E 0
    type Cat Counter f g = EPlus f g

    xpure = Counter
    xbind act k = Counter $ runCounter $ k $ runCounter act

tick :: Counter '() '() (E 1) ()
tick = Counter ()

-- > :t hello
-- hello :: Counter '() '() ('E 3) Integer
hello = do
    tick
    tick
    x <- pure 4
    tick
    y <- pure 5
    pure $ x + y
  where
    pure = xpure @_ @_ @Counter
    (>>=) = xbind @_ @_ @Counter

    return = pure
    m >> n = m >>= \_ -> n