`hide` statements don't work with recursive functions defined in different modules

[dschoepe]

Dafny version

4.8.0-7af458b24f4511a54dc33b456b3711fe12f7ecd6

Code to produce this issue

module M1 {
    ghost opaque function RecFunc(x: nat): nat { 
        if x == 0 then 0
        else 1 + RecFunc(x - 1)
    }
}
module M2 {
    import opened M1
    lemma Lemma(x: nat) 
    ensures RecFunc(0) == 0 
    {
        hide *;
        reveal RecFunc;
        // reveal *
        // ^ this makes the assertion pass
    }
}

Command to run and resulting output

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

What happened?

I expected Lemma to be successfully verified. However, verification fails. To get verification to succeed, one needs to either put the lemma and function into the same module or use reveal *.

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

Mac