Contracts: some additional annotations for type ch...

# language-proposals

[dmitry.petrov]

Contracts: some additional annotations for type checking and data flow analysis performed by the compiler.
We need them, for example, to know that high-order functions like let, run, and so on
invoke their functional arguments once and only once
(so that, for example, you'd be able to initialize a variable under run).