function refinement broken

[erniecohen]

Dafny version

4.5.0, 4.6.0, nightly

Code to produce this issue

abstract module A {
  function F(x: int): (r: int)
    ensures r > x
}

module B refines A {
  function F ... 
  // the result type of function 'F' (bool) differs from the result type of the corresponding function in the module it refines (int)
  // function 'F' is declared with a different number of parameter (0 instead of 1) than the corresponding function in the module it refines
  { x + 1 }
}

Command to run and resulting output

vscode

What happened?

The example above from the manual fails in the resolver. It worked through 4.4.0.

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

Mac

[keyboardDrummer]

The documentation seems to indicate this should work, although I'm not used to this syntax either:

We could check with @RustanLeino to see whether he intends to keep the semantics as the documentation currently defines it.

[erniecohen]

A workaround is to skip the refinement notation, e.g.

module B refines A {
  function F(x: int): (r: int)
  { x + 1 }
}

Note that if the refined module defines a precondition, you cannot repeat this precondition in the refining module.