From 8a1cd890191d8e92f0d478445740d9ee24086429 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 28 Oct 2014 23:19:34 -0700
Subject: Fixed type-inference bug that could create cycles in proxy type graph

---
 Source/Dafny/Resolver.cs | 49 ++++++++++++++++++++++++++++++++++--------------
 1 file changed, 35 insertions(+), 14 deletions(-)

(limited to 'Source/Dafny')

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;
-- 
cgit v1.2.3