Imprecise error message with partial functions

[txiang61]

Dafny version

4.8.1

Code to produce this issue

function Map<T, U>(s: seq<T>, f: T ~> U): (res: seq<U>)
  reads set x, y | x in s && y in f.reads(x) :: y
  requires forall x: T :: x in s ==> f.requires(x)
  ensures |res| == |s|
  ensures forall i: nat :: i < |s| ==> res[i] == f(s[i])
  decreases |s|
{
  if s == [] then
    []
  else
    [f(s[0])] + Map(s[1..], f)
}

predicate R<T>(x: T)
predicate P<U>(x: U)

function goo<T, U>(x: T): (r: U)
  requires R(x)
  ensures P(r)

function foo<T, U>(x: seq<T>): (res: seq<U>)
  //   requires forall a <- x :: R(a)
  ensures forall r <- res :: P(r)
{
  Map(x, a requires R(a) => goo(a))
}

Command to run and resulting output

(22,9): Error: a postcondition could not be proved on this return path
   |
22 | function foo<T, U>(x: seq<T>): (res: seq<U>)
   |          ^^^

(24,10): Related location: this is the postcondition that could not be proved
   |
24 |   ensures forall r <- res :: P(r)
   |           ^^^^^^^^^^^^^^^^^^^^^^^

(26,2): Error: function precondition could not be proved
   |
26 |   Map(x, a requires R(a) => goo(a))
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

(3,11): Related location: this proposition could not be proved
  |
3 |   requires forall x: T :: x in s ==> f.requires(x)
  |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

What happened?

The error message is complaining about the failure to satisfy the post-condition as well. The pre-condition should have turned into an assume for the post-condition to be proven. I also encountered a case where the error message only returned one error complaining about the post-condition and not the pre-condition, which caused some confusion.

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

Mac