fix: Incompleteness in the resolver when detecting support for equality

Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs

@@ -395,7 +395,7 @@ bool TryEquateBounds() {
       return null;
     }
 
-    TopLevelDecl/*?*/ MeetHeads(TopLevelDecl a, TopLevelDecl b, SystemModuleManager systemModuleManager) {
+    public static TopLevelDecl/*?*/ MeetHeads(TopLevelDecl a, TopLevelDecl b, SystemModuleManager systemModuleManager) {
       var aAncestors = new HashSet<TopLevelDecl>();
       PreTypeResolver.ComputeAncestors(a, aAncestors, systemModuleManager);
       if (aAncestors.Contains(b)) {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -505,7 +505,7 @@ resolutionContext.CodeContext is ConstantField ||
                 }
                 return string.Format(errorMessageFormat, toPreType, e.E.PreType);
               };
-              AddComparableConstraint(toPreType, e.E.PreType, expr.Origin, true, errorMessage);
+              AddComparableConstraint(toPreType, e.E.PreType, expr.Origin, true, false, errorMessage);
               e.PreType = toPreType;
             } else {
               e.PreType = CreatePreTypeProxy("'as' target type");
@@ -519,8 +519,7 @@ resolutionContext.CodeContext is ConstantField ||
             testExpr.PreType = ConstrainResultToBoolFamilyOperator(testExpr.Origin, "is");
             resolver.ResolveType(e.Origin, e.ToType, resolutionContext, new ModuleResolver.ResolveTypeOption(ResolveTypeOptionEnum.InferTypeProxies), null);
             var toPreType = Type2PreType(e.ToType);
-            AddComparableConstraint(toPreType, e.E.PreType, testExpr.Origin, true,
-              "type test for type '{0}' must be from an expression assignable to it (got '{1}')");
+            AddComparableConstraint(toPreType, e.E.PreType, testExpr.Origin, true, false, "type test for type '{0}' must be from an expression assignable to it (got '{1}')");
             break;
           }
         case BinaryExpr binaryExpr: {
@@ -540,8 +539,7 @@ resolutionContext.CodeContext is ConstantField ||
               case TernaryExpr.Opcode.PrefixNeqOp:
                 ternaryExpr.PreType = ConstrainResultToBoolFamily(ternaryExpr.Origin, "ternary op", "boolean literal used as if it had type {0}");
                 AddConfirmation(PreTypeConstraints.CommonConfirmationBag.IntOrORDINAL, e.E0.PreType, ternaryExpr.Origin, "prefix-equality limit argument must be an ORDINAL or integer expression (got {0})");
-                AddComparableConstraint(e.E1.PreType, e.E2.PreType, ternaryExpr.Origin, false,
-                  "arguments must have the same type (got {0} and {1})");
+                AddComparableConstraint(e.E1.PreType, e.E2.PreType, ternaryExpr.Origin, false, true, "arguments must have the same type (got {0} and {1})");
                 AddConfirmation(PreTypeConstraints.CommonConfirmationBag.IsCoDatatype, e.E1.PreType, ternaryExpr.Origin, "arguments to prefix equality must be codatatypes (instead of {0})");
                 break;
               default:
@@ -1095,7 +1093,7 @@ private PreType ResolveBinaryExpr(IOrigin tok, BinaryExpr.Opcode opcode, Express
         case BinaryExpr.Opcode.Eq:
         case BinaryExpr.Opcode.Neq:
           resultPreType = ConstrainResultToBoolFamilyOperator(tok, opString);
-          AddComparableConstraint(e0.PreType, e1.PreType, tok, false, "arguments must have comparable types (got {0} and {1})");
+          AddComparableConstraint(e0.PreType, e1.PreType, tok, false, true, "arguments must have comparable types (got {0} and {1})");
           break;
 
         case BinaryExpr.Opcode.Disjoint:
@@ -1251,7 +1249,7 @@ private PreType ResolveBinaryExpr(IOrigin tok, BinaryExpr.Opcode opcode, Express
             var coll = a1.UrAncestor(this).AsCollectionPreType();
             if (coll != null) {
               Constraints.DebugPrint($"    guard applies: Innable {a0} {a1}");
-              AddComparableConstraint(coll.Arguments[0], a0, tok, false, "expecting element type to be assignable to {0} (got {1})");
+              AddComparableConstraint(coll.Arguments[0], a0, tok, false, true, "expecting element type to be assignable to {0} (got {1})");
               return true;
             } else if (a1 is DPreType) {
               // type head is determined and it isn't a collection type

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -532,11 +532,13 @@ void AddConfirmation(PreTypeConstraints.CommonConfirmationBag check, PreType pre
       Constraints.AddConfirmation(check, preType, tok, errorFormatString, onProxyAction);
     }
 
-    void AddComparableConstraint(PreType a, PreType b, IOrigin tok, bool allowBaseTypeCast, string errorFormatString) {
-      AddComparableConstraint(a, b, tok, allowBaseTypeCast, () => string.Format(errorFormatString, a, b));
+    void AddComparableConstraint(PreType a, PreType b, IOrigin tok, bool allowBaseTypeCast,
+      bool allowCommonSuperType, string errorFormatString) {
+      AddComparableConstraint(a, b, tok, allowBaseTypeCast, allowCommonSuperType, () => string.Format(errorFormatString, a, b));
     }
 
-    void AddComparableConstraint(PreType a, PreType b, IOrigin tok, bool allowBaseTypeCast, Func<string> errorMessage) {
+    void AddComparableConstraint(PreType a, PreType b, IOrigin tok, bool allowBaseTypeCast, bool allowCommonSuperType,
+      Func<string> errorMessage) {
       // A "comparable types" constraint involves a disjunction. This can get gnarly for inference, so the full disjunction
       // is checked post inference. The constraint can, however, be of use during inference, so we also add an approximate
       // constraint (which is set up NOT to generate any error messages by itself, since otherwise errors would be duplicated).
@@ -545,7 +547,7 @@ void AddComparableConstraint(PreType a, PreType b, IOrigin tok, bool allowBaseTy
       if (!allowBaseTypeCast) {
         AddComparableTypesDefault(a, b);
       }
-      Constraints.AddConfirmation(tok, () => CheckComparableTypes(a, b, allowBaseTypeCast), errorMessage);
+      Constraints.AddConfirmation(tok, () => CheckComparableTypes(a, b, allowBaseTypeCast, allowCommonSuperType), errorMessage);
     }
 
     private void AddComparableTypesDefault(PreType a, PreType b) {
@@ -567,18 +569,20 @@ private void AddComparableTypesDefault(PreType a, PreType b) {
     /// is the disjunction
     ///     A ::> B    or    B ::> A
     ///
-    /// If "!allowConversion", then "X ::> Y" means
+    /// If "!allowConversion" and "!allowCommonSuperType", then "X ::> Y" means
     ///     X :> Y
     ///
-    /// If "allowConversion", then "X ::> Y" means
-    ///     X' :> Y', or
+    /// If "allowConversion", then "X ::> Y" also means
     ///     X' and Y' are various bv types, or
     ///     X' is int and Y' is in {int, char, bv, ORDINAL, real}.
     /// where X' and Y' are the newtype ancestors of X and Y, respectively.
+    ///
+    /// If "allowCommonSuperType", then "X<T> ::> Y<U>" also means
+    ///     T and U have common supertype S such that S :> T and S :> U.
     /// Additionally, under the legacy option /generalNewtypes:0 (which will be phased out over time), the latter also allows
     /// several additional cases, see IsConversionCompatible.
     /// </summary>
-    bool CheckComparableTypes(PreType a, PreType b, bool allowConversion) {
+    bool CheckComparableTypes(PreType a, PreType b, bool allowConversion, bool allowCommonSuperType) {
       if (PreType.Same(a, b)) {
         // this allows the case where "a" and "b" are proxies that are equal
         return true;
@@ -589,6 +593,9 @@ bool CheckComparableTypes(PreType a, PreType b, bool allowConversion) {
       if (IsSuperPreTypeOf(aa, bb) || IsSuperPreTypeOf(bb, aa)) {
         return true;
       }
+      if (allowCommonSuperType && HaveCommonSuperPreType(aa, bb)) {
+        return true;
+      }
       if (!allowConversion) {
         return false;
       }
@@ -640,6 +647,35 @@ bool IsConversionCompatible(DPreType fromType, DPreType toType) {
       return false;
     }
 
+    bool HaveCommonSuperPreType(DPreType t, DPreType u) {
+      return PreTypeConstraints.MeetHeads(t.Decl, u.Decl, resolver.SystemModuleManager) is not null && ComparablePretypes(t, u);
+
+      bool ComparablePretypes(DPreType t, DPreType u) {
+        var joined = PreTypeConstraints.JoinHeads(t.Decl, u.Decl, resolver.SystemModuleManager);
+
+        if (joined is null) {
+          return false;
+        }
+
+        var tArgs = Constraints.GetTypeArgumentsForSuperType(joined, t, true);
+        var uArgs = Constraints.GetTypeArgumentsForSuperType(joined, u, true);
+        if (tArgs == null || uArgs == null) {
+          return false;
+        }
+
+        for (var i = 0; i < joined.TypeArgs.Count; i++) {
+          if (tArgs[i].Normalize() is not DPreType tt || uArgs[i].Normalize() is not DPreType uu) {
+            return false;
+          }
+
+          if (!ComparablePretypes(tt, uu)) {
+            return false;
+          }
+        }
+        return true;
+      }
+    }
+
     bool ApproximateComparableConstraints(PreType a, PreType b, IOrigin tok, bool allowBaseTypeCast, string errorFormatString, bool reportErrors = true) {
       // See CheckComparableTypes for the meaning of "comparable type".
       // To decide between these two possibilities, enough information must be available about A and/or B.

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

@@ -0,0 +1,10 @@
+// RUN: %testDafnyForEachResolver "%s"
+
+trait Number extends object { }
+class Integer extends Number { }
+
+method M(i: Integer, j: Integer) returns (r: bool) {
+    var a: (Number, Integer) := (i, j);
+    var b: (Integer, Number) := (i, j);
+    return a == b;
+}

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

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

docs/dev/news/6231.fix

@@ -0,0 +1 @@
+Incompleteness in the new resolver when detecting support for equality