Keep type synonyms in some special cases (#1086)

Co-authored-by: David Cok <[email protected]>

Author: RustanLeino

Source/Dafny/DafnyAst.cs

@@ -1843,6 +1843,11 @@ public static Type MeetX(Type a, Type b, BuiltIns builtIns) {
       Contract.Requires(b != null);
       Contract.Requires(builtIns != null);
 
+      // As a special-case optimization, check for equality here, which will better preserve un-expanded type synonyms
+      if (a.Equals(b, true)) {
+        return a;
+      }
+
       // Before we do anything else, make a note of whether or not both "a" and "b" are non-null types.
       var abNonNullTypes = a.IsNonNullRefType && b.IsNonNullRefType;
 

Source/Dafny/Resolver.cs

@@ -4378,7 +4378,7 @@ private bool AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, boo
       Contract.Requires(!(t is TypeProxy));
       Contract.Requires(!(t is ArtificialType));
 
-      t = keepConstraints ? t.NormalizeExpandKeepConstraints() : t.NormalizeExpand();
+      t = keepConstraints ? t.Normalize() : t.NormalizeExpand();
       // never violate the type constraint of a literal expression
       var followedRequestedAssignment = true;
       foreach (var su in proxy.Supertypes) {
@@ -6051,7 +6051,7 @@ bool AssignKnownEndsFullstrength_SuperDirection(TypeProxy proxy) {
       var meets = new List<Type>();
       foreach (var xc in AllXConstraints) {
         if (xc.ConstraintName == "Assignable" && xc.Types[1].Normalize() == proxy) {
-          var su = xc.Types[0].NormalizeExpandKeepConstraints();
+          var su = xc.Types[0].Normalize();
           if (su is TypeProxy) {
             continue;  // don't include proxies in the meet computation
           }

Test/git-issues/git-issue-623.dfy

@@ -0,0 +1,107 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// ----- example reported in Issue 623
+
+module M1 {
+  export Abs
+    provides M, T
+  export Conc
+    provides M, MyClass
+    reveals T
+
+  class MyClass {
+  }
+
+  type T = MyClass
+
+  lemma M(f: T ~> bool)
+    requires forall t :: f.requires(t) ==> f(t)  // regression test: this once crashed during checking of M2
+  { }
+}
+
+module M2 {
+  import M1`Abs
+
+  method K(t: M1.T) {
+  }
+}
+
+module M3 {
+  import M1`Conc
+
+  method K(t: M1.T) {
+  }
+}
+
+// ----- example reported in Issue 150
+
+module N1 {
+  export
+    provides T, Equal, Foo
+
+  type T(==) = seq<real>
+
+  predicate Equal(u: T, v: T)
+  {
+    u == v
+  }
+
+  lemma Foo()
+    ensures forall u, v :: Equal(u, v) ==> u == v  // regression test: this once crashed during checking of N2
+  { }
+}
+
+module N2 {
+  import N1
+
+  lemma Bar(u: N1.T, v: N1.T)
+    requires N1.Equal(u, v)
+  {
+    N1.Foo();
+    assert u == v;
+  }
+}
+
+
+// ------------------- additional examples
+
+module Library {
+  export
+    provides W, P, X, Q
+    provides M0, M1
+
+  type W = MyTrait
+  trait MyTrait {
+  }
+  predicate P(u: W)
+
+  type X = MyClass
+  class MyClass extends MyTrait {
+  }
+  predicate Q(x: X)
+
+  lemma M0()
+    requires forall t :: P(t)
+  { }
+  lemma M1()
+    requires forall t :: Q(t)
+  { }
+
+  lemma Private0()
+    requires forall t :: P(t) && Q(t)  // error: t is inferred as MyTrait, so can't prove that Q(t) is well-formed
+  { }
+  lemma Private1()
+    requires forall t :: Q(t) && P(t)  // error: t is inferred as MyTrait, so can't prove that Q(t) is well-formed
+  { }
+}
+
+module Client {
+  import Library
+
+  method K()
+    requires forall t :: Library.P(t)
+    requires forall t :: Library.Q(t)
+  {
+  }
+}

Test/git-issues/git-issue-623.dfy.expect

@@ -0,0 +1,8 @@
+git-issue-623.dfy(92,35): Error: the RHS value (a MyTrait) is not known to be an instance of the LHS type (MyClass)
+Execution trace:
+    (0,0): anon0
+git-issue-623.dfy(95,27): Error: the RHS value (a MyTrait) is not known to be an instance of the LHS type (MyClass)
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 2 errors