language/least_upper_bound/least_upper_bound_greatest_closure_2_test causes stack overflow in SubtypeHelper.isSubtypeOf

[scheglov]

scheglov@scheglov-macbookpro2:~/Source/Dart/sdk.git/sdk (master)$ sdk/bin/dartanalyzer --ignore-unrecognized-flags --packages=/Users/scheglov/Source/Dart/sdk.git/sdk/.packages --format=json --no-hints /Users/scheglov/Source/Dart/sdk.git/sdk/tests/language/least_upper_bound/least_upper_bound_greatest_closure_2_test.dart
Unhandled exception:
Stack Overflow
#0      InterfaceTypeImpl.isDartCoreObject (package:analyzer/src/dart/element/type.dart:771:3)
#1      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:76:56)
#2      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:284:25)
#3      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:164:11)
#4      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:284:25)
#5      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:164:11)
#6      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:284:25)
#7      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:164:11)
#8      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:284:25)
#9      SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:164:11)
#10     SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:284:25)
#11     SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:164:11)
#12     SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:284:25)
#13     SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:164:11)
#14     SubtypeHelper.isSubtypeOf (package:analyzer/src/dart/element/subtype.dart:284:25)

[scheglov]

The minimal reproduction so far

import 'dart:async';

void f<X extends FutureOr<X>>(X x) {
  x ?? 0;
}

[scheglov]

Spec https://github.com/dart-lang/language/blob/master/resources/type-system/subtyping.md

[scheglov]

We apply rules:

1. Right Object: if T1 is Object then:
   1.1. if T0 is an unpromoted type variable with bound B then T0 <: T1 iff B <: Object
   1.1.1. Here T0 = X, B = FutureOr<X>.
   1.2. if T0 is FutureOr<S> for some S, then T0 <: T1 iff S <: Object
   1.2.1. Here T0 = FutureOr<X>, S = X.

[srawlins]

CC @eernstg for bug which may be an infinite loop which is specified in the spec

[eernstg]

Right, the subtype rules do give rise to an attempt to prove X <: Object by proving X <: Object, so we do have a loop in the spec. The problem is that the type variable rule lets us go from X <: T1 to B <: T1 where X extends B, and the FutureOr rule lets us go from FutureOr<X> <: T1 to X <: T1.

However, the bound X extends FutureOr<X> is trivially satisfied because FutureOr is a union where X is one of the operands, so we could actually eliminate such bounds: We could simply consider X extends FutureOr<X> to be a verbose way to write a type variable with no bound. If we do this early then the looping query should never arise.

In the specification we could have a notion of normalization of type variable bounds, which is applied before we proceed to use any subtyping rules (and those rules would be the same as today).

It is not trivial to see that any particular change would eliminate all looping cases. For instance, Left Null may seem similar to Right Object, but it is different: We have Null <: FutureOr<X> if Null <: X, but the latter never true anyway.

@leafpetersen, WDYT?

[leafpetersen]

Is this not just another instance of dart-lang/language#433 ?

[eernstg]

I don't think dart-lang/language#433 mentions the connection to looping subtype checks. This issue would then serve as a concrete motivation for re-opening dart-lang/language#433 (and the fix would then be to make those bounds an error, rather than normalizing them away).

[eernstg]

Awaiting dart-lang/language#433.

[polina-c]

• @nshahan

[johnniwinther]

@chloestefantsova Is there any work here for the CFE?

[chloestefantsova]

@johnniwinther We should report an error in this case instead of crashing; however, the well-formed Dart programs aren't broken.

[mraleph]

This test is still failing on all configurations with StackOverflow in the CFE.

[johnniwinther]

@chloestefantsova Can you take at the CFE-side of things?

[chloestefantsova]

@chloestefantsova Can you take at the CFE-side of things?

Sure thing!

[chloestefantsova]

However, the bound X extends FutureOr<X> is trivially satisfied because FutureOr is a union where X is one of the operands, so we could actually eliminate such bounds: We could simply consider X extends FutureOr<X> to be a verbose way to write a type variable with no bound. If we do this early then the looping query should never arise.

@eernstg I like this idea. I'm working on a CL (https://dart-review.googlesource.com/c/sdk/+/342920) to mitigate the amount of crashes due to the infinite recursion, and the approach I'm taking there is that the bounds of the form X extends FutureOr<X> are treated as no bound, that is, as Object?. Would that be enough to address the issue fully?

[eernstg]

I do think it is benign to simply eliminate bounds from type parameter declarations of the form X extends FutureOr<X>, and similarly for type parameter declarations that normalize to that form after type alias expansion. A similar step could be taken with X extends X? and X extends FutureOr<X?> etc. We can have an arbitrary number of "union operators" applied to X, it is still going to have X as one of the operands of the resulting union, which implies that it is impossible to violate this bound.

@leafpetersen, WDYT? Do you prefer to make those vacuous bounds an error?

[chloestefantsova]

A similar step could be taken with X extends X? and X extends FutureOr<X?> etc. We can have an arbitrary number of "union operators" applied to X, it is still going to have X as one of the operands of the resulting union, which implies that it is impossible to violate this bound.

Good point. We should probably consider self-dependency via another variable too, for example, X extends FutureOr<Y>, Y extends X.