Think of ATM state machine

use typed-fsm demo: I add new state CheckPin.
The function checkPinFun determines the subsequent state.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeFamilies #-}

module TypedFsm.ATM where

import Control.Monad.State
import Data.IFunctor (IMonad (..))
import Data.IFunctor qualified as I
import Data.Kind
import Data.SR
import TypedFsm.Core
import TypedFsm.Driver

data ATMSt
  = Ready
  | CardInserted
  | CheckPin
  | Session

data SATMSt :: ATMSt -> Type where
  SReady :: SATMSt Ready
  SCardInserted :: SATMSt CardInserted
  SCheckPin :: SATMSt CheckPin
  SSession :: SATMSt Session

data CheckPINResult :: ATMSt -> Type where
  Incorrect :: CheckPINResult CardInserted
  Correct :: CheckPINResult Session

instance StateTransMsg ATMSt where
  data Msg ATMSt from to where
    InsertCard :: Msg ATMSt Ready CardInserted
    CIEject :: Msg ATMSt CardInserted Ready
    ---------------
    CheckPIN :: Int -> Msg ATMSt CardInserted CheckPin
    ---------------
    GetAmount :: Msg ATMSt Session Session
    Dispense :: Int -> Msg ATMSt Session Session
    SEject :: Msg ATMSt Session Ready

checkPinFun
  :: Int
  -> Operate (StateT () IO) CheckPINResult CheckPin
checkPinFun i = I.do
  if i == 1234
    then LiftM $ pure (ireturn Correct)
    else LiftM $ pure (ireturn Incorrect)

readHandler :: Op ATMSt () Ready Ready
readHandler = I.do
  msg <- getInput
  case msg of
    InsertCard -> cardInsertedHandler

cardInsertedHandler :: Op ATMSt () Ready CardInserted
cardInsertedHandler = I.do
  msg <- getInput
  case msg of
    CIEject -> readHandler
    CheckPIN i -> I.do
      res <- checkPinFun i
      case res of
        Incorrect -> cardInsertedHandler
        Correct -> sessionHandler

sessionHandler :: Op ATMSt () Ready Session
sessionHandler = I.do
  msg <- getInput
  case msg of
    GetAmount -> I.do
      liftm $ liftIO $ putStrLn "GetAmount"
      sessionHandler
    Dispense i -> I.do
      liftm $ liftIO $ putStrLn ("Dispense " ++ show i)
      sessionHandler
    SEject -> readHandler

instance Reify Ready where
  reifyProxy _ = Ready

instance Reify CardInserted where
  reifyProxy _ = CardInserted

instance Reify CheckPin where
  reifyProxy _ = CheckPin

instance Reify Session where
  reifyProxy _ = Session

type instance Sing = SATMSt

instance SingI Ready where
  sing = SReady

instance SingI CardInserted where
  sing = SCardInserted

instance SingI CheckPin where
  sing = SCheckPin

instance SingI Session where
  sing = SSession
sdzx-1 / typed-fsm

Think of ATM state machine #1
