From 92e1f0bd7c66aa63027bff6d23049aad2a4d3a65 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 14:29:30 -0800
Subject: [PATCH 01/15] chore: Improve whitespace in C# output

---
 Source/DafnyCore/Compilers/Compiler-Csharp.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Compilers/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
index 85fa0bbbe08..475546e3eab 100644
--- a/Source/DafnyCore/Compilers/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
@@ -1727,7 +1727,7 @@ protected void DeclareField(string name, bool isPublic, bool isStatic, bool isCo
               $"{publik}{konst} {virtuall} {typeName} {name} {{get;}}");
           } else {
             cw.InstanceMemberWriter.Write(
-              $"{publik} {virtuall} {typeName} {name} {{get; set;}}");
+              $"{publik}{virtuall} {typeName} {name} {{get; set;}}");
           }
         } else {
           cw.InstanceMemberWriter.WriteLine($"{publik}{konst} {typeName} {name}");

From 00171eca722b61be8ac9cdda5a94db9b2466e893 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 14:08:42 -0800
Subject: [PATCH 02/15] chore: Remove unused parameter

---
 Source/DafnyCore/AST/Types.cs | 3 +--
 Source/DafnyCore/Resolver.cs  | 4 ++--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/Source/DafnyCore/AST/Types.cs b/Source/DafnyCore/AST/Types.cs
index 50deb663849..c6bd773246e 100644
--- a/Source/DafnyCore/AST/Types.cs
+++ b/Source/DafnyCore/AST/Types.cs
@@ -937,10 +937,9 @@ public static bool IsSupertype(Type super, Type sub) {
     }
   }
 
-  public static bool FromSameHead_Subtype(Type t, Type u, BuiltIns builtIns, out Type a, out Type b) {
+  public static bool FromSameHead_Subtype(Type t, Type u, out Type a, out Type b) {
     Contract.Requires(t != null);
     Contract.Requires(u != null);
-    Contract.Requires(builtIns != null);
     if (FromSameHead(t, u, out a, out b)) {
       return true;
     }
diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs
index 9452daa777c..4a9b121a3cb 100644
--- a/Source/DafnyCore/Resolver.cs
+++ b/Source/DafnyCore/Resolver.cs
@@ -5376,7 +5376,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto
                 }
               }
               Type a, b;
-              satisfied = Type.FromSameHead_Subtype(t, u, resolver.builtIns, out a, out b);
+              satisfied = Type.FromSameHead_Subtype(t, u, out a, out b);
               if (satisfied) {
                 Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count);
                 var cl = a is UserDefinedType ? ((UserDefinedType)a).ResolvedClass : null;
@@ -5436,7 +5436,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto
               }
               Type a, b;
               // okay if t<:u or u<:t (this makes type inference more manageable, though it is more liberal than one might wish)
-              satisfied = Type.FromSameHead_Subtype(t, u, resolver.builtIns, out a, out b);
+              satisfied = Type.FromSameHead_Subtype(t, u, out a, out b);
               if (satisfied) {
                 Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count);
                 var cl = a is UserDefinedType ? ((UserDefinedType)a).ResolvedClass : null;

From 6d7bb2220e58cbcf266b3a38792ecf82a56697a3 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 14:20:21 -0800
Subject: [PATCH 03/15] Print class objects as their Dafny names in Java

---
 Source/DafnyCore/Compilers/Compiler-java.cs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs
index 11745127683..dc2820acb10 100644
--- a/Source/DafnyCore/Compilers/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Compiler-java.cs
@@ -925,9 +925,21 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
       var wRestOfBody = wBody.Fork();
       var targetTypeName = BoxedTypeName(UserDefinedType.FromTopLevelDecl(cls.tok, cls, null), wTypeMethod, cls.tok);
       EmitTypeMethod(cls, javaName, typeParameters, typeParameters, targetTypeName, null, wTypeMethod);
+
+      if (fullPrintName != null) {
+        // By emitting a toString() method, printing an object will give the same output as with other target languages.
+        EmitToString(fullPrintName, wBody);
+      }
+
       return new ClassWriter(this, wRestOfBody, wCtorBody);
     }
 
+    private void EmitToString(string fullPrintName, ConcreteSyntaxTree wr) {
+      wr.WriteLine("@Override");
+      var wrBody = wr.NewBlock("public java.lang.String toString()");
+      wrBody.WriteLine($"return \"{fullPrintName}\";");
+    }
+
     /// <summary>
     /// Generate the "_typeDescriptor" method for a generated class.
     /// "enclosingType" is allowed to be "null", in which case the target values are assumed to be references.

From b390493e53595f93cfac8e1acdfd89e41584ac85 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 15:04:42 -0800
Subject: [PATCH 04/15] fix: Emit type arguments for codatatypes in Java

---
 Source/DafnyCore/Compilers/Compiler-java.cs | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs
index dc2820acb10..cd60606973d 100644
--- a/Source/DafnyCore/Compilers/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Compiler-java.cs
@@ -1800,7 +1800,9 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
       } else {
         var nonGhostFormals = groundingCtor.Formals.Where(f => !f.IsGhost).ToList();
         var args = nonGhostFormals.Comma(f => DefaultValue(f.Type, wDefault, f.tok));
-        EmitDatatypeValue(dt, groundingCtor, null, dt is CoDatatypeDecl, args, wDefault);
+        EmitDatatypeValue(dt, groundingCtor,
+          dt.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(dt.tok, tp)),
+          dt is CoDatatypeDecl, args, wDefault);
       }
 
       var targetTypeName = BoxedTypeName(UserDefinedType.FromTopLevelDecl(dt.tok, dt, null), wr, dt.tok);
