feat: Add bounded polymorphism (#5547)

# Description

This PR adds bounded polymorphism to the Dafny language. This feature
allows any formal type parameter to be declared with a suffix of any
number of

```
extends Type
```

clauses, where `Type` is any trait or subset type thereof. At call
sites, the actual type arguments are checked to be subtypes of the
listed type bounds. Where the formal type parameters are in scope, an
expression whose type is the type parameter can be converted to a
supertype of any of the type bounds by an explicit type conversion
(`as`). In some cases, the type conversion is inferred automatically and
can then be omitted from the program text.

The feature requires `--type-system-refresh` for full functionality.

Closes #5211 

# Example

For `test.dfy` being the program

``` dafny
trait Printable {
  method Print()
}

method SelectPrintReturn<T extends Printable>(operateOnLeft: bool, left: T, right: T) returns (r: T)
{
  r := if operateOnLeft then left else right;
  (r as Printable).Print();
}

datatype Dt extends Printable = Dt(u: int) {
  method Print() {
    print u, "\n";
  }
}

method Main() {
  var d0 := Dt(500);
  var d1 := Dt(702);
  var e0 := SelectPrintReturn(true, d0, d1); // 500
  var e1 := SelectPrintReturn(false, d0, d1); // 702
  print (d0, d1) == (d0, d1), "\n"; // true
}
```

we get:

```
> dafny run test.dfy --type-system-refresh --general-traits=datatype

Dafny program verifier finished with 3 verified, 0 errors
500
702
true
```

# Bonus

The PR also

* suppresses near-identical error messages (in particular, it reports
only one error for conditions that split into several checks, like the
type equality `A==B` which turns into both `A :> B` and `B >: A`)


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

Author: RustanLeino

Source/DafnyCore/AST/Cloner.cs

@@ -194,7 +194,7 @@ public DatatypeCtor CloneCtor(DatatypeCtor ct) {
     public TypeParameter CloneTypeParam(TypeParameter tp) {
       return (TypeParameter)typeParameterClones.GetOrCreate(tp,
         () => new TypeParameter(Range(tp.RangeToken), tp.NameNode.Clone(this), tp.VarianceSyntax,
-          CloneTPChar(tp.Characteristics)));
+          CloneTPChar(tp.Characteristics), tp.TypeBounds.ConvertAll(CloneType)));
     }
 
     public virtual MemberDecl CloneMember(MemberDecl member, bool isReference) {

Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs

@@ -238,7 +238,6 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field)
     var receiverType = obj.Type.NormalizeExpand();
     this.TypeApplication_AtEnclosingClass = receiverType.TypeArgs;
     this.TypeApplication_JustMember = new List<Type>();
