Soundness issue: Map's range not inferred to require equality for datatype to support equality

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

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;
}

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);
  if !b {
    assert false;
    print 1/0;
  }
}

Command to run and resulting output

dafny run file.dfy

What happened?

It outputs a run-time exception whereas the program verifies.
The problem is that the second argument of the map requires supporting equality for the datatype to support equality but it is not added

What type of operating system are you experiencing the problem on?

Any