Re: Type checker's expected and inferred types (reformatted)

From: Isaac Dupree David Menendez wrote:

...

On Sun, Oct 25, 2009 at 1:37 PM, Isaac Dupree 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