Rethinking this a bit:

The purpose of switching to a dynamic semantics built on "static await" criteria would be that programs are more comprehensible when it is specified directly that an await operation will definitely occur, or will definitely not occur.

However, the rules turn out to be so complex that it might not help the reader of code in practice. So maybe we should simply keep the old semantics? It's somewhat quirky, and they do make it less predictable when there will be an await operation, but the old semantics is considerably simpler...

As I mentioned in my review, I think we may need to use future value type in the dynamic semantics for reasons that I filed an issue about (unless I'm confusing myself in the late hour). I'm not convinced that the rest of the change to the dynamic semantics pulls its weight though. I think it's more breaking than advertised, and I don't see that it really makes anything clearer (if anything, less so).

I don't see that it really makes anything clearer

I agree, and I'm also worried about the breakage. So I'd suggest that we use the existing dynamic semantics, except for the 'future value type' soundness fix.

I uploaded another commit where we use the old semantics, only adjusted to have the 'future value type' correction.

My reason for preferring a static approach is not (just) simplicity, but lack of run-time overhead for type-checking - at least when it's possible.

So, the static rule for return e; in an async function is:

Let T be the future value type of the function, let S be the static type of e with context type FutureOr<T>.
It's a static type error unless S is assignable to T or flatten(S) is a subtype of T.

and the dynamic semantics are:

1. Evaluate e to a value o.
2. If o implements Future<X>, X <: T, let r be the object resulting from awaiting o.
3. Otherwise let r be o.
4. Then return e; returns with the value r.

Those two match up, but I'd still prefer to change 2. to:

2. If o implements Future<X>, X <: flatten(S), let r be the object resulting from awaiting o.

The only difference would occur when S <: Future<T> and flatten(S) is not a subtype of T. That ... cannot happen? If it can't, then the change is safe and it matches the static check better. If it can happen, ... I'd like to see how :)

@lrhn wrote:

S <: Future<T> and flatten(S) is not a subtype of T.

If S <: Future<T> then S is Never or S implements Future<U> for some U such that U <: T, and then flatten(S) is equal to Never or U, so said subtype relation is guaranteed to hold (and we don't even need to invoke the non-evaluability of an expression of type Never). How lucky. ;-)