Name resolution error

[MikaelMayer]

datatype DT = DT {
  static method m(){}
}

datatype DD = AA | BB | CC
{
  method problem() {
    match this {
      case CC =>
      case _ =>
        var a := "value";
        DT.m();
    }
  }
}

This minimal code, if executed with Dafny, will trigger the following error:

file.dfy(11,12): Error:
 more than one declaration of variable name: a#1_0
1 name resolution errors detected in file.bpl

*** Encountered internal translation error - re-running Boogie to get better deb
ug information

file.bpl(3069,6): Error: more than
one declaration of variable name: a#1_0
1 name resolution errors detected in file.bpl

[MikaelMayer]

Two workarounds for now, until @keyboardDrummer or myself find a fix

1. Declare the variable a before the match case statement.
2. Wrap the second case in a match true { case true => ... }

[keyboardDrummer]

I think this PR will fix it: #2734

[cpitclaudel]

The issue seems to be new in 3.8.0; the original example was OK in 3.7.3.
The following shows a variant of this problem, I think:

datatype DT = A | B

method M(dt: DT) {
  match dt {
    case A | B => var x := 1; assert x == 1;
  }
}

function method F(dt: DT): int {
  match dt {
    case A | B => var x := 1; assert x == 1; 0
  }
}

[cpitclaudel]

Looks like we might be able to fix this before the refactoring by reverting / fixing this commit:

commit d65085d22a97371ac33c77de7e77b3b95a41acbb
Date:   Fri Jul 29 13:50:32 2022 -0500

    Fix: null pointer exception in the case of hovering local variables (#2437)

[keyboardDrummer]

Looks like we might be able to fix this before the refactoring by reverting / fixing this commit:

Yes, I'd be in favour of that, although note that it would break the hover feature in the IDE which #2437 fixed.

[cpitclaudel]

I wonder why we use OptionalType and null instead of Type with an InferredProxyType; do you know?
If we were using an InferredProxyType we could share that between duplicated variables.
Or at the very least we wouldn't have a crash (we just wouldn't know the type of the variable)

Bad patch:

diff --git a/Source/DafnyCore/Cloner.cs b/Source/DafnyCore/Cloner.cs
index ccfe66355..a01ce6e53 100644
--- a/Source/DafnyCore/Cloner.cs
+++ b/Source/DafnyCore/Cloner.cs
@@ -208,7 +208,7 @@ namespace Microsoft.Dafny {
     }
 
     public virtual LocalVariable CloneLocalVariable(LocalVariable local) {
-      return new LocalVariable(Tok(local.Tok), Tok(local.EndTok), local.Name, CloneType(local.OptionalType), local.IsGhost);
+      return new LocalVariable(Tok(local.Tok), Tok(local.EndTok), local.Name, local.OptionalType, local.IsGhost);
     }
     public virtual VT CloneIVariable<VT>(VT v) where VT : IVariable {
       var iv = (IVariable)v;
diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs
index 3cd4261f0..c90d816ee 100644
--- a/Source/DafnyCore/Resolver.cs
+++ b/Source/DafnyCore/Resolver.cs
@@ -12174,7 +12174,7 @@ namespace Microsoft.Dafny {
     private class ClonerKeepLocalVariablesIfTypeNotSet : Cloner {
       public override LocalVariable CloneLocalVariable(LocalVariable local) {
         if (local.type == null) {
-          return local;
+          local.type = new InferredTypeProxy();
         }
 
         return base.CloneLocalVariable(local);