Refining a module with a class containing opaque functions causes resolution error

[EkanshdeepGupta]

Dafny version

4.2.0

Code to produce this issue

module M1 {
  class C {
    opaque function f() : bool { true }
  }
}

module M2 refines M1 {
}

Command to run and resulting output

$ ./Binaries/Dafny verify ~/test/scratch.dfy
    |
173 | <nonexistent line>
    |                     ^

/Users/ekanshdg/test/scratch.dfy[M2](173,20): Error: 'this' is not allowed in a 'static' context
1 resolution/type errors detected in scratch.dfy

What happened?

Due to the change making reveal lemmas static, there is a resolution error when the static reveal lemma tries to set the fuel for its non-static originating function. This only gets triggered when a module is resolved again, like when it is being refined, because the reveal lemma is added after the resolution is complete.

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

Mac