@@ -2582,9 +2584,9 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string arguments, C
       EmitDatatypeValue(dt, dtv.Ctor, typeArgs, dtv.IsCoCall, arguments, wr);
     }
 
-    void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List<Type>/*?*/ typeArgs, bool isCoCall, string arguments, ConcreteSyntaxTree wr) {
+    void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List<Type> typeArgs, bool isCoCall, string arguments, ConcreteSyntaxTree wr) {
       var dtName = dt is TupleTypeDecl tupleDecl ? DafnyTupleClass(tupleDecl.NonGhostDims) : dt.FullCompileName;
-      var typeParams = typeArgs == null || typeArgs.Count == 0 ? "" : $"<{BoxedTypeNames(typeArgs, wr, dt.tok)}>";
+      var typeParams = typeArgs.Count == 0 ? "" : $"<{BoxedTypeNames(typeArgs, wr, dt.tok)}>";
       if (!isCoCall) {
         // For an ordinary constructor (that is, one that does not guard any co-recursive calls), generate:
         //   Dt.<T>create_Cons( args )
@@ -2592,7 +2594,7 @@ void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List<Type>/*?*/ typeA
       } else {
         wr.Write($"new {dt.CompileName}__Lazy(");
         wr.Write("() -> { return ");
-        wr.Write($"new {DtCtorName(ctor)}({arguments})");
+        wr.Write($"new {DtCtorName(ctor)}{typeParams}({arguments})");
         wr.Write("; })");
       }
     }

From 35a5e59bcb59775620154efc5cc729e853b86fe1 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 14:29:19 -0800
Subject: [PATCH 05/15] feat: Emit upcasts in Java

Fixes #2013
---
 Source/DafnyCore/Compilers/Compiler-java.cs      | 15 +++++----------
 Source/DafnyCore/Compilers/SinglePassCompiler.cs | 14 +++++++++-----
 2 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs
index cd60606973d..34a316356d9 100644
--- a/Source/DafnyCore/Compilers/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Compiler-java.cs
@@ -828,15 +828,6 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
       Contract.Assume(variance.Count == typeArgs.Count);
       string s = IdProtect(fullCompileName);
       if (typeArgs.Count != 0 && !omitTypeArguments) {
-        for (var i = 0; i < typeArgs.Count; i++) {
-          var v = variance[i];
-          var ta = typeArgs[i];
-          if (ComplicatedTypeParameterForCompilation(v, ta)) {
-            UnsupportedFeatureError(tok, Feature.TraitTypeParameters,
-              "compilation does not support trait types as a type parameter (got '{0}'{1}); consider introducing a ghost", wr,
-              ta, typeArgs.Count == 1 ? "" : $" for type parameter {i}");
-          }
-        }
         s += "<" + BoxedTypeNames(typeArgs, wr, tok) + ">";
       }
       return s;
