Fix: Map range requires equality for enclosing type to support equali…

…ty (#5973)

This PR fixes #5972
I added the corresponding test.

<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/Resolver/ModuleResolver.cs

@@ -2884,26 +2884,8 @@ void MarkSCCAsNotSupportingEquality() {
         }
         foreach (var ctor in dt.Ctors) {
           foreach (var arg in ctor.Formals) {
-            var typeArg = arg.Type.AsTypeParameter;
-            if (typeArg != null) {
-              typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
-              thingsChanged = true;
-            } else {
-              var otherDt = arg.Type.AsIndDatatype;
-              if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) {  // datatype is in a different SCC
-                var otherUdt = (UserDefinedType)arg.Type.NormalizeExpand();
-                var i = 0;
-                foreach (var otherTp in otherDt.TypeArgs) {
-                  if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
-                    var tp = otherUdt.TypeArgs[i].AsTypeParameter;
-                    if (tp != null) {
-                      tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
-                      thingsChanged = true;
-                    }
-                  }
-                }
-              }
-            }
+            var type = arg.Type;
+            DetermineEqualitySupportType(type, ref thingsChanged);
           }
         }
       }
@@ -2943,6 +2925,33 @@ void MarkSCCAsNotSupportingEquality() {
       }
     }
 
+    private static void DetermineEqualitySupportType(Type type, ref bool thingsChanged) {
+      if (type.AsTypeParameter is { } typeArg) {
+        typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+        thingsChanged = true;
+      } else if (type.AsMapType is { } typeMap) {
+        DetermineEqualitySupportType(typeMap.Range, ref thingsChanged);
+      } else if (type.AsSeqType is { } typeSeq) {
+        DetermineEqualitySupportType(typeSeq.Arg, ref thingsChanged);
+      } else if (type.AsIndDatatype is { } otherDt) {
+        if (otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) {  // datatype is in a different SCC
+          var otherUdt = (UserDefinedType)type.NormalizeExpand();
+          var i = 0;
+          foreach (var otherTp in otherDt.TypeArgs) {
+            if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
+              var tp = otherUdt.TypeArgs[i].AsTypeParameter;
+              if (tp != null) {
+                tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+                thingsChanged = true;
+              }
+            }
+
+            i++;
+          }
+        }
+      }
+    }
+
     /// <summary>
     /// Check to see if the attribute is one that is supported by Dafny.  What check performed here is,
     /// unfortunately, just an approximation, since the usage rules of a particular attribute is checked

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

@@ -0,0 +1,57 @@
+// RUN: %exits-with 2 %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype M<T, U> = M(m: map<T, U>)
+
+method CompareAnything<A>(f: A, g: A) returns (b: bool) 
+   ensures b <==> f == g
+{
+  var m1 := M(map[0 := f]);
+  var m2 := M(map[0 := g]);
+  assert m1 == m2 <==> f == g by {
+    if f == g {
+      assert m1 == m2;
+    }
+    if m1 == m2 {
+      assert m1.m[0] == m2.m[0];
+    }
+  }
+  return m1 == m2;
+}
+
+datatype S<T> = S(s: seq<T>)
+
+method CompareAnythingS<A>(f: A, g: A) returns (b: bool) 
+   ensures b <==> f == g
+{
+  var m1 := S([f]);
+  var m2 := S([g]);
+  assert m1 == m2 <==> f == g by {
+    if f == g {
+      assert m1 == m2;
+    }
+    if m1 == m2 {
+      assert m1.s[0] == m2.s[0];
+    }
+  }
+  return m1 == m2;
+}
+
+
+codatatype Stream = Stream(head: int, tail: Stream)
+{
+  static function From(i: int): Stream {
+    Stream(i, From(i + 1))
+  }
+}
+
+method Main() {
+  var s1 := Stream.From(0);
+  var s2 := Stream.From(0);
+  var b := CompareAnything(s1, s2);
+  var b2 := CompareAnythingS(s1, s2);
+  if !b || !b2 {
+    assert false;
+    print 1/0;
+  }
+}

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

@@ -0,0 +1,3 @@
+git-issue-5972.dfy(19,9): Error: == can only be applied to expressions of types that support equality (got M<int, A>)
+git-issue-5972.dfy(37,9): Error: == can only be applied to expressions of types that support equality (got S<A>)
+2 resolution/type errors detected in git-issue-5972.dfy

docs/dev/news/5972.fix

@@ -0,0 +1 @@
+Map range requires equality for enclosing type to support equality