Confusing error message for monadic function with wrong number of arguments

[tim]

If I compile the following code:

import Control.Monad.State

foo :: MonadIO m => Int -> m ()
foo x y = return ()

I get the error message:

bug.hs:6:10:
    Couldn't match expected type `()' against inferred type `m ()'
    In the expression: return ()
    In the definition of `foo': foo x y = return ()

On the other hand, if I change foo's type signature to:

foo :: Int -> IO ()

I get the more helpful:

bug.hs:6:0:
    The equation(s) for `foo' have two arguments,
    but its type `Int -> IO ()' has only one

It would be good if the second error message appeared in the first case as well.

[simonpj]

Good example! Sadly, it's quite awkward to fix. Here's what is happening.

• GHC tries to make the type Int -> m () look like ty1 -> ty2 -> ty3 (to match the syntactic form of the LHS.
• It's possible that the context (MonadIO m) might have, as a "superclass" the equality m ~ (->) Int. In that case we'd get ty2 = Int, ty3 = ().
• Because m might be elucidated by the context, GHC can't reject the result type (m ()) right away. Instead it invents a fresh type variable alpha, and generates the contraint that (m ~ (->) alpha), leaving the constraint to be solved later.
• Now we go on to the RHS, and that gives a type error.

What we really want here is to solve the first constraint "eagerly", and proceed only if it succeeds. The type checker isn't set up to do that at the moment, but this is an interesting example to bear in mind, thank you.

Simon

[monoidal]

GHC 7.6 gives

X.hs:4:1:
    Couldn't match type `()' with `m0 ()'
    Expected type: t0 -> m0 ()
      Actual type: m ()
    The equation(s) for `foo' have two arguments,
    but its type `Int -> m ()' has only one