Type checker's expected and inferred types (reformatted)

[John Lato]

> From: Isaac Dupree <ml at isaac.cedarswampstudios.org>
> David Menendez wrote:
>> On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree
>> <ml at isaac.cedarswampstudios.org> wrote:
>>> 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.
>>
>> This had me confused for a while, but I think I've worked out what's
>> happening. (+) is polymorphic,   ...
>
> Oh darn, it sounds like you're right. And polymorphism is so common.  I
> just came up with that example randomly as the first nontrivial
> type-error-with-a-lambda I could think of...

I think this is a great example of why the current type errors are not
as helpful as they could be.  The code where the type checker
determines 'x' has type [a] is several steps removed from where the
error arises.  This is how I understand this process (I've probably
left out some details):

1.  checker infers x :: [a] from 'length x'
2.  checker infers (3 + x) :: [a] from (+) and step 1
3.  checker infers the second (+) :: [a] -> [a] -> [a] from step 2
4.  conflict - checker expects (length x) :: [a] from step 3
     and infers (length x) :: Int from definition of 'length'.

Even with this simple example the error message given doesn't directly
point to the problem.  I don't think it's uncommon for there to be
more steps in practice.  I frequently find myself adding explicit type
signatures to let-bound functions to debug these.  This is a pain
because it also usually involves enabling ScopedTypeVariables.

I personally would find it useful if error messages showed the
sequence of how the type checker determined the given context.
Especially if it would also do so for infinite type errors, which
don't provide much useful information to me.

Cheers,
John