Use mutual subtyping for bounds to determine function subtype relationships

[eernstg]

This issue is a proposal to change the rules for subtyping such that generic function types rely on mutual subtyping for bounds, rather than requiring the bounds to be "the same type".

Currently, the subtype rules in the language specification require the bounds to be pairwise the same type in order to establish a subtype relationship between two generic function types, relying on consistent renaming (alpha-equivalence) to eliminate differences that only arise because of different choices in naming.

For example, void Function<S extends dynamic>() and void Function<S extends Object>() are unrelated according to these rules.

The rules in subtyping.md contain updates for NNBD which will be integrated into the spec. These rules are very similar in this area: They use substitution to perform the renaming explicitly (that makes no difference), but they require === among each pair of bounds, which is slightly different; === means 'the two types are structurally equal up to renaming of bound type variables, and equating all top types'.

An example where this matters is void Function<S extends dynamic>() and void Function<S extends Object?>(): They are subtypes of each other with NNBD rules. But void Function<S extends Never?>() and void Function<S extends Null>() are still unrelated, even though Never? and Null is "the same type" from several different points of view (for instance, exactly the same set of objects have that type).

This issue is a proposal to use mutual subtyping for the bounds in the rule for generic function type subtyping. This will ensure S <: T in all the cases where the NNBD rules have S <: T, plus a few additional ones.

As an example, void Function<X extends B1>([X x]) is a subtype of void Function<X extends B2>() iff B1 <: B2 and B2 <: B1. Also, all pairs mentioned above will be subtypes of each other with these rules, in particular void Function<S extends Never?>() <: void Function<S extends Null>().

The precise proposed change is shown in #497.

For an earlier discussion touching on this topic, see dart-lang/sdk#37484. A topic which is related is == on instances of Type, cf. dart-lang/sdk#32782. Note that the analyzer, dart2js, and the VM already allow some assignments where bounds differ, but are mutual subtypes (including some that don't rely on top types):

main() {
  void Function<X extends Object>(X) Function() f1 = null;
  void Function<X extends Object>(X) Function() f2;
  void Function<X extends dynamic>(X) Function() f3;
  void Function<X extends D>(X) Function() f4pre<D>() => null;
  var f4 = f4pre<dynamic>();
  f2 = f1; f1 = f2; f3 = f2; f2 = f3; f3 = f4; f4 = f3;
  f3 = f1; f1 = f3; f4 = f2; f2 = f4; f4 = f1; f1 = f4;

  void Function<X extends List<dynamic>>(X) f6;
  void Function<X extends List<FutureOr<void>>>(X) f7;
  f6 = f7; f7 = f6;

  void Function<X extends FutureOr<Null>>(X) f8;
  void Function<X extends Future<Null>>(X) f9;
  f8 = f9; f9 = f8;
}

@leafpetersen, @lrhn, @munificent, what do you think?

[leafpetersen]

I think either this or normalization are the right choices. Ideally the two are equivalent.

[eernstg]

Closing: NNBD rules now include this.