fix: Use Downcast for let RHS and for function body

Fixes dafny-lang#5597

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -576,7 +576,9 @@ protected virtual void EmitSetterParameter(ConcreteSyntaxTree wr) {
     protected virtual void EmitReturnExpr(Expression expr, Type resultType, bool inLetExprBody, ConcreteSyntaxTree wr) {  // emits "return <expr>;" for function bodies
       var wStmts = wr.Fork();
       var w = EmitReturnExpr(wr);
-      EmitExpr(expr, inLetExprBody, EmitCoercionIfNecessary(expr.Type, resultType, null, w), wStmts);
+      w = EmitCoercionIfNecessary(expr.Type, resultType, expr.tok, w);
+      w = EmitDowncastIfNecessary(expr.Type, resultType, expr.tok, w);
+      EmitExpr(expr, inLetExprBody, w, wStmts);
     }
     protected virtual void EmitReturnExpr(string returnExpr, ConcreteSyntaxTree wr) {  // emits "return <returnExpr>;" for function bodies
       var w = EmitReturnExpr(wr);
@@ -2868,7 +2870,8 @@ void TrCasePatternOpt<VT>(CasePattern<VT> pat, Expression rhs, Action<ConcreteSy
           var wStmts = wr.Fork();
           var w = DeclareLocalVar(IdName(bv), bv.Type, rhsTok, wr);
           if (rhs != null) {
-            w = EmitCoercionIfNecessary(from: rhs.Type, to: bv.Type, tok: rhsTok, wr: w);
+            w = EmitCoercionIfNecessary(rhs.Type, bv.Type, rhsTok, wr: w);
+            w = EmitDowncastIfNecessary(rhs.Type, bv.Type, rhsTok, w);
             EmitExpr(rhs, inLetExprBody, w, wStmts);
           } else {
             emitRhs(w);

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CovariantCollections.dfy

@@ -342,7 +342,8 @@ method Downcasts() {
   s, s' := DowncastM2(m);  // cast in, cast out
   s := var v: set<Integer> := m; v;  // regression test -- this once tripped up the compilation to Java, whereas the next line had not
   s' := var u: set<Number> := var v: set<Integer> := m; v; u;
-  var eq := s == m && m == s;
+  var s'' := DowncastFunction(a, b); // regression test -- the same error was later discovered in top-level function bodies
+  var eq := s == m && m == s && s == s'';
   print eq, "\n";  // true
 
   s := FId<Integer>(m);  // cast in
@@ -367,6 +368,12 @@ method Create<T>(a: T, b: T) returns (m: set<T>, n: multiset<T>, o: seq<T>, p: m
   p := map[a := b, b := a];
 }
 
+function DowncastFunction(a: Integer, b: Integer): set<Integer> {
+  var m: set<Number> := {a, b};
+  var v: set<Integer> := m;
+  v
+}
+
 function DowncastF(s: set<Integer>): set<Number> { s }
 method DowncastM(s: set<Integer>) returns (r: set<Number>)
   ensures r == s

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5597.dfy

@@ -0,0 +1,51 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+method Main() {
+  var n: set<Number> := {};
+  var s: set<Integer>;
+  s := DoItWithAssignment(n);
+  print |s|, " ";
+  s := DoItWithPlainLet(n);
+  print |s|, " ";
+  s := DoItWithOptimizedLet(n);
+  print |s|, " ";
+  s := DoItViaFunctionBodyResult(n);
+  print |s|, "\n";
+}
+
+trait Number {
+  const value: int
+}
+
+class Integer extends Number {
+  constructor(value: int) {
+    this.value := value;
+  }
+}
+
+method DoItWithAssignment(numbers: set<Number>) returns (integers00: set<Integer>)
+  requires |numbers| == 0
+{
+  integers00 := numbers;
+}
+
+function DoItWithPlainLet(numbers: set<Number>): set<Integer>
+  requires |numbers| == 0
+{
+  {} +
+  var integers11: set<Integer> := numbers;
+  integers11
+}
+
+function DoItWithOptimizedLet(numbers: set<Number>): set<Integer>
+  requires |numbers| == 0
+{
+  var integers22: set<Integer> := numbers;
+  integers22
+}
+
+function DoItViaFunctionBodyResult(numbers: set<Number>): set<Integer>
+  requires |numbers| == 0
+{
+  numbers
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5597.dfy.expect

@@ -0,0 +1 @@
+0 0 0 0