Add tests for issue 3860 and resolve it

Source/DafnyCore/Resolver/Resolver.cs

@@ -1828,6 +1828,7 @@ public class ModuleBindings {
  // add deconstructors now (that is, after the query methods have been added)
  foreach (DatatypeCtor ctor in dt.Ctors) {
  var formalsUsedInThisCtor = new HashSet<string>();
+ var duplicates = new HashSet<Formal>();
  foreach (var formal in ctor.Formals) {
  MemberDecl previousMember = null;
  var localDuplicate = false;
@@ -1837,6 +1838,7 @@ public class ModuleBindings {
  if (localDuplicate) {
  reporter.Error(MessageSource.Resolver, ctor,
  "Duplicate use of deconstructor name in the same constructor: {0}", formal.Name);
+ duplicates.Add(formal);
  } else if (previousMember is DatatypeDestructor) {
  // this is okay, if the destructor has the appropriate type; this will be checked later, after type checking
  } else {
@@ -1867,6 +1869,10 @@ public class ModuleBindings {
 
  ctor.Destructors.Add(dtor);
  }
+
+ foreach (var duplicate in duplicates) {
+ ctor.Formals.Remove(duplicate);
+ }
  }
 
  // finally, add any additional user-defined members

Test/git-issues/github-issue-3860.dfy

@@ -0,0 +1,15 @@
+// RUN: ! %baredafny verify %args %s > %t
+// RUN: %diff "%s.expect" "%t"
+
+datatype Type = 
+ | Cons()
+
+datatype Test = Test(
+ y : Type,
+ y : Type
+) 
+
+predicate pred(t: Test, t': Test)
+{
+ && t' == t.(y := Cons())
+}

Test/git-issues/github-issue-3860.dfy.expect

@@ -0,0 +1,2 @@
+github-issue-3860.dfy(7,16): Error: Duplicate use of deconstructor name in the same constructor: y
+1 resolution/type errors detected in github-issue-3860.dfy

docs/dev/news/3860.fix

@@ -0,0 +1 @@
+Prevent a compiler crash that could occur when a datatype constructor was defined that has multiple parameters with the same name.