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.

3 files changed, 32 insertions, 5 deletions

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