Verification: map should not allow .Values if the value type is not equality supporting

[sorawee]

method Main() {
  var x := map[1 := () => 1];
  print x.Values;
}

verifies, but it should not.

[robin-aws]

Good catch!

[cpitclaudel]

This is a soundness issue:

function method makefun(y: int): int -> int {
  x => x + y
}

method Main() {
  var f := makefun(0);
  var g := makefun(0);
  assert f == g;

  var m := map[0 := g];
  assert m[0] == g;
  assert f in m.Values;

  if f !in m.Values {
    print 1 / 0;
  }
}

[RustanLeino]

For sequences, I think the type seq<X> is allowed even if X doesn’t support equality. However, seq<X> itself supports equality only if X does.

Therefore, I like the idea (suggested in a private conversion by @MikaelMayer) of allowing map<A, B> even if B doesn’t support equality, but with the restrictions that:

• we require B to support equality for any map where .Values or .Items is used
• we consider a type map<A, B> as supporting equality only if (A and) B do(es)