Fixed type-inference bug that could create cycles in proxy type graph

3 files changed, 64 insertions, 15 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 01ef0a4b..fe7d80d5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4162,11 +4162,34 @@ namespace Microsoft.Dafny
       if (t is NatType) {

         proxy.T = Type.Int;

       } else {

-        proxy.T = t;

+        return AssignProxyAfterCycleCheck(proxy, t);

       }

       return true;

     }

 

+    bool AssignProxyAfterCycleCheck(TypeProxy proxy, Type t) {

+      Contract.Requires(proxy != null && proxy.T == null);

+      Contract.Requires(t != null);

+      if (TypeArgumentsIncludeProxy(t, proxy)) {

+        return false;

+      } else {

+        proxy.T = t;

+        return true;

+      }

+    }

+

+    bool TypeArgumentsIncludeProxy(Type t, TypeProxy proxy) {

+      Contract.Requires(t != null);

+      Contract.Requires(proxy != null);

+      foreach (var ta in t.TypeArgs) {

+        var a = ta.Normalize();

+        if (a == proxy || TypeArgumentsIncludeProxy(a, proxy)) {

+          return true;

+        }

+      }

+      return false;

+    }

+

     bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -4195,9 +4218,8 @@ namespace Microsoft.Dafny
           // Note, we're calling ResolvedArrayType here, which in turn calls ResolveType on ib.Arg.  However, we

           // don't need to worry about what ICodeContext we're passing in, because ib.Arg should already have been

           // resolved.

-          a.T = ResolvedArrayType(Token.NoToken, 1, ib.Arg, new DontUseICallable());

-          b.T = a.T;

-          return UnifyTypes(ib.Arg, ib.Range);

+          var c = ResolvedArrayType(Token.NoToken, 1, ib.Arg, new DontUseICallable());

+          return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c) && UnifyTypes(ib.Arg, ib.Range);

         } else {

           return false;

         }

@@ -4212,8 +4234,8 @@ namespace Microsoft.Dafny
             b.T = a;  // a is a stronger constraint than b

           } else {

             // a says set<T>,seq<T> and b says numeric,set; the intersection is set<T>

-            a.T = new SetType(((CollectionTypeProxy)a).Arg);

-            b.T = a.T;

+            var c = new SetType(((CollectionTypeProxy)a).Arg);

+            return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c);

           }

           return true;

         } else if (b is IndexableTypeProxy) {

@@ -4256,8 +4278,9 @@ namespace Microsoft.Dafny
             a.T = b;  // b has the stronger requirement

           } else {

             Type c = !i && !r && h && !q && !s ? new CharType() : (Type)new OperationTypeProxy(i, r, h, q, s);

-            a.T = c;

-            b.T = c;

+            // the calls to AssignProxyAfterCycleCheck are needed only when c is a non-proxy type, but it doesn't

+            // hurt to do them in both cases

+            return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c);

           }

           return true;

         } else {

@@ -4267,14 +4290,12 @@ namespace Microsoft.Dafny
           // So, the intersection could include multiset and seq.

           if (pa.AllowSetVarieties && !pa.AllowSeq) {

             // strengthen a and b to a multiset type

-            b.T = new MultiSetType(ib.Arg);

-            a.T = b.T;

-            return true;

+            var c = new MultiSetType(ib.Arg);

+            return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c);

           } else if (pa.AllowSeq && !pa.AllowSetVarieties) {

             // strengthen a and b to a sequence type

-            b.T = new SeqType(ib.Arg);

-            a.T = b.T;

-            return true;

+            var c = new SeqType(ib.Arg);

+            return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c);

           } else if (!pa.AllowSeq && !pa.AllowSetVarieties) {

             // over-constrained

             return false;

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 6086fcf1..141e48cb 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -144,3 +144,28 @@ ghost method GhostM() returns (x: int)
 {

   x :| true;  // no problem (but there once was a problem with this case, where an error was generated for no reason)

 }

+

+// ------------------ cycles that could arise from proxy assignments ---------

+

+module ProxyCycles {

+  datatype Dt<X> = Ctor(X -> Dt<X>)

+  method M0()

+  {

+    var dt: Dt<int>;

+    var f := x => x;

+    dt := Ctor(f);  // error: cannot infer a type for f

+  }

+  method M1()

+  {

+    var dt: Dt;

+    var f := x => x;

+    dt := Ctor(f);  // error: cannot infer a type for f

+  }

+

+  function method F<X>(x: X): set<X>

+  method N()

+  {

+    var x;

+    x := F(x);  // error: cannot infer type for x

+  }

+}

diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 5d78fe16..55fc916c 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -1,3 +1,6 @@
+TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

+TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)

+TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)

 TypeTests.dfy(7,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(7,13): Error: incorrect type of function argument 1 (expected D, got C)

 TypeTests.dfy(8,13): Error: incorrect type of function argument 0 (expected C, got int)

@@ -31,4 +34,4 @@ TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification
 TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-33 resolution/type errors detected in TypeTests.dfy

+36 resolution/type errors detected in TypeTests.dfy