Couldn't match type variables-CodePudding

I'm trying to create telegram bot with quite specific architecture (Finite-state machines). For example, there can be (1) state that will run some function, that will return other state or (2) state that will move bot into some other machine with different states.

So I created class and two types that look something like that:

{-# LANGUAGE DeriveAnyClass, GADTs #-}
module Main where

class (Eq a) => TeleClass a

type BotView a = String -> a

data TeleState a where
    TeleState :: TeleClass a => a -> BotView a -> TeleState a
    TeleMachineChange :: (TeleClass a, TeleClass b) => a -> TeleMachine b -> TeleState a

data TeleMachine a = TeleMachine
    { defaultState :: a
    , stateMachine :: [TeleState a]
    }

And then GHC allows me to create some FSMs that look exactly like I want:

data MainStates = MAIN_MENU | TASK_CHOOSING | CHANGE_VIEW | MODER_VIEW
    deriving (TeleClass, Eq)
data AdminStates = ADMIN_MENU | PUBLISH_TASK
    deriving (TeleClass, Eq)
data ModerStates = MODER_MENU | EDIT_TASK
    deriving (TeleClass, Eq)

fMainMenu _  = TASK_CHOOSING
fChooseTask _ = CHANGE_VIEW

fAdminMenu _ = PUBLISH_TASK
fPublishTask _ = ADMIN_MENU

fModerMenu _ = EDIT_TASK
fEditTask _ = MODER_MENU

moderMachine = TeleMachine
    { defaultState = MODER_MENU
    , stateMachine =
        [ TeleState MODER_MENU fModerMenu
        , TeleState EDIT_TASK fEditTask
        ]
    }

adminMachine = TeleMachine
    { defaultState = ADMIN_MENU
    , stateMachine =
        [ TeleState ADMIN_MENU fAdminMenu
        , TeleState PUBLISH_TASK fPublishTask
        ]
    }

mainMachine = TeleMachine
    { defaultState = MAIN_MENU
    , stateMachine =  
        [ TeleState MAIN_MENU fMainMenu
        , TeleState TASK_CHOOSING fChooseTask
        , TeleMachineChange CHANGE_VIEW adminMachine
        , TeleMachineChange MODER_VIEW moderMachine
        ] 
    }

And then to apply some state to FSM I added this function:

data MatchResult a b = Func a | Machine b | None

matchState :: (TeleClass a, TeleClass c) =>
    [TeleState a] -> a -> MatchResult (BotView a) (TeleMachine c)
matchState (TeleState mState fFunc : stateMachine) state
    | mState == state = Func fFunc
    | otherwise = matchState stateMachine state
matchState (TeleMachineChange mState mMachine : stateMachine) state
    | mState == state = Machine mMachine
    | otherwise = matchState stateMachine state
matchState [] _ = None

And compiler complained that it couldn't match type 'b' with 'c':

    • Couldn't match type ‘b’ with ‘c’
      ‘b’ is a rigid type variable bound by
        a pattern with constructor:
          TeleMachineChange :: forall a b.
                               (TeleClass a, TeleClass b) =>
                               a -> TeleMachine b -> TeleState a,
        in an equation for ‘matchState’
        at example.hs:70:13-45
      ‘c’ is a rigid type variable bound by
        the type signature for:
          matchState :: forall a c.
                        (TeleClass a, TeleClass c) =>
                        [TeleState a] -> a -> MatchResult (BotView a) (TeleMachine c)
        at example.hs:(65,1)-(66,65)
      Expected type: MatchResult (BotView a) (TeleMachine c)
        Actual type: MatchResult (BotView a) (TeleMachine b)
    • In the expression: Machine mMachine
      In an equation for ‘matchState’:
          matchState (TeleMachineChange mState mMachine : stateMachine) state
            | mState == state = Machine mMachine
            | otherwise = matchState stateMachine state
    • Relevant bindings include
        mMachine :: TeleMachine b (bound at example.hs:70:38)
        matchState :: [TeleState a]
                      -> a -> MatchResult (BotView a) (TeleMachine c)
          (bound at example.hs:67:1)
   |
71 |     | mState == state = Machine mMachine
   |                         ^^^^^^^^^^^^^^^^

I tried to use ExistentialQuantification and QuantifiedConstraints extensions, but couldn't fix this problem with them. Right now I don't know if this is viable idea to implement something like this in language like haskell.

CodePudding user response：

The signature

matchState :: (TeleClass a, TeleClass c) =>
    [TeleState a] -> a -> MatchResult (BotView a) (TeleMachine c)

...which is just shorthand for

matchState :: ∀ a c . (TeleClass a, TeleClass c) =>
    [TeleState a] -> a -> MatchResult (BotView a) (TeleMachine c)

expresses that for whatever type c the caller picks, this function will be able to procure a suitable TeleMachine from the input list. It seems a tough thing to do.

I think what you're trying to express is instead “ok, I'll try to find a matching machine in there, but I don't know what its type is going to be”. That is indeed an existential type

matchState :: ∀ a . ∃ c . (TeleClass a, TeleClass c) =>
    [TeleState a] -> a -> MatchResult (BotView a) (TeleMachine c)

Haskell doesn't allow functions with existential type, but you could make the MatchResult type existential, similary to how the TeleMachineChange constructor of TeleMachine is existential:

data MatchResult a where
  Func :: a -> MatchResult a
  Machine :: TeleClass b => b -> MatchResult a
  None :: MatchResult a

matchState :: ∀ a . TeleClass a =>
    [TeleState a] -> a -> MatchResult (BotView a)

Alternatively, you can fake an existential type for matchState with continuation-passing style:

matchState :: ∀ a r . TeleClass a =>
     [TeleState a]
  -> a
  -> (∀ c . TeleClass a
       => MatchResult (BotView a) (TeleMachine c) -> r)
  -> r
matchState (TeleState mState fFunc : stateMachine) state φ
    | mState == state = φ (Func fFunc)
    | otherwise = matchState stateMachine state φ
matchState (TeleMachineChange mState mMachine : stateMachine) state
    | mState == state = φ (Machine mMachine)
    | otherwise = matchState stateMachine state φ
matchState [] _ = φ None