Question on bind implementation for ExceptT e m a

Learn
#1

Hi all,

let’s say we have a newtype for ExceptT goes like:

newtype ExceptT (e :: Type) (m :: Type -> Type) (a :: Type) = ExceptT
  {runExceptT :: m (Either e a)}

and say we want to implement the Monad for it,

instance (Monad m) => Monad (ExceptT e m) where
  return = pure

  a >>= f = ExceptT $ do
      a' <- runExceptT a
      case a' of
          Left err -> pure $ Left err
          Right val -> runExceptT $ f val

The above version works fine. But the below one doesn’t:

instance (Monad m) => Monad (ExceptT e m) where
  return = pure

  a >>= f = do
    a' <- runExceptT a
    case a' of
      Left err -> ExceptT $ pure $ Left err
      Right val -> f val

compiler throw the error:

• Couldn't match type ‘m’ with ‘ExceptT e m’
  Expected: ExceptT e (ExceptT e m) a
    Actual: ExceptT e m a
  ‘m’ is a rigid type variable bound by
    the instance declaration
    at /home/longlong/hcat/src/BasicStateDemo.hs:36:10-41
• In the first argument of ‘runExceptT’, namely ‘a’
  In a stmt of a 'do' block: a' <- runExceptT a
  In the expression:
    do a' <- runExceptT a
       case a' of
         Left err -> ExceptT $ pure $ Left err
         Right val -> f val
• Relevant bindings include
    f :: a -> ExceptT e m b
      (bound at /home/longlong/hcat/src/BasicStateDemo.hs:39:9)
    a :: ExceptT e m a
      (bound at /home/longlong/hcat/src/BasicStateDemo.hs:39:3)
    (>>=) :: ExceptT e m a -> (a -> ExceptT e m b) -> ExceptT e m b
      (bound at /home/longlong/hcat/src/BasicStateDemo.hs:39:5)

This error made me confused, can anyone help explain the difference and the error to me?
Thanks!

BRs,
Longlong

1 Like
#2

When you change from ExceptT $ do ... to do ... ExceptT ..., you’re changing the monad that the do-notation uses. In the version that works fine, the monad that the do-notation uses is m (Either e a) (the contents of the ExceptT newtype), while the broken version uses the monad ExceptT e m a.

Changing the monad of the do-notation also changes the types of the binds (the ... <- ... notation). In the working version the types are <a> <- <m a> while in the broken version the types are <a> <- <ExceptT e m a>. Note that this means you’re defining the monad of ExceptT in terms of itself in the broken version. That’s already a huge red flag.

In the first bind a' <- runExceptT a the types are <Either e a> <- <m (Either e a)>, that does fit the pattern of the working version, but not the broken version hence the error. At this point GHC should have stopped and reported:

  a' <- runExceptT a
        ^^^^^^^^^^^^
Expected: ExceptT e m b
  Actual: m (Either e a)

• Note: This is a bind in the monad `ExceptT e m'

(If GHC was really smart it could even replace that placeholder b by Either e a. That would require looking at the case expression on the next line.)

Unfortunately, GHC’s type inference does not stop there and tries really hard to make things work. It knows that runExceptT a could produce something of type ExceptT e m a which would be required in the broken version, however then the type of a must be ExceptT e (ExceptT e m) a. There it does finally finds a true dead end and it reports that it expected a to have type ExceptT e (ExceptT e m) a but it has type ExceptT e m a.

I’ve opened Confusion around do notation and GHC going too far · Issue #551 · haskell/error-messages · GitHub about this thread. Please share your opinion on how this error message could be improved. It would also really help if you could explain from your perspective what exactly was/is confusing.

2 Likes
#3

Great explanation!

if you could explain from your perspective what exactly was/is confusing.

[longlong]: Well, the confusion was,
I thought the type of a' in a' <- runExceptT a is always Either e a, and the monad of the do-notation would always be m (Either e a).

BTW, I already know the reason why the error goes like that, Thank you! I have one more question that how the compiler knows which monad should be used in a do-notation block?

#4

The type of monad is also inferred.

In you working example you are using ExceptT $ do ... and the type of ExceptT is:

ExceptT :: m (Either e a) -> ExceptT e m a

So it knows that the result of the do-notation needs to have type m (Either e a) which means the do-notation must use the monad m.

In the broken version you directly write a >>= f = do .... There it knows that you’re defining the >>= operator for the ExceptT e m monad, so the type of >>= is:

(>>=) :: ExceptT e m a -> (a -> ExceptT e m b) -> ExceptT e m b

From that it knows that the right hand side of the definition a >>= f = do ..., must have type ExceptT e m b. So the do-notation must use the monad ExceptT e m.

2 Likes
#5

So the Monad is inferred by the context around do-notation, make sense to me. Thank you! :grin: