Indexed ResourceT monad (repl.it link: https://repl.it/repls/EsteemedDeficientArea)

IndexedResourceT.hs

{-# LANGUAGE KindSignatures 
           , PolyKinds
           , DataKinds
           , TypeFamilies
           , TypeOperators
           , GADTs
#-}

module IxResourceT where

class IxMonad (m :: state -> state -> * -> *) where
  ireturn :: a -> m s s a
  ibind   :: m i o a -> (a -> m o o' b) -> m i o' b
  
data Deallocator m a = Deallocator { runDeallocator :: m () }

data IxResourceT :: (* -> *) -> [*] -> [*] -> * -> * where
  IxResourceT :: m a -> IxResourceT m rsi rso a
  
instance (Monad m) => IxMonad (IxResourceT m) where
  ireturn = IxResourceT .return
  (IxResourceT ma) `ibind` f = IxResourceT $ do
    a <- ma
    let (IxResourceT mb) = f a
    mb
    
lift :: (Monad m) => m a -> IxResourceT m rs rs a
lift = IxResourceT
    
type family Elem (x :: k) (xs :: [k]) :: Bool where
  Elem x '[] = 'False
  Elem x (x ': xs) = 'True
  Elem x (y ': xs) = Elem x xs

type family Remove (x :: k) (xs :: [k]) :: [k] where
  Remove x '[] = '[]
  Remove x (x ': xs) = xs
  Remove x (y ': xs) = Remove x xs
  
allocate :: (Monad m) => (m a, a -> m ()) -> IxResourceT m rs (a ': rs) (a, Deallocator m a)
allocate (allocateResource, deallocateResource) =  IxResourceT $ do
  resource <- allocateResource 
  return (resource, Deallocator (deallocateResource resource))

release :: (Monad m, Elem a rs ~ True) => Deallocator m a -> IxResourceT m rs (Remove a rs) ()
release deallocator = IxResourceT (runDeallocator deallocator)
  
runIxResourceT :: (Monad m) => IxResourceT m '[] '[] a -> m a
runIxResourceT (IxResourceT ma) = ma

main.hs

{-# LANGUAGE DataKinds
           , RebindableSyntax
#-}

module Main where

import IxResourceT
import qualified Prelude as P
import Prelude hiding ((>>=), (>>), return)

return :: (Monad m) => a -> IxResourceT m rs rs a
return = ireturn

(>>=) :: (Monad m) 
      => IxResourceT m rs rs' a 
      -> (a -> IxResourceT m rs' rs'' b)
      -> IxResourceT m rs rs'' b
(>>=) = ibind

(>>) :: (Monad m)
     => IxResourceT m rs rs' a
     -> IxResourceT m rs' rs'' b
     -> IxResourceT m rs rs'' b
ma >> mb = ma >>= \_ -> mb

-- Can't run it with runIxResourceT because Int resource is not cleaned up
ixResourceTEx1 :: IxResourceT IO '[] '[Int] ()
ixResourceTEx1 = do 
  allocate (allocateInt 2, releaseInt)
  return ()

ixResourceTEx2 :: IxResourceT IO '[] '[] ()
ixResourceTEx2 = do
  (intResource, releaseIntResource) <- allocate (allocateInt 2, releaseInt) 
  (strResource, releaseStrResource) <- allocate (allocateString "asd", releaseString)
  lift (print $ "Acquired resource: " ++ show intResource) 
  -- release (Deallocator (P.return ()) :: Deallocator IO Double) -- Doesn't work because no Doubles to free
  release releaseStrResource
  -- release (Deallocator (P.return ()) :: Deallocator IO String) -- Doesn't work because no more Strings to free
  release releaseIntResource
  
allocateInt :: Int -> IO Int
allocateInt n = print ("Allocating[Int]: " ++ show n) P.>> P.return n

releaseInt :: Int -> IO ()
releaseInt n = print ("Releasing[Int]: " ++ show n) P.>> P.return ()

main :: IO ()
main = runIxResourceT ixResourceTEx2