feat: Allow type parameters on newtypes (dafny-lang#5495)

This PR adds the following language features:

* type parameters of `newtype` declarations
* optional `witness` clause of constraint-less `newtype` declarations
* tool tips show auto-completed type parameters
* tool tips show inferred `(==)` characteristics

Along the way, the PR also fixes two previous soundness issues:

* fix: Check the emptiness status of constraint-less `newtype`
declarations (dafny-lang#5520)
* fix: Don't let `newtype` well-formedness checking affect witness
checking (dafny-lang#5521)

Fixes dafny-lang#5520
Fixes dafny-lang#5521

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

Source/DafnyCore/AST/Cloner.cs

@@ -86,12 +86,13 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
       } else if (d is NewtypeDecl) {
         var dd = (NewtypeDecl)d;
         if (dd.Var == null) {
-          return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneType(dd.BaseType),
+          return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent,
+            CloneType(dd.BaseType), dd.WitnessKind, CloneExpr(dd.Witness),
             dd.ParentTraits.ConvertAll(CloneType),
             dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         } else {
-          return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, CloneBoundVar(dd.Var, false),
-            CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness),
+          return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent,
+            CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness),
             dd.ParentTraits.ConvertAll(CloneType),
             dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         }

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

@@ -308,11 +308,11 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
             wr.Write("| ");
             PrintExpression(dd.Constraint, true);
             wr.WriteLine();
-            if (dd.WitnessKind != SubsetTypeDecl.WKind.CompiledZero) {
-              Indent(indent + IndentAmount);
-              PrintWitnessClause(dd);
-              wr.WriteLine();
-            }
+          }
+          if (dd.WitnessKind != SubsetTypeDecl.WKind.CompiledZero) {
+            Indent(indent + IndentAmount);
+            PrintWitnessClause(dd);
+            wr.WriteLine();
           }
           if (dd.Members.Count != 0) {
             Indent(indent);
@@ -765,42 +765,43 @@ void PrintClassMethodHelper(string kind, Attributes attrs, string name, List<Typ
     private void PrintTypeParams(List<TypeParameter> typeArgs) {
       Contract.Requires(typeArgs != null);
       Contract.Requires(
-        typeArgs.All(tp => tp.Name.StartsWith("_")) ||
-        typeArgs.All(tp => !tp.Name.StartsWith("_")));
+        typeArgs.All(tp => tp.IsAutoCompleted) ||
+        typeArgs.All(tp => !tp.IsAutoCompleted));
 
-      if (typeArgs.Count != 0 && !typeArgs[0].Name.StartsWith("_")) {
+      if (typeArgs.Count != 0 && !typeArgs[0].IsAutoCompleted) {
         wr.Write("<{0}>", Util.Comma(typeArgs, TypeParamString));
       }
     }
 
+    public static string TypeParameterToString(TypeParameter tp) {
+      return TypeParamVariance(tp) + tp.Name + TPCharacteristicsSuffix(tp.Characteristics, true);
+    }
+
     public string TypeParamString(TypeParameter tp) {
       Contract.Requires(tp != null);
-      string variance;
+      var paramString = TypeParamVariance(tp) + tp.Name + TPCharacteristicsSuffix(tp.Characteristics);
+      foreach (var typeBound in tp.TypeBounds) {
+        paramString += $" extends {typeBound.TypeName(options, null, true)}";
+      }
+      return paramString;
+    }
+
+    public static string TypeParamVariance(TypeParameter tp) {
       switch (tp.VarianceSyntax) {
         case TypeParameter.TPVarianceSyntax.Covariant_Permissive:
-          variance = "*";
-          break;
+          return "*";
         case TypeParameter.TPVarianceSyntax.Covariant_Strict:
-          variance = "+";
-          break;
+          return "+";
         case TypeParameter.TPVarianceSyntax.NonVariant_Permissive:
-          variance = "!";
-          break;
+          return "!";
         case TypeParameter.TPVarianceSyntax.NonVariant_Strict:
-          variance = "";
-          break;
+          return "";
         case TypeParameter.TPVarianceSyntax.Contravariance:
-          variance = "-";
-          break;
+          return "-";
         default:
           Contract.Assert(false);  // unexpected VarianceSyntax
           throw new cce.UnreachableException();
       }
-      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) {
@@ -1184,9 +1185,13 @@ public void PrintType(string prefix, Type ty) {
     }
 
     public string TPCharacteristicsSuffix(TypeParameter.TypeParameterCharacteristics characteristics) {
+      return TPCharacteristicsSuffix(characteristics, options.DafnyPrintResolvedFile != null);
+    }
+
+    public static string TPCharacteristicsSuffix(TypeParameter.TypeParameterCharacteristics characteristics, bool printInferredTypeCharacteristics) {
       string s = null;
       if (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Required ||
-        (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.InferredRequired && options.DafnyPrintResolvedFile != null)) {
+          (characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.InferredRequired && printInferredTypeCharacteristics)) {
         s = "==";
       }
       if (characteristics.HasCompiledValue) {

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -145,6 +145,8 @@ public interface RedirectingTypeDecl : ICallable {
   Attributes Attributes { get; }
   ModuleDefinition Module { get; }
   BoundVar/*?*/ Var { get; }
+  PreType BasePreType { get; }
+  Type BaseType { get; }
   Expression/*?*/ Constraint { get; }
   SubsetTypeDecl.WKind WitnessKind { get; }
   Expression/*?*/ Witness { get; }  // non-null iff WitnessKind is Compiled or Ghost

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -9,6 +9,7 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect
   public override string WhatKind { get { return "newtype"; } }
   public override bool CanBeRevealed() { return true; }
   public PreType BasePreType;
+  PreType RedirectingTypeDecl.BasePreType => BasePreType;
   public Type BaseType { get; set; } // null when refining
   public BoundVar Var { get; set; }  // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType))
   public Expression Constraint { get; set; }  // is null iff Var is
@@ -31,19 +32,25 @@ bool RedirectingTypeDecl.ConstraintIsCompilable {
 
   [FilledInDuringResolution] public bool TargetTypeCoversAllBitPatterns; // "target complete" -- indicates that any bit pattern that can fill the target type is a value of the newtype
 
-  public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Type baseType, List<Type> parentTraits,
-    List<MemberDecl> members, Attributes attributes, bool isRefining)
-    : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining, parentTraits) {
+  public NewtypeDecl(RangeToken rangeToken, Name name, List<TypeParameter> typeParameters, ModuleDefinition module,
+    Type baseType,
+    SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
+    : base(rangeToken, name, module, typeParameters, members, attributes, isRefining, parentTraits) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);
     Contract.Requires(isRefining ^ (baseType != null));
+    Contract.Requires((witnessKind == SubsetTypeDecl.WKind.Compiled || witnessKind == SubsetTypeDecl.WKind.Ghost) == (witness != null));
     Contract.Requires(members != null);
     BaseType = baseType;
+    Witness = witness;
+    WitnessKind = witnessKind;
     this.NewSelfSynonym();
   }
-  public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint,
-    SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining) : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining, parentTraits) {
+  public NewtypeDecl(RangeToken rangeToken, Name name, List<TypeParameter> typeParameters, ModuleDefinition module,
+    BoundVar bv, Expression constraint,
+    SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
+    : base(rangeToken, name, module, typeParameters, members, attributes, isRefining, parentTraits) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);
@@ -60,11 +67,16 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Bo
 
   public Type ConcreteBaseType(List<Type> typeArguments) {
     Contract.Requires(TypeArgs.Count == typeArguments.Count);
+    if (typeArguments.Count == 0) {
+      // this optimization seems worthwhile
+      return BaseType;
+    }
     var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArguments);
     return BaseType.Subst(subst);
   }
 
-  /// <summary>  /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope.
+  /// <summary>
+  /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope.
   /// </summary>
   public Type RhsWithArgument(List<Type> typeArgs) {
     Contract.Requires(typeArgs != null);
@@ -78,21 +90,7 @@ public Type RhsWithArgument(List<Type> typeArgs) {
         return rtd.SelfSynonym(typeArgs);
       }
     }
-    return RhsWithArgumentIgnoringScope(typeArgs);
-  }
-  /// <summary>
-  /// Returns the declared .BaseType but with formal type arguments replaced by the given actuals.
-  /// </summary>
-  public Type RhsWithArgumentIgnoringScope(List<Type> typeArgs) {
-    Contract.Requires(typeArgs != null);
-    Contract.Requires(typeArgs.Count == TypeArgs.Count);
-    // Instantiate with the actual type arguments
-    if (typeArgs.Count == 0) {
-      // this optimization seems worthwhile
-      return BaseType;
-    } else {
-      return ConcreteBaseType(typeArgs);
-    }
+    return ConcreteBaseType(typeArgs);
   }
 
   public TopLevelDecl AsTopLevelDecl => this;
@@ -121,7 +119,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport {
   bool ICodeContext.IsGhost {
     get { throw new NotSupportedException(); }  // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper
   }
-  List<TypeParameter> ICodeContext.TypeArgs { get { return new List<TypeParameter>(); } }
+  List<TypeParameter> ICodeContext.TypeArgs { get { return TypeArgs; } }
   List<Formal> ICodeContext.Ins { get { return new List<Formal>(); } }
   ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } }
   bool ICodeContext.MustReverify { get { return false; } }

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -50,6 +50,8 @@ public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParame
       );
 
   BoundVar RedirectingTypeDecl.Var => Var;
