Chore: No extra newtype test

[MikaelMayer]

Description

Let's consider the following code:

newtype UX = x: int | 129 <= x < 256
method Main() {
  var u8toInt := map[1 as u8 := 1, 2 as u8 := 2];
  var IntToU8 := map k <- u8toInt :: u8toInt[k] := k;
}

in every backend, for IntToU8 it is generating code lilke

c = MapCollectionBuilder()
for k in u8toInt 
  if k is u8 {
   if u8toInt contains k {
     col.Add(u8toInt[k], k)
   }
  }
}
k.build()

I already filed an issue that the "contains" test is redundant when we are already iterating over the collection.
But here there is another test that is redundant: The membership test to the newtype.
Indeed, contrary to subset types which can be erased, newtype conversions must be explicit. So we cannot iterate over a newtype different than the newtype obtain like we do for subset types.
Moreover, the test of being a newtype involves a conversion from a U8 (how the newtype is encoded) to a DafnyInt because otherwise we would not be able to compare it with the number "256" which is out of the range.
So this test is not only redundant, it actually adds computation that is not necessary.

How has this been tested?

All existing tests should pass.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

Apparently the following case fails so this PR is unsound:

  newtype Big = x: int | 0 <= x < 10_000 && x != 22

  function EmptySequence<Y>(): seq<Y> {
    []
  }

  type AnotherInBetween<HH(0), GG> = y: Big | y != 10
  type SubsetInBetween<G, H(0)> = y: AnotherInBetween<H, G> | y != 34 && |EmptySequence<G>()| == |EmptySequence<H>()|
  newtype Middle = SubsetInBetween<bool, char>
  newtype Little = z: Middle | z < 200 && z != 16

  method Main() {
    var u := set ltl: Little | 3 <= ltl < 35 && ltl % 3 == 1; // {4, 7, 13, 19, 25, 28, 31}
    print |u|, "\n"; // should be 7, but this PR outputs 11
  }

It makes sense that, when we iterate over numbers from a set's perspective, numbers have the right byte size but the newtype's predicate might not match. What I had observed is that, when we have a SetBoundedPool or a MapBoundedPool, this is where the conversion had to be done manually anyway.

I'm changing this PR so that it emits this optimization only when encountering a collection, not a range.

[RustanLeino]

This is an excellent thing to address. Thanks!

[atomb]

Re-approving based on approval from @RustanLeino and no substantive changes since.