Do not refer to an implicit assignment in error messages on return stmts

[dijkstracula]

I had a bit of time this morning, and since #3125 was derived from an essentially-not-an-issue issue that I filed, made sense that I should take a swing at resolving it!

Previously, a type error in a method return statement refers to an assignment, because the Resolver treats a return as an implicit update to the named return variable. This patch checks whether an assignment is updating a formal outparameter and produces a more specific error message if so.

Given the following Dafny program,

method Foo(s: string) returns (i : int) {
    i := "hello";
    return "hi";
}

function foo(): int {
    "hello"
}

The errors produced are:

git-issue-3125.dfy(5,6): Error: RHS (of type string) not assignable to LHS (of type int)
git-issue-3125.dfy(6,4): Error: Method return value mismatch (expected int, got string)
git-issue-3125.dfy(9,9): Error: Function body type mismatch (expected int, got string)

This also updates existing unit tests that expected the old error message - I think I've caught them all but CI will let me know if I'm wrong :-)

Fixes #3125

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[dijkstracula]

Note that a consequence of this patch is that direct assignments to the named return variable talk about the return type of the method, rather than the assignment.

+++ b/Test/dafny0/ConstantErrors.dfy
@@ -41,7 +41,7 @@ module D {  // const's with inferred types

   newtype SmallInt = x | 0 <= x < 100
   method M() returns (sm: SmallInt) {
-    sm := ten;  // error: "int" is not assignable to "Smallint"
+    sm := ten;  // Method return value mismatch (expecting SmallInt, got int)
   }

Personally, I don't think this is confusing, but I don't know if folks have strong opinions about this; given that during treewalking, at the point of reporting the type error we've forgotten whether the statement is an UpdateStmt or a ReturnStmt, I'm not sure there's an ideal solution here that isn't super-invasive...

[MikaelMayer]

That sounds great ! I have an idea to mitigate the effect and use this new error message more precisely. See my comments.