Equality support inferred for nullable iterator but not non-null iterator

[RustanLeino]

Dafny version

3.10.0

Code to produce this issue

The iterator declaration

iterator Iter<Y>(u: set<Y>) // this infers Y to be (==)

gives rise to two types, the nullable type Iter? and the non-null type Iter. From the signature of the iterator declaration, Dafny infers the (==) characteristic for type parameter Y (since the signature includes the type set<Y>).

Therefore, if D is a type that does not support equality, then neither the type Iter?<D> nor the type Iter<D>. Alas, Dafny reports an error only for Iter?<D>, not for Iter<D>.

Diagnosis: While Dafny infers (==) for Y for the type Iter?, it does not apply the same learning to type Iter.

Repro:

iterator Iter<Y>(u: set<Y>) // this infers Y to be (==)

method Repro<K>() {
  var iter: Iter<K>; // should be an error, because K is not (==)
}

Command to run and resulting output

$ dafny test.dfy

Dafny program verifier finished with 1 verified, 0 errors

What happened?

This is what is expected for the 8 cases of inferred/declared (==), passing in equality-support type or not, and using the nullable/non-null version of the iterator type:

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>;
}

The issue does not appear to affect soundness. The following example is close, but no cigar:

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 ought to be an error, because EqIter should take a (==) type argument.
  var iter: EqIter<Dt>;
  // 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:
  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
  }
}

What type of operating system are you experiencing the problem on?

Mac