Haskell confusion with ContT, callCC, when

Question

Continuing quest to make sense of ContT and friends. Please consider the (absurd but illustrative) code below:

v :: IO (Either String [String])
v = return $ Left "Error message"

doit :: IO (Either String ())
doit = (flip runContT return) $ callCC $ \k -> do
    x <- liftIO $ v
    x2 <- either (k . Left) return x
    when True $ k (Left "Error message 2")
    -- k (Left "Error message 3")
    return $ Right () -- success

This code does not compile. However, if the replace the when with the commented k call below it, it compiles. What's going on?

Alternatively, if I comment out the x2 line, it also compiles. ???

Obviously, this is a distilled version of the original code and so all of the elements serve a purpose. Appreciate explanatory help on what's going on and how to fix it. Thanks.

Answer 1

The problem here has to do with the types of when and either, not anything particular to ContT:

when :: forall (m :: * -> *). (Monad m) => Bool -> m () -> m ()
either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c

The second argument needs to be of type m () for some monad m. The when line of your code could thus be amended like so:

when True $ k (Left "Error message 2") >> return ()

to make the code compile. This is probably not what you want to do, but it gives us a hint as to what might be wrong: k's type has been inferred to be something unpalatable to when.

Now for the either signature: notice that the two arguments to either must be functions which produce results of the same type. The type of return here is determined by the type of x, which is in turn fixed by the explicit signature on v. Thus the (k . Left) bit must have the same type; this in turn fixes the type of k at (GHC-determined)

k :: Either String () -> ContT (Either String ()) IO [String]

This is incompatible with when's expectations.

When you comment out the x2 line, however, its effect on the type checker's view of the code is removed, so k is no longer forced into an inconvenient type and is free to assume the type

k :: Either [Char] () -> ContT (Either [Char] ()) IO ()

which is fine in when's book. Thus, the code compiles.

As a final note, I used GHCi's breakpoints facility to obtain the exact types of k under the two scenarios -- I'm nowhere near expert enough to write them out by hand and be in any way assured of their correctness. :-) Use :break ModuleName line-number column-number to try it out.