Allow non-reference-type traits

Source/DafnyCore/AST/Cloner.cs

@@ -64,7 +64,10 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition pa
 
       if (d is AbstractTypeDecl) {
         var dd = (AbstractTypeDecl)d;
-        return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
+        return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent,
+          CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam),
+          dd.ParentTraits.ConvertAll(CloneType),
+          dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
       } else if (d is SubsetTypeDecl) {
         Contract.Assume(!(d is NonNullTypeDecl));  // don't clone the non-null type declaration; close the class, which will create a new non-null type declaration
         var dd = (SubsetTypeDecl)d;
@@ -78,10 +81,12 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition pa
         var dd = (NewtypeDecl)d;
         if (dd.Var == null) {
           return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, CloneType(dd.BaseType),
+            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), parent, 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);
         }
       } else if (d is TupleTypeDecl) {
@@ -92,13 +97,17 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition pa
         var dd = (IndDatatypeDecl)d;
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
         var ctors = dd.Ctors.ConvertAll(CloneCtor);
-        var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
+        var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, ctors,
+          dd.ParentTraits.ConvertAll(CloneType),
+          dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         return dt;
       } else if (d is CoDatatypeDecl) {
         var dd = (CoDatatypeDecl)d;
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
         var ctors = dd.Ctors.ConvertAll(CloneCtor);
-        var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, ctors, dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
+        var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), parent, tps, ctors,
+          dd.ParentTraits.ConvertAll(CloneType),
+          dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
         return dt;
       } else if (d is IteratorDecl) {
         var dd = (IteratorDecl)d;

Source/DafnyCore/AST/Grammar/ParseErrors.cs

@@ -137,7 +137,7 @@ public enum ErrorId {
     p_deprecated_statement_refinement,
     p_internal_exception,
     p_file_has_no_code,
-
+    p_general_traits_beta,
   }
 
   static ParseErrors() {
@@ -153,6 +153,10 @@ static ParseErrors() {
 Only modules may be declared abstract.
 ", Remove(true));
 
+    Add(ErrorId.p_general_traits_beta,
+      @"Use of traits as non-reference types is a beta feature. To engage, use /generalTraits:1.
+", Remove(true));
+
     Add(ErrorId.p_no_ghost_for_by_method,
     @"
 Functions with a [by method](https://dafny.org/latest/DafnyRef/DafnyRef#sec-function-declarations)

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -271,6 +271,7 @@ public void PrintTopLevelDecls(Program program, IEnumerable<TopLevelDecl> decls,
           if (i++ != 0) { wr.WriteLine(); }
           Indent(indent);
           PrintClassMethodHelper("type", at.Attributes, at.Name + TPCharacteristicsSuffix(at.Characteristics), d.TypeArgs);
+          PrintExtendsClause(at);
           if (at.Members.Count == 0) {
             wr.WriteLine();
           } else {
@@ -284,6 +285,7 @@ public void PrintTopLevelDecls(Program program, IEnumerable<TopLevelDecl> decls,
           if (i++ != 0) { wr.WriteLine(); }
           Indent(indent);
           PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List<TypeParameter>());
+          PrintExtendsClause(dd);
           wr.Write(" = ");
           if (dd.Var == null) {
             PrintType(dd.BaseType);
@@ -359,6 +361,11 @@ public void PrintTopLevelDecls(Program program, IEnumerable<TopLevelDecl> decls,
           if (i++ != 0) { wr.WriteLine(); }
           PrintClass(cl, indent, fileBeingPrinted);
 
+        } else if (d is ClassLikeDecl) {
+          var cl = (ClassLikeDecl)d;
+          if (i++ != 0) { wr.WriteLine(); }
+          PrintClass(cl, indent, fileBeingPrinted);
+
         } else if (d is ValuetypeDecl) {
           var vtd = (ValuetypeDecl)d;
           if (i++ != 0) { wr.WriteLine(); }
@@ -608,7 +615,7 @@ void PrintIteratorSignature(IteratorDecl iter, int indent) {
       Indent(indent);
       PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs);
       if (iter.IsRefining) {
-        wr.Write(" ... ");
+        wr.Write(" ...");
       } else {
         PrintFormals(iter.Ins, iter);
         if (iter.Outs.Count != 0) {
@@ -654,14 +661,9 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
       Indent(indent);
       PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
       if (c.IsRefining) {
-        wr.Write(" ... ");
+        wr.Write(" ...");
       } else {
-        string sep = " extends ";
-        foreach (var trait in c.ParentTraits) {
-          wr.Write(sep);
-          PrintType(trait);
-          sep = ", ";
-        }
+        PrintExtendsClause(c);
       }
 
       if (c.Members.Count == 0) {
@@ -684,6 +686,15 @@ public void PrintClass(ClassLikeDecl c, int indent, string fileBeingPrinted) {
       }
     }
 
+    private void PrintExtendsClause(TopLevelDeclWithMembers c) {
+      string sep = " extends ";
+      foreach (var trait in c.ParentTraits) {
+        wr.Write(sep);
+        PrintType(trait);
+        sep = ", ";
+      }
+    }
+
     public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingPrinted) {
       Contract.Requires(members != null);
 
@@ -809,6 +820,7 @@ public void PrintDatatype(DatatypeDecl dt, int indent, string fileBeingPrinted)
       Contract.Requires(dt != null);
       Indent(indent);
       PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs);
+      PrintExtendsClause(dt);
       wr.Write(" =");
       string sep = "";
       foreach (DatatypeCtor ctor in dt.Ctors) {

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -123,8 +123,8 @@ public static void AddParseResultToProgram(DfyParseResult parseResult, Program p
         literalModuleDecl.ModuleDef.EnclosingModule = defaultModule;
       }
 
-      if (declToMove is ClassLikeDecl classDecl) {
-        classDecl.NonNullTypeDecl.EnclosingModuleDefinition = defaultModule;
+      if (declToMove is ClassLikeDecl { NonNullTypeDecl: { } nonNullTypeDecl }) {
+        nonNullTypeDecl.EnclosingModuleDefinition = defaultModule;
       }
       if (declToMove is DefaultClassDecl defaultClassDecl) {
         foreach (var member in defaultClassDecl.Members) {

Source/DafnyCore/AST/Modules/ScopeCloner.cs

@@ -94,7 +94,10 @@ public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m
       var tps = d.TypeArgs.ConvertAll(CloneTypeParam);
       var characteristics = TypeParameter.GetExplicitCharacteristics(d);
       var members = based is TopLevelDeclWithMembers tm ? tm.Members : new List<MemberDecl>();
-      var otd = new AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps, members, CloneAttributes(d.Attributes), d.IsRefining);
+      // copy the parent traits only if "d" is already an AbstractTypeDecl and is being export-revealed
+      var otd = new AbstractTypeDecl(Range(d.RangeToken), d.NameNode.Clone(this), m, characteristics, tps,
+        new List<Type>(), // omit the parent traits
+        members, CloneAttributes(d.Attributes), d.IsRefining);
       based = otd;
       if (d is ClassLikeDecl { IsReferenceTypeDecl: true } cl) {
         reverseMap.Add(based, cl.NonNullTypeDecl);

Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs

@@ -11,8 +11,9 @@ public bool SupportsEquality {
     get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; }
   }
 
-  public AbstractTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List<TypeParameter> typeArgs, List<MemberDecl> members, Attributes attributes, bool isRefining)
-    : base(rangeToken, name, module, typeArgs, members, attributes, isRefining) {
+  public AbstractTypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics,
+    List<TypeParameter> typeArgs, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
+    : base(rangeToken, name, module, typeArgs, members, attributes, isRefining, parentTraits) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);

Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs

@@ -8,7 +8,6 @@ public class ClassDecl : ClassLikeDecl, IHasDocstring {
   public override bool IsReferenceTypeDecl => true;
   public override bool AcceptThis => true;
 
-  public override bool CanBeRevealed() { return true; }
   [FilledInDuringResolution] public bool HasConstructor;  // filled in (early) during resolution; true iff there exists a member that is a Constructor
   [ContractInvariantMethod]
   void ObjectInvariant() {

Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs

@@ -6,9 +6,18 @@ namespace Microsoft.Dafny;
 public abstract class ClassLikeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICanFormat {
   public NonNullTypeDecl NonNullTypeDecl; // returns non-null value iff IsReferenceTypeDecl
 
+  public override bool CanBeRevealed() { return true; }
+
   public bool IsObjectTrait {
     get => Name == "object";
   }
+
+  /// <summary>
+  /// The IsReferenceTypeDecl getter must not be called before this information is available.
+  /// For most types, this information is known immediately, but for a TraitDecl, the information is not known until
+  /// SetUpAsReferenceType has been called. The SetUpAsReferenceType method is called very early during resolution,
+  /// namely during name registration of the enclosing module.
+  /// </summary>
   public abstract bool IsReferenceTypeDecl { get; }
 
   public TopLevelDecl AsTopLevelDecl => this;
@@ -63,18 +72,6 @@ public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatte
     return true;
   }
 
-  public List<Type> PossiblyNullTraitsWithArgument(List<Type> typeArgs) {
-    Contract.Requires(typeArgs != null);
-    Contract.Requires(typeArgs.Count == TypeArgs.Count);
-    // Instantiate with the actual type arguments
-    var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArgs);
-    return ParentTraits.ConvertAll(traitType => (Type)UserDefinedType.CreateNullableType((UserDefinedType)traitType.Subst(subst)));
-  }
-
-  public override List<Type> ParentTypes(List<Type> typeArgs) {
-    return PossiblyNullTraitsWithArgument(typeArgs);
-  }
-
   protected override string GetTriviaContainingDocstring() {
     IToken candidate = null;
     foreach (var token in OwnedTokens) {

Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs

@@ -9,8 +9,8 @@ public class CoDatatypeDecl : DatatypeDecl {
   [FilledInDuringResolution] public CoDatatypeDecl SscRepr;
 
   public CoDatatypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, List<TypeParameter> typeArgs,
-    [Captured] List<DatatypeCtor> ctors, List<MemberDecl> members, Attributes attributes, bool isRefining)
-    : base(rangeToken, name, module, typeArgs, ctors, members, attributes, isRefining) {
+    [Captured] List<DatatypeCtor> ctors, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
+    : base(rangeToken, name, module, typeArgs, ctors, parentTraits, members, attributes, isRefining) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);

Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs

@@ -20,8 +20,8 @@ void ObjectInvariant() {
   public override IEnumerable<Node> PreResolveChildren => Ctors.Concat<Node>(base.PreResolveChildren);
 
   public DatatypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, List<TypeParameter> typeArgs,
-    [Captured] List<DatatypeCtor> ctors, List<MemberDecl> members, Attributes attributes, bool isRefining)
-    : base(rangeToken, name, module, typeArgs, members, attributes, isRefining) {
+    [Captured] List<DatatypeCtor> ctors, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
+    : base(rangeToken, name, module, typeArgs, members, attributes, isRefining, parentTraits) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);

Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs

@@ -17,8 +17,8 @@ public enum ES { NotYetComputed, Never, ConsultTypeArguments }
   public ES EqualitySupport = ES.NotYetComputed;
 
   public IndDatatypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, List<TypeParameter> typeArgs,
-    [Captured] List<DatatypeCtor> ctors, List<MemberDecl> members, Attributes attributes, bool isRefining)
-    : base(rangeToken, name, module, typeArgs, ctors, members, attributes, isRefining) {
+    [Captured] List<DatatypeCtor> ctors, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
+    : base(rangeToken, name, module, typeArgs, ctors, parentTraits, members, attributes, isRefining) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -15,17 +15,19 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect
   public SubsetTypeDecl.WKind WitnessKind { get; set; } = SubsetTypeDecl.WKind.CompiledZero;
   public Expression/*?*/ Witness { get; set; } // non-null iff WitnessKind is Compiled or Ghost
   [FilledInDuringResolution] public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers)
-  public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Type baseType, List<MemberDecl> members, Attributes attributes, bool isRefining)
-    : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining) {
+  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) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);
     Contract.Requires(isRefining ^ (baseType != null));
     Contract.Requires(members != null);
     BaseType = baseType;
   }
-  public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint, SubsetTypeDecl.WKind witnessKind, Expression witness, List<MemberDecl> members, Attributes attributes, bool isRefining)
-    : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining) {
+  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) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(module != null);

Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs

@@ -39,7 +39,7 @@ public override List<Type> ParentTypes(List<Type> typeArgs) {
     foreach (var rhsParentType in Class.ParentTypes(typeArgs)) {
       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.CreateNonNullType(rhsParentUdt));
+      result.Add(UserDefinedType.CreateNonNullTypeIfReferenceType(rhsParentUdt));
     }
 
     return result;

Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs

@@ -96,6 +96,21 @@ public void SetMembersBeforeResolution() {
     MembersBeforeResolution = Members.ToImmutableList();
   }
 
+  public List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
+    Contract.Requires(typeArgs != null);
+    Contract.Requires(typeArgs.Count == TypeArgs.Count);
+    // Instantiate with the actual type arguments
+    var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArgs);
+    return ParentTraits.ConvertAll(traitType => {
+      var ty = (UserDefinedType)traitType.Subst(subst);
+      return (Type)UserDefinedType.CreateNullableTypeIfReferenceType(ty);
+    });
+  }
+
+  public override List<Type> ParentTypes(List<Type> typeArgs) {
+    return RawTraitsWithArgument(typeArgs);
+  }
+
   public static List<UserDefinedType> CommonTraits(TopLevelDeclWithMembers a, TopLevelDeclWithMembers b) {
     Contract.Requires(a != null);
     Contract.Requires(b != null);
@@ -132,8 +147,12 @@ private void AddTraitAncestors(ISet<TraitDecl> s) {
     Contract.Requires(s != null);
     foreach (var parent in ParentTraits) {
       var udt = (UserDefinedType)parent;  // in a successfully resolved program, we expect all .ParentTraits to be a UserDefinedType
-      var nntd = (NonNullTypeDecl)udt.ResolvedClass;  // we expect the trait type to be the non-null version of the trait type
-      var tr = (TraitDecl)nntd.Class;
+      TraitDecl tr;
+      if (udt.ResolvedClass is NonNullTypeDecl nntd) {
+        tr = (TraitDecl)nntd.Class;
+      } else {
+        tr = (TraitDecl)udt.ResolvedClass;
+      }
       s.Add(tr);
       tr.AddTraitAncestors(s);
     }

Source/DafnyCore/AST/TypeDeclarations/TraitDecl.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using Microsoft.Dafny.Auditor;
+using System.Diagnostics.Contracts;
 
 namespace Microsoft.Dafny;
 
@@ -8,14 +9,25 @@ public class TraitDecl : ClassLikeDecl {
   public bool IsParent { set; get; }
   public override bool AcceptThis => true;
 
-  public override bool IsReferenceTypeDecl => true; // SOON: IsObjectTrait || ParentTraits.Any(parent => parent.IsRefType);
+  internal void SetUpAsReferenceType(bool isReferenceType) {
+    // Note, it's important to set .NonNullTypeDecl first, before calling NewSelfSynonym(), since the latter will look at the former.
+    Contract.Assert(NonNullTypeDecl == null); // SetUpAsReferenceType should be called only once
+    if (isReferenceType) {
+      NonNullTypeDecl = new NonNullTypeDecl(this);
+    }
+
+    this.NewSelfSynonym();
+  }
 
+  public override bool IsReferenceTypeDecl => NonNullTypeDecl != null;
+
+  /// <summary>
+  /// This constructor creates a TraitDecl object. However, before the object really functions as a TraitDecl, it is necessary
+  /// to call SetUpAsReferenceType, which sets .NonNullTypeDecl (if necessary) and calls NewSelfSynonym().
+  /// </summary>
   public TraitDecl(RangeToken rangeToken, Name name, ModuleDefinition module,
     List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, bool isRefining, List<Type> /*?*/ traits)
     : base(rangeToken, name, module, typeArgs, members, attributes, isRefining, traits) {
-
-    NonNullTypeDecl = new NonNullTypeDecl(this); // SOON: this should be done only if the trait is a reference type
-    this.NewSelfSynonym();
   }
 
   public override IEnumerable<Assumption> Assumptions(Declaration decl) {