Reference trait not recognized in separate modules with opened

[txiang61]

Dafny version

4.4.0

Code to produce this issue

module X {
  trait {:termination false} A extends object {}
}

module Y {
  import opened X

  trait B extends A {
    function getIndex(): nat
      reads this
  }
}

Command to run and resulting output

dafny verify --general-traits=Datatype --type-system-refresh

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)

What happened?

It’s fine if the traits are in the same module, but not in different modules when importing with opened.

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

Mac

[jtristan]

No issues when not using --general-traits=Datatype --type-system-refresh
@RustanLeino , you may find this interesting

[RustanLeino]

Evidently, the extends object seems to get lost in module Y.

Here's another face of this bug:

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) {
    a := b;
  }

This one results in malformed Boogie. So, again, it seems the extends object gets lost across the module boundary.