Re: Type checker's expected and inferred types

23 Oct 2009

      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.

Re: Type checker's expected and inferred types

Daniel Fischer