@@ -3691,6 +3682,10 @@ protected override void EmitApplyExpr(Type functionType, IToken tok, Expression
 
     protected override bool NeedsCastFromTypeParameter => true;
 
+    protected override bool TargetSubtypingRequiresEqualTypeArguments(Type type) {
+      return type.AsCollectionType == null;
+    }
+
     protected override bool IsCoercionNecessary(Type/*?*/ from, Type/*?*/ to) {
       if (from == null || to == null || !from.IsArrayType || !to.IsArrayType) {
         return false;
@@ -3717,7 +3712,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty
     }
 
     protected override ConcreteSyntaxTree EmitDowncast(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) {
-      wr.Write($"(({TypeName(to, wr, tok)})(");
+      wr.Write($"(({TypeName(to, wr, tok)})(java.lang.Object)(");
       var w = wr.Fork();
       wr.Write("))");
       return w;
diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
index 64e53d13064..a6b1c7cfa14 100644
--- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs
+++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
@@ -732,6 +732,8 @@ protected virtual ConcreteSyntaxTree EmitSign(Type type, ConcreteSyntaxTree wr)
 
     protected virtual bool NeedsCastFromTypeParameter => false;
 
+    protected virtual bool TargetSubtypingRequiresEqualTypeArguments(Type type) => false;
+
     protected virtual bool IsCoercionNecessary(Type /*?*/ from, Type /*?*/ to) {
       return NeedsCastFromTypeParameter;
     }
@@ -751,9 +753,11 @@ protected ConcreteSyntaxTree EmitDowncastIfNecessary(Type /*?*/ from, Type /*?*/
       Contract.Requires(wr != null);
       if (from != null && to != null) {
         if (!IsTargetSupertype(to, from)) {
-          // The following assert is a sanity check. Note, in a language with NeedsCastFromTypeParameter, "to" and "from" may
-          // contain uninstantiated formal type parameters.
-          Contract.Assert(NeedsCastFromTypeParameter || IsTargetSupertype(from, to));
+          // By the way, it is tempting that think that IsTargetSupertype(from, to)) would hold here, but that's not true.
+          // For one, in a language with NeedsCastFromTypeParameter, "to" and "from" may contain uninstantiated formal type parameters.
+          // Also, it is possible (subject to a check enforced by the verifier) to assign Datatype<X> to Datatype<Y>,
+          // where Datatype is co-variant in its argument type and X and Y are two incomparable types with a common supertype.
+
           wr = EmitDowncast(from, to, tok, wr);
         }
       }
@@ -766,7 +770,7 @@ protected ConcreteSyntaxTree EmitDowncastIfNecessary(Type /*?*/ from, Type /*?*/
     /// This to similar to Type.IsSupertype and Type.Equals, respectively, but ignores subset types (that
     /// is, always uses the base type of any subset type).
     /// </summary>
-    public static bool IsTargetSupertype(Type to, Type from, bool typeEqualityOnly = false) {
+    public bool IsTargetSupertype(Type to, Type from, bool typeEqualityOnly = false) {
       Contract.Requires(from != null);
       Contract.Requires(to != null);
       to = to.NormalizeExpand();
@@ -778,7 +782,7 @@ public static bool IsTargetSupertype(Type to, Type from, bool typeEqualityOnly =
         Contract.Assert(formalTypeParameters != null || to.TypeArgs.Count == 0 || to is CollectionType);
         for (var i = 0; i < to.TypeArgs.Count; i++) {
           bool okay;
-          if (typeEqualityOnly) {
+          if (typeEqualityOnly || TargetSubtypingRequiresEqualTypeArguments(to)) {
             okay = IsTargetSupertype(to.TypeArgs[i], from.TypeArgs[i], true);
           } else if (formalTypeParameters == null || formalTypeParameters[i].Variance == TypeParameter.TPVariance.Co) {
             okay = IsTargetSupertype(to.TypeArgs[i], from.TypeArgs[i]);

From 49975938c9fddb09ec4a80e515924a746b8ac0b3 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 14:28:14 -0800
Subject: [PATCH 06/15] Update tests

---
 Test/comp/DowncastClone.dfy               |  4 +---
 Test/comp/DowncastClone.dfy.expect        | 15 +++++----------
 Test/comp/Variance.dfy                    |  3 +--
 Test/comp/Variance.dfy.expect             | 20 +++++++++++++-------
 Test/dafny0/RuntimeTypeTests0.dfy         |  8 ++++----
 Test/dafny0/RuntimeTypeTests0.dfy.expect  | 21 ++++++++++++++++++---
 Test/git-issues/git-issue-1815.dfy        | 20 +++++++++++---------
 Test/git-issues/git-issue-1815.dfy.expect | 10 +++++++---
 8 files changed, 60 insertions(+), 41 deletions(-)

diff --git a/Test/comp/DowncastClone.dfy b/Test/comp/DowncastClone.dfy
index 65aa4b1a04e..a0ae89eb920 100644
--- a/Test/comp/DowncastClone.dfy
+++ b/Test/comp/DowncastClone.dfy
@@ -2,11 +2,9 @@
 // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
-// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
-// To enable this in cs we needed to implement DowncastClone for datatypes.
-// Java avoids this problem by not even allowing traits in datatypes.
 
 datatype Co<+T> = Co(T) | C
 datatype ReCo<+T> = ReCo(T)
diff --git a/Test/comp/DowncastClone.dfy.expect b/Test/comp/DowncastClone.dfy.expect
index d89a9ebd309..6c03a049e6c 100644
--- a/Test/comp/DowncastClone.dfy.expect
+++ b/Test/comp/DowncastClone.dfy.expect
@@ -23,16 +23,11 @@ _module.Y and _module.Y
 Done
 
 Dafny program verifier did not attempt verification
-DowncastClone.dfy(24,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-DowncastClone.dfy(32,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-DowncastClone.dfy(40,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-DowncastClone.dfy(42,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-DowncastClone.dfy(42,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-DowncastClone.dfy(49,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-DowncastClone.dfy(51,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-DowncastClone.dfy(51,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-(0,-1): Error: compilation does not support trait types as a type parameter (got 'X' for type parameter 1); consider introducing a ghost
-Wrote textual form of partial target program to DowncastClone-java/DowncastClone.java
+Co.Co(_module.Y) and Co.Co(_module.Y)
+ReCo.ReCo(_module.Y) and ReCo.ReCo(_module.Y)
+false and false
+_module.Y and _module.Y
+Done
 
 Dafny program verifier did not attempt verification
 Co.Co(_module.Y) and Co.Co(_module.Y)
diff --git a/Test/comp/Variance.dfy b/Test/comp/Variance.dfy
index 1893cfb5ca9..fb41f0a1732 100644
--- a/Test/comp/Variance.dfy
+++ b/Test/comp/Variance.dfy
@@ -2,10 +2,9 @@
 // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
-// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
-// The Java compiler lacks support for this (see dafny0/RuntimeTypeTests0.dfy).
 
 datatype Co<+T> = Co(z: T) {
     const x: int;
diff --git a/Test/comp/Variance.dfy.expect b/Test/comp/Variance.dfy.expect
index 8858ffa1abe..cf08d82ac07 100644
--- a/Test/comp/Variance.dfy.expect
+++ b/Test/comp/Variance.dfy.expect
@@ -47,13 +47,19 @@ _module.Int0[]0000
 Done
 
 Dafny program verifier did not attempt verification
-Variance.dfy(109,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-Variance.dfy(135,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-Variance.dfy(140,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-Variance.dfy(149,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-Variance.dfy(174,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-Variance.dfy(179,9): Error: compilation does not support trait types as a type parameter (got 'X'); consider introducing a ghost
-Wrote textual form of partial target program to Variance-java/Variance.java
+Co.Co(_module.Int) and Co.Co(_module.Int)
+true0[]0000
+Non.Non(_module.Int) and Non.Non(_module.Int)
+true0[]0000
+0 and 0
+_module.Int0[]0000
+CCo.CCo and CCo.CCo
+true0[]0000
+CNon.CNon and CNon.CNon
+true0[]0000
+CCon.CCon and CCon.CCon
+_module.Int0[]0000
+Done
 
 Dafny program verifier did not attempt verification
 Co.Co(_module.Int) and Co.Co(_module.Int)
diff --git a/Test/dafny0/RuntimeTypeTests0.dfy b/Test/dafny0/RuntimeTypeTests0.dfy
index b5013dbb807..b8ce6ad759b 100644
--- a/Test/dafny0/RuntimeTypeTests0.dfy
+++ b/Test/dafny0/RuntimeTypeTests0.dfy
@@ -1,15 +1,15 @@
 // UNSUPPORTED: windows
 // RUN: %dafny /compile:0 "%s" > "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
-// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 // The code in this file demonstrates complications in sorting out covariance in some
-// compilation target languages. Compilation support is currently spotty, where Java only
-// supports collection types (not datatypes), and only in the "upcast" direction.
+// compilation target languages.
 //
-// The solution in Java is to use Java's wildcard types: a "Dafny.Sequence<T>"" is assignable to
+// Part of the solution in Java is to use Java's wildcard types: a "Dafny.Sequence<T>"" is assignable to
 // a "Dafny.Sequence<? extends T>".
 //
 // Covariance is not a problem in JavaScript, since JavaScript has no static types. It's also
diff --git a/Test/dafny0/RuntimeTypeTests0.dfy.expect b/Test/dafny0/RuntimeTypeTests0.dfy.expect
index 914c0b0b7f8..90535aed979 100644
--- a/Test/dafny0/RuntimeTypeTests0.dfy.expect
+++ b/Test/dafny0/RuntimeTypeTests0.dfy.expect
@@ -12,9 +12,24 @@ map[7 := _module.Class0] and map[7 := _module.Class0]
 [_module.Class0, _module.Class0] and [_module.Class0, _module.Class0]
 
 Dafny program verifier did not attempt verification
-RuntimeTypeTests0.dfy(42,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost
-RuntimeTypeTests0.dfy(51,9): Error: compilation does not support trait types as a type parameter (got 'object'); consider introducing a ghost
-Wrote textual form of partial target program to RuntimeTypeTests0-java/RuntimeTypeTests0.java
+{5, 7} and {5, 7}
+Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
+Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
+{_module.Class0} and {_module.Class0}
+[_module.Class0] and [_module.Class0]
+multiset{_module.Class0} and multiset{_module.Class0}
+map[7 := _module.Class0] and map[7 := _module.Class0]
+[_module.Class0, _module.Class0] and [_module.Class0, _module.Class0]
+
+Dafny program verifier did not attempt verification
+{5, 7} and {5, 7}
+Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
+Dt.Atom(_module.Class0) and Dt.Atom(_module.Class0)
+{_module.Class0} and {_module.Class0}
+[_module.Class0] and [_module.Class0]
+multiset{_module.Class0} and multiset{_module.Class0}
+map[7 := _module.Class0] and map[7 := _module.Class0]
+[_module.Class0, _module.Class0] and [_module.Class0, _module.Class0]
 
 Dafny program verifier did not attempt verification
 {5, 7} and {5, 7}
diff --git a/Test/git-issues/git-issue-1815.dfy b/Test/git-issues/git-issue-1815.dfy
index 2cae5e7c597..76c3d35c803 100644
--- a/Test/git-issues/git-issue-1815.dfy
+++ b/Test/git-issues/git-issue-1815.dfy
@@ -1,21 +1,23 @@
 // RUN: %dafny /compile:0 "%s" > "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
 // RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
-// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
-// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
-// The Java compiler lacks support for this (see dafny0/RuntimeTypeTests0.dfy).
 
-datatype X<+U> = X(x: U)
+datatype Dt<+U> = Dt(x: U)
 
 trait Tr {}
 class Cl extends Tr {
-    constructor () {}
+  constructor () {}
 }
 
 method Main() {
-    var cl := new Cl();
-    var e: X<Tr> := X(cl);
-    match e
-    case X(tr) => return;
+  var cl: Cl := new Cl();
+  var e: Dt<Tr> := Dt(cl);
+  match e {
+    case Dt(tr) =>
+  }
+  print "done\n";
 }
diff --git a/Test/git-issues/git-issue-1815.dfy.expect b/Test/git-issues/git-issue-1815.dfy.expect
index 359bcf4f99c..7b2651302d9 100644
--- a/Test/git-issues/git-issue-1815.dfy.expect
+++ b/Test/git-issues/git-issue-1815.dfy.expect
@@ -2,12 +2,16 @@
 Dafny program verifier finished with 1 verified, 0 errors
 
 Dafny program verifier did not attempt verification
+done
 
 Dafny program verifier did not attempt verification
+done
 
 Dafny program verifier did not attempt verification
-git-issue-1815.dfy(18,11): Error: compilation does not support trait types as a type parameter (got 'Tr'); consider introducing a ghost
-git-issue-1815.dfy(18,11): Error: compilation does not support trait types as a type parameter (got 'Tr'); consider introducing a ghost
-Wrote textual form of partial target program to git-issue-1815-java/git_issue_1815.java
+done
 
 Dafny program verifier did not attempt verification
+done
+
+Dafny program verifier did not attempt verification
+done

From 28e817981e64bf617781b75337009d2030f6acb1 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 15:23:31 -0800
Subject: [PATCH 07/15] Add new tests

---
 Test/git-issues/git-issue-2013.dfy        | 191 ++++++++++++++++++++++
 Test/git-issues/git-issue-2013.dfy.expect |  57 +++++++
 2 files changed, 248 insertions(+)
 create mode 100644 Test/git-issues/git-issue-2013.dfy
 create mode 100644 Test/git-issues/git-issue-2013.dfy.expect

diff --git a/Test/git-issues/git-issue-2013.dfy b/Test/git-issues/git-issue-2013.dfy
new file mode 100644
index 00000000000..9c877ad3e83
--- /dev/null
+++ b/Test/git-issues/git-issue-2013.dfy
@@ -0,0 +1,191 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+method Main() {
+  TestTraits();
+  TestSiblings();
+  TestException();
+  MoreTests.Test();
+  Conveyance.Test();
+}
+
+// ----- reference types -----
+
+datatype Dt<+U> = Dt(u: U)
+
+trait Tr {
+  var y: int
+}
+
+class Cl extends Tr {
+  constructor () {
+    y := 15;
+  }
+}
+
+method Print(e: Dt<Cl>) {
+  print e.u.y, "\n";
+}
+
+method CreateDtForTrait(e: Dt<Cl>) returns (d: Dt<Tr>)
+  ensures d.u == e.u
+{
+  d := e; // upcast
+}
+
+method TestTraits() {
+  var cl := new Cl();
+  var e: Dt<Cl> := Dt(cl);
+  var d: Dt<Tr> := CreateDtForTrait(e);
+  cl.y := cl.y + 1;
+  var f: Dt<Cl> := d; // downcast
+
+  Print(f); // 16
+  Print(e); // 16
+}
+
+// ----- sibling types -----
+
+type Even = x | x % 2 == 0
+
+method TestSiblings() {
+  // downcasts
+  var a: Dt<int> := Dt(10);
+  var b: Dt<nat> := a;
+  var c: Dt<Even> := a;
+
+  // upcasts
+  b := Dt(11);
+  c := Dt(12);
+  a := b;
+  a := c;
+
+  // sideway casts
+  b := Dt(20);
+  c := b;
+  c := Dt(30);
+  b := c;
+
+  print a, " ", b, " ", c, "\n"; // Dt.Dt(12) Dt.Dt(30) Dt.Dt(30)
+}
+
+// ----- Result -----
+
+datatype Result<+T, +R> = | Success(value: T) | Failure(error: R)
+
+trait Exception {}
+
+class MyClassException extends Exception { }
+
+class MyClass {
+  const error: Exception
+
+  constructor () {
+    error := new MyClassException;
+  }
+
+  function method Foo(u: int): Result<int, Exception> {
+    if u < 8 then
+      Success(8)
+    else
+      Failure(error)
+  }
+}
+
+method TestException() {
+  var c := new MyClass();
+  print c.Foo(2), " ", c.Foo(22), "\n"; // Result.Success(8) Result.Failure(_module.MyClassException)
+}
+
+module MoreTests {
+  type Even = x | x % 2 == 0
+
+  datatype Dt<T> = Make(T)
+  datatype DtCovariant<+T> = MakeCovariant(T)
+
+  trait Z { }
+  trait X extends Z { }
+  trait Y extends Z { }
+  class C extends X, Y { }
+
+  method Test() {
+    var c := new C;
+
+    var s: set<int> := {100};
+    var t: set<nat> := s;
+    var u: set<Even> := s;
+    t := u;
+    u := t;
+    print s, " ", t, " ", u, "\n"; // {100} {100} {100}
+
+    var S: set<Z> := {c};
+    var T: set<X> := S;
+    var U: set<Y> := S;
+    T := U;
+    U := T;
+    print S, " ", T, " ", U, "\n"; // {_module.C} {_module.C} {_module.C}
+
+    // The assignments in the following example don't need covariance of Dt, because
+    // Dafny checks that the value with its payment is suitable for the target type.
+    var k: Dt<int> := Make(100);
+    var m: Dt<nat> := k;
+    var n: Dt<Even> := k;
+    m := n;
+    n := m;
+    print k, " ", m, " ", n, "\n"; // Dt.Make(100) Dt.Make(100) Dt.Make(100)
+
+    var K: DtCovariant<Z> := MakeCovariant(c);
+    var M: DtCovariant<X> := K;
+    var N: DtCovariant<Y> := K;
+    M := var u: DtCovariant<Z> := N; u; // like M := N, but allowed by Dafny's type system
+    N := var u: DtCovariant<Z> := M; u; // like N := M, but allowed by Dafny's type system
+    print K, " ", M, " ", N, "\n"; // DtCovariant.MakeCovariant(_module.C) DtCovariant.MakeCovariant(_module.C) DtCovariant.MakeCovariant(_module.C)
+  }
+}
+
+// ----- Vehicle -----
+
+module Conveyance {
+  trait Vehicle {
+  }
+  class Car extends Vehicle {
+    constructor() {}
+  }
+
+  trait Error {
+  }
+  class FlatTireError extends Error {
+    constructor() {}
+  }
+
+  datatype NonVariantResult<T, E> = NVSuccess(value: T) | NVFailure(error: E)
+  datatype CovariantResult<+T, +E> = CVSuccess(value: T) | CVFailure(error: E)
+
+  method Test() {
+    var myCar: Car := new Car();
+    var error: Error := new FlatTireError();
+
+    var cvSuccess: CovariantResult<Vehicle, Error> := CVSuccess(myCar);
+    var cvFailure: CovariantResult<Vehicle, Error> := CVFailure(error);
+
+    var nvSuccess: NonVariantResult<Vehicle, Error> := NVSuccess(myCar);
+    var nvFailure: NonVariantResult<Vehicle, Error> := NVFailure(error);
+
+    // This was and remains just fine
+    var nvCarSuccess: NonVariantResult<Car, Error> := NVSuccess(myCar);
+    // The following would not be type correct for the non-variant NonVariantResult:
+    //     var nvVehicleSuccess: NonVariantResult<Vehicle, Error> := nvCarSuccess; // RHS (...) not assignable to LHS (...)
+
+    // Once, the following was not support for the Java target, but now it is
+    var cvCarSuccess: CovariantResult<Car, Error> := CVSuccess(myCar);
+    var cvVehicleSuccess: CovariantResult<Vehicle, Error> := cvCarSuccess;
+
+    print nvCarSuccess, " ", cvCarSuccess, "\n"; // NonVariantResult.NVSuccess(_module.Car) CovariantResult.CVSuccess(_module.Car)
+  }
+}
diff --git a/Test/git-issues/git-issue-2013.dfy.expect b/Test/git-issues/git-issue-2013.dfy.expect
new file mode 100644
index 00000000000..8d95fab39df
--- /dev/null
+++ b/Test/git-issues/git-issue-2013.dfy.expect
@@ -0,0 +1,57 @@
+
+Dafny program verifier finished with 11 verified, 0 errors
+
+Dafny program verifier did not attempt verification
+16
+16
+Dt.Dt(12) Dt.Dt(30) Dt.Dt(30)
+Result.Success(8) Result.Failure(_module.MyClassException)
+{100} {100} {100}
+{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C}
+MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
+MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
+Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+
+Dafny program verifier did not attempt verification
+16
+16
+Dt.Dt(12) Dt.Dt(30) Dt.Dt(30)
+Result.Success(8) Result.Failure(_module.MyClassException)
+{100} {100} {100}
+{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C}
+MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
+MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
+Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+
+Dafny program verifier did not attempt verification
+16
+16
+Dt.Dt(12) Dt.Dt(30) Dt.Dt(30)
+Result.Success(8) Result.Failure(_module.MyClassException)
+{100} {100} {100}
+{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C}
+MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
+MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
+Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+
+Dafny program verifier did not attempt verification
+16
+16
+Dt.Dt(12) Dt.Dt(30) Dt.Dt(30)
+Result.Success(8) Result.Failure(_module.MyClassException)
+{100} {100} {100}
+{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C}
+MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
+MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
+Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+
+Dafny program verifier did not attempt verification
+16
+16
+Dt.Dt(12) Dt.Dt(30) Dt.Dt(30)
+Result.Success(8) Result.Failure(_module.MyClassException)
+{100} {100} {100}
+{MoreTests_Compile.C} {MoreTests_Compile.C} {MoreTests_Compile.C}
+MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
+MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
+Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)

From 6f9df38c2ebf8b810d3f4d93ef66170d8cc19c04 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 17 Nov 2022 17:05:48 -0800
Subject: [PATCH 08/15] Add release notes

---
 docs/dev/news/3072.feat | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 docs/dev/news/3072.feat

diff --git a/docs/dev/news/3072.feat b/docs/dev/news/3072.feat
new file mode 100644
index 00000000000..61770820602
--- /dev/null
+++ b/docs/dev/news/3072.feat
@@ -0,0 +1 @@
+feat: support for traits as type arguments with variance on datatypes in Java

From ddbf7436342c93429b9b170183733a661184a7b9 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 28 Nov 2022 17:25:20 -0800
Subject: [PATCH 09/15] Update Source/DafnyCore/Compilers/Compiler-Csharp.cs

Co-authored-by: Fabio Madge <fabio@madge.me>
---
 Source/DafnyCore/Compilers/Compiler-Csharp.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Compilers/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
index 44cdfbddab9..9edc63dee78 100644
--- a/Source/DafnyCore/Compilers/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
@@ -1743,7 +1743,7 @@ protected void DeclareField(string name, bool isPublic, bool isStatic, bool isCo
         if (isPublic) {
           if (isConst) {
             cw.InstanceMemberWriter.Write(
-              $"{publik}{konst} {virtuall} {typeName} {name} {{get;}}");
+              $"{publik}{konst}{virtuall} {typeName} {name} {{get;}}");
           } else {
             cw.InstanceMemberWriter.Write(
               $"{publik}{virtuall} {typeName} {name} {{get; set;}}");

From fdb63aa694e1c03c865386d2e6c95d4b839921c2 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 28 Nov 2022 17:25:35 -0800
Subject: [PATCH 10/15] Update Source/DafnyCore/Compilers/SinglePassCompiler.cs

Co-authored-by: Fabio Madge <fabio@madge.me>
---
 Source/DafnyCore/Compilers/SinglePassCompiler.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
index ee77ae7ff54..e271abe5fa7 100644
--- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs
+++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs
@@ -761,7 +761,7 @@ protected ConcreteSyntaxTree EmitDowncastIfNecessary(Type /*?*/ from, Type /*?*/
       Contract.Requires(wr != null);
       if (from != null && to != null) {
         if (!IsTargetSupertype(to, from)) {
-          // By the way, it is tempting that think that IsTargetSupertype(from, to)) would hold here, but that's not true.
+          // By the way, it is tempting to think that IsTargetSupertype(from, to)) would hold here, but that's not true.
           // For one, in a language with NeedsCastFromTypeParameter, "to" and "from" may contain uninstantiated formal type parameters.
           // Also, it is possible (subject to a check enforced by the verifier) to assign Datatype<X> to Datatype<Y>,
           // where Datatype is co-variant in its argument type and X and Y are two incomparable types with a common supertype.

From bbdfde3d89a54e3e8f1fcf9ada528a881da399b3 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 28 Nov 2022 17:29:55 -0800
Subject: [PATCH 11/15] Improve release notes

---
 docs/dev/news/3072.feat | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/dev/news/3072.feat b/docs/dev/news/3072.feat
index 61770820602..b7228598a1e 100644
--- a/docs/dev/news/3072.feat
+++ b/docs/dev/news/3072.feat
@@ -1 +1 @@
-feat: support for traits as type arguments with variance on datatypes in Java
+feat: support for traits as type arguments by fully allowing variance on datatypes in Java

From 52adeac05d97be994fb3cb53860414819e0a7a90 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 28 Nov 2022 17:30:24 -0800
Subject: [PATCH 12/15] Update Test/git-issues/git-issue-2013.dfy

Co-authored-by: Fabio Madge <fabio@madge.me>
---
 Test/git-issues/git-issue-2013.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Test/git-issues/git-issue-2013.dfy b/Test/git-issues/git-issue-2013.dfy
index 9c877ad3e83..da638fa5e08 100644
--- a/Test/git-issues/git-issue-2013.dfy
+++ b/Test/git-issues/git-issue-2013.dfy
@@ -132,7 +132,7 @@ module MoreTests {
     print S, " ", T, " ", U, "\n"; // {_module.C} {_module.C} {_module.C}
 
     // The assignments in the following example don't need covariance of Dt, because
-    // Dafny checks that the value with its payment is suitable for the target type.
+    // Dafny checks that the value with its payload is suitable for the target type.
     var k: Dt<int> := Make(100);
     var m: Dt<nat> := k;
     var n: Dt<Even> := k;

From 737a6ba89453fe007eed789b9790113127e04375 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 28 Nov 2022 17:30:54 -0800
Subject: [PATCH 13/15] Update Source/DafnyCore/Compilers/Compiler-java.cs

Co-authored-by: Fabio Madge <fabio@madge.me>
---
 Source/DafnyCore/Compilers/Compiler-java.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs
index cfc5f2368ab..2f68196912c 100644
--- a/Source/DafnyCore/Compilers/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Compiler-java.cs
@@ -940,8 +940,8 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
 
     private void EmitToString(string fullPrintName, ConcreteSyntaxTree wr) {
       wr.WriteLine("@Override");
-      var wrBody = wr.NewBlock("public java.lang.String toString()");
-      wrBody.WriteLine($"return \"{fullPrintName}\";");
+      wr.NewBlock("public java.lang.String toString()")
+        .WriteLine($"return \"{fullPrintName}\";");
     }
 
     /// <summary>

From 6da83bfc2f4a8f5f8575a9f01ae4b3d6731188d3 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 28 Nov 2022 17:35:03 -0800
Subject: [PATCH 14/15] Add some tests

---
 Test/git-issues/git-issue-2013.dfy | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Test/git-issues/git-issue-2013.dfy b/Test/git-issues/git-issue-2013.dfy
index da638fa5e08..1eef6636232 100644
--- a/Test/git-issues/git-issue-2013.dfy
+++ b/Test/git-issues/git-issue-2013.dfy
@@ -122,6 +122,8 @@ module MoreTests {
     var u: set<Even> := s;
     t := u;
     u := t;
+    s := u;
+    s := t;
     print s, " ", t, " ", u, "\n"; // {100} {100} {100}
 
     var S: set<Z> := {c};
@@ -129,6 +131,8 @@ module MoreTests {
     var U: set<Y> := S;
     T := U;
     U := T;
+    S := U;
+    S := T;
     print S, " ", T, " ", U, "\n"; // {_module.C} {_module.C} {_module.C}
 
     // The assignments in the following example don't need covariance of Dt, because
@@ -138,6 +142,8 @@ module MoreTests {
     var n: Dt<Even> := k;
     m := n;
     n := m;
+    k := m;
+    k := n;
     print k, " ", m, " ", n, "\n"; // Dt.Make(100) Dt.Make(100) Dt.Make(100)
 
     var K: DtCovariant<Z> := MakeCovariant(c);

From 07d4a446fffda182870e76061034830512a1f9c1 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 28 Nov 2022 17:59:52 -0800
Subject: [PATCH 15/15] fix: Qualify codatatype in other module

---
 Source/DafnyCore/Compilers/Compiler-Csharp.cs |  6 ++---
 Source/DafnyCore/Compilers/Compiler-go.cs     |  3 ++-
 Source/DafnyCore/Compilers/Compiler-java.cs   |  2 +-
 Test/git-issues/git-issue-2013.dfy            | 22 +++++++++++++++++++
 Test/git-issues/git-issue-2013.dfy.expect     |  7 +++++-
 5 files changed, 34 insertions(+), 6 deletions(-)

diff --git a/Source/DafnyCore/Compilers/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
index 9edc63dee78..de791b58ec2 100644
--- a/Source/DafnyCore/Compilers/Compiler-Csharp.cs
+++ b/Source/DafnyCore/Compilers/Compiler-Csharp.cs
@@ -522,7 +522,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
         if (dt is CoDatatypeDecl) {
           var wCo = wDefault;
           wDefault = new ConcreteSyntaxTree();
-          wCo.Format($"new {dt.CompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})");
+          wCo.Format($"new {dt.FullCompileName}__Lazy{DtT_TypeArgs}(() => {{ return {wDefault}; }})");
         }
 
         wDefault.Write(DtCreateName(groundingCtor));
@@ -609,7 +609,7 @@ bool InvalidType(Type ty, bool refTy) =>
       var typeArgs = TypeParameters(nonGhostTypeArgs);
       var dtArgs = "_I" + datatype.CompileName + uTypeArgs;
       var converters = $"{nonGhostTypeArgs.Comma((_, i) => $"converter{i}")}";
-      var lazyClass = $"{datatype.CompileName}__Lazy";
+      var lazyClass = $"{datatype.FullCompileName}__Lazy";
       string PrintConverter(TypeParameter tArg, int i) {
         var name = IdName(tArg);
         return $"Func<{name}, __{name}> converter{i}";
@@ -2390,7 +2390,7 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string arguments, C
         //     new Dt__Lazy<T>( LAMBDA )
         // where LAMBDA is:
         //     () => { return Dt_Cons<T>( ...args... ); }
-        wr.Write($"new {dtv.DatatypeName}__Lazy{typeParams}(");
+        wr.Write($"new {dtName}__Lazy{typeParams}(");
         wr.Write("() => { return ");
         wr.Write("new {0}({1})", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr), arguments);
         wr.Write("; })");
diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs
index d680e496e36..832e95b7459 100644
--- a/Source/DafnyCore/Compilers/Compiler-go.cs
+++ b/Source/DafnyCore/Compilers/Compiler-go.cs
@@ -2477,7 +2477,8 @@ void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, bool isCoCall, string
       } else {
         // Co-recursive call
         // Generate:  Companion_Dt_.LazyDt(func () Dt => Companion_Dt_.CreateCtor(args))
-        wr.Write("{0}.{1}(func () {2} ", companionName, FormatLazyConstructorName(dt.CompileName), IdName(dt));
+        wr.Write("{0}.{1}(func () {2} ", companionName, FormatLazyConstructorName(dt.CompileName),
+          TypeName(UserDefinedType.FromTopLevelDecl(dt.tok, dt), wr, dt.tok));
         wr.Write("{{ return {0}.{1}({2}) }}", companionName, FormatDatatypeConstructorName(ctorName), arguments);
         wr.Write(')');
       }
diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs
index 2f68196912c..c180f4c03ee 100644
--- a/Source/DafnyCore/Compilers/Compiler-java.cs
+++ b/Source/DafnyCore/Compilers/Compiler-java.cs
@@ -1965,7 +1965,7 @@ void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx) {
         wr.WriteLine();
         EmitSuppression(wr); //TODO: Fix implementations so they do not need this suppression
         var w = wr.NewNamedBlock($"public class {dt.CompileName}__Lazy{typeParams} extends {IdName(dt)}{typeParams}");
-        w.WriteLine($"interface Computer {{ {dt.CompileName} run(); }}");
+        w.WriteLine($"public interface Computer {{ {dt.CompileName} run(); }}");
         w.WriteLine("Computer c;");
         w.WriteLine($"{dt.CompileName}{typeParams} d;");
         w.WriteLine($"public {dt.CompileName}__Lazy(Computer c) {{ this.c = c; }}");
diff --git a/Test/git-issues/git-issue-2013.dfy b/Test/git-issues/git-issue-2013.dfy
index 1eef6636232..7705f3d49dc 100644
--- a/Test/git-issues/git-issue-2013.dfy
+++ b/Test/git-issues/git-issue-2013.dfy
@@ -13,6 +13,7 @@ method Main() {
   TestException();
   MoreTests.Test();
   Conveyance.Test();
+  Regression.Test();
 }
 
 // ----- reference types -----
@@ -195,3 +196,24 @@ module Conveyance {
     print nvCarSuccess, " ", cvCarSuccess, "\n"; // NonVariantResult.NVSuccess(_module.Car) CovariantResult.CVSuccess(_module.Car)
   }
 }
+
+// ----- Regression test -----
+
+module Regression {
+  module M {
+    // A previous bug was that the following declaration was not exported correctly (in several compilers).
+    codatatype Stream<T> = Next(shead: T, stail: Stream)
+  }
+
+  function method CoUp(n: int, b: bool): M.Stream<int>
+  {
+    if b then
+      CoUp(n, false)  // recursive, not co-recursive, call
+    else
+      M.Next(n, CoUp(n+1, true))  // CoUp is co-recursive call
+  }
+
+  method Test(){
+    print CoUp(0, false), "\n";
+  }
+}
diff --git a/Test/git-issues/git-issue-2013.dfy.expect b/Test/git-issues/git-issue-2013.dfy.expect
index 8d95fab39df..15a160ae382 100644
--- a/Test/git-issues/git-issue-2013.dfy.expect
+++ b/Test/git-issues/git-issue-2013.dfy.expect
@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
 
 Dafny program verifier did not attempt verification
 16
@@ -11,6 +11,7 @@ Result.Success(8) Result.Failure(_module.MyClassException)
 MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
 MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
 Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+Regression_mM_Compile.Stream.Next
 
 Dafny program verifier did not attempt verification
 16
@@ -22,6 +23,7 @@ Result.Success(8) Result.Failure(_module.MyClassException)
 MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
 MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
 Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+Regression_mM_Compile.Stream.Next
 
 Dafny program verifier did not attempt verification
 16
@@ -33,6 +35,7 @@ Result.Success(8) Result.Failure(_module.MyClassException)
 MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
 MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
 Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+Regression_mM_Compile.Stream.Next
 
 Dafny program verifier did not attempt verification
 16
@@ -44,6 +47,7 @@ Result.Success(8) Result.Failure(_module.MyClassException)
 MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
 MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
 Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+Regression_mM_Compile.Stream.Next
 
 Dafny program verifier did not attempt verification
 16
@@ -55,3 +59,4 @@ Result.Success(8) Result.Failure(_module.MyClassException)
 MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100) MoreTests_Compile.Dt.Make(100)
 MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C) MoreTests_Compile.DtCovariant.MakeCovariant(MoreTests_Compile.C)
 Conveyance_Compile.NonVariantResult.NVSuccess(Conveyance_Compile.Car) Conveyance_Compile.CovariantResult.CVSuccess(Conveyance_Compile.Car)
+Regression_mM_Compile.Stream.Next