Better error message for confusing ":=" with "=".

lukaszcz commented 2 years ago

If I write

id : (A : Type) → A → A;
id _ a = a;

I get the error message

   |
23 | id _ a = a;
   |           ^^
unexpected ";<newline>"
expecting ":=", '(', '.', '_', '{', or '≔'

which is pretty bad, because it doesn't explain what really is wrong ("=" instead of ":=") and doesn't point at the source of the problem but at the end of the line.

The error message should be improved. This issue comes up very often for novices, and one occasionally gets confused even after some time using Juvix.

jonaprieto commented 2 years ago

Closed by https://github.com/anoma/juvix/pull/1535

lukaszcz commented 1 year ago

Currently, I get the following error:

/home/heliax/Documents/juvix/juvix-stdlib/Stdlib/Data/Nat.juvix:23:18: error:
/home/heliax/Documents/juvix/juvix-stdlib/Stdlib/Data/Nat.juvix:23:18:
   |
23 | div zero b = zero;
   |                  ^
unexpected ';'
expecting '.', :=, <pattern>, or @

It's still quite confusing. := is just one among many suggestions and the error points at the end of the line. It's even worse if the definition is multi-line, because then you even don't see the = in the error message, only the last line.

The error message should point at the = sign and/or strongly suggest that the user probably meant := instead of =. This is such a common case that I think there is no excuse for producing a suboptimal error message here.

anoma / juvix

Better error message for confusing ":=" with "=". #1483