Check for proper use of equality-supporting types also in local variables and forall statements, and more expressions

5 files changed, 182 insertions, 16 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index a0912f19..e7cf1108 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -342,14 +342,9 @@ namespace Microsoft.Dafny {
         } else {

           var syn = type.AsTypeSynonym;

           if (syn != null) {

+            var udt = (UserDefinedType)type;  // correctness of cast follows from the AsTypeSynonym != null test.

             // Instantiate with the actual type arguments

-            if (syn.TypeArgs.Count == 0) {

-              // this optimization seems worthwhile

-              type = syn.Rhs;

-            } else {

-              var subst = Resolver.TypeSubstitutionMap(syn.TypeArgs, ((UserDefinedType)type).TypeArgs);

-              type = Resolver.SubstType(syn.Rhs, subst);

-            }

+            type = syn.RhsWithArgument(udt.TypeArgs);

           } else {

             return type;

           }

@@ -589,7 +584,9 @@ namespace Microsoft.Dafny {
     }

     public override bool SupportsEquality {

       get {

-        return Arg.SupportsEquality;

+        // Note that all collection types support equality. There is, however, a requirement (checked during resolution)

+        // that the argument types of collections support equality.

+        return true;

       }

     }

   }

@@ -867,7 +864,7 @@ namespace Microsoft.Dafny {
           return true;

         } else if (ResolvedClass is TypeSynonymDecl) {

           var t = (TypeSynonymDecl)ResolvedClass;

-          return t.Rhs.SupportsEquality;

+          return t.RhsWithArgument(TypeArgs).SupportsEquality;

         } else if (ResolvedParam != null) {

           return ResolvedParam.MustSupportEquality;

         }

@@ -2003,6 +2000,21 @@ namespace Microsoft.Dafny {
       Contract.Requires(rhs != null);

       Rhs = rhs;

     }

+    /// <summary>

+    /// Returns the declared .Rhs but with formal type arguments replaced by the given actuals.

+    /// </summary>

+    public Type RhsWithArgument(List<Type> typeArgs) {

+      Contract.Requires(typeArgs != null);

+      Contract.Requires(typeArgs.Count == TypeArgs.Count);

+      // Instantiate with the actual type arguments

+      if (typeArgs.Count == 0) {

+        // this optimization seems worthwhile

+        return Rhs;

+      } else {

+        var subst = Resolver.TypeSubstitutionMap(TypeArgs, typeArgs);

+        return Resolver.SubstType(Rhs, subst);

+      }

+    }

   }

 

   [ContractClass(typeof(IVariableContracts))]

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index a96efb8b..73568fcf 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -138,9 +138,7 @@ namespace Microsoft.Dafny {
           if (i++ != 0) { wr.WriteLine(); }

           Indent(indent);

           PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());

-          if (at.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {

-            wr.Write("(==)");

-          }

+          wr.Write(EqualitySupportSuffix(at.EqualitySupport));

           wr.WriteLine();

         } else if (d is TypeSynonymDecl) {

           var syn = (TypeSynonymDecl)d;

@@ -336,7 +334,7 @@ namespace Microsoft.Dafny {
       if (typeArgs.Count != 0) {

         wr.Write("<" +

                  Util.Comma(", ", typeArgs,

-                   tp => tp.Name + (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Required ? "(==)" : ""))

+                   tp => tp.Name + EqualitySupportSuffix(tp.EqualitySupport))

                  + ">");

       }

     }

@@ -617,6 +615,15 @@ namespace Microsoft.Dafny {
       }

     }

 

+    string EqualitySupportSuffix(TypeParameter.EqualitySupportValue es) {

+      if (es == TypeParameter.EqualitySupportValue.Required ||

+        (es == TypeParameter.EqualitySupportValue.InferredRequired && DafnyOptions.O.DafnyPrintResolvedFile != null)) {

+        return "(==)";

+      } else {

+        return "";

+      }

+    }

