fix: Java --unicode-char mode coercion improvements

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -2874,6 +2874,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -2884,6 +2885,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.EqCommon: {
@@ -3015,7 +3017,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
@@ -3037,8 +3039,14 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
           ConvertFromChar(e.E, wr, inLetExprBody, wStmts);
           wr.Write(", BigInteger.One)");
         } else if (e.ToType.IsCharType) {
-          wr.Write($"({CharTypeName})");
-          TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+          if (UnicodeCharEnabled) {
+            wr.Write($"new {CharTypeName}((int)");
+            TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+            wr.Write(")");
+          } else {
+            wr.Write($"({CharTypeName})");
+            TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+          }
         } else {
           // (int or bv or char) -> (int or bv or ORDINAL)
           var fromNative = AsNativeType(e.E.Type);

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -2053,6 +2053,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -2063,6 +2064,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.Iff:

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -529,6 +529,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -539,6 +540,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.Iff:

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -3114,6 +3114,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -3124,6 +3125,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.BitwiseAnd:
@@ -3368,7 +3370,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
@@ -3659,7 +3661,7 @@ protected override void EmitCollectionDisplay(CollectionType ct, IToken tok, Lis
           wr.Write("_dafny.SeqOf");
         }
       }
-      TrExprList(elements, wr, inLetExprBody, wStmts, type: ct.TypeArgs[0]);
+      TrExprList(elements, wr, inLetExprBody, wStmts, typeAt: _ => ct.TypeArgs[0]);
     }
 
     protected override void EmitMapDisplay(MapType mt, IToken tok, List<ExpressionPair> elements,