Couldn't match type ‘a’ with ‘b’

Question

Full code http://codepad.org/of3mTarF

I'm trying to use monad-mock to test my code, but I run into a problem which I have no idea how to solve.

The monad I'm trying to mock:

class Monad m => MonadAccess m where
  getItem :: FromJSON a => ItemId -> m a
  getNextPage :: (FromJSON a, Show a, Eq a) => Pager a -> m (Maybe (Pager a))

I also have a function which is defined in terms of that monad:

getAllPages
  :: (MonadAccess m, FromJSON a, Show a, Eq a)
  => String
  -> m [a]
getAllPages s = do
    firstPage <- getItem s
    go (pagerItems firstPage) (pagerNext firstPage)
  where
    go acc mp =
      case mp of
        Nothing -> return acc
        Just p  -> getNextPage p >>= go (acc ++ pagerItems p)

I define the mock using TemplateHaskell:

makeAction "AccessAction" [ts| MonadAccess |]

But even if I define all the necessary bits manually the errors I'm getting are the same:

mock.hs:65:1: error:
    • Couldn't match type ‘a’ with ‘b’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          eqAction :: forall a b.
                      AccessAction a
                      -> AccessAction b -> Maybe (a Data.Type.Equality.:~: b)
        at mock.hs:65:1
      ‘b’ is a rigid type variable bound by
        the type signature for:
          eqAction :: forall a b.
                      AccessAction a
                      -> AccessAction b -> Maybe (a Data.Type.Equality.:~: b)
        at mock.hs:65:1
      Expected type: Maybe (a Data.Type.Equality.:~: b)
        Actual type: Maybe (a Data.Type.Equality.:~: a)
    • In the expression: Just Data.Type.Equality.Refl
      In the expression:
        if (&&) ((==) x_amxO y_amxP) True then
            Just Data.Type.Equality.Refl
        else
            Nothing
      In an equation for ‘eqAction’:
          eqAction (GetItem x_amxO) (GetItem y_amxP)
            = if (&&) ((==) x_amxO y_amxP) True then
                  Just Data.Type.Equality.Refl
              else
                  Nothing
    • Relevant bindings include
        eqAction :: AccessAction a
                    -> AccessAction b -> Maybe (a Data.Type.Equality.:~: b)
          (bound at mock.hs:65:1)

mock.hs:65:1: error:
    • Could not deduce: a2 ~ a1
      from the context: (a ~ Maybe (Pager a1),
                         FromJSON a1,
                         Show a1,
                         Eq a1)
        bound by a pattern with constructor:
                   GetNextPage :: forall a_Xe30.
                                  (FromJSON a_Xe30, Show a_Xe30, Eq a_Xe30) =>
                                  Pager a_Xe30 -> AccessAction (Maybe (Pager a_Xe30)),
                 in an equation for ‘eqAction’
        at mock.hs:65:1-45
      or from: (b ~ Maybe (Pager a2), FromJSON a2, Show a2, Eq a2)
        bound by a pattern with constructor:
                   GetNextPage :: forall a_Xe30.
                                  (FromJSON a_Xe30, Show a_Xe30, Eq a_Xe30) =>
                                  Pager a_Xe30 -> AccessAction (Maybe (Pager a_Xe30)),
                 in an equation for ‘eqAction’
        at mock.hs:65:1-45
      ‘a2’ is a rigid type variable bound by
        a pattern with constructor:
          GetNextPage :: forall a_Xe30.
                         (FromJSON a_Xe30, Show a_Xe30, Eq a_Xe30) =>
                         Pager a_Xe30 -> AccessAction (Maybe (Pager a_Xe30)),
        in an equation for ‘eqAction’
        at mock.hs:65:1
      ‘a1’ is a rigid type variable bound by
        a pattern with constructor:
          GetNextPage :: forall a_Xe30.
                         (FromJSON a_Xe30, Show a_Xe30, Eq a_Xe30) =>
                         Pager a_Xe30 -> AccessAction (Maybe (Pager a_Xe30)),
        in an equation for ‘eqAction’
        at mock.hs:65:1
      Expected type: Pager a1
        Actual type: Pager a2
    • In the second argument of ‘(==)’, namely ‘y_amxR’
      In the first argument of ‘(&&)’, namely ‘(==) x_amxQ y_amxR’
      In the expression: (&&) ((==) x_amxQ y_amxR) True
    • Relevant bindings include
        y_amxR :: Pager a2 (bound at mock.hs:65:1)
        x_amxQ :: Pager a1 (bound at mock.hs:65:1)