+

     // ----------------------------- PrintStatement -----------------------------

 

     /// <summary>

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d391ab4e..4d19338b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2430,6 +2430,11 @@ namespace Microsoft.Dafny
       protected override bool VisitOneStmt(Statement stmt, ref bool st) {

         if (stmt.IsGhost) {

           return false;  // no need to recurse to sub-parts, since all sub-parts must be ghost as well

+        } else if (stmt is VarDeclStmt) {

+          var s = (VarDeclStmt)stmt;

+          foreach (var v in s.Locals) {

+            CheckEqualityTypes_Type(v.Tok, v.Type);

+          }

         } else if (stmt is WhileStmt) {

           var s = (WhileStmt)stmt;

           // don't recurse on the specification parts, which are ghost

@@ -2478,6 +2483,11 @@ namespace Microsoft.Dafny
             i++;

           }

           return false;  // we've done what there is to be done

+        } else if (stmt is ForallStmt) {

+          var s = (ForallStmt)stmt;

+          foreach (var v in s.BoundVars) {

+            CheckEqualityTypes_Type(v.Tok, v.Type);

+          }

         }

         return true;

       }

@@ -2558,6 +2568,9 @@ namespace Microsoft.Dafny
             i++;

           }

           return false;  // we've done what there is to be done

+        } else if (expr is SetDisplayExpr || expr is MultiSetDisplayExpr || expr is MapDisplayExpr || expr is MultiSetFormingExpr) {

+          // This catches other expressions whose type may potentially be illegal

+          CheckEqualityTypes_Type(expr.tok, expr.Type);

         }

         return true;

       }

@@ -2618,6 +2631,8 @@ namespace Microsoft.Dafny
             }

           }

 

+        } else if (type is TypeProxy) {

+          // the type was underconstrained; this is checked elsewhere, but it is not in violation of the equality-type test

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

         }

@@ -5200,7 +5215,7 @@ namespace Microsoft.Dafny
         } else if (update.Lhss.Count != update.Rhss.Count) {

           Error(update, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", update.Lhss.Count, update.Rhss.Count);

         } else if (ErrorCount == errorCountBeforeCheckingLhs) {

-          // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)

+          // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translate properly as multi-assignment)

           for (int i = 0; i < update.Lhss.Count; i++) {

             var a = new AssignStmt(update.Tok, update.EndTok, update.Lhss[i].Resolved, update.Rhss[i]);

             update.ResolvedStatements.Add(a);

@@ -6687,7 +6702,7 @@ namespace Microsoft.Dafny
               c++;

             }

             if (c == 0) {

-              // Every identifier-looking thing in the patterned resolved to a constructor; that is, this LHS is a constant literal

+              // Every identifier-looking thing in the pattern resolved to a constructor; that is, this LHS is a constant literal

               Error(lhs.tok, "LHS is a constant literal; to be legal, it must introduce at least one bound variable");

             }

             i++;

diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy
index a327fd1d..c04ee2c1 100644
--- a/Test/dafny0/EqualityTypes.dfy
+++ b/Test/dafny0/EqualityTypes.dfy
@@ -135,3 +135,109 @@ module Gh {
     }

   }

 }

+

+// ------ deeper nesting ------

+

