Fix: Variable declarations in match cases, formals do not trigger errors anymore

Source/DafnyCore/Cloner.cs

@@ -195,7 +195,7 @@ public virtual Type CloneType(Type t) {
       }
     }
 
-    public Formal CloneFormal(Formal formal) {
+    public virtual Formal CloneFormal(Formal formal) {
       Formal f = new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost,
         CloneExpr(formal.DefaultValue), formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation);
       return f;

Source/DafnyCore/Resolver.cs

@@ -12112,28 +12112,44 @@ public override string ToString() {
       }
     }
 
-    private class ClonerKeepLocalVariablesIfTypeNotSet : Cloner {
-      public override LocalVariable CloneLocalVariable(LocalVariable local) {
-        if (local.type == null) {
+    private class ClonerButIVariablesAreKeptOnce : Cloner {
+      private HashSet<IVariable> alreadyCloned = new();
+
+      private VT CloneIVariableHelper<VT>(VT local, Func<VT, VT> returnMethod) where VT : IVariable {
+        if (!alreadyCloned.Contains(local)) {
+          alreadyCloned.Add(local);
           return local;
         }
 
-        return base.CloneLocalVariable(local);
+        return returnMethod(local);
+      }
+
+      public override LocalVariable CloneLocalVariable(LocalVariable local) {
+        return CloneIVariableHelper(local, base.CloneLocalVariable);
+      }
+
+      public override Formal CloneFormal(Formal local) {
+        return CloneIVariableHelper(local, base.CloneFormal);
+      }
+      public override BoundVar CloneBoundVar(BoundVar local) {
+        return CloneIVariableHelper(local, base.CloneBoundVar);
       }
     }
 
+    private Cloner matchBranchCloner = new ClonerButIVariablesAreKeptOnce();
+
     // deep clone Patterns and Body
-    private static RBranchStmt CloneRBranchStmt(RBranchStmt branch) {
-      Cloner cloner = new ClonerKeepLocalVariablesIfTypeNotSet();
+    private RBranchStmt CloneRBranchStmt(RBranchStmt branch) {
+      Cloner cloner = matchBranchCloner;
       return new RBranchStmt(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), branch.Body.ConvertAll(x => cloner.CloneStmt(x)), cloner.CloneAttributes(branch.Attributes));
     }
 
-    private static RBranchExpr CloneRBranchExpr(RBranchExpr branch) {
-      Cloner cloner = new Cloner();
+    private RBranchExpr CloneRBranchExpr(RBranchExpr branch) {
+      Cloner cloner = matchBranchCloner;
       return new RBranchExpr(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), cloner.CloneExpr(branch.Body), cloner.CloneAttributes((branch.Attributes)));
     }
 
-    private static RBranch CloneRBranch(RBranch branch) {
+    private RBranch CloneRBranch(RBranch branch) {
       if (branch is RBranchStmt) {
         return CloneRBranchStmt((RBranchStmt)branch);
       } else {
@@ -12654,14 +12670,14 @@ private IEnumerable<ExtendedPattern> FlattenDisjunctivePatterns(ExtendedPattern
     }
 
     private IEnumerable<NestedMatchCaseExpr> FlattenNestedMatchCaseExpr(NestedMatchCaseExpr c) {
-      var cloner = new Cloner();
+      var cloner = matchBranchCloner;
       foreach (var pat in FlattenDisjunctivePatterns(c.Pat)) {
         yield return new NestedMatchCaseExpr(c.Tok, pat, c.Body, c.Attributes);
       }
     }
 
     private IEnumerable<NestedMatchCaseStmt> FlattenNestedMatchCaseStmt(NestedMatchCaseStmt c) {
-      var cloner = new Cloner();
+      var cloner = matchBranchCloner;
       foreach (var pat in FlattenDisjunctivePatterns(c.Pat)) {
         yield return new NestedMatchCaseStmt(c.Tok, pat, new List<Statement>(c.Body), c.Attributes);
       }

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

@@ -85,6 +85,53 @@ method CallDoIt() returns () {
 }");
     }
 
+
+    [TestMethod]
+    public async Task HoveringBoundVariablesFormalsLocalVariablesInMatchExprOrStatement() {
+      await AssertHover(@"
+datatype DT = A | B | C
+
+method M(dt: DT) {
+  match dt {
+    case C => 
+    case A | B => var x := (y => y)(1); assert x == 1;
+                      ^[```dafny\nx: int\n```]
+                            ^[```dafny\ny: int\n```]
+                                 ^[```dafny\ny: int\n```]
+  }
+}
+
+method M2(dt: DT) {
+  match dt {
+    case C => 
+    case _ => var x := (y => y)(1); assert x == 1;
+                  ^[```dafny\nx: int\n```]
+                        ^[```dafny\ny: int\n```]
+                             ^[```dafny\ny: int\n```]
+  }
+}
+
+function method F(dt: DT): int {
+  match dt {
+    case C => 0
+    case A | B => var x := (y => y)(1); assert x == 1; 0
+                      ^[```dafny\nx: int\n```]
+                            ^[```dafny\ny: int\n```]
+                                 ^[```dafny\ny: int\n```]
+  }
+}
+function method F2(dt: DT): int {
+  match dt {
+    case C => 0
+    case _ => var x := (y => y)(1); assert x == 1; 0
+                  ^[```dafny\nx: int\n```]
+                        ^[```dafny\ny: int\n```]
+                             ^[```dafny\ny: int\n```]
+  }
+}
+");
+    }
+
     [TestMethod]
     public async Task HoverReturnsBeforeVerificationIsComplete() {
       var documentItem = CreateTestDocument(NeverVerifies);

Test/patterns/OrPatterns.dfy

@@ -67,6 +67,40 @@ module Lists {
 
 import opened Lists
 
+module TestVariables {
+  datatype DT = A | B | C
+
+  method M(dt: DT) returns (j: int) {
+    match dt {
+      case C => return 0;
+      case A | B => var x := (y => y)(1); assert x == 1;
+        return x;
+    }
+  }
+
+  method M2(dt: DT) returns (j: int) {
+    match dt {
+      case C => return 0;
+      case _ => var x := (y => y)(1); assert x == 1;
+        return x;
+    }
+  }
+
+  function method F(dt: DT): int {
+    match dt {
+      case C => 0
+      case A | B => var x := (y => y)(1); assert x == 1; x
+    }
+  }
+  function method F2(dt: DT): int {
+    match dt {
+      case C => 0
+      case _ => var x := (y => y)(1); assert x == 1; x
+    }
+  }
+}
+import opened TestVariables
+
 method Main() {
   expect One.Even() == One.Even'() == One.Even''() == false;
   expect Two.Even() == Two.Even'() == Two.Even''() == true;
@@ -80,6 +114,16 @@ method Main() {
   expect ContainsOne(a2) == ContainsOne'(a2) == true;
   var a3 := Cons(0, Cons(0, Cons(1, Nil)));
   expect ContainsOne(a3) == ContainsOne'(a3) == true;
-
+
+  var b0 := M(A);
+  var b1 := M(B);
+  var b2 := M2(A);
+  var b3 := M2(B);
+  var b4 := F(A);
+  var b5 := F(B);
+  var b6 := F2(A);
+  var b7 := F2(B);
+  expect 1 == b0 == b1 == b2 == b3 == b4 == b5 == b6 == b7;
+
   print "OK\n";
 }

Test/patterns/OrPatterns.dfy.expect

@@ -1,3 +1,3 @@
 
-Dafny program verifier finished with 7 verified, 0 errors
+Dafny program verifier finished with 11 verified, 0 errors
 OK

docs/dev/news/2910.fix

@@ -0,0 +1 @@
+Variable declarations and formals in match cases do not trigger errors anymore.