A contravariant type variable in a superinterface causes twisted subtype relationships

[eernstg]

Consider the following program:

class A<X> {
  X x;
  A(this.x);
}

class B<X> extends A<void Function(X)> {
  B(void Function(X) f): super(f);
}

main() {
  // Upcast: `B<int> <: B<num>` by class covariance.
  B<num> b = B<int>((int i) => print(i.runtimeType));
  // Upcast: `B<num> <: A<void Function(num)>` by `extends` clause.
  A<void Function(num)> a = b;
  // Upcast: `A<void Function(num)> <: A<void Function(double)>`
  // by class covariance, plus `double <: num` and `void <: void`.
  a.x(3.14);
}

Every assignment in main involves an upcast, so there are no downcasts at all and the program should be safe. However, execution fails at a.x(3.14) because we are passing an actual argument of type double to a function whose corresponding parameter type is int.

Note that soundness (that is: the heap invariant) is violated during execution at the point where a is initialized, but none of our tools detect any errors statically.

(OK, slightly older versions of dartanalyzer will flag the initialization of a as an error, and current dartdevc-chrome raises the same error, perhaps because it uses an older analyzer, but that's clearly a bug, and newer versions of dartanalyzer, at least 2.1.0-dev.6.0 and up, have 'No issues!').

Next, none of the configurations for execution (running dart, running JavaScript code from dart2js, running code from dartdevc , etc.) detect the heap invariant violation, they only fail when they get to the invocation of a.x(3.14), and that's because we're so lucky that the function literal checks the type of its argument (so it's not a caller-side check of a.x).

The problem is, of course, that the contravariant usage of a type variable in a superinterface creates a twisted subtype lattice where B "goes in one direction" (B<int> <: B<num>) and the superinterface A "goes in the opposite direction" (A<void Function(int)> is a direct superinterface of B<int> and A<void Function(num)> is a direct superinterface of B<num>, but we have A<void Function(num)> <: A<void Function(int)> rather than the opposite):

  A<void Function(int)> :>  A<void Function(num)>
     ^                         ^
     |                         |
     |                         |
  B<int>                <:  B<num>

So where we typically have a "parallel" subtype relationship (

  Iterable<int>  <:    Iterable<num>
     ^                    ^
     |                    |
     |                    |
  List<int>      <:    List<num>

) this is an "anti-parallel" relationship. And that creates the opportunity to have a series of upcasts that takes us from int to double in part of the type without ever seeing a discrepancy (because we can just as well go up to A<void Function(double)> in the last step rather than A<void Function(int)>).

I believe that this creates a number of problems for the static analysis and comprehensibility of Dart code, and also that it is difficult to find a really good motivation for how it can be used in a meaningful and constructive manner.

[ds84182]

Would an alternative solution be making B also contravariant, like it's superinterface?

[eernstg]

Yes, the following would be a relevant design alternative (of course, client code would then be different), and that would give us the "parallel" subtype structure that we need for soundness:

class A<X> {
  X x;
  A(this.x);
}

class B<X extends void Function(Null)> extends A<X> {
  B(X f): super(f);
}

typedef F_int = void Function(int);
typedef F_num = void Function(num);

main() {
  B<F_int> b = B((int i) => print(i.runtimeType));
  // Now a downcast, prevented at run time or (with --no-implicit-casts) at compile-time:
  B<F_num> bNum = b;
  // Next line is rejected: `B<F_int> <: A<F_int>` and `A<F_num> <: A<F_int>`,
  // but `B<F_int>` and `A<F_num>` are unrelated, as they should be.
  A<F_num> a = b;  // ERROR.
  a.x(3.14); // So we don't get to do this on an instance of `B<F_int>`.
}

So there's nothing stopping us from using function types as type arguments, we just shouldn't allow variances to be swapped in a subtyping step. Hence, the only solution I've proposed for this issue (#39) is to introduce a compile-time error that simply prevents it.

[leafpetersen]

I believe the fix for this issue has rolled out.