fix: Generate proper default string value for JavaScript

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -974,7 +974,11 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
         return $"{DafnyMultiSetClass}.Empty";
       } else if (xType is SeqType seq) {
         if (seq.Arg.IsCharType) {
-          return "''";
+          if (UnicodeCharEnabled) {
+            return "_dafny.Seq.UnicodeFromString(\"\")";
+          } else {
+            return "\"\"";
+          }
         }
         return $"{DafnySeqClass}.of()";
       } else if (xType is MapType) {

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -713,7 +713,13 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
         case RealType:
           return $"{DafnyRuntimeModule}.BigRational()";
         case CollectionType:
-          return $"{TypeHelperName(xType)}({{}})";
+          if (xType is SeqType { Arg: { IsCharType: true } }) {
+            var wrString = new ConcreteSyntaxTree();
+            StringLiteralWrapper(wrString).Write("\"\"");
+            return wrString.ToString();
+          } else {
+            return $"{TypeHelperName(xType)}({{}})";
+          }
         case UserDefinedType udt: {
             var cl = udt.ResolvedClass;
             Contract.Assert(cl != null);
@@ -1027,16 +1033,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
           }
           break;
         case StringLiteralExpr str:
-          if (UnicodeCharEnabled) {
-            wr.Write($"{DafnySeqMakerFunction}(map({DafnyRuntimeModule}.CodePoint, ");
-            TrStringLiteral(str, wr);
-            wr.Write("))");
-          } else {
-            wr.Write($"{DafnySeqMakerFunction}(");
-            TrStringLiteral(str, wr);
-            wr.Write(")");
-          }
-
+          TrStringLiteral(str, StringLiteralWrapper(wr));
           break;
         case StaticReceiverExpr:
           wr.Write(TypeName(e.Type, wr, e.tok));
@@ -1063,6 +1060,20 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
       }
     }
 
+    private ConcreteSyntaxTree StringLiteralWrapper(ConcreteSyntaxTree wr) {
+      ConcreteSyntaxTree wrStringGoesHere;
+      if (UnicodeCharEnabled) {
+        wr.Write($"{DafnySeqMakerFunction}(map({DafnyRuntimeModule}.CodePoint, ");
+        wrStringGoesHere = wr.Fork();
+        wr.Write("))");
+      } else {
+        wr.Write($"{DafnySeqMakerFunction}(");
+        wrStringGoesHere = wr.Fork();
+        wr.Write(")");
+      }
+      return wrStringGoesHere;
+    }
+
     protected override void EmitStringLiteral(string str, bool isVerbatim, ConcreteSyntaxTree wr) {
       if (!isVerbatim) {
         wr.Write($"\"{TranslateEscapes(str)}\"");

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

@@ -0,0 +1,12 @@
+// RUN: %testDafnyForEachCompiler "%s"
+// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char=false
+
+method Main() {
+  var s: seq<char>;
+  s := *;
+  print "(", s, ") ", s == "", " ", "" == s, " ", |s|, "\n";
+  s := "";
+  print "(", s, ") ", s == "", " ", "" == s, " ", |s|, "\n";
+  s := "hello";
+  print "(", s, ") ", s == "", " ", "" == s, " ", |s|, "\n";
+}

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

@@ -0,0 +1,3 @@
+() true true 0
+() true true 0
+(hello) false false 5

docs/dev/news/5239.fix

@@ -0,0 +1 @@
+Fix the default string value emitted for JavaScript