Trait postcondition ignored

[jaylorch]

Dafny version

4.8.1

Code to produce this issue

module Testing {

  trait V {
    ghost function Repr() : set<object>
      reads this

    ghost predicate Valid()
      reads this
      reads Repr()

    method Update()
      requires this.Valid()
      modifies Repr()
      ensures  this.Valid()
  }

  class C<T extends V>
  {
    var t: T

    ghost function Repr() : set<object>
        reads this
        reads t as V
    {
      { this, t as V } + (t as V).Repr()
    }

    ghost predicate Valid()
      reads Repr()
    {
      (t as V).Valid()
    }

    constructor Create(x: T)
    {
      t := x;
    }

    method HUpdate()
      requires Valid()
      modifies Repr()
      ensures  Valid()
    {
      (t as V).Update();
      assert((t as V).Valid()); // Why doesn't this follow from the postcondition of `V.Update`?
    }
  }

}

Command to run and resulting output

C:\Apps\TestDafny>C:\Bin\dafny-4.8.1-win\Dafny.exe verify --type-system-refresh test.dfy
test.dfy(45,12): Error: assertion might not hold
   |
45 |       assert((t as V).Valid()); // Why doesn't this follow from the postcondition of `V.Update`?
   |             ^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 4 verified, 1 error

What happened?

I expected the assert to hold, since it follows directly from the postcondition of V.Update.

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

Windows