dart-lang / dart-lang/language
Should use-site variance be allowed almost everywhere with legacy type variables?
- Dominant language
- TeX
- Stars
- 2.9k
- Forks
- 239
- Avg merge
- 2d 18h
- Merged PRs (30d)
- 14
Description
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:
```dart
class C {
X x;
void foo(List xs) { // (1). Error or not?
xs.add(x); // Statically safe.
}
}
main() {
// When the receiver has `exactly`, it just works.
C c = C();
c.foo([]); // Compile-time error, List not subtype of List.
c.foo([]); // OK, statically and dynamically.
List xs = [];
c.foo(xs); // Error (downcast); with `xs as List`: fails at run time.
// When the receiver has just the legacy type, the `foo` signature is misleading.
C c2 = C(); // Allowed, type parameter `X` is legacy-covariant.
c2.foo([]); // Compile-time error, even though `[]` has exactly the required type.
c2.foo([]); // OK statically, but fails at run time.
List xs2 = [];
c2.foo(xs2); // Error (downcast); with `xs as List`: 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 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 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 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([])` even though the actual parameter type of `c2.foo` is `List` and `[]` has exactly that type; and we do _not_ get an error at compile-time for `c2.foo([])`, even though the type of `[]` 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 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([])`) as well as the one that fails (`c2.foo([])`), 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 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?
Contributor guide
Research direction
Read the variance mechanism discussion in #524 and the upcoming variance proposal first. Use the C examples and the two c.foo call-site cases to compare the proposed alternatives. Done means deciding whether legacy-covariant variables may use exactly in these positions and documenting the resulting rule and behavior.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- dart
- Domain
- compilers
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 25/100