Kind-indexed Category instance for Kleisli

Kleisli_Category.hs

-- https://www.reddit.com/r/haskell/comments/abxem5/experimenting_with_kleisli_instance_of/

{-# Language TypeApplications     #-}
{-# Language RankNTypes           #-}
{-# Language DataKinds            #-}
{-# Language KindSignatures       #-}
{-# Language PolyKinds            #-}
{-# Language TypeOperators        #-}
{-# Language GADTs                #-}
{-# Language TypeFamilies         #-}
{-# Language TypeSynonymInstances #-}
{-# Language FlexibleInstances    #-}
{-# Language InstanceSigs         #-}

import Data.Kind
import Prelude hiding (id, (<), (>))
import Control.Monad

type Obj = Type

-- Kleisli
newtype KleisliKind :: (Type -> Type) -> Obj where
  Kl :: Type -> KleisliKind m

type family
 UnKl (kl :: KleisliKind m) :: Type where
 UnKl (Kl a) = a

class    kl ~ Kl (UnKl kl) => UnKl_ (kl :: KleisliKind m)
instance kl ~ Kl (UnKl kl) => UnKl_ (kl :: KleisliKind m)

-- Kleisli :: forall m -> Cat (KleisliKind m)
data Kleisli m :: Cat (KleisliKind m) where
  MkKleisli :: (a -> m b) -> Kleisli m (Kl a) (Kl b)

-- Category
type Cat (ob :: Obj) = ob -> ob -> Obj

class    Empty a
instance Empty a

class Category (ob :: Obj) where
 type (-->)  :: Cat ob
 type Object :: ob -> Constraint
 type Object = Empty

 id :: Object (a :: ob)
    => (a --> a)

 (>) :: (a --> b)
     -> (b --> c)
     -> (a --> (c :: ob))

instance Category (Type :: Obj) where
 type (-->) = (->)

 id :: a -> a
 id a = a

 (>) :: (a -> b) -> (b -> c) -> (a -> c)
 (one > two) a = two (one a)

instance Monad m => Category (KleisliKind m :: Obj) where
 -- type (-->) @(KleisliKind m) = Kleisli m
 type (-->) = (Kleisli m :: Cat (KleisliKind m))

 type Object = UnKl_

 id :: forall a. Kleisli m (Kl a) (Kl a)
 id = MkKleisli pure

 (>) :: Kleisli m kl_a kl_b
     -> Kleisli m kl_b kl_c
     -> Kleisli m kl_a kl_c
 MkKleisli one > MkKleisli two = MkKleisli (one >=> two)