Purescript: Better error messages for TypesDoNotUnify

[ad-si]

I just refactored a big code base, and I felt like the type errors were unnecessary cryptic. Probably there are some good reasons for how they are right now that I'm not aware of. So I'll just drop my thoughts here and I hope one of you can enlighten me 😅.

This is the correct code:

add :: Int -> Int -> Int
add a b = a + b

test :: Int
test = add 1 2

Pass incorrect value

test :: Int
test = add 1 "string"

yields

[1/1 TypesDoNotUnify] src/Main.purs:14:14

  14  test = add 1 "string"
                   ^^^^^^^^

  Could not match type

    String

  with type

    Int

  while checking that type String
    is at least as general as type Int
  while checking that expression "string"
    has type Int
  in value declaration test

It's not obvious in one glance which type is the actual one and which is the
expected one. How about:

  Could not match encountered type

    String

  with expected type

    Int

Incorrect type annotation

add :: Int -> Int -> Int
add a b = a + (b :: String)

test :: Int
test = add 1 2

yields

[1/1 TypesDoNotUnify] src/Main.purs:11:16

  11  add a b = a + (b :: String)
                     ^^^^^^^^^^^

  Could not match type

    String

  with type

    Int

  while checking that type String
    is at least as general as type Int
  while checking that expression b
    has type Int
  in value declaration add

Maybe something like this is possible?:

  Could not match type annotation

    String

  with encountered type

    Int

Incorrect annotation and usage

add :: Int -> Int -> Int
add a b = a + (b :: String)

test :: Int
test = add 1 "string"

yields

[1/1 TypesDoNotUnify] src/Main.purs:11:16

  11  add a b = a + (b :: String)
                     ^^^^^^^^^^^

  Could not match type

    String

  with type

    Int

  while checking that type String
    is at least as general as type Int
  while checking that expression b
    has type Int
  in value declaration add

I feel like this should actually generate 2 errors.
One for using add differently than specified by its type signature and one for the implementation being incorrect.

I guess one problem right now is that implementations, type annotations, and signatures are somehow treated equally, where normally the importance is like: signature > annotation > implementation.
In the sense that my signature is what I want, but I my implementation isn't there yet. I think errors should be worded accordingly.

[garyb]

Re: "pass incorrect value"

There have been a number of discussions on this in the past (#3703, #3399, #3127, #2620), and there was a short period where an implementation of it was attempted but then reverted. Due to the typechecker being bi-directional it's somewhat seemingly random as to which type comes first just now, but even with some work on that there will still be many situations where it's subjective as to which is the "expected" type in the programmer's mind. This issue hasn't been given up on, #3399 is open, but it's not something that is going to be solved easily or in the immediate future.

Re: Incorrect type annotation

Type annotations will never be treated as incorrect, as they exist exactly for the programmer to tell the compiler "this is the type the value should be". Maybe b should have had length run on it before being fed into +, or perhaps some operator other than + should have been used instead, etc.

Re: Incorrect annotation and usage

See above answer again... but aside from that, the amount of "I know better than you" the compiler would have to do to suggest the kind of thing you're talking about here would be quite magical and, well, probably annoying :smile:. Since it seems what you're proposing is the compiler should look at both the implementation and usage of add, and from that determine that the signature is wrong. What if there were more correct usages of add than incorrect? Should it then only say that the usage is wrong? What if add is more often used in a 3rd incorrect way, would it only suggest that as being the correct one? etc. There's a lot of context required to propose the kind of error/suggestion you're talking about here, and even if it's technically possible to do it would probably make the typechecker a lot slower than it already is.

I'm not sure what you mean about the various aspects being treated equally, as they're not. Signature and annotation are not actually different things (they're indistinguishable in the type checker - it's just syntax in the source that differs), and if provided they are always accepted by the compiler as correct. Even if it seems nonsensical, because again, if you provide annotations the compiler isn't going to say "no, you're wrong", the assumption is the implementation is incorrect in some way instead.

[hdgarrood]

I agree with @garyb's analysis. So it looks like the first example is a duplicate of #3399, and the second two are wontfix. Can this be closed, then?