Я пытаюсь воспроизвести в Haskell этот фрагмент кода Idris, который обеспечивает правильную последовательность действий по типам:

 data DoorState = DoorClosed | DoorOpen
 data DoorCmd : Type ->
                DoorState ->
 DoorState ->
                Type where
      Open : DoorCmd     () DoorClosed DoorOpen
      Close : DoorCmd    () DoorOpen   DoorClosed
      RingBell : DoorCmd () DoorClosed DoorClosed
      Pure : ty -> DoorCmd ty state state
      (>>=) : DoorCmd a state1 state2 ->
              (a -> DoorCmd b state2 state3) ->
              DoorCmd b state1 state3

Благодаря перегрузке(>>=) оператор, можно написать монадический код как:

do Ring 
   Open 
   Close

но компилятор отклоняет неправильные переходы, такие как:

do Ring
   Open 
   Ring
   Open

Я попытался следовать этому шаблону в следующем фрагменте Haskell:

 data DoorState = Closed | Opened

 data DoorCommand (begin :: DoorState) (end :: DoorState) a where
   Open  :: DoorCommand 'Closed 'Opened ()
   Close :: DoorCommand 'Opened 'Closed ()
   Ring  :: DoorCommand 'Closed 'Closed ()

   Pure  :: x -> DoorCommand b e x
   Bind  :: DoorCommand b e x -> (x -> DoorCommand e f y) -> DoorCommand b f y

 instance Functor (DoorCommand b e) where
   f `fmap` c = Bind c (\ x -> Pure (f x))

 -- instance Applicative (DoorCommand b e) where
 --    pure    = Pure
 --    f <*> x = Bind f (\ f' -> Bind x (\ x' -> Pure (f' x')))

 -- instance Monad (DoorCommand b e) where
 --   return = Pure
 --   (>>=) = Bind

Но, конечно, это не удается:Applicative а такжеMonad экземпляры не могут быть определены правильно, поскольку они требуют двух разных экземпляров для правильной последовательности операций. КонструкторBind может быть использован для обеспечения правильной последовательности, но я не могу использовать «более приятные» do-нотации.

Как я мог написать этот код, чтобы иметь возможность использовать do-notation, например, предотвратить недопустимые последовательностиCommandс?