Specify null-safety async returns

[eernstg]

This PR on the nnbd spec introduces the requirement "S assignable to T_v or flatten(S) <: T_v" (aka model 1) for a return statement in an async function, where S is the static type of the returned expression, and T_v is the future value type of the function.

This PR also specifies the dynamic semantics, using an approach where the presence/absence of an await step is statically determined whenever possible.

The new dynamic semantics is the same as the pre-null-safety dynamic semantics (that is, the one which is currently specified in dartLangSpec.tex), except for the case where the returned object dynamic type is a subtype of as well T_v as Future<T_v>, and the returned object static type is not dynamic, but it is a subtype of T_v. This case is expected to be very rare.

@lrhn, I made some changes to the rules that you proposed: (1) The case where S is dynamic is now first: This ensures that we will await a Future<T_v>, even in the case where T_v is a top type. If we check S <: T_v first then that case will apply, and we wouldn't await the future. The typical case is f() async => Future.value(1) as dynamic;, and I think it is an unnecessary breaking change if f would stop awaiting the future and instead use it to complete the returned Future<dynamic>.

(2) I removed the case for S implements Future<dynamic>, because that is a compile-time error with model 1 (because otherwise an earlier case would apply). (3) I removed the case for S is FutureOr<dynamic> for the same reason.

[eernstg]

Great feedback, thanks! Made various changes, PTAL.

[eernstg]

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...

[leafpetersen]

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).

[eernstg]

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.

[eernstg]

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

[lrhn]

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 :)

[leafpetersen]

This LGTM. Can you write tests and file implementation issues?

[eernstg]

@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. ;-)