Fix issue #70. Check the ctors for equality before marking them as duplicates.

1 files changed, 7 insertions, 2 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 7f198946..568424f0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -833,8 +833,13 @@ namespace Microsoft.Dafny
             foreach (var kv in s.Ctors) {

               Tuple<DatatypeCtor, bool> pair;

               if (sig.Ctors.TryGetValue(kv.Key, out pair)) {

-                // mark it as a duplicate

-                sig.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);

+                // The same ctor can be imported from two different imports (e.g "diamond" imports), in which case, 

+                // they are not duplicates. For TopLevelDecls and static members, they are handled by 

+                // ReallyAmbiguousThing() during resolving.

+                if (kv.Value.Item1 != pair.Item1) {

+                  // mark it as a duplicate

+                  sig.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);

+                }

               } else {

                 // add new

                 sig.Ctors.Add(kv.Key, kv.Value);