fix: Fix traits-on-datatype scoping and translation issues

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -435,26 +435,23 @@ public bool Resolve(ModuleSignature sig, ModuleResolver resolver, string exportS
     sig.VisibilityScope.Augment(resolver.ProgramResolver.SystemModuleManager.systemNameInfo.VisibilityScope);
     // make sure all imported modules were successfully resolved
     foreach (var d in TopLevelDecls) {
-      if (d is AliasModuleDecl || d is AbstractModuleDecl) {
-        ModuleSignature importSig;
-        if (d is AliasModuleDecl) {
-          var alias = (AliasModuleDecl)d;
-          importSig = alias.TargetQId.Root != null ? alias.TargetQId.Root.Signature : alias.Signature;
-        } else {
-          importSig = ((AbstractModuleDecl)d).OriginalSignature;
+      if (d is AliasModuleDecl importDecl) {
+        var importSig = importDecl.TargetQId.Root != null ? importDecl.TargetQId.Root.Signature : importDecl.Signature;
+        if (importSig is not { ModuleDef: { SuccessfullyResolved: true } }) {
+          return false;
         }
-
+      } else if (d is AbstractModuleDecl abstractImportDecl) {
+        var importSig = abstractImportDecl.OriginalSignature;
         if (importSig is not { ModuleDef: { SuccessfullyResolved: true } }) {
           return false;
         }
-      } else if (d is LiteralModuleDecl) {
-        var nested = (LiteralModuleDecl)d;
-        if (!nested.ModuleDef.SuccessfullyResolved) {
+      } else if (d is LiteralModuleDecl nestedModuleDecl) {
+        if (!nestedModuleDecl.ModuleDef.SuccessfullyResolved) {
           if (!IsEssentiallyEmptyModuleBody()) {
             // say something only if this will cause any testing to be omitted
-            resolver.reporter.Error(MessageSource.Resolver, nested,
+            resolver.reporter.Error(MessageSource.Resolver, nestedModuleDecl,
               "not resolving module '{0}' because there were errors in resolving its nested module '{1}'", Name,
-              nested.Name);
+              nestedModuleDecl.Name);
           }
 
           return false;
@@ -952,6 +949,7 @@ private void DetermineReferenceTypes(ModuleResolver resolver, ModuleSignature si
     // In the following dictionary, a TraitDecl not being present among the keys means it has not been visited in the InheritsFromObject traversal.
     // If a TraitDecl is a key and maps to "false", then it is currently being visited.
     // If a TraitDecl is a key and maps to "true", then its .IsReferenceTypeDecl has been computed and is ready to be used.
+    var openedImports = TopLevelDecls.OfType<ModuleDecl>().Where(d => d.Opened).ToList();
     var traitsProgress = new Dictionary<TraitDecl, bool>();
     foreach (var decl in TopLevelDecls.Where(d => d is TraitDecl)) {
       // Resolve a "path" to a top-level declaration, if possible. On error, return null.
@@ -969,9 +967,22 @@ TopLevelDecl ResolveNamePath(Expression path) {
             // For "object" and other reference-type declarations from other modules, we're picking up the NonNullTypeDecl; if so, return
             // the original declaration.
             return topLevelDecl is NonNullTypeDecl nntd ? nntd.ViewAsClass : topLevelDecl;
-          } else {
-            return null;
           }
+          // Look through opened imports (which haven't yet been added to the module's signature). There may be ambiguities among the declarations
+          // of these opened imports. Still, we'll just pick the first declaration that matches, if any. If this declaration turns out to be
+          // ambiguous, then an error will be reported later; in the meantime, all that would have happened is that the resolved name path here
+          // is referring to some top-level declaration that won't accurately answer the question of whether "path" is referring to a reference
+          // type or not.
+          foreach (var importDecl in openedImports) {
+            Contract.Assert(importDecl is AliasModuleDecl or AbstractModuleDecl); // only these ModuleDecl's can be .Opened
+            if (importDecl.AccessibleSignature(false).TopLevels.TryGetValue(nameSegment.Name, out topLevelDecl)) {
+              // For "object" and other reference-type declarations from other modules, we're picking up the NonNullTypeDecl; if so, return
+              // the original declaration.
+              return topLevelDecl is NonNullTypeDecl nntd ? nntd.ViewAsClass : topLevelDecl;
+            }
+          }
+          // We didn't find "path"
+          return null;
         }
 
         // convert the ExprDotName to a list of strings

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -408,8 +408,7 @@ public void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature s
 
       foreach (var s in sigs) {
         foreach (var decl in s.TopLevels) {
-          if (decl.Value is ModuleDecl && !(decl.Value is ModuleExportDecl)) {
-            var modDecl = (ModuleDecl)decl.Value;
+          if (decl.Value is ModuleDecl modDecl and not ModuleExportDecl) {
             s.VisibilityScope.Augment(modDecl.AccessibleSignature().VisibilityScope);
           }
         }
@@ -428,7 +427,7 @@ public void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature s
           }
         }
 
-        if (e.Opaque && (decl is DatatypeDecl || decl is TypeSynonymDecl)) {
+        if (e.Opaque && (decl is DatatypeDecl or TypeSynonymDecl)) {
           // Datatypes and type synonyms are marked as _provided when they appear in any provided export.  If a
           // declaration is never provided, then either it isn't visible outside the module at all or its whole
           // definition is.  Datatype and type-synonym declarations undergo some inference from their definitions.

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -893,17 +893,18 @@ public Boogie.Expr TrExpr(Expression expr) {
                     e0 = BoxIfNecessary(expr.tok, e0, e.E0.Type);
                     oe0 = BoxIfNecessary(expr.tok, oe0, e.E0.Type);
                   }
-                  var cot = e.E0.Type.AsCoDatatype;
-                  if (cot != null) {
+                  if (e.E0.Type.IsCoDatatype && e.E1.Type.IsCoDatatype) {
                     var e0args = e.E0.Type.NormalizeExpand().TypeArgs;
                     var e1args = e.E1.Type.NormalizeExpand().TypeArgs;
-                    return BoogieGenerator.CoEqualCall(cot, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr));
+                    return BoogieGenerator.CoEqualCall(e.E0.Type.AsCoDatatype, e0args, e1args, null,
+                      this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr));
                   }
-                  if (e.E0.Type.IsIndDatatype) {
+                  if (e.E0.Type.IsIndDatatype && e.E1.Type.IsIndDatatype) {
                     return BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1);
                   }
                   typ = Boogie.Type.Bool;
-                  bOpcode = BinaryOperator.Opcode.Eq; break;
+                  bOpcode = BinaryOperator.Opcode.Eq;
+                  break;
                 case BinaryExpr.ResolvedOpcode.NeqCommon:
                   if (ModeledAsBoxType(e.E0.Type)) {
                     e1 = BoxIfNecessary(expr.tok, e1, e.E1.Type);
@@ -912,19 +913,20 @@ public Boogie.Expr TrExpr(Expression expr) {
                     e0 = BoxIfNecessary(expr.tok, e0, e.E0.Type);
                     oe0 = BoxIfNecessary(expr.tok, oe0, e.E0.Type);
                   }
-                  var cotx = e.E0.Type.AsCoDatatype;
-                  if (cotx != null) {
+                  if (e.E0.Type.IsCoDatatype && e.E1.Type.IsCoDatatype) {
                     var e0args = e.E0.Type.NormalizeExpand().TypeArgs;
                     var e1args = e.E1.Type.NormalizeExpand().TypeArgs;
-                    var eq = BoogieGenerator.CoEqualCall(cotx, e0args, e1args, null, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr));
+                    var eq = BoogieGenerator.CoEqualCall(e.E0.Type.AsCoDatatype, e0args, e1args, null,
+                      this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr));
                     return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq);
                   }
-                  if (e.E0.Type.IsIndDatatype) {
+                  if (e.E0.Type.IsIndDatatype && e.E1.Type.IsIndDatatype) {
                     var eq = BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1);
                     return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq);
                   }
                   typ = Boogie.Type.Bool;
-                  bOpcode = BinaryOperator.Opcode.Neq; break;
+                  bOpcode = BinaryOperator.Opcode.Neq;
+                  break;
                 case BinaryExpr.ResolvedOpcode.Lt:
                   if (0 <= bvWidth) {
                     return TrToFunctionCall(GetToken(binaryExpr), "lt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit);
@@ -2112,15 +2114,13 @@ public Expr CanCallAssumption(Expression expr) {
             case BinaryExpr.ResolvedOpcode.EqCommon:
             case BinaryExpr.ResolvedOpcode.NeqCommon: {
                 Boogie.Expr r = Boogie.Expr.True;
-                var dt = e.E0.Type.AsDatatype;
-                if (dt != null) {
-                  var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.tok, "$IsA#" + dt.FullSanitizedName, Boogie.Type.Bool));
-                  if (!(e.E0.Resolved is DatatypeValue)) {
-                    r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List<Boogie.Expr> { TrExpr(e.E0) }));
-                  }
-                  if (!(e.E1.Resolved is DatatypeValue)) {
-                    r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List<Boogie.Expr> { TrExpr(e.E1) }));
-                  }
+                if (e.E0 is { Type: { AsDatatype: { } dt0 }, Resolved: not DatatypeValue }) {
+                  var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.tok, "$IsA#" + dt0.FullSanitizedName, Boogie.Type.Bool));
+                  r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List<Boogie.Expr> { TrExpr(e.E0) }));
+                }
+                if (e.E1 is { Type: { AsDatatype: { } dt1 }, Resolved: not DatatypeValue }) {
+                  var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.tok, "$IsA#" + dt1.FullSanitizedName, Boogie.Type.Bool));
+                  r = BplAnd(r, new Boogie.NAryExpr(expr.tok, funcID, new List<Boogie.Expr> { TrExpr(e.E1) }));
                 }
                 return BplAnd(r, BplAnd(t0, t1));
               }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy

