feat: support for traits as type arguments with variance on datatypes…

… in Java (#3072)

This PR removes that pesky "not supported" error for Java where it
wouldn't allow a `trait` to be passed in as a variant type parameter of
a (co)datatype.

Fixes #2013

The solution is pretty simple. Basically, it just emits casts when
needed. To be accepted by Java's static type checker, these casts first
upcast to `Object` and then downcast to the desired type. Since the JVM
doesn't keep track of type parameters, it'll never know what hit it. (In
particular, this means that we don't need the expensive `DowncastClone`
mechanism that we're using for C# to satisfy .NET's more informed
runtime.)

To make it work, this PR also makes more precise the `IsTargetSupertype`
method for Java. In particular, to check if `A<X, Y>` is a supertype of
`B<U, V, W>`, first keep converting the latter up the `trait` parents of
`B` until it gets to `A` (if ever). This is already done for all the
compilers. Call the result `A<X', Y'>`. For the other compilers, one
would now start to see if the parameters `X, Y` are target supertypes of
`X', Y'` with variance in mind (for example, if the first type parameter
is contravariant, we would actually check if `X'` is a supertype of
`X`). For Java, however, we continue with variance in mind only if `A`
is a collection type (because those already have run-time support for
variance, using Java's bounded existential types). For non-collection
types, we instead check if `X, Y` are target-type equal to `X', Y'`. If
they are not, the compiler calls `EmitDowncast`. (To read these in the
code, look at `EmitDowncastIfNecessary` in `SinglePassCompiler.cs`.)

We could have used simple casts like this for collection types, too. But
since I already have those, I left those alone.


<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>

Co-authored-by: Fabio Madge <[email protected]>

Source/DafnyCore/AST/Types.cs

@@ -944,10 +944,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;
     }

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}";
@@ -1743,10 +1743,10 @@ 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;}}");
+              $"{publik}{virtuall} {typeName} {name} {{get; set;}}");
           }
         } else {
           cw.InstanceMemberWriter.WriteLine($"{publik}{konst} {typeName} {name}");
@@ -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("; })");

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(')');
       }

Source/DafnyCore/Compilers/Compiler-java.cs

@@ -841,15 +841,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;
@@ -938,9 +929,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");
+      wr.NewBlock("public java.lang.String toString()")
+        .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.
@@ -1835,7 +1838,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);
@@ -1960,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; }}");
@@ -2623,17 +2628,17 @@ 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 )
         wr.Write($"{dtName}.{typeParams}{DtCreateName(ctor)}({arguments})");
       } 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("; })");
       }
     }
@@ -3731,6 +3736,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 (to == NativeObjectType) {
         return false;
@@ -3802,7 +3811,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;

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -736,6 +736,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;
     }
@@ -759,9 +761,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 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.
+
           wr = EmitDowncast(from, to, tok, wr);
         }
       }
@@ -774,7 +778,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();
@@ -786,7 +790,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]);

Source/DafnyCore/Resolver/Resolver.cs

@@ -5329,7 +5329,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;
@@ -5389,7 +5389,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;

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)

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)

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;

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)

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

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}