Am Samstag 24 Oktober 2009 03:12:14 schrieb C Rodrigues:

I came across a type error that misled me for quite a while, because the expected and inferred types were backwards (from my point of view). A simplified example is below. Can someone explain how GHC's type checker creates the error message? In this example, fun1 and fun2 are basically the same. The type error is because they try to run an IO () together with a Maybe ().

import Control.Monad foo :: Maybe () foo = return () bar :: IO () bar = return () fun1 = let fooThen m = foo >> m in fooThen (bar >> undefined) fun2 = let fooThen m = foo >> m in fooThen (do {bar; undefined})

With ghc 6.10.4, both functions attribute the error message to `bar'. However, the expected and inferred monads are swapped.fun1 produces the error message:

Couldn't match expected type `Maybe a' against inferred type `IO ()' In the first argument of `(>>=)', namely `bar'

fun2 produces the error message:

Couldn't match expected type `IO ()' against inferred type `Maybe ()' In a stmt of a 'do' expression: bar

It's confusing because 'bar' is inferred to have type Maybe (), even though it's explicitly declared to be an IO ().

I don't know the intricate details, but the order in which type inference/type checking proceeds has something to do with it. In fun1, apparently first the type of fooThen is inferred to be `Maybe a -> Maybe a'. Then, in the body of the let-expression, fooThen *expects* a `Maybe a'. Thus the (>>) in fooThen's argument is inferred to have the type `Maybe a -> Maybe b -> Maybe b'. Hence the first argument of (>>) [or (>>=), apparently it has been expanded to that] is *expected* to have type `Maybe a'. But from bar's definition, its type is *inferred* to be `IO ()'. Perfectly clear and transparent (not really). Had the type of fooThen's argument been inferred before fooThen's type, it would've said that it expected fooThen to have type `IO a -> b', but inferred it to have type `Maybe a -> Maybe a'. The error for fun2 is baffling. I can't explain how ghci comes to *expect* bar to have type `IO ()'. Also intriguing is that if you swap bar and undefined in the do-expression, you get the error message you'd expect: Couldn't match expected type `Maybe b' against inferred type `IO ()' In the expression: bar In the first argument of `fooThen', namely `(do undefined bar)' In the expression: fooThen (do undefined bar) But if you sandwich bar between two actions which may have type `Maybe a', it's back to expecting `IO ()': Couldn't match expected type `IO ()' against inferred type `Maybe ()' In a stmt of a 'do' expression: bar In the first argument of `fooThen', namely `(do Just 1 bar Nothing)' In the expression: fooThen (do Just 1 bar Nothing) Seems typechecking do-expressions has some strange corners.