Analyzer awaiting X&F? where F is a proper subtype of Future, behaves weirdly

[lrhn]

Example:

extension type ExtF(Future<int> _) implements Future<int> {}

class ClassF implements Future<int> {
  then<T>(onValue, {onError}) => Future.value(42).then(onValue);  
  noSuchMethod(i) => super.noSuchMethod(i);
}

typedef F = ExtF;
// typedef F = ClassF; 
// typedef F = Future<int>; // CHange to this to see difference.

void main() {
  test<Object?>(ClassF());
  test<Object?>(null);
}

void test<X extends Object?>(X x) async {
  if (x is F?) (await x).st<E<int?>>(); // Is error: Analyzer (type `int`)
  if (x is F?) (await x).st<E<int?>>; // ??
  if (x is F?) (await x).st<E<String>>; // ??
}

extension<T> on T {
  // Expect static type to be `E`(xactly) `T`
  void st<X extends E<T>>() {
    print("$this: $runtimeType @ $T");
  }
}
typedef E<T> = T Function(T);

This shows both with an extension type and a class implementing Future<int>, so it's not specific to extenstion types.
The promoted type of x is F?, where F is a proper subtype of Future<int>.

Awaiting that should give an int?, but analyzer says it's an int. (Comment out the String line, and the code will run in DartPad and give a null result from the int-typed expression.)

Further, if I remove the () from the st invocation, making it a tear-off which should have the same parameter requirements as a call, it seems the type parameters are not checked at all.

