Type parameter Equality wrongly inferred

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

method Test<T>(ghost s: iset<T>) {
}
ghost function domain<T>(s: seq<T>): iset<T> {
  iset t: T | t in s
}
method TestWrapper<T>(s: seq<T>) {
  var d := domain(s);
  Test(d);
}

Command to run and resulting output

dafny verify

What happened?

It complains that the type parameter of TestWrapper should support equality when it's not necessary. So there are two contradicting issues here:

1. The type parameter of domain is not inferred to require equality although it returns a ghost iset
2. The type parameter of Test is inferred to require equality because of a ghost iset.

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

Windows