Should use-site variance be allowed almost everywhere with legacy type variables?

[eernstg]

Considering the variance mechanism exactly (cf. #524), it is not obvious whether we'd want to allow this modifier in certain contexts. In particular, we could allow exactly on a type parameter that occurs non-covariantly in a member signature even if it contains legacy type variables (that is, type variables that have no variance modifiers) in non-covariant positions.

For example:

class C<X> {
  X x;
  void foo(List<exactly X> xs) { // (1). Error or not?
    xs.add(x); // Statically safe.
  }
}

main() {
  // When the receiver has `exactly`, it just works.
  C<exactly num> c = C();
  c.foo(<int>[]); // Compile-time error, List<exactly int> not subtype of List<exactly num>.
  c.foo(<num>[]); // OK, statically and dynamically.
  List<num> xs = <int>[];
  c.foo(xs); // Error (downcast); with `xs as List<exactly num>`: fails at run time.
 
  // When the receiver has just the legacy type, the `foo` signature is misleading.
  C<num> c2 = C<int>(); // Allowed, type parameter `X` is legacy-covariant.
  c2.foo(<int>[]); // Compile-time error, even though `<int>[]` has exactly the required type.
  c2.foo(<num>[]); // OK statically, but fails at run time.
  List<num> xs2 = <int>[];
  c2.foo(xs2); // Error (downcast); with `xs as List<exactly num>`: fails at run time.
}

The upcoming variance proposal makes it an error to have exactly on any type argument T in a non-covariant position in the signature of an instance member when T contains any class/mixin type variable which isn't marked inout.

In the example, at (1), void foo(List<exactly X> xs) is then an error because exactly X contains X, which isn't inout.

The reason for having this error is that it should be possible to compute a sound approximation of the member signature which can be used for type checking (and then any slack would give rise to a dynamic check). But void foo(List<exactly X> xs) can only be approximated soundly by void foo(Never xs), and that's not sufficiently useful at call sites.

If we don't approximate the signature at all, but just keep it as written void foo(List<exactly X> xs), then we get the undesirable properties shown in the second half of main in the example above: We get a compile-time error for the case c2.foo(<int>[]) even though the actual parameter type of c2.foo is List<exactly int> and <int>[] has exactly that type; and we do not get an error at compile-time for c2.foo(<num>[]), even though the type of <num>[] is unrelated to the actual parameter type. So we reject some invocations that would work, and we accept other invocations that do fail; this is simply misleading.

So for type variables marked out or in we will keep this error, because we can't obtain a useful sound approximation, and such type variables should be treated soundly.

However, if we focus exclusively on legacy-covariant type variables occurring in non-covariant positions, we already know that there will be a dynamic check on the corresponding parameters (or a read check on the returned value, if that's where we have the non-covariant occurrence). This means that we don't have to approximate the member signature soundly, we could actually approximate it by any type whatsoever, and rely on the dynamic check.

So, for example, we could give c.foo the signature void foo(List<X> xs) (that is, we erase exactly) when the receiver does not have exactly on its type argument at C.

This would allow the case that works (c2.foo(<int>[])) as well as the one that fails (c2.foo(<num>[])), but the latter is just another example of the kind of dynamic type error that type parameters (the 'normal' type parameters that we now call legacy-covariant) have always carried with them. So in that sense it would actually fit in with the unsound variance that we have used until now in Dart.

If we do allow this then client code using exactly on some legacy-covariant type parameters will be able to maintain better type safety than they could otherwise achieve. But if there is no exactly in the receiver type then there is no improvement compared to the situation where the ocurrences of exactly in signature are eliminated (in the example that would be void foo(List<X> xs)).

So the question is: Do we want to go for this type safety improvement, even though it forces clients to write exactly in order to get it?