From 0d003990dd503ceb9cc56e7fb590981e752b5cfa Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Tue, 2 Feb 2016 15:36:36 -0800
Subject: Fix issue 129. When looking for a constructor for which Dafny knows
 how to instantiate all it arguments, don't stop as soon as one instantiable
 constructor is found. Instead, figure out all instantiable constructors and
 then pick the best among these. A simple and reasonable "best" is an
 instantiable constructor that requires a minimal number of already
 constructed type arguments, and to break ties among these, pick the first one
 listed.

---
 Source/Dafny/Resolver.cs      | 23 ++++++++++++++++++-----
 Test/dafny4/Bug129.dfy        | 12 ++++++++++++
 Test/dafny4/Bug129.dfy.expect |  2 ++
 3 files changed, 32 insertions(+), 5 deletions(-)
 create mode 100644 Test/dafny4/Bug129.dfy
 create mode 100644 Test/dafny4/Bug129.dfy.expect

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bddf62e2..e47220d7 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4171,23 +4171,36 @@ namespace Microsoft.Dafny
       Contract.Ensures(!Contract.Result<bool>() || dt.DefaultCtor != null);
 
       // Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
+      DatatypeCtor defaultCtor = null;
+      List<TypeParameter> lastTypeParametersUsed = null;
       foreach (DatatypeCtor ctor in dt.Ctors) {
-        var typeParametersUsed = new List<TypeParameter>();
+        List<TypeParameter>  typeParametersUsed = new List<TypeParameter>();
         foreach (Formal p in ctor.Formals) {
           if (!CheckCanBeConstructed(p.Type, typeParametersUsed)) {
             // the argument type (has a component which) is not yet known to be constructable
             goto NEXT_OUTER_ITERATION;
           }
         }
-        // this constructor satisfies the requirements, so the datatype is allowed
-        dt.DefaultCtor = ctor;
+        // this constructor satisfies the requirements, check to see if it is a better fit than the 
+        // one found so far. By "better" it means fewer type arguments. Between the ones with
+        // the same number of the type arguments, pick the one shows first.
+        if (defaultCtor == null || typeParametersUsed.Count < lastTypeParametersUsed.Count)  { 
+          defaultCtor = ctor;
+          lastTypeParametersUsed = typeParametersUsed;
+        }
+
+      NEXT_OUTER_ITERATION: { }
+      }
+
+      if (defaultCtor != null) {
+        dt.DefaultCtor = defaultCtor;
         dt.TypeParametersUsedInConstructionByDefaultCtor = new bool[dt.TypeArgs.Count];
         for (int i = 0; i < dt.TypeArgs.Count; i++) {
-          dt.TypeParametersUsedInConstructionByDefaultCtor[i] = typeParametersUsed.Contains(dt.TypeArgs[i]);
+          dt.TypeParametersUsedInConstructionByDefaultCtor[i] = lastTypeParametersUsed.Contains(dt.TypeArgs[i]);
         }
         return true;
-      NEXT_OUTER_ITERATION: { }
       }
+
       // no constructor satisfied the requirements, so this is an illegal datatype declaration
       return false;
     }
diff --git a/Test/dafny4/Bug129.dfy b/Test/dafny4/Bug129.dfy
new file mode 100644
index 00000000..f6cf0fe8
--- /dev/null
+++ b/Test/dafny4/Bug129.dfy
@@ -0,0 +1,12 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Maybe<T> = Some(v:T) | None
+datatype B = B(b:Maybe<B>)
+
+datatype List<T> = Nil | Cons(T, List<T>)
+datatype Tree<T> = Nodes(children: List<Tree<T>>)
+
+
+
+
diff --git a/Test/dafny4/Bug129.dfy.expect b/Test/dafny4/Bug129.dfy.expect
new file mode 100644
index 00000000..a1c1f7b9
--- /dev/null
+++ b/Test/dafny4/Bug129.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
-- 
cgit v1.2.3