+  PreType RedirectingTypeDecl.BasePreType => Var.PreType;
+  Type RedirectingTypeDecl.BaseType => Var.Type;
   Expression RedirectingTypeDecl.Constraint => Constraint;
   WKind RedirectingTypeDecl.WitnessKind => WitnessKind;
   Expression RedirectingTypeDecl.Witness => Witness;

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -64,6 +64,8 @@ public Type RhsWithArgumentIgnoringScope(List<Type> typeArgs) {
   Attributes RedirectingTypeDecl.Attributes { get { return Attributes; } }
   ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } }
   BoundVar RedirectingTypeDecl.Var { get { return null; } }
+  PreType RedirectingTypeDecl.BasePreType { get { return null; } }
+  Type RedirectingTypeDecl.BaseType { get { return null; } }
   Expression RedirectingTypeDecl.Constraint { get { return null; } }
 
   bool RedirectingTypeDecl.ConstraintIsCompilable {

Source/DafnyCore/AST/Types/TypeParameter.cs

@@ -7,10 +7,13 @@ namespace Microsoft.Dafny;
 public class TypeParameter : TopLevelDecl {
   public interface ParentType {
     string FullName { get; }
+    IToken Tok { get; }
   }
 
   public override string WhatKind => "type parameter";
 
+  public bool IsAutoCompleted => Name.StartsWith("_");
+
   ParentType parent;
   public ParentType Parent {
     get {

Source/DafnyCore/AST/Types/Types.cs

@@ -338,11 +338,10 @@ public bool IsNumericBased(NumericPersuasion p) {
       } else if (t.IsRealType) {
         return p == NumericPersuasion.Real;
       }
-      var d = t.AsNewtype;
-      if (d == null) {
+      if (t.AsNewtype is not { } newtypeDecl) {
         return false;
       }
-      t = d.BaseType;
+      t = newtypeDecl.RhsWithArgument(t.TypeArgs);
     }
   }
 

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -1572,19 +1572,19 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok,
         return "bool";
       } else if (xType is CharType) {
         return CharTypeName;
-      } else if (xType is IntType || xType is BigOrdinalType) {
+      } else if (xType is IntType or BigOrdinalType) {
         return "BigInteger";
       } else if (xType is RealType) {
         return "Dafny.BigRational";
       } else if (xType is BitvectorType) {
         var t = (BitvectorType)xType;
         return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigInteger";
       } else if (xType.AsNewtype != null && member == null) {  // when member is given, use UserDefinedType case below
-        var nativeType = xType.AsNewtype.NativeType;
-        if (nativeType != null) {
+        var newtypeDecl = xType.AsNewtype;
+        if (newtypeDecl.NativeType is { } nativeType) {
           return GetNativeTypeName(nativeType);
         }
-        return TypeName(xType.AsNewtype.BaseType, wr, tok);
+        return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok);
       } else if (xType.IsObjectQ) {
         return "object";
       } else if (xType.IsArrayType) {
@@ -1679,7 +1679,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
         return "false";
       } else if (xType is CharType) {
         return UnicodeCharEnabled ? $"new {CharTypeName}({CharType.DefaultValueAsString})" : CharType.DefaultValueAsString;
-      } else if (xType is IntType || xType is BigOrdinalType) {
+      } else if (xType is IntType or BigOrdinalType) {
         return "BigInteger.Zero";
       } else if (xType is RealType) {
         return "Dafny.BigRational.ZERO";
@@ -1708,7 +1708,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
         } else if (td.NativeType != null) {
           return "0";
         } else {
-          return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
+          return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
         }
       } else if (cl is SubsetTypeDecl) {
         var td = (SubsetTypeDecl)cl;

Source/DafnyCore/Backends/CodeGeneratorTypeExtensions.cs

@@ -14,8 +14,7 @@ public static class CompilerTypeExtensions {
   /// </summary>
   public static Type GetRuntimeType(this Type typ) {
     while (typ.AsNewtype is { NativeType: null } newtypeDecl) {
-      var subst = TypeParameter.SubstitutionMap(newtypeDecl.TypeArgs, typ.TypeArgs);
-      typ = newtypeDecl.BaseType.Subst(subst);
+      typ = newtypeDecl.ConcreteBaseType(typ.TypeArgs);
     }
     return typ.NormalizeExpand();
   }

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -923,7 +923,7 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe
         return "bool";
       } else if (xType is CharType) {
         return "char";
-      } else if (xType is IntType || xType is BigOrdinalType) {
+      } else if (xType is IntType or BigOrdinalType) {
         UnsupportedFeatureError(tok, Feature.UnboundedIntegers);
         return "BigNumber";
       } else if (xType is RealType) {
@@ -933,11 +933,11 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe
         var t = (BitvectorType)xType;
         return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "BigNumber";
       } else if (xType.AsNewtype != null) {
-        NativeType nativeType = xType.AsNewtype.NativeType;
-        if (nativeType != null) {
+        var newtypeDecl = xType.AsNewtype;
+        if (newtypeDecl.NativeType is { } nativeType) {
           return GetNativeTypeName(nativeType);
         }
-        return TypeName(xType.AsNewtype.BaseType, wr, tok);
+        return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok, member);
       } else if (xType.IsObjectQ) {
         return "object";
       } else if (xType.IsArrayType) {
@@ -1046,7 +1046,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
         } else if (td.NativeType != null) {
           return "0";
         } else {
-          return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
+          return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
         }
       } else if (cl is SubsetTypeDecl) {
         var td = (SubsetTypeDecl)cl;

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -1593,11 +1593,11 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok,
         var t = (BitvectorType)xType;
         return t.NativeType != null ? GetNativeTypeName(t.NativeType) : "_dafny.BV";
       } else if (xType.AsNewtype != null && member == null) {  // when member is given, use UserDefinedType case below
-        NativeType nativeType = xType.AsNewtype.NativeType;
-        if (nativeType != null) {
+        var newtypeDecl = xType.AsNewtype;
+        if (newtypeDecl.NativeType is { } nativeType) {
           return GetNativeTypeName(nativeType);
         }
-        return TypeName(xType.AsNewtype.BaseType, wr, tok);
+        return TypeName(newtypeDecl.ConcreteBaseType(xType.TypeArgs), wr, tok);
       } else if (xType.IsObjectQ) {
         return AnyType;
       } else if (xType.IsArrayType) {
@@ -1652,7 +1652,7 @@ string nil() {
         return "false";
       } else if (xType is CharType) {
         return $"{CharTypeName}({CharType.DefaultValueAsString})";
-      } else if (xType is IntType || xType is BigOrdinalType) {
+      } else if (xType is IntType or BigOrdinalType) {
         return "_dafny.Zero";
       } else if (xType is RealType) {
         return "_dafny.ZeroReal";
@@ -1696,7 +1696,7 @@ string nil() {
         } else if (td.NativeType != null) {
           return GetNativeTypeName(td.NativeType) + "(0)";
         } else {
-          return TypeInitializationValue(td.BaseType, wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
+          return TypeInitializationValue(td.ConcreteBaseType(udt.TypeArgs), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
         }
       } else if (cl is SubsetTypeDecl) {
         var td = (SubsetTypeDecl)cl;
@@ -3915,9 +3915,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Ty
           return w;
         }
       } else if (from.AsNewtype is { } fromNewtypeDecl) {
-        var subst = TypeParameter.SubstitutionMap(fromNewtypeDecl.TypeArgs, from.TypeArgs);
-        from = fromNewtypeDecl.BaseType.Subst(subst);
-        return EmitCoercionIfNecessary(from, to, tok, wr, toOrig);
+        return EmitCoercionIfNecessary(fromNewtypeDecl.ConcreteBaseType(from.TypeArgs), to, tok, wr, toOrig);
       } else {
         // It's unclear to me whether it's possible to hit this case with a valid Dafny program,
         // so I'm not using UnsupportedFeatureError for now.