Compiled code has useless duplicate membership test

[MikaelMayer]

Consider the following code:

method ExpectAllPositiveSeq(a: seq<int>) {
  expect forall x <- a + a :: x > 0;
}
method ExpectAllPositiveSet(a: set<int>) {
  expect forall x <- a + a :: x > 0;
}
method ExpectAllPositiveMultiset(a: multiset<int>) {
  expect forall x <- a + a :: x > 0;
}
method ExpectAllPositiveMap(a: map<int, int>) {
  expect forall x <- a + a :: x > 0;
}
method Main() {
  ExpectAllPositiveSeq([1, 2, 3]);
  ExpectAllPositiveSet({1, 2, 3});
  ExpectAllPositiveMultiset(multiset{1, 2, 3});
  ExpectAllPositiveMap(map[1 := 1, 2 := 2, 3 := 3]);
}

In all compilers, the compilation of the forall expression is done in two ways:

1. First, we emit a bounded pool from which we iterate
2. Second, we emit the whole forall expression, including the range check.

However, by construction, in many cases the bounded pool arise from one of the range check, so the range check is useless.
For example, let's consider the C# case (but all other languages have the same issue)

C#

      if (!(Dafny.Helpers.Id<Func<Dafny.ISequence<BigInteger>, bool>>((_0_a) => Dafny.Helpers.Quantifier<BigInteger>((Dafny.Sequence<BigInteger>.Concat(_0_a, _0_a)).UniqueElements, true, (((_forall_var_0) => {
        BigInteger _1_x = (BigInteger)_forall_var_0;
        return !((Dafny.Sequence<BigInteger>.Concat(_0_a, _0_a)).Contains(_1_x)) || ((_1_x).Sign == 1);
      }))))(a))) {
        throw new Dafny.HaltException("testfile.dfy(2,2): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}=

Performance slowdown:

• The check !((Dafny.Sequence<BigInteger>.Concat(_0_a, _0_a)).Contains(_1_x)) is always false by construction.
• Keeping it makes the collection to be concatenated n + 1 times, once for each element of the sequence, when it really should be computed once.

I'm reporting this because I'm working on the Dafny-to-Rust code generator, and since performance of the generated code is a requirement, this one thing is something we'll need to cover.