fix: Optimize datatype wrappers only in the absence of trait parents (#…

…5234)

This PR makes two changes to when the "erase datatype wrapper"
optimization is engaged.

* The optimization is disabled if the datatype implements any traits.
(Previously, the optimization was still allowed under this condition,
which had caused malformed code, see issue #5233.)
* Allow the optimization in the presence of ghost fields. (Previously,
the optimization was disabled if the datatype contained _any_ fields.
But ghost fields pose no problems for compilation.)

Fixes #5233

### How has this been tested?

The tests (including the test case from the bug report) were added to
`comp/ErasableTypeWrappers.dfy`.

<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/Backends/DatatypeWrapperEraser.cs

@@ -136,9 +136,10 @@ public static bool GetInnerTypeOfErasableDatatypeWrapper(DafnyOptions options, D
     ///   2 -- be an inductive datatype (not a "codatatype"), and
     ///   3 -- have exactly one non-ghost constructor, and
     ///   4 -- that constructor must have exactly one non-ghost destructor parameter (say, "d" of type "D"), and
-    ///   5 -- have no fields declared as members, and
-    ///   6 -- the compiled parts of type "D" must not include the datatype itself, and
-    ///   7 -- not be declared with {:extern} (since extern code may rely on it being there).
+    ///   5 -- have no non-ghost fields declared as members, and
+    ///   6 -- have no parent traits, and
+    ///   7 -- the compiled parts of type "D" must not include the datatype itself, and
+    ///   8 -- not be declared with {:extern} (since extern code may rely on it being there).
     ///
     /// If the conditions above apply, then the method returns true and sets the out-parameter to the core DatatypeDestructor "d".
     /// From this return, the compiler (that is, the caller) will arrange to compile type "dt" as type "D".
@@ -161,12 +162,13 @@ public static bool IsErasableDatatypeWrapper(DafnyOptions options, DatatypeDecl
     }
 
     /// <summary>
-    /// Check for conditions 2, 3, 4, 5, and 7 (but not 0, 1, and 6) mentioned in the description of IsErasableDatatypeWrapper.
+    /// Check for conditions 2, 3, 4, 5, 6, and 8 (but not 0, 1, and 7) mentioned in the description of IsErasableDatatypeWrapper.
     /// </summary>
     private static bool FindUnwrappedCandidate(DafnyOptions options, DatatypeDecl datatypeDecl, out DatatypeDestructor coreDtor) {
       if (datatypeDecl is IndDatatypeDecl &&
           !datatypeDecl.IsExtern(options, out _, out _) &&
-          !datatypeDecl.Members.Any(member => member is Field)) {
+          !datatypeDecl.Members.Any(member => member is Field { IsGhost: false }) &&
+          datatypeDecl.ParentTraits.Count == 0) {
         var nonGhostConstructors = datatypeDecl.Ctors.Where(ctor => !ctor.IsGhost).ToList();
         if (nonGhostConstructors.Count == 1) {
           // there is exactly one non-ghost constructor

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false --type-system-refresh --general-traits=datatype
 
 datatype SingletonRecord = SingletonRecord(u: int)
 datatype GhostOrNot = ghost Ghost(a: int, b: int) | Compiled(x: int)
@@ -18,6 +18,7 @@ method Main() {
   TestMembers();
   OptimizationChecks.Test();
   PrintRegressionTests.Test();
+  ConditionsThatDisableTheOptimization.Test();
 }
 
 method TestTargetTypesAndConstructors() {
@@ -412,3 +413,33 @@ module PrintRegressionTests {
     print x, "\n";
   }
 }
+
+// --------------------------------------------------------------------------------
+
+module ConditionsThatDisableTheOptimization {
+  trait Trait {
+    function F(): int
+  }
+  datatype WithTrait extends Trait = WithTrait(u: int)
+  {
+    function F(): int { 5 }
+  }
+
+  datatype WithCompiledField = WithCompiledField(u: int)
+  {
+    const n: int := 100
+  }
+
+  datatype WithGhostField = WithGhostField(u: int)
+  {
+    ghost const n: int := 100
+  }
+
+  method Test() {
+    var t0 := WithTrait(40);
+    var t1 := WithCompiledField(41);
+    var t2 := WithGhostField(42);
+    print t0, " ", t0.F(), " ", (t0 as Trait).F(), "\n"; // WithTrait(40) 5 5
+    print t1, " ", t1.n, " ", t2, "\n"; // WithCompiledField(41) 100 42
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ErasableTypeWrappers.dfy.expect

@@ -18,3 +18,5 @@ HasConst.MakeC(4) (4, 4)
 OptimizationChecks.Ints.Ints(5, 7) OptimizationChecks.Ints.Ints(5, 7) OptimizationChecks.Ints.AnotherIntsWrapper(OptimizationChecks.Ints.Ints(5, 7))
 D D
 5 5
+ConditionsThatDisableTheOptimization.WithTrait.WithTrait(40) 5 5
+ConditionsThatDisableTheOptimization.WithCompiledField.WithCompiledField(41) 100 42

docs/dev/news/5234.fix

@@ -0,0 +1,2 @@
+fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits.
+feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields.