voidness propagation as a lint

[MichaelRFairhurst]

Dart 2 was originally going to have "voidness propagation"

Note that while this is illegal:

A:

void x;
int y = x; // error! use of void

this is not an error until runtime:

B:

List<void> x;
List<int> y = x;

and worse, this is not an error at all:

C:

List<void> x;
List<Object> y = x;

A is currently caught by the analyzer, but B & C were supposed to be handled by the not-landed "voidness_propagation."

Currently B is both a runtime error and can be caught by turning off implicit downcasts, but C is completely silent.

We could add this to the linter in the meantime. It also could be added to void_checks, but maybe it would be better to make it "voidness_propagation" because then users who don't want "void_checks" but do want to be future-proof for voidness_propagation could get what they want and nothing more. (this would be a good way to incrementally roll that out as part of the language).

@eernstg

[eernstg]

Right, we have the base level checks enforcing a static approximation¹ of "void typed values must be discarded", and voidness preservation is concerned with the higher order version of the same thing, that is, it is concerned with the situation where a "void typed value" is accidentally made available for general usage indirectly:

List<void> xs = [1];
List<Object> ys = xs; // OK now, flagged under voidness preservation.
int i = ys[0]; // Oops, nobody should use this value, but we forgot its voidness!

We have studied several different approaches to voidness preservation. The obvious starting point is that type transitions (that is, upcasts/downcasts and similar relationships) should not just be guarded by assignability (according to which there is no difference between Object and void an other top types), they should also be checked according to a different ruleset specifically for voidness preservation. That ruleset would be similar to subtyping, but it would consider void (and FutureOr^k<void> for all k) to be a proper supertype of all other types (including all other top types like dynamic, FutureOr<Object>, etc).

We don't have implicit "voidness downcasts" (which will stop int x = print("");, and ys = xs given the declarations above, and String Function(void) f = (Object x) => x.toString();), but "voidness upcasts" are OK (so void v = 42; is OK, and so are xs = ys and String Function(Object) f = (void v) => "42";). As you can see, this notion of a separate "voidness preservation type system" and the associated "voidness preservation subtype (not assignability) check" will subsume the base level checks that we already have in the language, and we may have to drill a hole or two in the system in order to allow stuff that we have already made non-errors at the base level (await voidExpression comes to mind, unwelcomely), but otherwise we have a pretty simple approach here that would probably work just fine.

We did have one other discussion in the language team which is relevant, though: I argued that we should actually erase certain occurrences of top types to Object as seen from the client side, in particular, the ones that occur in a contravariant position in the method signatures of the interface of a class. This would mean that we would consider the following two methods f1 and f2 to have the same signature:

abstract class C {
  int f1(void x, dynamic y, void Function(void) z);
  int f2(Object x, Object y, Object Function(void) z);
}

But if the third argument of f2 had had type void Function(Object) then they would have differed (because the place that differs is a covariant occurrence in the signature of f2, so we don't erase that void to Object when we compare, so voidness preservation would note that the signatures are incompatible). Conceptually, the point is that z is a callback, and if I'm writing myC.f2(_, _, (v) => e) then it does matter (for me as a client of C) whether e will be allowed to use v or not.

The point that I'm making is that it is fine that we can enforce that a given implementation of a method does not use one of its arguments (so (void v) => e can't use v in e, except the exceptions), but this is an implementation detail that clients will not be allowed to rely on; in return for that "looseness" (that we will not get a promise that any given first class function that we are calling won't use certain arguments), we will get the improvement of having fewer conflicts:

abstract class I { foo(void x); }
abstract class J { foo(Object x); }
abstract class C implements I,J {}

Without this particular kind of "top type erasure" we would have a conflict: "On a receiver x of static type C I'm calling foo(e); will you promise that the callee will not use that value?" and the compiler would say "That's none of your business, if you don't want a first class function to use a given value, don't pass that value to that function as an actual argument in the first place!!".

With the top type erasure we just have two method signatures for foo which are both dynamic Function(Object), so there's no conflict. I believe that these conflicts would, more often than not, be spurious, so we should make it an implementation detail whether any given callee uses one or the other top type in contravariant positions.

Each method implementation would still be checked without the erasure, of course, so with class D { int foo(void x) => e; }, e can't use v unless there is an explicit cast with as etc.

Footnote 1: Even base level void checks are incomplete, because no constraints are imposed on expressions whose type is a type variable X, even though the actual type argument might be specified as void, and since the run-time value of X is Object we cannot check it dynamically.

[a14n]

Regarding the following case:

List<void> x;
List<Object> y = x;

what should be do for dynamic?

List<void> x;
List<dynamic> y = x;  // OK or not for voidness_propagation ?

[eernstg]

We have two (strong) opinions on List<dynamic> y = x: (1) This should be an error because it allows developers to silently get to a situation where elements from x are used, even though they should be discarded; and (2) this should not be an error because the whole point of dynamic is that it tells the type checker to stop complaining. I'd lean towards (1), but (2) seems more consistent with the treatment of void and dynamic in the context of return e; statements.

[a14n]

An other question about inheritance/implementation: is the following code legal regarding voidness?

abstract class A {
  List m1();
  List<void> m2();
  List<void> m3();
}
class B extends A {
  @override
  List<void> m1() => null;  // ok or not to replace dynamic by void?
  @override
  List m2() => null; // ok or not to replace void by dynamic?
  @override
  List<int> m3() => null; // ok or not to replace void by int?
}

[eernstg]

It would not be OK to override List<dynamic> as a return type by List<void>, but the converse is OK. Similarly, the return type List<void> can be overridden by List<int>.

In general, you may think of the subtype lattice as being refined such that void is the most general type, then dynamic, then Object, and then all the other types (using the subtype rules), and it is then allowed to override a return type with a "refined subtype" thereof, but not vice versa.

But there are several details that we need to settle. For instance, I'd prefer to erase top types to Object when they occur in a contravariant position: It is none of the client's business whether a given method takes an argument of type dynamic or Object, because that just means that "any object whatsoever" can be passed in both cases, and it is only the body of the actually invoked method which will treat dynamic myParameter and Object myParameter differently. Because of that, I'd prefer to avoid having a conflict when we have things like implements I, J where I contains foo(dynamic d) and J contains foo(Object o). Taking this to the natural extreme (that I prefer), it would also be none of the client's business whether a given argument has type void or Object (etc.), which would eliminate even more conflicts, but it would take away the ability of a type to promise that "the method that you're calling will ignore this actual argument". I think the caller should just not pass that argument, if it is so important to ensure that the callee doesn't get access to it. ;-)

[MichaelRFairhurst]

Re the two strong opinions:

Its probably better to disallow assigning a List<void> to a List<dynamic> in the lint, at least for now. It's easier to relax that than restrict that in the future in the linter itself. It also is a good case for what users would expect re 1 or 2.

If it gets implemented as a feature in Dart 3, and for some reason that's done via method 2 while the linter is on 1, then we can rename the lint rule to strict_voidness_propagation.

FWIW, void_checks should probably catch:

void x;
dynamic y() => x;

even though Dart allows it.