Inconsistent use of arrow types about libraries HOT 4 OPEN

that wouldn't be a breaking change, would it?

It could be, since the new proofs are harder.
It may be that Dafny managed to call the previous function with the simpler spec and not the one with the more general spec.

For example Map(f: A -> B, xs: seq<A>) has no preconditions. But Map(f: A --> B, xs: seq<A>) has requires forall a | a in xs :: f.requires(a). It should be easy to satisfy this new precondition, but it's still extra work.

Sometimes it's worse, and the most general version of the function has complex preconditions that can be satisfied in various ways that are not immediately obvious (for example, Fold)

from libraries.

Good questions. I think we can always promote -> to --> and then to ~>` for arguments when it will be necessary, correct?

from libraries.

Correct @MikaelMayer, but that entails additional proof obligations (the preconditions of the more general function that you're calling).

from libraries.

That's part of the upgrade, but for a user of the library, that wouldn't be a breaking change, would it?

from libraries.