+module Deep {

+  codatatype Co = Mo(Co) | NoMo

+  class C<T> { }

+

+  method M(a: set<C<Co>>) {

+    var s: set<C<Co>>;

+    var t: set<Co>;  // error: set element type must support equality

+    var co: Co;

+    var d := G(co, NoMo);  // error: actual type parameter for Y (namely, Co) does

+                           // not support equality

+    d := G(t, t) + G(s, s);  // fine, because all sets support equality

+  }

+

+  function method G<Y(==)>(y: Y, z: Y): int { if y == z then 5 else 7 }

+

+  method P(b: set<Co>) {  // error: set element type must be a type with equality

+  }

+

+  ghost method Q(b: set<Co>) {  // fine, since this is a ghost method

+  }

+

+  method R(ghost b: set<Co>) {  // fine, since this is a ghost parameter

+  }

+

+  datatype Dt<T> = Bucket(T)

+  datatype Left<T,U> = Bucket(T)

+  datatype Right<T,U> = Bucket(set<U>)  // note, Dafny infers that U should be U(==)

+  datatype RightExplicit<T,U(==)> = Bucket(set<U>)

+  type Syn<A,B,C> = Left<C,A>

+

+  method W<alpha(==)>()

+  {

+    var a: set<Dt<Co>>;  // error: Dt<Co> does not support equality

+    var b: set<Dt<int>>;

+    var c: set<Left<int,Co>>;

+    var d: set<Left<Co,int>>;  // error: Left<Co,...> does not support equality

+    var e: set<Right<Co,Co>>;  // error: type parameter 1 to Right is required to support equality

+    ghost var e': set<Right<Co,Co>>;  // fine, since this is a ghost field

+    var e'': set<RightExplicit<Co,Co>>;  // error: cannot instantiate argument 1 with Co

+    var f: set<Syn<Co,Co,int>>;

+    var g: set<Syn<int,int,Co>>;  // error: Syn<int,int,Co> does not support equality

+    ghost var h: set<Syn<int,int,Co>>;  // in a ghost context, it's cool, though

+

+    var i;  // error: inferred type (set<Co>) uses invalid set-element type

+    var j: set;  // error: ditto

+    ghost var k: set<Co>;  // type allowed here, because it's a ghost

+    assert i == k || j == k || true;  // this infers the types of 'i' and 'j'

+  }

+

+  method StatementsWithVariables(a: set<C<Co>>) {

+    var s: set<C<Co>>;

+    var t: set<Co>;  // error: bad type

+    ghost var u: set<Co>;

+

+    var c := new ABC;

+    forall x | x in {t} {  // error: bad type for x

+      c.f := 0;

+    }

+    if t == u {

+      forall x | x in {t}  // fine, because this is a ghost statement

+        ensures true;

+      {

+      }

+    }

+  }

+

+  class ABC { var f: int; }

+

+  method Expressions() {

+    var t: set<Co>;  // error: bad type

+    var b := forall x | x in {t} :: x == x;  // error: bad type

+    var y := var k: set<Co> := t; k <= t;  // error: bad type

+  }

+

+  ghost method GhostThings0(t: set<Co>) {

+    assert forall x | x in {t} :: x == x;

+    var y := var k: set<Co> := t; k <= t;

+    assert y;

+  }

+

+  method GhostThings1(ghost t: set<Co>) {

+    assert forall x | x in {t} :: x == x;

+    ghost var y := var k: set<Co> := t; k <= t;

+    assert y;

+  }

+

+  method InferEqualitySupportIsRequired<A>(s: set<A>)

+  ghost method DontInferEqualitySupportIsRequired<A>(s: set<A>)

+  method Explicit<A(==)>(s: set<A>)

+  method TakesABoolean(b: bool)

+  method AClient(co: Co, ko: Co) {

+    Explicit({5});

+    Explicit({co});  // error: bad type

+    var b := ko in {co};  // error: bad type (argument for the set)

+    ghost var bg := ko in {co};  // fine, it's a ghost

+    InferEqualitySupportIsRequired({co});  // error: bad type

+    DontInferEqualitySupportIsRequired({co});

+    TakesABoolean(ko in {co});  // error: bad type

+    var x := multiset([co,ko,co,ko])[ko];  // error: bad type

+    var m0 := map[5 := ko];  // no prob

+    var m1 := map[ko := 5];  // error: bad type

+  }

+}

diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index 70e46ff0..f296ed4b 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -9,4 +9,30 @@ EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must sup
 EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)

 EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)

-11 resolution/type errors detected in EqualityTypes.dfy

+EqualityTypes.dfy(147,8): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(149,13): Error: type parameter 0 (Y) passed to function G must support equality (got Co)

+EqualityTypes.dfy(156,11): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(173,8): Error: set argument type must support equality (got Dt<Co>)

+EqualityTypes.dfy(176,8): Error: set argument type must support equality (got Left<Co,int>)

+EqualityTypes.dfy(177,8): Error: type parameter 1 (U) passed to type Right must support equality (got Co)

+EqualityTypes.dfy(179,8): Error: type parameter 1 (U) passed to type RightExplicit must support equality (got Co)

+EqualityTypes.dfy(181,8): Error: set argument type must support equality (got Syn<int,int,Co>)

+EqualityTypes.dfy(184,8): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(185,8): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(192,8): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(196,11): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(196,20): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(210,8): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(211,20): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(211,29): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(212,17): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(233,4): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)

+EqualityTypes.dfy(233,13): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(234,19): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(236,4): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)

+EqualityTypes.dfy(236,35): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(238,24): Error: set argument type must support equality (got Co)

+EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)

+EqualityTypes.dfy(241,8): Error: map domain type must support equality (got Co)

+EqualityTypes.dfy(241,14): Error: map domain type must support equality (got Co)

+37 resolution/type errors detected in EqualityTypes.dfy