Verification error on repeating method specification from trait

[robin-aws]

Dafny version

latest master (regression since 4.9.1)

Code to produce this issue

trait T {

  ghost function Modifies(): set<object>

  method Foo()
    modifies Modifies()
}

class C extends T {

  const Repr: set<object>

  ghost function Modifies(): set<object> {
    Repr
  }

  // Error: method might modify an object not in the parent trait context's modifies clause
  method Foo()
    modifies Modifies()
}

Command to run and resulting output

% dafny verify github-issue-XXX.dfy 
github-issue-XXX.dfy(17,9): Error: method might modify an object not in the parent trait context's modifies clause
   |
17 |   method Foo()
   |   ^^^^^^^^^^^^


Dafny program verifier finished with 1 verified, 1 error

What happened?

The example verifies successfully on Dafny 4.9.1. I suspect this is a consequence of the recent change to CanCall but haven't confirmed yet. It seems to have something to do with invoking a trait function within the modifies clause.

Having trouble seeing a workaround, and even if there is one, it's really unfortunate that simply repeating the definition from a trait in a class doesn't verify without help.

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

Mac