Indexed monads for state machines

I decided to experiment with indexed monads to create a type-safe state machine. That means Haskell will refuse to compile illegal state transitions. My questions are.

1. I created a Door type with operations over it. It's impossible to code illegal state transitions for it, for example it cannot call close for the already closed door. This code works fine however I have a question: can it be better? Maybe it can be be enhanced, extended with useful stuff etc.
2. I tried to create a DSL based on indexed free monad but I failed. Can someone help me?

Here is my code:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
import Control.Monad.Indexed
import Control.Monad.Indexed.Free
import Data.Coerce
import Language.Haskell.DoNotation
import Prelude hiding (Monad (..), pure)
import qualified Prelude (pure)

-- Handy Indexed container type borrowed from Sandy Maguire
newtype Indexed m i j a = Indexed { unsafeRunIndexed :: m a }
  deriving (Functor, Applicative, Monad)

instance Functor m => IxFunctor (Indexed m) where
  imap :: (a -> b) -> Indexed m i j a -> Indexed m i j b
  imap = fmap

instance Applicative m => IxPointed (Indexed m) where
  ireturn :: a -> Indexed m i i a
  ireturn = Prelude.pure

instance Applicative m => IxApplicative (Indexed m) where
  iap :: forall i j k a b. Indexed m i j (a -> b) -> Indexed m j k a -> Indexed m i k b
  iap = coerce $ (<*>) @m @a @b

instance Monad m => IxMonad (Indexed m) where
  ibind :: forall i j k a b. (a -> Indexed m j k b) -> Indexed m i j a -> Indexed m i k b
  ibind = coerce $ (=<<) @m @a @b

-- Door stuff
data DoorState = Opened | Closed deriving (Show, Eq, Ord)

newtype Door s (i :: DoorState) (j :: DoorState) a = Door
  { unsafeRunDoor :: Indexed IO i j a }
  deriving (IxFunctor, IxPointed, IxApplicative, IxMonad)

runDoor :: (forall s . Door s st1 st2 a) -> IO a
runDoor = coerce

class State (a :: DoorState) where
  state :: DoorState
instance State 'Opened where
  state = Opened
instance State 'Closed where
  state = Closed

stateM :: forall a m . (State a, Monad m) => m DoorState
stateM = return (state @a)

getState :: forall s st . State st => Door s st st DoorState
getState = coerce $ stateM @st @IO

openDoor :: Door s 'Closed 'Opened ()
openDoor = coerce $ putStrLn "open!"

closeDoor :: Door s 'Opened 'Closed ()
closeDoor = coerce $ putStrLn "close!"

ringBell :: Door s 'Closed 'Closed ()
ringBell = coerce $ putStrLn "ring!"
  
displayMessage :: String -> Door s st st ()
displayMessage = coerce . putStrLn

doorProgram :: Door s 'Closed 'Closed ()
doorProgram = do
  ringBell
  openDoor
  st <- getState
  displayMessage $ "State is: " ++ show st
  closeDoor

Now the problematic code:

• Expected kind ‘* -> * -> * -> *’, but ‘DoorF’ has kind ‘DoorState -> DoorState -> * -> *’
• In the first argument of ‘IxFree’, namely ‘DoorF’
• In the type ‘IxFree DoorF’
• In the type declaration for ‘DoorDSL’

Any ideas how to create free indexed monad DSL for the Door?

data DoorF (i :: DoorState) (j :: DoorState) next where
  Open    :: next -> DoorF 'Closed 'Opened next
  Close   :: next -> DoorF 'Opened 'Closed next
  Ring    :: next -> DoorF 'Closed 'Closed next
  Display :: String -> next -> DoorF st st next
  State   :: (DoorState -> next) -> DoorF st st next

instance Functor (DoorF i j) where
  fmap f (Open next) = Open (f next)
  fmap f (Close next) = Close (f next)
  fmap f (Ring next) = Ring (f next)
  fmap f (Display s next) = Display s (f next)
  fmap f (State nextF) = State (f . nextF)

instance IxFunctor DoorF where
  imap = fmap

type DoorDSL = IxFree DoorF

UPDATE: Li-yao Xia answered my question. Here is the working version of free indexed monadic DSL:

data Opened
data Closed

data DoorF i j next where
  Open    :: next -> DoorF Closed Opened next
  Close   :: next -> DoorF Opened Closed next
  Ring    :: next -> DoorF Closed Closed next
  Display :: String -> next -> DoorF st st next

instance Functor (DoorF i j) where
  fmap f (Open next) = Open (f next)
  fmap f (Close next) = Close (f next)
  fmap f (Ring next) = Ring (f next)
  fmap f (Display s next) = Display s (f next)

instance IxFunctor DoorF where
  imap = fmap

type DoorDSL = IxFree DoorF

open :: DoorDSL Closed Opened ()
open = Free (Open (Pure ()))

close :: DoorDSL Opened Closed ()
close = Free (Close (Pure ()))

ring :: DoorDSL Closed Closed ()
ring = Free (Ring (Pure ()))

display :: String -> DoorDSL st st ()
display msg = Free (Display msg (Pure ()))

The error is because IxFree is monomorphic when it could be generalized. The indexed-free library should be patched to use PolyKinds.

In the meantime, a workaround is, instead of DataKind, to declare the DoorState constructors as their own data types:

-- Promoted DoorState without DataKind
type DoorState' = Type
data Opened
data Closed