Subtyping issue with Positional Function Types

[sgrekhov]

Please see https://github.com/dart-lang/sdk/blob/master/docs/language/informal/subtyping.md

Positional Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn, [Vn+1 xn+1, ..., Vm xm])

and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sp yp, [Sp+1 yp+1, ..., Sq yq])
and p >= n
and m >= q
and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...q
and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]

This rule is brocken in the following example

class U {}
class B0 {}
class B1 {}

class X0 extends B0 {}
class X1 extends B1 {}

class Y0 extends B0 {}

typedef U T0<X extends B0, Y extends B1>();
typedef U T1<X extends B0, Y extends B0>(); //  Y extends B0, not B1

U t0<X extends B0, Y extends B1>() => null;
U t1<X extends B0, Y extends B0>() => null;

main() {
  T0<X0, X1> t0Instance = t0;
  T1<Y0, Y0> t1Instance = t0Instance;
}

Here, in T1, Y extends B0, not B1. This brokes the rule

and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k

That means that in example above T0<X0, X1> is not a subtype of T1<Y0, Y0> and
T1<Y0, Y0> t1Instance = t0Instance; shold produce an error. But it does not (in VM and analyzer).

Dart VM version: 2.0.0-dev.60.0 (Mon Jun 4 22:09:13 2018 +0200) on "windows_x64"

[vsmenon]

@eernstg @leafpetersen - can one of you triage? is this an implementation bug?

[leafpetersen]

Two parts: the test as written is wrong, and the analyzer only fairy recently fixed the issue that this test is intended to test for: #29014 . This was fixed about two weeks ago though, so should be available in recent dev builds.

For the test, the confusion is around the different typedef syntax. As written

typedef U T0<X extends B0, Y extends B1>();

is not the type of a generic function. It is a parameterized type which when instantiated produces a regular function type. So this line:

  T0<X0, X1> t0Instance = t0;

declares a variable of type U Function() and assigns a generic function to it. Inference instantiates the generic function appropriately, so the test correctly does not issue an error. The corrected version of the test is below: both the CFE and the analyzer correctly report a static error. If you comment out the second to last line in main, the last line causes a runtime error on the VM.

class U {}
class B0 {}
class B1 {}

class X0 extends B0 {}
class X1 extends B1 {}

class Y0 extends B0 {}

typedef T0 = U Function<X extends B0, Y extends B1>();
typedef T1 = U Function<X extends B0, Y extends B0>(); //  Y extends B0, not B1

U t0<X extends B0, Y extends B1>() => null;
U t1<X extends B0, Y extends B0>() => null;

main() {
  T0 t0Instance = t0;
  T1 t1Instance = t0Instance;
  t1Instance = (t0Instance as dynamic);
}