Chore: No extra newtype test (#5506)

### Description
Let's consider the following code:

```dafny
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](#5465) 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.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -18,6 +18,7 @@
 
 namespace Microsoft.Dafny.Compilers {
   class GoCodeGenerator : SinglePassCodeGenerator {
+    protected override bool RequiresAllVariablesToBeUsed => true;
     //TODO: This is tentative, update this to point to public module once available.
     private string DafnyRuntimeGoModule = "github.com/dafny-lang/DafnyRuntimeGo/";
 

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs

@@ -395,7 +395,8 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
               var bound = e.Bounds[i];
               var bv = e.BoundVars[i];
 
-              var collectionElementType = CompileCollection(bound, bv, inLetExprBody, false, su, out var collection, wStmts,
+              var collectionElementType = CompileCollection(bound, bv, inLetExprBody, false, su, out var collection,
+            out var newtypeConversionsWereExplicit, wStmts,
                 e.Bounds, e.BoundVars, i);
               wBody = EmitQuantifierExpr(collection, quantifierExpr is ForallExpr, collectionElementType, bv, wBody);
               var native = AsNativeType(e.BoundVars[i].Type);
@@ -409,7 +410,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
               EmitDowncastVariableAssignment(
                 IdName(bv), bv.Type, tmpVarName, collectionElementType, true, e.tok, newWBody);
               newWBody = MaybeInjectSubsetConstraint(
-                bv, bv.Type, inLetExprBody, e.tok, newWBody, isReturning: true, elseReturnValue: e is ForallExpr);
+                bv, bv.Type, inLetExprBody, e.tok, newWBody, newtypeConversionsWereExplicit, isReturning: true, elseReturnValue: e is ForallExpr);
               wBody = newWBody;
             }
 
@@ -458,8 +459,8 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
               processedBounds.Add(bv);
               var tmpVar = ProtectedFreshId("_compr_");
               var wStmtsLoop = wr.Fork();
-              var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop);
-              wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, inLetExprBody, e.tok, collection, wr);
+              var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, out var newtypeConversionsWereExplicit, wStmtsLoop);
+              wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, newtypeConversionsWereExplicit, true, inLetExprBody, e.tok, collection, wr);
               wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr);
             }
 
@@ -512,8 +513,8 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
               processedBounds.Add(bv);
               var tmpVar = ProtectedFreshId("_compr_");
               var wStmtsLoop = wr.Fork();
-              var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop);
-              wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, false, bv.tok, collection, wr);
+              var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, out var newtypeConversionsWereExplicit, wStmtsLoop);
+              wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, newtypeConversionsWereExplicit, true, false, bv.tok, collection, wr);
               wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr);
             }
 

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -684,6 +684,7 @@ protected abstract ConcreteSyntaxTree CreateForeachLoop(
     private ConcreteSyntaxTree CreateGuardedForeachLoop(
       string tmpVarName, Type collectionElementType,
       IVariable boundVar,
+      bool newtypeConversionsWereExplicit,
       bool introduceBoundVar, bool inLetExprBody,
       IToken tok, Action<ConcreteSyntaxTree> collection, ConcreteSyntaxTree wr
       ) {
@@ -692,7 +693,7 @@ private ConcreteSyntaxTree CreateGuardedForeachLoop(
       wr = MaybeInjectSubtypeConstraintWrtTraits(tmpVarName, collectionElementType, boundVar.Type, inLetExprBody, tok, wr);
       EmitDowncastVariableAssignment(IdName(boundVar), boundVar.Type, tmpVarName, collectionElementType,
           introduceBoundVar, tok, wr);
-      wr = MaybeInjectSubsetConstraint(boundVar, boundVar.Type, inLetExprBody, tok, wr);
+      wr = MaybeInjectSubsetConstraint(boundVar, boundVar.Type, inLetExprBody, tok, wr, newtypeConversionsWereExplicit);
       return wr;
     }
 
@@ -3367,8 +3368,8 @@ protected ConcreteSyntaxTree CompileGuardedLoops(List<BoundVar> bvs, List<Bounde
         var bv = bvs[i];
         var tmpVar = ProtectedFreshId("_guard_loop_");
         var wStmtsLoop = wr.Fork();
-        var elementType = CompileCollection(bound, bv, false, false, null, out var collection, wStmtsLoop, bounds, bvs, i);
-        wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, false, range.tok, collection, wr);
+        var elementType = CompileCollection(bound, bv, false, false, null, out var collection, out var newtypeConversionsWereExplicit, wStmtsLoop, bounds, bvs, i);
+        wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, newtypeConversionsWereExplicit, true, false, range.tok, collection, wr);
       }
 
       // if (range) {
@@ -3398,7 +3399,8 @@ protected virtual ConcreteSyntaxTree EmitAnd(Action<ConcreteSyntaxTree> lhs, Con
     /// not be legal "bv.Type" values -- that is, it could be that "bv.Type" has further constraints that need to be checked.
     /// </summary>
     Type CompileCollection(BoundedPool bound, IVariable bv, bool inLetExprBody, bool includeDuplicates,
-        Substituter/*?*/ su, out Action<ConcreteSyntaxTree> collectionWriter, ConcreteSyntaxTree wStmts,
+        Substituter/*?*/ su, out Action<ConcreteSyntaxTree> collectionWriter, out bool newtypeConversionsWereExplicit,
+        ConcreteSyntaxTree wStmts,
         List<BoundedPool>/*?*/ bounds = null, List<BoundVar>/*?*/ boundVars = null, int boundIndex = 0) {
       Contract.Requires(bound != null);
       Contract.Requires(bounds == null || (boundVars != null && bounds.Count == boundVars.Count && 0 <= boundIndex && boundIndex < bounds.Count));
@@ -3408,6 +3410,9 @@ Type CompileCollection(BoundedPool bound, IVariable bv, bool inLetExprBody, bool
       var propertySuffix = SupportsProperties ? "" : "()";
       su = su ?? new Substituter(null, new Dictionary<IVariable, Expression>(), new Dictionary<TypeParameter, Type>());
 
+      newtypeConversionsWereExplicit =
+        bound is SetBoundedPool or MapBoundedPool or SeqBoundedPool or MultiSetBoundedPool;
+
       if (bound is BoolBoundedPool) {
         collectionWriter = (wr) => EmitBoolBoundedPool(inLetExprBody, wr, wStmts);
         return new BoolType();
@@ -3742,8 +3747,8 @@ private void TrAssignSuchThat(List<IVariable> lhss, Expression constraint, List<
         }
         var tmpVar = ProtectedFreshId("_assign_such_that_");
         var wStmts = currentBlock.Fork();
-        var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmts);
-        wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, false, inLetExprBody, bv.Tok, collection, wr);
+        var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, out var newtypeConversionsWereExplicit, wStmts);
+        wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, newtypeConversionsWereExplicit, false, inLetExprBody, bv.Tok, collection, wr);
         currentBlock = wr;
         if (needIterLimit) {
           var varName = $"{iterLimit}_{i}";
@@ -4952,28 +4957,34 @@ private ConcreteSyntaxTree MaybeInjectSubtypeConstraintWrtTraits(string tmpVarNa
       return wr;
     }
 
+    protected virtual bool RequiresAllVariablesToBeUsed => false;
+
     /// <summary>
     /// If needed, emit an if-statement wrapper that checks that the value stored in "boundVar" satisfies any (subset-type or newtype) constraints
     /// of "boundVarType".
     /// </summary>
     private ConcreteSyntaxTree MaybeInjectSubsetConstraint(IVariable boundVar, Type boundVarType,
-      bool inLetExprBody, IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false) {
+      bool inLetExprBody, IToken tok, ConcreteSyntaxTree wr, bool newtypeConversionsWereExplicit,
+      bool isReturning = false, bool elseReturnValue = false) {
 
       if (boundVarType.NormalizeExpandKeepConstraints() is UserDefinedType { ResolvedClass: (SubsetTypeDecl or NewtypeDecl) } udt) {
         var declWithConstraints = (RedirectingTypeDecl)udt.ResolvedClass;
 
-        var thenWriter = EmitIf(out var guardWriter, hasElse: isReturning, wr);
+        if (!newtypeConversionsWereExplicit || declWithConstraints is not NewtypeDecl || RequiresAllVariablesToBeUsed) {
+          var thenWriter = EmitIf(out var guardWriter, hasElse: isReturning, wr);
 
-        EmitCallToIsMethod(declWithConstraints, udt.TypeArgs, guardWriter).Write(IdName(boundVar));
+          // Newtype conversions have to be explicit so we don't need to emit a call to their IsMethod 
+          EmitCallToIsMethod(declWithConstraints, udt.TypeArgs, guardWriter).Write(IdName(boundVar));
 
-        if (isReturning) {
-          var elseBranch = wr;
-          elseBranch = EmitBlock(elseBranch);
-          elseBranch = EmitReturnExpr(elseBranch);
-          var wStmts = elseBranch.Fork();
-          EmitExpr(Expression.CreateBoolLiteral(tok, elseReturnValue), inLetExprBody, elseBranch, wStmts);
+          if (isReturning) {
+            var elseBranch = wr;
+            elseBranch = EmitBlock(elseBranch);
+            elseBranch = EmitReturnExpr(elseBranch);
+            var wStmts = elseBranch.Fork();
+            EmitExpr(Expression.CreateBoolLiteral(tok, elseReturnValue), inLetExprBody, elseBranch, wStmts);
+          }
+          wr = thenWriter;
         }
-        wr = thenWriter;
       }
 
       if (isReturning) {