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

Source/DafnyCore/AST/Expressions/Expressions.cs

@@ -1078,6 +1078,24 @@ public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
   public IToken NameToken => tok;
 }
 
+/// <summary>
+/// An implicit identifier is used in the context of a ReturnStmt tacetly
+/// assigning a value to a Method's out parameter.
+/// </summary>
+public class ImplicitIdentifierExpr : IdentifierExpr {
+  public ImplicitIdentifierExpr(IToken tok, string name)
+    : base(tok, name) { }
+
+  /// <summary>
+  /// Constructs a resolved implicit identifier.
+  /// </summary>
+  public ImplicitIdentifierExpr(IToken tok, IVariable v)
+    : base(tok, v) { }
+
+  public override bool IsImplicit => true;
+}
+
+
 /// <summary>
 /// If an "AutoGhostIdentifierExpr" is used as the out-parameter of a ghost method or
 /// a method with a ghost parameter, resolution will change the .Var's .IsGhost to true

Source/DafnyCore/Resolver/Resolver.cs

@@ -9557,7 +9557,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
             foreach (Formal f in cmc.Outs) {
               Expression produceLhs;
               if (stmt is ReturnStmt) {
-                var ident = new IdentifierExpr(f.tok, f.Name);
+                var ident = new ImplicitIdentifierExpr(f.tok, f.Name);
                 // resolve it here to avoid capture into more closely declared local variables
                 ident.Var = f;
                 ident.Type = ident.Var.Type;
@@ -9742,7 +9742,12 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
           ExprRhs rr = (ExprRhs)s.Rhs;
           ResolveExpression(rr.Expr, resolutionContext);
           Contract.Assert(rr.Expr.Type != null);  // follows from postcondition of ResolveExpression
-          AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "RHS (of type {1}) not assignable to LHS (of type {0})");
+
+          if (s.Lhs is ImplicitIdentifierExpr { Var: Formal { InParam: false } }) {
+            AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "Method return value mismatch (expected {0}, got {1})");
+          } else {
+            AddAssignableConstraint(stmt.Tok, lhsType, rr.Expr.Type, "RHS (of type {1}) not assignable to LHS (of type {0})");
+          }
         } else if (s.Rhs is TypeRhs) {
           TypeRhs rr = (TypeRhs)s.Rhs;
           Type t = ResolveTypeRhs(rr, stmt, resolutionContext);

Test/dafny0/BitvectorResolution.dfy

@@ -35,8 +35,8 @@ module OrdinaryTypeChecking {
     x := b67 << 3;  // error: result not assignable to an int
     x := b67 << 3 as int;  // error: ditto (the "as" applies only to the "3")
     x := (b67 << 3) as int;
-    x := b67.RotateLeft(3);
-    x := b67.RotateRight(3);
+    x := b67.RotateLeft(3); // error: bitwise rotations produce bitvectors
+    x := b67.RotateRight(3); // error: ditto
     b67 := b67 << r;  // error: cannot shift by a real
     b67 := b67 << small;  // error: cannot shift by a real
     b67 := b67.RotateLeft(r);

Test/dafny0/ByMethodResolution.dfy.expect

@@ -1,5 +1,5 @@
 ByMethodResolution.dfy(17,6): Error: number of return parameters does not match declaration (found 2, expected 1)
-ByMethodResolution.dfy(25,4): Error: RHS (of type bv9) not assignable to LHS (of type real)
+ByMethodResolution.dfy(25,4): Error: Method return value mismatch (expected real, got bv9)
 ByMethodResolution.dfy(24,6): Error: RHS (of type int) not assignable to LHS (of type real)
 ByMethodResolution.dfy(63,13): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function with 'function method')
 ByMethodResolution.dfy(64,13): Error: a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')

Test/git-issues/git-issue-3125.dfy

@@ -0,0 +1,11 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Foo() returns (i: int) {
+    i := "explicit assignment";
+    return "implicit assignment";
+}
+
+function foo(): int {
+    "hello"
+}

Test/git-issues/git-issue-3125.dfy.expect

@@ -0,0 +1,4 @@
+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)
+3 resolution/type errors detected in git-issue-3125.dfy

docs/dev/news/3125.fix

@@ -0,0 +1 @@
+Do not refer to an implicit assignment in error messages on return statements