chore: Update general-traits error message (#5191)

Previously, the error message for using `extends` with a non-reference
type said that this was a beta feature. It is supported, but requires
the CLI option. This PR rewords these error messages.

<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/Grammar/ParseErrors.cs

@@ -137,7 +137,8 @@ public enum ErrorId {
     p_deprecated_statement_refinement,
     p_internal_exception,
     p_file_has_no_code,
-    p_general_traits_beta,
+    p_general_traits_datatype,
+    p_general_traits_full,
   }
 
   static ParseErrors() {
@@ -153,9 +154,16 @@ static ParseErrors() {
 Only modules may be declared abstract.
 ".TrimStart(), Remove(true));
 
-    Add(ErrorId.p_general_traits_beta,
+    Add(ErrorId.p_general_traits_datatype,
       @"
-Use of traits as non-reference types is a beta feature. To engage, use /generalTraits:datatype.
+A newtype extending a trait is not generally supported. The option --general-traits=full causes
+Dafny to allow them in the input, but is not recommended.
+".TrimStart(), Remove(true));
+
+    Add(ErrorId.p_general_traits_full,
+      @"
+Use of traits as non-reference types is supported, but is not yet the default. Until it becomes the
+default, use --general--traits=datatype to enable it.
 ".TrimStart(), Remove(true));
 
     Add(ErrorId.p_no_ghost_for_by_method,

Source/DafnyCore/Dafny.atg

@@ -544,14 +544,16 @@ ClassDecl<DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out TopLevel
 ExtendsClause<. List<Type> parentTraits, out IToken tokenWithTrailingDocString, string requiresNonReferenceTraitsFor .>
 = (. Type parentTrait;
   .)
-  "extends"                   (. if (requiresNonReferenceTraitsFor == "newtype" && theOptions.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Full) {
-                                   SemErr(ErrorId.p_general_traits_beta, t,
-                                     $"{requiresNonReferenceTraitsFor} extending traits is a beta feature; use /generalTraits:full to engage");
-                                 } else if (requiresNonReferenceTraitsFor != null && theOptions.Get(CommonOptionBag.GeneralTraits) == CommonOptionBag.GeneralTraitsOptions.Legacy) {
-                                   SemErr(ErrorId.p_general_traits_beta, t,
-                                     $"{requiresNonReferenceTraitsFor} extending traits is a beta feature; use /generalTraits:datatype to engage");
-                                 }
-                              .)
+  "extends"
+    (. if (requiresNonReferenceTraitsFor == "newtype" && theOptions.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Full) {
+       SemErr(ErrorId.p_general_traits_full, t,
+         $"{requiresNonReferenceTraitsFor} extending traits is not fully supported (specifically, compilation of such types is not supported); " +
+         "to use them for verification only, use --general-traits=full");
+     } else if (requiresNonReferenceTraitsFor != null && theOptions.Get(CommonOptionBag.GeneralTraits) == CommonOptionBag.GeneralTraitsOptions.Legacy) {
+       SemErr(ErrorId.p_general_traits_datatype, t,
+         $"{requiresNonReferenceTraitsFor} extending traits is not yet enabled by default; use --general-traits=datatype to enable it");
+     }
+    .)
   Type<out parentTrait>       (. parentTraits.Add(parentTrait); tokenWithTrailingDocString = t; .)
   {"," Type<out parentTrait>  (. parentTraits.Add(parentTrait); tokenWithTrailingDocString = t; .) }
   .

docs/HowToFAQ/Errors-Parser.md

@@ -248,14 +248,25 @@ module N refines M { datatype D = ... Y | Z }
 There are limitations on refining a datatype, namely that the set of constructors cannot be changed.
 It is only allowed to add members to the body of the datatype.
 
-## **Error: datatype extending traits is a beta feature; use /generalTraits:datatype to engage** {#p_general_traits_beta}
+## **Error: datatype extending traits is not yet enabled by default; use --general-traits=datatype to enable it** {#p_general_traits_datatype}
 
 ```dafny
 trait Trait { }
 datatype D extends Trait = A | B
 ```
 
-Use of traits as non-reference types is a beta feature. To engage, use /generalTraits:datatype.
+A newtype extending a trait is not generally supported. The option --general-traits=full causes
+Dafny to allow them in the input, but is not recommended.
+
+## **Error: newtype extending traits is not fully supported (specifically, compilation of such types is not supported); to use them for verification only, use --general-traits=full** {#p_general_traits_full}
+
+```dafny
+trait Trait { }
+newtype N extends Trait = int
+```
+
+Use of traits as non-reference types is supported, but is not yet the default. Until it becomes the
+default, use --general--traits=datatype to enable it.
 
 ## **Warning: module-level const declarations are always non-instance, so the 'static' keyword is not allowed here {#p_module_level_const_always_static}
 

docs/HowToFAQ/Errors-Parser.template

@@ -204,7 +204,7 @@ module N refines M { datatype D = ... Y | Z }
 
 <!-- INSERT-TEXT -->
 
-## **Error: datatype extending traits is a beta feature; use /generalTraits:datatype to engage** {#p_general_traits_beta}
+## **Error: datatype extending traits is not yet enabled by default; use --general-traits=datatype to enable it** {#p_general_traits_datatype}
 
 ```dafny
 trait Trait { }
@@ -213,6 +213,15 @@ datatype D extends Trait = A | B
 
 <!-- INSERT-TEXT -->
 
+## **Error: newtype extending traits is not fully supported (specifically, compilation of such types is not supported); to use them for verification only, use --general-traits=full** {#p_general_traits_full}
+
+```dafny
+trait Trait { }
+newtype N extends Trait = int
+```
+
+<!-- INSERT-TEXT -->
+
 ## **Warning: module-level const declarations are always non-instance, so the 'static' keyword is not allowed here {#p_module_level_const_always_static}
 
 <!-- %check-resolve-warn -->