fix: Infer (==) for non-null iterator type

Fixes dafny-lang#3273

Source/DafnyCore/Resolver/Resolver.cs

@@ -3059,12 +3059,17 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
  if (d is IteratorDecl) {
  var iter = (IteratorDecl)d;
  var done = false;
- foreach (var tp in iter.TypeArgs) {
+ var nonnullIter = iter.NonNullTypeDecl;
+ Contract.Assert(nonnullIter.TypeArgs.Count == iter.TypeArgs.Count);
+ for (var i = 0; i < iter.TypeArgs.Count; i++) {
+ var tp = iter.TypeArgs[i];
+ var correspondingNonnullIterTypeParameter = nonnullIter.TypeArgs[i];
  if (tp.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
  // here's our chance to infer the need for equality support
  foreach (var p in iter.Ins) {
  if (InferRequiredEqualitySupport(tp, p.Type)) {
  tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
+ correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
  done = true;
  break;
  }
@@ -3076,6 +3081,7 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
 
  if (InferRequiredEqualitySupport(tp, p.Type)) {
  tp.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
+ correspondingNonnullIterTypeParameter.Characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
  break;
  }
  }

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

@@ -0,0 +1,54 @@
+// RUN: %exits-with 2 %dafny "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+iterator Iter<Y>(u: set<Y>) // this infers Y to be (==)
+
+method Repro<K>() {
+ var iter: Iter<K>; // error: K is not (==)
+}
+
+iterator IterA<X(==)>() // this declares X to be (==)
+
+iterator IterB<Y>(u: set<Y>) // this infers Y to be (==)
+
+method Test<K, L(==)>() {
+ var a0: IterA<K>; // error: K is not (==)
+ var a1: IterA<L>;
+ var b0: IterB<K>; // error: K is not (==)
+ var b1: IterB<L>;
+
+ var c0: IterA?<K>; // error: K is not (==)
+ var c1: IterA?<L>;
+ var d0: IterB?<K>; // error: K is not (==)
+ var d1: IterB?<L>;
+}
+
+iterator EqIter<Y>(u: set<Y>, x: Y, y: Y) yields (eq: bool)
+ yield ensures eq == (x == y)
+ ensures false
+{
+ while true {
+ yield x == y;
+ }
+}
+
+datatype Dt = Dt(a: int, ghost b: int)
+
+method Main() {
+ var d0 := Dt(0, 0);
+ var d1 := Dt(0, 1);
+ assert d0 != d1; // clearly
+
+ // The following is error (but was not always detected by Dafny), because EqIter should take a (==) type argument.
+ var iter: EqIter<Dt>; // error: Dt is not an equality-supporting type
+ // The following does give an error, since the constructor lives in class EqIter whose
+ // type parameer has been inferred to be (==).
+ iter := new EqIter({}, d0, d1); // error: Dt is not an equality-supporting type
+ var more := iter.MoveNext();
+ assert more;
+ assert iter.eq == (d0 == d1) == false; // according to the yield-ensures clause
+ print iter.eq, "\n";
+ if iter.eq {
+ var ugh := 1 / 0; // according to the verifier, we never get here
+ }
+}

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

@@ -0,0 +1,9 @@
+git-issue-3273.dfy(7,12): Error: type parameter (Y) passed to type Iter must support equality (got K) (perhaps try declaring type parameter 'K' on line 6 as 'K(==)', which says it can only be instantiated with a type that supports equality)
+git-issue-3273.dfy(15,10): Error: type parameter (X) passed to type IterA must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality)
+git-issue-3273.dfy(17,10): Error: type parameter (Y) passed to type IterB must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality)
+git-issue-3273.dfy(20,10): Error: type parameter (X) passed to type IterA must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality)
+git-issue-3273.dfy(22,10): Error: type parameter (Y) passed to type IterB must support equality (got K) (perhaps try declaring type parameter 'K' on line 14 as 'K(==)', which says it can only be instantiated with a type that supports equality)
+git-issue-3273.dfy(43,12): Error: type parameter (Y) passed to type EqIter must support equality (got Dt)
+git-issue-3273.dfy(46,14): Error: type parameter (Y) passed to type EqIter must support equality (got Dt)
+git-issue-3273.dfy(46,21): Error: set argument type must support equality (got Dt)
+8 resolution/type errors detected in git-issue-3273.dfy