MonadIx (example instance of the interface described in https://stackoverflow.com/questions/28690448/what-is-indexed-monad/28696299#28696299)

MonadIx.hs

{-# LANGUAGE
    BlockArguments,
    InstanceSigs,
    TypeOperators,
    DataKinds,
    PolyKinds,
    RankNTypes,
    ScopedTypeVariables,
    GADTs
  #-}

import Data.Kind

type a ~> b = forall t. a t -> b t

class MonadIx (m :: (s -> Type) -> (s -> Type)) where
  returnix :: forall a. a ~> m a
  substix :: forall a b. (a ~> m b) -> (m a ~> m b)

-- State of a DVD drive
data DVDState = Unknown | Empty | Full

data DVD = DVD String
  deriving Show

-- A DVD drive action indexed by an initial state (unknown, empty, full),
-- returning some value (f s0) where s0 is the final state.
data DVDDrive (f :: DVDState -> Type) :: DVDState -> Type where
  -- The DVD drive is in the empty state. We insert a DVD, and continue in the full state.
  Insert :: DVD -> DVDDrive f 'Full -> DVDDrive f 'Empty

  -- The DVD drive is in the full state. We take out a DVD, and continue in the
  -- empty state.
  Eject :: (DVD -> DVDDrive f 'Empty) -> DVDDrive f 'Full

  -- The DVD drive could be in any state (even a known one). We check the
  -- state, and continue in the empty or full state depending on the
  -- observation.
  Peek :: DVDDrive f 'Empty -> DVDDrive f 'Full -> DVDDrive f s

  -- We can lend our DVD drive, and get it back in an unknown state.
  Lend :: DVDDrive f 'Unknown -> DVDDrive f s

  -- The action terminates in the final state s.
  Pure :: f s -> DVDDrive f s

-- * Type combinators (to instantiate f with)

data Is :: s -> s -> Type where
  IsRefl :: Is t t

coerceIs :: Is t t' -> f t -> f t'
coerceIs IsRefl = id

data (a :+: b) :: s -> Type where
  L1 :: a t -> (a :+: b) t
  R1 :: b t -> (a :+: b) t

data (a :*: b) (t :: s) = (:*:) { fst1 :: a t, snd1 :: b t }

newtype Const (u :: Type) (t :: s) = Const { getConst :: u }

-- * Examples

insertDVD :: DVD -> DVDDrive (Is 'Full) 'Empty
insertDVD dvd =
  Insert dvd $
  Pure IsRefl

ejectDVD :: DVDDrive (Is 'Empty :*: Const DVD) 'Full
ejectDVD =
  Eject \dvd ->
  Pure (IsRefl :*: Const dvd)

peekDVD :: DVDDrive (Is 'Empty :+: Is 'Full) 'Unknown
peekDVD =
  Peek
    (Pure (L1 IsRefl))
    (Pure (R1 IsRefl))

lendDVD :: DVDDrive (Is 'Unknown) 'Empty
lendDVD =
  Lend $
  Pure IsRefl

swapDVD :: DVD -> DVDDrive (Is 'Full :*: Const DVD) 'Full
swapDVD dvd =
  Eject \dvd' ->
  Insert dvd $
  Pure (IsRefl :*: Const dvd')

lendAndCheckDVD :: DVDDrive (Is 'Empty :+: Is 'Full) 'Empty
lendAndCheckDVD =
  Lend $
  peekDVD

instance MonadIx DVDDrive where
  returnix :: a ~> DVDDrive a
  returnix = Pure

  substix :: (a ~> DVDDrive b) -> (DVDDrive a ~> DVDDrive b)
  substix k (Insert dvd p) = Insert dvd (substix k p)
  substix k (Eject p) = Eject \dvd -> substix k (p dvd)
  substix k (Peek p1 p2) = Peek (substix k p1) (substix k p2)
  substix k (Lend p) = Lend (substix k p)
  substix k (Pure r) = k r

(>>=*) :: DVDDrive a t -> (a ~> DVDDrive b) -> DVDDrive b t
(>>=*) u k = substix k u

-- Alternative definition of swapDVD with MonadIx combinators
swapDVD' :: DVD -> DVDDrive (Is 'Full :*: Const DVD) 'Full
swapDVD' dvd =
  ejectDVD >>=* \(isEmpty :*: Const dvd) -> coerceIs isEmpty $
  insertDVD dvd >>=* \isFull ->
  returnix (isFull :*: Const dvd)

main :: IO ()
main = pure ()