[Bug]: Preservation of {:opaque} not verified on classes implementing a trait

[cpitclaudel]

Dafny version

latest

Code to produce this issue

trait TTT {
  function {:opaque} FFF(): int
}

class CCC extends TTT {
  function FFF() : int { 412 }
}

method M0() {
  var c := new CCC;
  assert c.FFF() == 412; // This passes
}

method M1() {
  var c := new CCC;
  reveal c.FFF();
  assert c.FFF() == 412; // This fails
}

Command to run and results

No response

What happened?

This is a follow up to the fix in #2974 . The difference between M0 and M1 in the example above is the type inference:

method M0'() {
  var c: TTT := new CCC;
  assert c.FFF() == 412; // This fails
}

method M1'() {
  var c: CCC := new CCC;
  reveal c.FFF();
  assert c.FFF() == 412; // This passes
}

What type of Operating System are you seeing the problem on?

Other

[MikaelMayer]

Verification being inherently static, if we can't know what is the reveal lemma to invoke (which requires dynamic dispatch), we can't actually reveal a function defined on a trait. We need to have a function body to be able to declare a function opaque.
This remark made it possible to close one long standing issue #4546
I'm closing this thread now.