Make it an error to use a type variable non-covariantly in a superinterface #39
Description
This is a proposal for how to deal with the issue described in #38.
Related feature specification.
As described in #38, the ability to use a type variable contravariantly in a superinterface creates an "anti-parallel" subtype relationship for a given generic class and a direct superinterface thereof (and, of course, the same thing can happen indirectly in many ways). This creates various complications for the static analysis and the enforcement of the heap invariant ("soundness"). It easily generalizes to the invariant case, hence we'll target "non-covariant" occurrences here.
Discussion
I believe that it would be beneficial for Dart to introduce a new compile-time error, and I suspect that it would break a very small amount of code. Here is the proposed error:
Let C be a generic class that declares a formal type parameter X, and assume that T is a direct superinterface of C. It is a compile-time error if X occurs contravariantly or invariantly in T.
For example:
class A<X> {}
class B<X> extends A<void Function(X)> {} // Compile-time error.
class C<X> extends A<void Function<Y extends X>(Y)> {} // Compile-time error.With that error in place, it is no longer possible to create the "anti-parallel" subtyping relationship that we used in #38 to violate the heap invariant.
Alternative Proposal
One other approach could be used: We could specify that an upcast from B<T> for some T to a parameterized type based on A must yield A<void Function(Null)> rather than A<void Function(T)>. In general, we would perform such an upcast by replacing the relevant type variable by Null rather than replacing it by the actual type argument T. This would be sound, but it might also give rise to some confusion. I believe that a compile-time error is the better choice for superinterfaces.
A Useful Property
If we introduce the above-mentioned error then we will have the following property: "A well-bounded type will have well-bounded superinterfaces".
That is a useful property because it enables the use of super-bounded types along with the ordinary subtype relationships, without forcing all types thus obtained to need a well-boundedness check.
To see this, we state without evidence that the current checks on regular-bounded types will ensure that superinterfaces are regular-bounded. That is, the bounds on the type parameters in a generic class declaration must be so strong that they enforce the bounds in each superinterface for the given actual type arguments.
Lemma 1: If C is a generic class with type parameters X1..Xk, C<S1..Sk> is a regular-bounded parameterized type, and D<U1..Up> is a superinterface of C (where Ui may contain type variables from X1..Xk), then [S1/X1..Sk/Xk]D<U1..Up> is regular-bounded.
The non-trivial step is the following:
Lemma 2: If C is a generic class with type parameters X1..Xk, C<S1..Sk> is a super-bounded parameterized type, and D<U1..Up> is a superinterface of C (where Ui may contain type variables from X1..Xk), then [S1/X1..Sk/Xk]D<U1..Up> is well-bounded.
With that result, we can easily see the following:
Theorem: If C is a generic class with type parameters X1..Xk, C<S1..Sk> is a well-bounded parameterized type, and D<U1..Up> is a superinterface of C (where Ui may contain type variables from X1..Xk), then [S1/X1..Sk/Xk]D<U1..Up> is well-bounded.
That's because C<S1..Sk> is either regular-bounded or super-bounded. So let's assume Lemma 1 and sketch a proof of Lemma 2:
Proof sketch: Let C be a generic class with type parameters X1..Xk, let C<S1..Sk> be a super-bounded parameterized type, and let D<U1..Up> be a superinterface of C (where Ui may contain type variables from X1..Xk).
Since C<S1..Sk> is super-bounded, we can let C<V1..Vk> be the parameterized type which is obtained from C<S1..Sk> by replacing each covariantly occurring top type by Null, and each contravariantly occurring Null by dynamic. By definition of super-bounded types, C<V1..Vk> is regular-bounded. That is:
Vj <: [V1/X1..Vk/Xk]Bj, for all j in 1..k
where Bj is the declared bound of Xj. Let D<U1..Up> be one of the superinterfaces of C. By Lemma 1, we know that [V1/X1..Vk/Xk]D<U1..Up> is regular-bounded, that is,
[V1/X1..Vk/Xk]Uj <: [V1/X1..Vk/Xk][U1/Y1..Up/Yp]BBj, for all j in 1..p
where Y1..Yp are the formal type parameters of D and BB1..BBp are the corresponding bounds. It must be true that none of the Yj occur in any of U1..Up nor in any of V1..Vk, but we assume that this has been achieved by a suitable choice of names.
What we need to show is that [S1/X1..Sk/Xk]D<U1..Up> is well-bounded. If it is regular-bounded we are done. Otherwise we must show that it is super-bounded, that is, the substitution of bottom/top types by their opposites will produce a regular-bounded type:
Let Wj, j \in 1..p, be the result of replacing covariantly occurring top types by Null and contravariantly occurring Null by dynamic in [S1/X1..Sk/Xk]Uj, then we need to show that D<W1..Wp> is regular-bounded:
Wj <: [W1/Y1..Wp/Yp]BBj, for all j in 1..p
If X1..Xk all occur covariantly in Uj then these replacements in Wj will occur with the same variance in Uj as in S1..Sk and hence
Wj == [V1/X1..Vk/Xk]Uj, for all j in 1..p
which means that we just need to show:
[V1/X1..Vk/Xk]Uj <: [V1/X1..Vk/Xk][U1/Y1..Up/Yp]BBj, for all j in 1..p
which is exactly what we already have. QED.
Metadata
Metadata
Assignees
Type
Projects
Status