-    this.ResolvedOutparameterTypes = new List<Type>();
 
     var typeMap = new Dictionary<TypeParameter, Type>();
     if (receiverType is UserDefinedType udt) {
@@ -299,4 +298,4 @@ public IEnumerable<IHasNavigationToken> GetReferences() {
   }
 
   public IToken NavigationToken => tok;
-}
+}

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -290,7 +290,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
           var dd = (NewtypeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
           Indent(indent);
-          PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List<TypeParameter>());
+          PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, dd.TypeArgs);
           PrintExtendsClause(dd);
           wr.Write(" = ");
           if (dd.Var == null) {
@@ -663,7 +663,7 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
       Contract.Requires(c != null);
 
       Indent(indent);
-      PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
+      PrintClassMethodHelper(c is TraitDecl ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
       if (c.IsRefining) {
         wr.Write(" ...");
       } else {
@@ -795,7 +795,11 @@ public string TypeParamString(TypeParameter tp) {
           Contract.Assert(false);  // unexpected VarianceSyntax
           throw new cce.UnreachableException();
       }
-      return variance + tp.Name + TPCharacteristicsSuffix(tp.Characteristics);
+      var paramString = variance + tp.Name + TPCharacteristicsSuffix(tp.Characteristics);
+      foreach (var typeBound in tp.TypeBounds) {
+        paramString += $" extends {typeBound.TypeName(options, null, true)}";
+      }
+      return paramString;
     }
 
     private void PrintArrowType(string arrow, string internalName, List<TypeParameter> typeArgs) {

Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs

@@ -13,7 +13,7 @@ public class NonNullTypeDecl : SubsetTypeDecl {
   /// in order to build values that depend on previously computed parameters.
   /// </summary>
   public NonNullTypeDecl(ClassLikeDecl cl)
-    : this(cl, cl.TypeArgs.ConvertAll(tp => new TypeParameter(tp.RangeToken, tp.NameNode, tp.VarianceSyntax, tp.Characteristics))) {
+    : this(cl, TypeParameter.CloneTypeParameters(cl.TypeArgs)) {
     Contract.Requires(cl != null);
   }
 
@@ -34,10 +34,10 @@ private NonNullTypeDecl(ClassLikeDecl cl, List<TypeParameter> tps, BoundVar id)
     Class = cl;
   }
 
-  public override List<Type> ParentTypes(List<Type> typeArgs) {
-    List<Type> result = new List<Type>(base.ParentTypes(typeArgs));
+  public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {
+    List<Type> result = new List<Type>(base.ParentTypes(typeArgs, includeTypeBounds));
 
-    foreach (var rhsParentType in Class.ParentTypes(typeArgs)) {
+    foreach (var rhsParentType in Class.ParentTypes(typeArgs, includeTypeBounds)) {
       var rhsParentUdt = (UserDefinedType)rhsParentType; // all parent types of .Class are expected to be possibly-null class types
       Contract.Assert(rhsParentUdt.ResolvedClass is TraitDecl);
       result.Add(UserDefinedType.CreateNonNullTypeIfReferenceType(rhsParentUdt));

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -54,7 +54,7 @@ public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParame
   WKind RedirectingTypeDecl.WitnessKind => WitnessKind;
   Expression RedirectingTypeDecl.Witness => Witness;
 
-  public override List<Type> ParentTypes(List<Type> typeArgs) {
+  public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {
     return new List<Type> { RhsWithArgument(typeArgs) };
   }
   public bool ShouldVerify => true; // This could be made more accurate

Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs

@@ -98,8 +98,10 @@ public TopLevelDecl ViewAsClass {
   ///     class C<X> extends J<X, int>
   /// C.ParentTypes(real) = J<real, int>    // non-null types C and J
   /// C?.ParentTypes(real) = J?<real, int>  // possibly-null type C? and J?
+  /// 
+  /// If "includeTypeBounds" is "true", then for a type parameter, ParentTypes() returns the type bounds.
   /// </summary>
-  public virtual List<Type> ParentTypes(List<Type> typeArgs) {
+  public virtual List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {
     Contract.Requires(typeArgs != null);
     Contract.Requires(this.TypeArgs.Count == typeArgs.Count);
     return new List<Type>();

Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs

@@ -104,7 +104,7 @@ public void SetMembersBeforeResolution() {
     MembersBeforeResolution = Members.ToImmutableList();
   }
 
-  public List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
+  private List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
     Contract.Requires(typeArgs != null);
     Contract.Requires(typeArgs.Count == TypeArgs.Count);
     // Instantiate with the actual type arguments
@@ -115,7 +115,7 @@ public List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
     });
   }
 
-  public override List<Type> ParentTypes(List<Type> typeArgs) {
+  public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {
     return RawTraitsWithArgument(typeArgs);
   }
 

Source/DafnyCore/AST/Types/TypeParameter.cs

@@ -171,16 +171,30 @@ public bool SupportsEquality {
   }
   public int PositionalIndex; // which type parameter this is (ie. in C<S, T, U>, S is 0, T is 1 and U is 2).
 
-  public TypeParameter(RangeToken rangeToken, Name name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics)
+  public readonly List<Type> TypeBounds;
+
+  public IEnumerable<TopLevelDecl> TypeBoundHeads {
+    get {
+      foreach (var typeBound in TypeBounds) {
+        if (typeBound is UserDefinedType { ResolvedClass: { } parentDecl }) {
+          yield return parentDecl;
+        }
+      }
+    }
+  }
+
+  public TypeParameter(RangeToken rangeToken, Name name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics,
+    List<Type> typeBounds)
     : base(rangeToken, name, null, new List<TypeParameter>(), null, false) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Characteristics = characteristics;
     VarianceSyntax = varianceS;
+    TypeBounds = typeBounds;
   }
 
   public TypeParameter(RangeToken rangeToken, Name name, TPVarianceSyntax varianceS)
-    : this(rangeToken, name, varianceS, new TypeParameterCharacteristics(false)) {
+    : this(rangeToken, name, varianceS, new TypeParameterCharacteristics(false), new List<Type>()) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
   }
@@ -191,6 +205,17 @@ public TypeParameter(RangeToken tok, Name name, int positionalIndex, ParentType
     Parent = parent;
   }
 
+  /// <summary>
+  /// Return a list of unresolved clones of the type parameters in "typeParameters".
+  /// </summary>
+  public static List<TypeParameter> CloneTypeParameters(List<TypeParameter> typeParameters) {
+    var cloner = new Cloner();
+    return typeParameters.ConvertAll(tp => {
+      var typeBounds = tp.TypeBounds.ConvertAll(cloner.CloneType);
+      return new TypeParameter(tp.RangeToken, tp.NameNode, tp.VarianceSyntax, tp.Characteristics, typeBounds);
+    });
+  }
+
   public override string FullName {
     get {
       // when debugging, print it all:
@@ -231,4 +256,7 @@ public static Dictionary<TypeParameter, Type> SubstitutionMap(List<TypeParameter
     return subst;
   }
 
+  public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {
+    return includeTypeBounds ? TypeBounds : new List<Type>();
+  }
 }

Source/DafnyCore/AST/Types/Types.cs

@@ -1665,7 +1665,7 @@ public bool ContainsProxy(TypeProxy proxy) {
     }
   }
 
-  public virtual List<Type> ParentTypes() {
+  public virtual List<Type> ParentTypes(bool includeTypeBounds) {
     return new List<Type>();
   }
 
@@ -1692,7 +1692,13 @@ public virtual bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignor
       return ignoreTypeArguments || CompatibleTypeArgs(super, sub);
     }
 
-    return sub.ParentTypes().Any(parentType => parentType.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity));
+    // There is a special case, namely when super is the non-null "object". Since "sub.ParentTypes()" only gives
+    // back the explicitly declared parent traits, the general case below may miss it.
+    if (super.IsObject) {
+      return sub.IsNonNullRefType;
+    }
+
+    return sub.ParentTypes(true).Any(parentType => parentType.IsSubtypeOf(super, ignoreTypeArguments, ignoreNullity));
   }
 
   public static bool CompatibleTypeArgs(Type super, Type sub) {

Source/DafnyCore/AST/Types/UserDefinedType.cs

@@ -503,8 +503,8 @@ public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl> visitedDatat
     return true;
   }
 
-  public override List<Type> ParentTypes() {
-    return ResolvedClass != null ? ResolvedClass.ParentTypes(TypeArgs) : base.ParentTypes();
+  public override List<Type> ParentTypes(bool includeTypeBounds) {
+    return ResolvedClass != null ? ResolvedClass.ParentTypes(TypeArgs, includeTypeBounds) : base.ParentTypes(includeTypeBounds);
   }
 
   public override bool IsSubtypeOf(Type super, bool ignoreTypeArguments, bool ignoreNullity) {

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -2748,18 +2748,24 @@ protected override void EmitIndexCollectionSelect(Expression source, Expression
 
     protected override void EmitIndexCollectionUpdate(Expression source, Expression index, Expression value,
         CollectionType resultCollectionType, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
-      if (resultCollectionType is SeqType or MapType) {
+      if (resultCollectionType is SeqType) {
         wr.Write(TypeHelperName(resultCollectionType, wr, source.tok) + ".Update");
         wr.Append(ParensList(
           Expr(source, inLetExprBody, wStmts),
           Expr(index, inLetExprBody, wStmts),
           CoercedExpr(value, resultCollectionType.ValueArg, inLetExprBody, wStmts)));
+      } else if (resultCollectionType is MapType resultMapType) {
+        wr.Write(TypeHelperName(resultCollectionType, wr, source.tok) + ".Update");
+        wr.Append(ParensList(
+          Expr(source, inLetExprBody, wStmts),
+          CoercedExpr(index, resultMapType.Domain, inLetExprBody, wStmts),
+          CoercedExpr(value, resultMapType.Range, inLetExprBody, wStmts)));
       } else {
         TrParenExpr(source, wr, inLetExprBody, wStmts);
         wr.Write(".Update");
         wr.Append(ParensList(
-          Expr(index, inLetExprBody, wStmts),
-          CoercedExpr(value, resultCollectionType.ValueArg, inLetExprBody, wStmts)));
+          CoercedExpr(index, resultCollectionType.ValueArg, inLetExprBody, wStmts),
+          Expr(value, inLetExprBody, wStmts)));
       }
     }
 
@@ -2890,12 +2896,14 @@ protected override ConcreteSyntaxTree ToFatPointer(Type type, ConcreteSyntaxTree
     protected override ConcreteSyntaxTree EmitDowncast(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) {
       from = from.NormalizeExpand();
       to = to.NormalizeExpand();
-      Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || from.IsRefType == to.IsRefType);
+      Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy ||
+                      from.IsRefType == to.IsRefType ||
+                      (from.IsTypeParameter && to.IsTraitType));
 
       var w = new ConcreteSyntaxTree();
       if (from.IsTraitType && to.AsNewtype != null) {
         wr.Format($"(({to.AsNewtype.GetFullCompileName(Options)})({w}))");
-      } else if (to.IsRefType || to.IsTraitType || from.IsTraitType) {
+      } else if (to.IsRefType || to.IsTraitType || from.IsTraitType || to.IsTypeParameter) {
         wr.Format($"(({TypeName(to, wr, tok)})({w}))");
       } else {
         Contract.Assert(Type.SameHead(from, to));

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -168,7 +168,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to
             to = toNonNull.RhsWithArgument(toUdt.TypeArgs);
           }
 
-          return EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree<ExprContainer>(nullConvert, this));
+          return base.EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree<ExprContainer>(nullConvert, this));
         } else {
           return base.EmitCoercionIfNecessary(from, to, tok, wr);
         }

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -2488,6 +2488,10 @@ private string IdName(Declaration decl) {
 
     protected override string PrefixForForcedCapitalization => "Go_";
 
+    public override Type ResultTypeAsViewedByFunctionBody(Function f) {
+      return f.Original.ResultType;
+    }
+
     protected override string IdMemberName(MemberSelectExpr mse) {
       return Capitalize(mse.MemberName);
     }
@@ -3899,7 +3903,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty
       } else if (to.IsTypeParameter || (from != null && EqualsUpToParameters(from, to))) {
         // do nothing
         return wr;
-      } else if (from != null && from.IsSubtypeOf(to, true, true)) {
+      } else if (from != null && !from.IsTypeParameter && from.IsSubtypeOf(to, true, true)) {
         // upcast
         return wr;
       } else if (from == null || from.IsTypeParameter || to.IsSubtypeOf(from, true, true)) {
@@ -3934,6 +3938,16 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty
       }
     }
 
+    protected override ConcreteSyntaxTree EmitDowncast(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) {
+      if (to.IsTraitType) {
+        wr.Write("{0}.CastTo_(", TypeName_Companion(to.AsTraitType, wr, tok));
+        var w = wr.Fork();
+        wr.Write(")");
+        return w;
+      }
+      return base.EmitDowncast(from, to, tok, wr);
+    }
+
     protected override ConcreteSyntaxTree EmitCoercionToNativeInt(ConcreteSyntaxTree wr) {
       var w = wr.Fork();
       wr.Write(".(int)");

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -1697,11 +1697,10 @@ protected override void EmitIndexCollectionSelect(Expression source, Expression
         ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
       // Taken from C# compiler, assuming source is a DafnySequence type.
       if (source.Type.NormalizeToAncestorType().AsMultiSetType is { } multiSetType) {
-        wr = EmitCoercionIfNecessary(from: NativeObjectType, to: Type.Int, tok: source.tok, wr: wr);
         wr.Write($"{DafnyMultiSetClass}.<{BoxedTypeName(multiSetType.Arg, wr, Token.NoToken)}>multiplicity(");
         TrParenExpr(source, wr, inLetExprBody, wStmts);
         wr.Write(", ");
-        wr.Append(Expr(index, inLetExprBody, wStmts));
+        wr.Append(JavaCoercedExpr(index, multiSetType.Arg, inLetExprBody, wStmts));
         wr.Write(")");
       } else if (source.Type.NormalizeToAncestorType().AsMapType is { } mapType) {
         wr = EmitCoercionIfNecessary(from: NativeObjectType, to: mapType.Range, tok: source.tok, wr: wr);
@@ -1731,21 +1730,31 @@ protected override void EmitIndexCollectionUpdate(Expression source, Expression
         wr.Append(Expr(source, inLetExprBody, wStmts));
         wr.Write(", ");
         TrExprAsInt(index, wr, inLetExprBody, wStmts);
+        wr.Write(", ");
+        wr.Append(JavaCoercedExpr(value, resultCollectionType.ValueArg, inLetExprBody, wStmts));
+        wr.Write(")");
       } else if (resultCollectionType.AsMapType is { } mapType) {
         wr.Write($"{DafnyMapClass}.<{BoxedTypeName(mapType.Domain, wr, Token.NoToken)}, {BoxedTypeName(mapType.Range, wr, Token.NoToken)}>update(");
         wr.Append(Expr(source, inLetExprBody, wStmts));
         wr.Write(", ");
-        wr.Append(Expr(index, inLetExprBody, wStmts));
+        wr.Append(JavaCoercedExpr(index, mapType.Domain, inLetExprBody, wStmts));
+        wr.Write(", ");
+        wr.Append(JavaCoercedExpr(value, mapType.Range, inLetExprBody, wStmts));
+        wr.Write(")");
       } else {
         Contract.Assert(resultCollectionType.AsMultiSetType != null);
         wr.Write($"{DafnyMultiSetClass}.<{BoxedTypeName(resultCollectionType.Arg, wr, Token.NoToken)}>update(");
         wr.Append(Expr(source, inLetExprBody, wStmts));
         wr.Write(", ");
-        wr.Append(Expr(index, inLetExprBody, wStmts));
+        wr.Append(JavaCoercedExpr(index, resultCollectionType.ValueArg, inLetExprBody, wStmts));
+        wr.Write(", ");
+        wr.Append(Expr(value, inLetExprBody, wStmts));
+        wr.Write(")");
       }
-      wr.Write(", ");
-      wr.Append(CoercedExpr(value, NativeObjectType, inLetExprBody, wStmts));
-      wr.Write(")");
+    }
+
+    private ConcreteSyntaxTree JavaCoercedExpr(Expression expr, Type toType, bool inLetExprBody, ConcreteSyntaxTree wStmts) {
+      return CoercedExpr(expr, expr.Type.IsTypeParameter ? toType : NativeObjectType, inLetExprBody, wStmts);
     }
 
     protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLeft, ConcreteSyntaxTree wr,

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs

@@ -290,11 +290,16 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
             var fromType = e.E.Type.GetRuntimeType();
             var toType = e.ToType.GetRuntimeType();
             Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy ||
-                            toType.IsRefType == fromType.IsRefType);
+                            toType.IsRefType == fromType.IsRefType ||
+                            (fromType.IsTypeParameter && toType.IsTraitType));
             if (toType.IsRefType || toType.IsTraitType || fromType.IsTraitType) {
               var w = EmitCoercionIfNecessary(e.E.Type, e.ToType, e.tok, wr);
               w = EmitDowncastIfNecessary(e.E.Type, e.ToType, e.tok, w);
               EmitExpr(e.E, inLetExprBody, w, wStmts);
+            } else if (e.E.Type.IsSubtypeOf(e.ToType, false, false)) {
+              // conversion is a no-op -- almost, because it may need a cast to deal with bounded type parameters
+              var w = EmitDowncastIfNecessary(e.E.Type, e.ToType, e.tok, wr);
+              EmitExpr(e.E, inLetExprBody, w, wStmts);
             } else {
               EmitConversionExpr(e.E, fromType, toType, inLetExprBody, wr, wStmts);
             }