Obsolete verification diagnostics prevent seeing resolution errors

[MikaelMayer]

Enter the following code in VSCode

predicate Ok(a: int) {
  a >= 0 &&
  a >= 1 &&
  a >= 2 &&
  a >= 3 &&
  a >= 4 &&
  a >= 5 &&
  a >= 6 &&
  a >= 7 &&
  a >= 8
}

function NeedsOk(i: int): int
  requires Ok(i)

lemma ok() {
  assert NeedsOk(0) == 1;
}

If one hovers over the call NeedsOk(), it says as expected that the first 5 preconditions don't hold, and it does not know for the remaining one. Ok.
Now, introduce a resolution error by changing NeedsOk(0) into NeedsOk(0, 1).
Hover over the call, you get this:

which is the same set of verification error and no clue about the resolution error. You'd have to scroll to the end. But if you do this naively, you'd see no resolution error

If you want to see the resolution error, you'd have to hover over the parenthesis (yes, very subtle) on which the resolution error is reported.

Of course, someone looking at the diagnostics window would immediately spot the resolution error and its message, but for users like me who don't like to be distracted by switching window, this recurring scenario above is really frustrating.
It ought to be that:

• The resolution error should not be reported on the token itself, but on the same kinds of ranges as of the verification ranges.
• When verification errors are obsolete, they should be written as such in the hover message. Currently, there is no difference and this is misleading.
• Parse and resolution errors should always be on the top of the hover message
• Assertions verified in the same batch should take much less space on the hovering window(the resource usage, for example, is the same because it's the assertion batch resource usage)
• The function precondition that might not hold should be visible in the error message. Otherwise that's impossible to guess!