I tried removing Maybe from the definition of the getNextPage but it didn't change anything. I also looked into Data.Type.Equality but I couldn't figure out what may be wrong.

Any pointers to get this piece of code to compile?

Answer 1

OK, let's try this again. If we use the -ddump-splices switch, and massage the output a little, we see what makeAction generated:

data AccessAction r
  where
    GetItem :: FromJSON a => ItemId -> AccessAction a
    GetNextPage :: (FromJSON a, Show a, Eq a) =>
                   Pager a -> AccessAction (Maybe (Pager a))
deriving instance Eq (AccessAction r)
deriving instance Show (AccessAction r)

instance Action AccessAction where
  eqAction (GetItem x) (GetItem y)
    = if x == y then
          Just Refl
      else
          Nothing
  eqAction (GetNextPage x) (GetNextPage y)
    = if x == y True then
          Just Refl
      else
          Nothing
  eqAction _ _ = Nothing

instance Monad m =>
         MonadAccess (MockT AccessAction m) where
  getItem x = mockAction "getItem" (GetItem x)
  getNextPage x = mockAction "getNextPage" (GetNextPage x)

The error occurs when creating the eqAction function for the AccessAction instance of Action. The function for this instance has type:

eqAction :: AccessAction a -> AccessAction b -> Maybe (a :~: b)

Which means it will be passed two AccessActions with potentially different result types, and must return Nothing if the two actions are different, or Just Refl if the two actions are the same (meaning they have the same data constructor, equal arguments, and matching return types).

The AccessAction constructors have type:

GetItem :: FromJSON a => ItemId -> AccessAction a
GetNextPage :: (FromJSON a, Show a, Eq a) => Pager a -> AccessAction (Maybe (Pager a))

The eqAction function pattern matches on the constructors, checks that the arguments are equal, and returns Just Refl if they are. However, Refl inhabits a :~: b iff a ~ b, but there's no constraint that guarantees that a ~ b, which results in the error. For example, one GetItem could be an AccessAction Int, and the other an AccessAction Bool, since both Int and Bool have FromJSON instances.

You would need to prove that the two FromJSON instances are the same type. The only way I can see to do this would be if AccessAction had a TestEquality instance, which would require the a to also have a TestEquality instance.

Rather, we can make a a parameter to the MonadAccess typeclass with a functional dependency (just like the state parameter in MonadState), and move the FromJSON, Eq, and Show constraints into the typeclass:

class (FromJSON a, Show a, Eq a, Monad m) => MonadAccess a m | m -> a where
  getItem :: ItemId -> m (Pager a)
  getNextPage :: Pager a -> m (Maybe (Pager a))

This requires that we add the FunctionalDependencies language extension.

Note that I also changed the return type of getItem from m a to m (Pager a), which is how it is used in practice (the compile gets upset if the type is too general).

The type of getAllPages now changes to:

getAllPages
  :: MonadAccess a m
  => String
  -> m [a]

And we can finally use makeAction to generate a mock for MonadAccess Item (which is the type of a we intend to use in the mock).

makeAction "AccessAction" [ts| MonadAccess Item |]

The generated code creates a context with FromJSON Item, which is not allowed unless you enable the FlexibleContexts language extension.

Now we have a guarantee that, within MonadAccess Item, all a type variables refer to the same type Item.