Type mismatch error message doesn't show the whole type

[brianhuffman]

Here's an example of a program with a type error:

f : {n} (fin n) => {a : [n]([n][2*n], [3*n]), b : [5*n]}  -> [5*n]
f x = x.b

g : {a : [4]([3][8], [12]), b : [20]} -> [20]
g y = f y

And here's the type error message:

[error] at foo.cry:5:9--5:10:
  Type mismatch:
    Expected type: 4
    Inferred type: 3
    When checking type of function argument

There is a lot of information missing from this error message that the user needs to reconstruct in order to be able to understand the problem. From the source location you can tell that it's referring to the y in the rhs of g, which is an argument to f. It says the "expected type" is 4, but no 4 appears in the type signature for f. So to understand the error, the user needs to unify the result type [20] of g with the result type [5*n] of f, and then instantiate n = 4. Then the user needs to match the argument types together to discover that the length parameter of the 0th tuple field of the element type of the a field doesn't match.

A more informative type error message would help. GHC's type error messages have lots of useful information: Not just the inner types that don't match, but also the expected and actual types, as well as the expressions themselves.

Prelude> map fromInteger "abcdef"

<interactive>:5:17: error:
    • Couldn't match type ‘Char’ with ‘Integer’
      Expected type: [Integer]
        Actual type: [Char]
    • In the second argument of ‘map’, namely ‘"abcdef"’
      In the expression: map fromInteger "abcdef"
      In an equation for ‘it’: it = map fromInteger "abcdef"

We should do something more like this.

[yav]

One idea I've considered is to show the whole mismatching types, but highlight in some way the bits that don't match, which might be nice.

I am not at all a fan of GHC printing the whole expressions though---I find it really hard to see what is the actual error. Do you find those useful?

[brianhuffman]

I actually like how GHC prints the expression, although technically that information is redundant: You can always find the expression yourself using the location information in the error message. Printing the expression saves me that step, but it can get a bit verbose sometimes. Editor integration that could highlight the expression in emacs for me would be very nice, and would totally obviate the need for printing it.

[brianhuffman]

I just ran into this problem again, and it was very annoying. My situation was that I was writing a function whose return type was a record with lots of fields, many of them with the same type. In the rhs of the function definition, I made a mistake in one of the record fields, and put in an expression with the wrong type.

How could I tell which record field contained the error? The error message was of no help. The indicated location referred to the entire function definition. And the types in the error message were only the mismatched parts of the expected vs encountered types. There was no indication of which field's type didn't match. I had to carefully look through the entire list of fields to see which one had a mismatched type.

We should prioritize improving this.

[yav]

I'll give it a go, there might be some low hanging fruit here that could improve the situation. Could you post an example, so we have something to check against.

[yav]

@brianhuffman I prototyped something that when executed on this code:

  type T = { a : [8] }
  type S = { a : [10] }
  
  
  f : T -> ()
  f _ = ()
  
  g : S -> ()
  g x = f x

Gives the following error:

[error] at test.cry:10:9--10:10:
  Type mismatch:
    Expected type: 8
    Inferred type: 10
    When checking type of function argument
    Context: {a : [ERROR]_, …}

The new part is the Context clause.

What do you think?