If I change the type F to be Future<int> directly, so the promoted type is Future<int>?, the type of await becomes int?, and the two tear-offs get checked again. (Which is why I'm guessing the issues are related.)

[bwilkerson]

@scheglov

[eernstg]

I believe that F? does not derive a future type when F is an extension type like ExtF or a class like ClassF. In other words, I'd say that the analyzer has the specified behavior when it concludes that await x has type X in those two cases, and the CFE uses a different (non-spec) approach when it gives await x the type int?.

We might want to change the language specification such that ExtF? and ClassF? can derive the future type Future<int>?, but unless and until we do that, the result should be X.

---

If we do make that change then we would probably want to add a rule saying that if S derives the future type F then S? derives the future type F?.

[lrhn]

I'll argue that's a bug in the specification of "Derives a future type".

The intent of that is to figure out whether a type suggests a specific future type, which will be the one flattened by flatten.

When you flatten Future<int>?, it becomes int?. When you flatten X&(Future<int>?) it should also become int?.
If it doesn't, we've made a mistake, and should fix that.

The behavior I'd want for "derives a future type" is:

• FutureOr<T> derives a future type.
• T derives a future type if T has Future<S> as superinterface for some S
• T? derives a future type if T does.
• X with bound B derives a future type if B does.
• X&B derives a future type either
  • if B does, or
  • if B doesn't and X does.

The point of "derives a future type" is to preserve X instead of B from X&B when B doesn't suggest a future type at all, but to flatten it when it does.
When B looks like something you'd otherwise want to await, then that should be the thing you await on X&B.
If not, we fall back on X, so you don't lose the original type to an await nonFuture.
I.e., is flatten(X & Object) = X and flatten(X & Future<int>) = int.

A type like Future<int>? is something you'd have reason to await, therefore X extends Future<int>? and X & Future<int>? will also be types you'd want to await, and we should include them in the "derives a future type".

[eernstg]

.. that's a bug ..

Yes, that's certainly a fair characterization. This is also the reason why I suggested that we might want to change the rules. However, we know that we must be careful in this area.

When you flatten Future<int>?, it becomes int?. When you flatten X&(Future<int>?) it should also become int?. If it doesn't, we've made a mistake, and should fix that.

This is already working just fine.

The missing part is that we're now focusing on proper subtypes of Future, and they are not handled in this situation.

Proper (non-bottom) subtypes of Future used to be very rare in user code. Instances of _Future would occur frequently at run-time, but the static type would typically be Future<S> or FutureOr<S> for some S, and very rarely a proper subtype of Future. In this issue we may suddenly have proper subtypes of Future as static types all over the place, because we're specifically focusing on extension types and await. The fact that we can create a class which is also a proper subtype of Future is relevant, but it hasn't played much of a role so far. In any case, we need to handle those proper subtypes in a meaningful way.

Returning to the example, flatten(X & (Future<int>?)) == int? as intended, but flatten(X & F?) == X when F is an extension type or class that implements Future<int>. We fail to see that F? is useful, because it doesn't "derive a future type", so we proceed to use X, whose flatten is just X (if we still have X extends Object?).

As I see the situation, we could just proceed and generalize 'derives a future type' in order to get a consistent and understandable semantics, and then ask for implementations. However, we don't want introduce breaking changes with respect to anything that isn't in need of improvements.

[eernstg]

I created dart-lang/language#3574 in order to handle a potential specification change.

[leafpetersen]

Awaiting that should give an int?, but analyzer says it's an int. (Comment out the String line, and the code will run in DartPad and give a null result from the int-typed expression.)

@lrhn I'm confused about what you're seeing. I can't reproduce this. What I do see is that the analyzer and the CFE are inconsistent here, but I don't see any unsoundness, and I don't see the analyzer producing int here. Specifically, if I modify your code to get the analyzer to print out the types, I get the following:

void f(int x) {}
void test<X extends Object?>(X x) async {
  if (x is F?) f(x); // Is error: Analyzer (type `X & ExtF`)
  if (x is F?) f((await x)); // Is error: Analyzer (type `X`)
}

This is inconsistent with the CFE, which seems to infer X & F for x (it doesn't print out the intersection type in the error, but adding an assignment seems to validate that the intersection is there) and int? for await x.

Either of these choices could, I believe, be sound in the sense that they are internally consistent: the await x would simply check that the value is of the type Future<X> in the analyzer interpretation and Future<int? for the CFE interpretation. Is that right? Or am I missing something?

Assuming the soundness issue is put to the side, the question then is, which is correct? I believe that the CFE is consistent with the current specification if we expand "derives a Future type" to extension types in the obvious way, right?

[lrhn]

I don't think this is an actual runtime unsoundness. It can't be since the issue is only aimed at the analyzer.

If I remember correctly, the "give a null result from the int-typed expression" tries to say that the runtime behavior (dart2js) gives a null value from the expression that the analyzer reported as having type int. Which makes the analyzer out of touch with reality, but the runtime isn't unsound because Dart2JS/CFE inferred int?.
(The analyzer can't really be unsound, if unsoundness is defined as a runtime value not satisfying the static type, since the analyzer has no runtime values. I'll sometimes say "unsound" about it meaning that the type it predicts is not a sound approximation of what the runtime semantics says the result will be, but that's only an analytical unsoundness, not a "real" one.)

It's hard to get a runtime unsoundness with await because of how we've defined it. We only await a future if it is a Future<T> where T is the static type of the await expression. That can't be wrong. So as long as any value which isn't awaited is also a subtype of T, soundness is pretty much certain. (That's the S <: FutureOr<flatten(S)> requirement for flatten, which it's defined to satisfy. If that's not satisfied, we do have a problem.)

Back to this issue: The analyzer does not appear to infer int any more, only int?, which is consistent with reality.
Not sure when it was fixed, can't find a commit mentioning this issue, so maybe it was fixed as a side effect of something else.

So what is left is the discrepancy between implementations of flatten(X&F?) where F is a proper subtype of Future, and my opinion that what we have specified (and the analyzer might now be implementing) is not necessarily the right choice.

extension type EF<T>(Future<T> _) implements Future<T> {}
void test<X extends Object?>(X o) async {
  if (o is EF<int>) {
    var v = await o;
    v.st<E<int>>();  // Both agree. (And this test would erase an intersection type to the variable)
  }
  if (o is EF<int>?) {
    // Promotion succeeds.
    var (Future<int>? _) = o;
    var (X _) = o;
    // Await it.
    var v = await o;

    var (X _) = v; // Analyzer accepts, CFE error (int? not assignable to X)
    v.st<E<X>>(); // Analyzer accepts, CFE error
    var (int? _) = v; // CFE accepts, analyzer error (X not assignable to int?)
    v.st<E<int?>>();  // CFE accepts, analyzer error
  }
}
extension <T> on T {
  void st<X extends E<T>>(){}
}
typedef E<T> = T Function(T);

The spec says that EF<int>? does not derive a future type.
Because of that flatten(X & EF<int>?) should be flatten(X) = X.

The CFE thinks it does, which is why its flatten gives flatten(EF<int>?) = int? instead.
(It doesn't just always uses the flatten of the promotion.)

My position is that the bug is in "derives a future type", and EF<int>? should derive one, and the CFE got it right.
When you promote a type variable to a type X&B, we should treat the promoted type variable type as B as much as possible. The user specifically asked for this type, and got it.

(Which is why I, now, think flatten(X&B) should just always be flatten(B). It's the most precise thing we know about the type of the value of that type. That may mean that awaiting an X&Object loses the assignability to X, but otherwise it loses the "is not null", which may be equally bad for the user. And I think if (x is T) { ... x used as T ...} should generally work exactly the same whether we promote x from Object? or X extends Object?. The only difference should be that x can be up-cast back to X in the latter case.)

[leafpetersen]

Back to this issue: The analyzer does not appear to infer int any more, only int?, which is consistent with reality.

@lrhn where do you see this? When I test this in the beta release and on current main, I see the analyzer inferring X for the type of await x.

Because of that flatten(X & EF<int>?) should be flatten(X) = X.

So it sounds like the analyzer is correctly implementing the current spec, the CFE is divergent. The question then does seem to be whether we want to change the spec. I mentioned this to @eernstg this morning, but this feels to me like a place where we would likely have stayed out of trouble if we had specified this via reference to an existing construct instead of inventing a new "derives a future type" algorithm. Am I correct that what we want "T derives a future type Future<U>" to mean is just "T is a subtype of Future<U>, and for all S such that T is a subtype of Future<S>, U is a subtype of S"? If so, we have an existing algorithm for finding this (subtype matching) and it would probably have saved us a bunch of trouble if we just re-used that algorithm in the specification.

[lrhn]

My bad, analyzer doesn't say the unsafe int any more, but it also doesn't say int?.

Yes, the analyzer is correctly implementing the spec. The spec is meaningless as written, because it doesn't actually say what it intended to say. It's not completely surprising that the CFE actually did what was intended, if they understood the intent and implemented it, and missed that the spec hadn't actually hit the mark.

Am I correct that what we want "T derives a future type Future<U>" to mean is just "T is a subtype of Future<U>, and for all S such that T is a subtype of Future<S>, U is a subtype of S"?

No.

The intent is to see if a type has a Future part which can meaningfully be awaited. Basically, whether flatten(T) ≠ T, except that that equality might be able to happen by accident even if T has some future-part. (Not sure, but can't rule out an X extends Future<X> type variable, or something similarly sinister.)

So "derives a future type" traverses the type structure just like flatten would, until it finds a type that is implements Future or is FutureOr, where flatten would actually do something.

The idea with it was that for flatten(X&B), if B doesn't derive a future type, then B really isn't interesting for flatten. Choosing flatten(B) = B as the result of flatten would mean that await x of that type would check if the value of x implements Future<B>, which it overwhelmingly likely doesn't, and otherwise just delay and evaluate to x again, at type B, which isn't even assignable to X.

If B of X&B has such a future part, we choose flatten(X&B) = flatten(B). Otherwise we choose flatten(X) instead, which is at least assignable to X, and might, hypothetically, derive a future type.

Seemed like a great idea at the time. I don't believe in it any more.
If someone promoted X to X&B, and B doesn't derive a future type, then most likely neither does X.
If X does, then either X has a, possibly nullable, Future-implementing type as bound, and B is a promotion to Null or Never, or X has a, possibly nullable, FutureOr type as bound, and B is a promotion into the non-future side of the FutureOr.
In either case, I don't think we should just ignore the promotion and fall back on the bound. That's not what the user asked for.
(The one argument for doing it anyway is that the user did await the type, so presumably they expected some kind of future.
But if X doesn't derive a future type either, should we go back to B again?)

I suggest we drop the "derives a future type", let flatten(X&B) = flatten(B), and don't try to be clever.

(I also wrote, not because I think I'll ever get it, a fresh design of await, as I would have made it from scratch today: https://gist.github.com/lrhn/2d9ed1485b3e146d0c2091ab294cf2bb)

[eernstg]

@leafpetersen wrote, and @lrhn responded:

Am I correct that what we want "T derives a future type Future<U>" to mean is just "T is a subtype of Future<U>, and for all S such that T is a subtype of Future<S>, U is a subtype of S"?

No.

The intent is to see if a type has a Future part

Right, that's the reason why I keep saying that if we're looking for the type S such that "T derives the future type S" for a given T then we must search the set of supertypes of T, looking for types of the forms Future<U>, Future<U>?, FutureOr<U>, and FutureOr<U>?. They are the forms of type that have a future part.

It's tempting to say the following:

• If T <: Future<U> and U is minimal then T derives the future type Future<U>, otherwise
• if T <: Future<U>?, and U is minimal then T derives the future type Future<U>?, otherwise
• if T <: FutureOr<U>, and U is minimal thenT derives the future type FutureOr<U>, otherwise
• if T <: FutureOr<U>?, and U is minimal then T derives the future type FutureOr<U>?, otherwise
• T does not derive a future type.

However, that won't quite work, because T could be int, say, and we don't want to say that int derives the future type FutureOr<int>.

So we don't just want to use the (nice, declarative, complete) subtype relationship. The approach we've taken so far in the specification is to refer to types with which T has an explicitly declared subtype relationship. We know that such subtype relationships can be introduced by superinterface relationships (extends ... with ..., implements, and mixin-on) and by type parameter bound declarations.

That gives rise to the following definition of "derives a future type" (which is exactly what I'm proposing in dart-lang/language#3574):

• If T is a type which is introduced by a class, mixin, mixin class, enum, or extension type declaration, and if T or a direct or indirect superinterface of T is Future<U> for some U, then T derives the future type Future<U>.
• If T is the type FutureOr<U> for some U, then T derives the future type FutureOr<U>.
• If T is S? for some S, and S derives the future type F, then T derives the future type F?.
• If T is a type variable with bound B, and B derives the future type F, then T derives the future type F.
• (There is no rule for the case where T is of the form X & S because this will never occur.)

Granted, this definition is much less declarative. However, the reliance on the subtyping relationship opens a door which is too large, and then we'd still have to say something along these lines in order to avoid introducing irrelevant supertypes (like int spuriously deriving FutureOr<int>). So I prefer to use a definition that never says 'subtype'.

It's very easy to see that T <: S whenever T derives the future type S, and also that S has one of the forms Future<U>, Future<U>?, FutureOr<U>, and FutureOr<U>?, and that U is minimal.

@lrhn mentioned that we might want to get rid of "derives a future type" entirely. I have been thinking about this, too, and I've been thinking about ways to simplify flatten (because we appear to have some kind of overlap in the definition of "derives a future type" and flatten). It would be nice if we could have something like the following:

• If T derives the future type Future<S> or FutureOr<S> then flatten(T) = S.
• If T derives the future type Future<S>? or FutureOr<S>? then flatten(T ) = S?.
• Otherwise, flatten(T) = T.

We could then change it to the following (in 2035 or so):

• If T derives the future type Future<S> or FutureOr<S> then flatten(T) = S.
• If T derives the future type Future<S>? or FutureOr<S>? then flatten(T) = S?.
• Otherwise, flatten(T) is undefined.

.. and we could make it a compile-time error to have await e when flatten of the type of e is undefined. ;-)

If we do that then we certainly have to introduce a rule about "X & S derives a future type".

However, I did not change flatten at this time: We do need to generalize "derives a future type" in order to handle types like X extends F? meaningfully, where F derives a future type, and I think we can refactor flatten later: It just needs to be expressed in a way which is more elegant, but still equivalent.

[leafpetersen]

However, that won't quite work, because T could be int, say, and we don't want to say that int derives the future type FutureOr<int>.

So we don't just want to use the (nice, declarative, complete) subtype relationship.

Thanks, that's a very useful example for me to understand why we're specifying this separately from subtyping.