Type checker's expected and inferred types

[Daniel Fischer]

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.