Clearer Dafny's error messages about arguments being wrong, not parameters

[MikaelMayer]

Fixed #1697
The following illustrate the changes brought by this PR, which more accurately uses the argument position instead of the parameter position, and makes it clear that it's not the parameter the problem.

before: incorrect type of function argument named 'w' (expected nat, found real)
after:  incorrect argument type for function parameter 'w' (expected nat, found real)

before: incorrect type of constructor in-parameter named 't' (expected bool, found int)
after:  incorrect argument type for constructor in-parameter 't' (expected bool, found int)

before: incorrect type at index 0 for datatype constructor parameter named 'hd' (expected _T0, found int)
after:  incorrect argument type at index 0 for datatype constructor parameter 'hd' (expected _T0, found int)

before: incorrect type of method in-parameter at index 1 named 'b'
after:  incorrect argument type at index 1 for method in-parameter 'b'

before: incorrect type at index 0 for datatype constructor parameter named 'hd' (expected _T0, found int)
after:  incorrect argument type at index 0 for datatype constructor parameter 'hd' (expected _T0, found int)

before: incorrect type of method out-parameter 1 named 'c' (expected C, got int)
after:  incorrect return type at index 1 for method out-parameter 'c' (expected C, got int)

before: incorrect type of prefix lemma in-parameter at index 0
after:  incorrect argument type at index 0 for prefix lemma in-parameter

Moreover, I enhanced the following error messages when arguments are missing ("argument" => "parameter", type hint, actionable formulation instead of negative formulation, added index even if name is provided)

Before: ParameterResolution.dfy(27,15): Error: no actual argument passed for function argument 'z'
After:  ParameterResolution.dfy(27,15): Error: function parameter 'z' at index 2 requires an argument of type int

Before: ParameterResolution.dfy(30,14): Error: no actual argument passed for datatype constructor argument 1
After:  ParameterResolution.dfy(30,14): Error: datatype constructor parameter at index 1 requires an argument of type bool

[cpitclaudel]

I think this is better! I wonder if we could make things a bit shorter, though. In most cases these errors are seen in an IDE, where the types are more important than the variable name; maybe we could put that information first, instead of in a parenthesis. Here is what other languages do, for reference:

error[E0308]: mismatched types
 --> src/main.rs:6:22
  |
6 |     println!("{}", f("A"));
  |                      ^^^ expected `i32`, found `&str`

And here is C#:

Compilation error (line 11, col 39): The best overloaded method match for 'Program.f(int)' has some invalid arguments
Compilation error (line 11, col 41): Argument 1: cannot convert from 'string' to 'int'

[MikaelMayer]

I think this is better! I wonder if we could make things a bit shorter, though. In most cases these errors are seen in an IDE, where the types are more important than the variable name; maybe we could put that information first, instead of in a parenthesis. Here is what other languages do, for reference:

error[E0308]: mismatched types
 --> src/main.rs:6:22
  |
6 |     println!("{}", f("A"));
  |                      ^^^ expected `i32`, found `&str`

And here is C#:

Compilation error (line 11, col 39): The best overloaded method match for 'Program.f(int)' has some invalid arguments
Compilation error (line 11, col 41): Argument 1: cannot convert from 'string' to 'int'

I remark that both examples you give do not give the parameter name, which is one of the things that was asked earlier. In this sense, our error message is more friendly than their's.
But I agree, it would be nicer to re-render the line and hats below every error.

This can and should be done independently of this PR, actually

[keyboardDrummer]

As the discussion suggests, there might be further improvements possible, but I'm approving this since I think it's already an improvement.