Dear GHCers, On Wed, 2009-10-28 at 12:14 +0000, John Lato wrote:

...

...

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):

I am a little ambiguous on this issue; I usually find GHC's type errors make me realize what I did wrong very quickly, i.e. until I start messing with combinations of GADTs, type classes and type families. When I've looked at an error for too long without understanding what's happening, I usually look for ways to express the same problem in simpler constructs. This case has me stumped, though.

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

Pardon? Judging from the error GHC gives, you must be right, but isn't *this* the point where things should go wrong? I'm not too intimately familiar with the type checker's internals, so this example leads me to speculate that "normal" types are inferred and checked *before* type class constraints are evaluated. However, I would have wanted this error: Prelude> [1] + [2] <interactive>:1:0: No instance for (Num [t]) arising from a use of `+' at <interactive>:1:0-8 Possible fix: add an instance declaration for (Num [t]) In the expression: [1] + [2] In the definition of `it': it = [1] + [2] In other words: isn't the problem in this case that the type checker does not gather all information (no instance of type class Num) to give the proper error? Is gathering type class information after "normal" types have already conflicted even possible? Regards, Philip

On Wednesday 28 October 2009 08:14:46 John Lato wrote:

...

...

Isaac Dupree wrote:

...

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)

This is how I understand this process

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'll second that. On Saturday 24 October 2009 15:21:51 Albert Y. C. Lai wrote:

I find it unnecessary to "decrypt" the two words "expected" and "inferred". They have their own definitions and they stand for themselves;

On the contrary, this is a perfect example of why the error message's choice of words is bad. One type is "expected" and the other is "inferred". In the example the contextual type [a] is inferred via steps 1-2-3, and the internal type Int is determined so trivially that the "inferred" designation is somewhere between confusing and misleading. I'd love to see "expected" kept, and "inferred" removed from the message.