@@ -0,0 +1,16 @@
+// RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype
+
+module X {
+  trait {:termination false} A extends object {}
+}
+
+module Y {
+  import opened X
+
+  trait B extends A {
+    function GetIndex(): nat
+      // The following once gave an error, complaining that B is not a reference type. The problem had been that
+      // the opened import A was, effectively, hiding the information that A is a reference type.
+      reads this
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy

@@ -0,0 +1,19 @@
+// RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype
+
+module X {
+  trait K { }
+  trait {:termination false} A extends object, K {}
+}
+
+module Y {
+  import opened X
+
+  trait B extends A { }
+
+  method Test(b: B) returns (a: A) {
+    // The following assignment once caused malformed Boogie to be generated. The reason had been that
+    // the resolver had not determined B to be a reference type. And that, in turn, had been caused by
+    // that the opened import, effectively, had lost the "extends object" information.
+    a := b;
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy

@@ -0,0 +1,97 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits:datatype
+
+// The early-resolver code that figures out if a trait is a reference type or not is operating so early
+// in the resolver pipeline that opened imports have not yet been resolved into the importing module.
+// Thus, this early-resolver code looks directly into the top-level members of opened imports, but does
+// so without consideration for possible ambiguities. This means that the early-resolver code may not
+// properly figure out if a trait is a reference type or not. But if it gets it wrong, the ambiguity
+// will still be reported as an error later in the resolver pipeline.
+//
+// This test file makes sure that the ambiguous-import errors are indeed being reported and that the
+// resolver doesn't crash until then.
+
+module X0 {
+  // Here, A is a reference type
+  trait {:termination false} A extends object {}
+}
+
+module X1 {
+  // Here, A is not a reference type
+  trait {:termination false} A {}
+}
+
+module X2 {
+  // Here, A is not a reference type; in fact, it isn't even a type
+  const A: object?
+}
+
+module Y01 {
+  import opened X0
+  import opened X1
+
+  trait B extends A { // error: A is ambiguous
+    function GetIndex(): nat
+      reads this
+  }
+}
+
+module Y10 {
+  import opened X1
+  import opened X0
+
+  trait B extends A { // error: A is ambiguous
+    function GetIndex(): nat
+      reads this
+  }
+}
+
+module Y0123 {
+  import opened X0
+  import opened X1
+  import opened X2
+
+  trait B extends A { // error: A is ambiguous
+    function GetIndex(): nat
+      reads this
+  }
+}
+
+module Y210 {
+  import opened X2
+  import opened X1
+  import opened X0
+
+  trait B extends A { // error: A is ambiguous
+    function GetIndex(): nat
+      reads this
+  }
+}
+
+module Z {
+  import opened X0
+  import opened X1
+  import opened X2
+
+}
+
+module Z1 {
+  import opened X0
+  import opened X1
+  import opened X2
+
+  trait B extends X0.A { // no problem, since X0.A is fully qualified
+    function GetIndex(): nat
+      reads this // no problem, since B is a reference type
+  }
+}
+
+module Z2 {
+  import opened X0
+  import opened X1
+  import opened X2
+
+  trait B extends X1.A { // no problem, since X1.A is fully qualified
+    function GetIndex(): nat
+      reads this // error: B is not a reference type
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy.expect

@@ -0,0 +1,6 @@
+git-issue-4936c.dfy(32,18): Error: The name A ambiguously refers to a type in one of the modules X0, X1 (try qualifying the type name with the module name)
+git-issue-4936c.dfy(42,18): Error: The name A ambiguously refers to a type in one of the modules X1, X0 (try qualifying the type name with the module name)
+git-issue-4936c.dfy(53,18): Error: The name A ambiguously refers to a type in one of the modules X0, X1 (try qualifying the type name with the module name)
+git-issue-4936c.dfy(64,18): Error: The name A ambiguously refers to a type in one of the modules X1, X0 (try qualifying the type name with the module name)
+git-issue-4936c.dfy(95,12): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got B)
+5 resolution/type errors detected in git-issue-4936c.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy

@@ -0,0 +1,58 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits:datatype
+
+module X {
+  export Public
+    provides A
+  export Friends
+    reveals A
+
+  trait {:termination false} A extends object {}
+}
+
+module Y0 {
+  import opened X`Public
+
+  trait B extends A { // error: A is not even known to be a trait
+    function GetIndex(): nat
+      reads this
+  }
+}
+
+module Y1 {
+  import opened X`Friends
+
+  trait B extends A {
+    function GetIndex(): nat
+      reads this // fine, since B is known to be a reference type
+  }
+}
+
+module Y2 {
+  import opened I = X`Friends
+  import opened J = X`Public
+
+  trait B extends A {
+    function GetIndex(): nat
+      reads this // fine, since B is known to be a reference type
+  }
+}
+
+module Y3 {
+  import opened X`Friends
+  import opened J = X`Public
+
+  trait B extends J.A { // fine, since the module also imports X`Friends
+    function GetIndex(): nat
+      reads this // fine, since B is known to be a reference type
+  }
+}
+
+module Y4 {
+  import I = X`Friends
+  import J = X`Public
+
+  trait B extends J.A { // fine, since the module also imports X`Friends
+    function GetIndex(): nat
+      reads this // fine, since B is known to be a reference type
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy.expect

@@ -0,0 +1,2 @@
+git-issue-4936d.dfy(15,18): Error: a trait can only extend traits (found 'A')
+1 resolution/type errors detected in git-issue-4936d.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy

@@ -0,0 +1,27 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 --refresh-exit-code=0 "%s" -- --general-traits:datatype
+
+trait Parent {}
+
+datatype Dt extends Parent = Dt {
+  function GetParent(): Parent {
+    // The implicit conversion in the following line once caused malformed Boogie to be generated
+    this // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent
+  }
+}
+
+function GetDtAsParent(): Parent {
+  // The implicit conversion in the following line once caused malformed Boogie to be generated
+  Dt // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent
+}
+
+type Abstract extends Parent {
+  function GetParent(): Parent {
+    this // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent
+  }
+}
+
+function GetAbstract(): Abstract
+
+function GetAbstractAsParent(): Parent {
+  GetAbstract() // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent
+}