NNBD, i-2-b: Analyzer throws unexpected error for contravariant function type parameter

[iarkh]

Dart VM version: 2.9.0-13.0.dev (dev) (Fri May 29 15:59:05 2020 +0200) on "windows_x64"

The following source code example prints "OK" with dart and throws a compile error with analyzer:

typedef G<X> = Function(X);
class A<X extends G<A<X,Y>>, Y extends X> {}

test<X>() { print("OK"); }

main() {
  test<A<G<A<Never, Never>>, dynamic>>();
}

Sample output is:

$ dart --enable-experiment=non-nullable test.dart
OK

$ dartanalyzer --enable-experiment=non-nullable test.dart
Analyzing test.dart...
error - 'dynamic Function(A<Never, Never>)' doesn't extend 'dynamic Function(A<dynamic Function(A<Never, Never>), dynamic>)'. - test.dart:7:10 - type_argument_not_matching_bounds
1 error found.

Please note that this problem is not reproducible in legacy code, i.e. the following example passes both with analyzer and dart when runs without --enable-experiment=non-nullable flag:

typedef G<X> = Function(X);
class A<X extends G<A<X,Y>>, Y extends X> {}

test<X>() { print("OK"); }

main() {
  test<A<G<A<Null, Null>>, dynamic>>();
}

[eernstg]

Looks like the analyzer with --enable-experiment=non-nullable does not detect that A<G<A<Never, Never>>, dynamic> is a correctly super-bounded type, because it violates the bound, but A<G<A<Object?, Object?>>, Never> is regular-bounded.

// Type variable mapping
X --> G<A<Object?, Object?>>
Y --> Never.

// Bounds check
X <: G<A<X, Y>> -->
  G<A<Object?, Object?>> <: G<A<G<A<Object?, Object?>>, Never>>, true if
  Function(A<Object?, Object?>) <: Function(A<G<A<Object?, Object?>>, Never>), true if
  A<G<A<Object?, Object?>>, Never> <: A<Object?, Object?>, which is true.

[scheglov]

I don't understand this area well enough to solve this issue.
In fact I even don't understand probably a helpful comment that @eernstg left :-(

[eernstg]

I was just checking that A<G<A<Never, Never>>, dynamic> is a correctly super-bounded type (which amounts to (1) checking that it violates its bounds, and (2) checking that replacing extreme types by their opposites according to variance yields a type that satisfies its bounds (that is: A<G<A<Object?, Object?>>, Never>). This makes A<G<A<Never, Never>>, dynamic> a well-bounded type, so no error should be reported when it is used as the actual argument in an invocation of test.

[devoncarew]

@MichaelRFairhurst - is this fixed as of https://dart-review.googlesource.com/c/sdk/+/156443 ?

[scheglov]

This was fixed.

[leafpetersen]

@eernstg I don't understand your comment above, I don't think we've updated the spec here for null safety have we? That is, I think there's missing spec work here.

[eernstg]

That's true, dart-lang/language#1133 updates the null-safety spec accordingly.