Type checker's expected and inferred types (reformatted)

[Isaac Dupree]

David Menendez wrote:
> The expected type is what the context wants (it's *ex*ternal). The
> inferred type is what the expression itself has (it's *in*ternal).
> 
> So inferring the type Maybe () for bar seems wrong.

well, maybe GHC just gets it wrong enough of the time, that I got confused.

Or maybe ... When there are bound variables interacting, on the inside 
and outside, it gets confusing.


ghci:
Prelude> \x -> (3+x) + (length x)

<interactive>:1:15:
     Couldn't match expected type `[a]' against inferred type `Int'
     In the second argument of `(+)', namely `(length x)'
     In the expression: (3 + x) + (length x)
     In the expression: \ x -> (3 + x) + (length x)

Your explanation of "expected" and "inferred" could make sense to me if 
the error message followed the "Couldn't match" line with, instead,
     "In the first argument of `length', namely `x'"
because 'length' gives the context of expected list-type, but we've 
found out from elsewhere (a vague word) that 'x' needs to have type Int.

If we flip around the expression-order, we get
Prelude> \x -> (length x) + (3+x)

<interactive>:1:20:
     Couldn't match expected type `Int' against inferred type `[a]'
     In the second argument of `(+)', namely `(3 + x)'
     In the expression: (length x) + (3 + x)
     In the expression: \ x -> (length x) + (3 + x)

...and yes, technically your explanation of expected/inferred works. But 
the location/parity depends on the evaluation-order that the type 
checker uses.  The error messages don't seem to specify location 
precisely enough that I can easily use the information about which type 
is the 'expected' type and which type is the 'inferred' one.  There are 
usually more chains of inference, let-clauses, etc. through which a 
contradiction is found, that muddy the issue.

hmm. Yes, I think I would appreciate for error messages to tell me 
exactly which piece of the expression is expected/inferred to be those 
types. (Is this always a sensible question? or are there sometimes 
typing-conflicts that can't be / aren't reduced to the expected/inferred 
type of a particular expression in the code?)

-Isaac