Suggested by Phil Wadler: add an expression-level type annotation operator:
Expression ::= ... | (Expression : Type)
so that programmers can write type assertions not just on bindings but arbitrary expressions. This creates a nice parallel to the "wrap" syntax so that programmers can gradually introduce tighter type invariants on their code.
For example, version 1 of a program might look like:
function f() : * { ... }
...
let x : int = (f() wrap int)
But then when you add type annotations to f, version two simply changes the "wrap" to a ":" annotation:
function f() : int { ... }
...
let x : int = (f() : int)
Phil also suggested both operators have similar syntax, in particular with the same column width, to minimize the cost of changing the annotation, for example ":" for type-constrain and "@" for wrap. Then the migration becomes a one-character fix, and doesn't disturb your program's indentation/line-breaking levels.