Fix: Variable declarations in match cases, formals do not trigger err…

…ors anymore

This PR ensures that, in the case of branch duplication in resolution, exactly one branch reuses the same
variables as the original branch (local variable declarations, formals, and bound variables in patterns).

That way, we fix #2905 and moreover fix the previous issue that hovering other variables in match cases was not displaying type information

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

@@ -12113,12 +12113,26 @@ public override string ToString() {
     }
 
     private class ClonerKeepLocalVariablesIfTypeNotSet : Cloner {
-      public override LocalVariable CloneLocalVariable(LocalVariable local) {
-        if (local.type == null) {
+      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);
       }
     }
 
@@ -12129,7 +12143,7 @@ private static RBranchStmt CloneRBranchStmt(RBranchStmt branch) {
     }
 
     private static RBranchExpr CloneRBranchExpr(RBranchExpr branch) {
-      Cloner cloner = new Cloner();
+      Cloner cloner = new ClonerKeepLocalVariablesIfTypeNotSet();
       return new RBranchExpr(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), cloner.CloneExpr(branch.Body), cloner.CloneAttributes((branch.Attributes)));
     }
 
@@ -12654,14 +12668,14 @@ private IEnumerable<ExtendedPattern> FlattenDisjunctivePatterns(ExtendedPattern
     }
 
     private IEnumerable<NestedMatchCaseExpr> FlattenNestedMatchCaseExpr(NestedMatchCaseExpr c) {
-      var cloner = new Cloner();
+      var cloner = new ClonerKeepLocalVariablesIfTypeNotSet();
       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 = new ClonerKeepLocalVariablesIfTypeNotSet();
       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);