From ae6506bb260770342c28e0512cf06075698529fd Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Mon, 21 Sep 2020 17:54:43 +0200 Subject: [PATCH 01/10] First iteration on variance feature specification --- .../variance/feature-specification.md | 418 ++++++++++++++++++ 1 file changed, 418 insertions(+) create mode 100644 accepted/future-releases/variance/feature-specification.md diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md new file mode 100644 index 0000000000..3b440bc9c8 --- /dev/null +++ b/accepted/future-releases/variance/feature-specification.md @@ -0,0 +1,418 @@ +# Sound and Explicit Declaration-Site Variance + +Author: eernst@google.com + +Status: Draft + + +## CHANGELOG + +2020.09.22: +- Initial version uploaded. + + +## Summary + +This document specifies sound and explicit declaration-site +[variance](https://github.com/dart-lang/language/issues/214) +in Dart. + +Issues on topics related to this proposal can be found +[here](https://github.com/dart-lang/language/issues?utf8=%E2%9C%93&q=is%3Aissue+label%3Avariance+). + +Currently, a parameterized class type is covariant in every type parameter. +For example, `List` is a subtype of `List` because `int` is a +subtype of `num` (so the list type and its type argument "co-vary"). + +This is sound for all covariant occurrences of such type parameters in the +class body (for instance, the getter `first` of a list has return type `E`, +which is sound). It is also sound for contravariant occurrences when a +sufficiently exact receiver type is known (e.g., for a literal like +`[].add(4.2)`, or for a generative constructor +`SomeClass.foo(4.2)`). + +However, in general, every member access where a covariant type parameter +occurs in a non-covariant position may cause a dynamic type error, because +the actual type annotation at run time—say, the type of a parameter +of a method—is a subtype of the one which occurs in the static type. + +This feature introduces explicit variance modifiers for type parameters. It +includes compile-time restrictions on type declarations and on the use of +objects whose static type includes these modifiers, ensuring that the +above-mentioned dynamic type errors cannot occur. + +In order to ease the transition where types with explicit variance are +created and used, this proposal allows for certain subtype relationships +where dynamic type checks are still needed when using legacy types (where +type parameters are _implicitly_ covariant) to access an object, even in +the case where the object has a type with explicit variance. For example, +it is allowed to declare `class MyList implements List {...}`, +even though this means that `MyList` has members such as `add` that require +dynamic checks and may incur a dynamic type error. + + +## Syntax + +The grammar is adjusted as follows: + +``` + ::= // Modified rule. + ? + ('extends' )? + + ::= // New. + 'out' | 'inout' | 'in' +``` + + +## Static Analysis + +This feature allows type parameters to be declared with a _variance +modifier_ which is one of `out`, `inout`, or `in`. This implies that the +use of such a type parameter is restricted, in return for improved static +type safety. Moreover, the rules for other topics like subtyping and for +determining the variance of a subterm in a type are adjusted. + + +### Subtype Rules + +The interface compositionality rule in [subtyping.md] is updated +as follows: + +[subtyping.md]: https://github.com/dart-lang/language/blob/master/resources/type-system/subtyping.md + +- **Interface Compositionality**: `T0` is an interface type `C0` + and `T1` is `C0`. For `i` in `0..k`, let `vi` be the declared + variance of the `i`th type parameter of `C0`. Then, for each `i` in `0..k`, + one of the following holds: + - `Si <: Ui` and `vi` is absent or `out`. + - `Ui <: Si` and `vi` is `in`. + - `Si <: Ui` and `Ui <: Si`, and `vi` is `inout`. + + +### Variance Rules + +The rules for determining the variance of a position are updated as follows: + +We say that a type parameter of a generic class is _covariant_ if it has no +variance modifier or it has the modifier `out`; we say that it is +_contravariant_ if it has the modifier `in`; and we say that it is +_invariant_ if it has the modifier `inout`. + +The covariant occurrences of a type (schema) `T` in another type (schema) +`S` are: + + - if `S` and `T` are the same type, + - `S` is a covariant occurrence of `T`. + - if `S` is `Future` + - the covariant occurrences of `T` in `U` + - if `S` is `FutureOr` + - the covariant occurrencs of `T` in `U` + - if `S` is an interface type `C` + - the union of the covariant occurrences of `T` in `Ti` + for `i` in `0, ..., k` where the `i`th type parameter of `C` is + covariant, and + the contravariant occurrences of `T` in `Ti` + for `i` in `0, ..., k` where the `i`th type parameter of `C` is + contravariant. + - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, + the union of: + - the covariant occurrences of `T` in `U` + - the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` + the union of: + - the covariant occurrences of `T` in `U` + - the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + +The contravariant occurrences of a type `T` in another type `S` are: + - if `S` is `Future` + - the contravariant occurrences of `T` in `U` + - if `S` is `FutureOr` + - the contravariant occurrencs of `T` in `U` + - if `S` is an interface type `C` + - the union of the contravariant occurrences of `T` in `Ti` + for `i` in `0, ..., k` where the `i`th type parameter of `C` is + covariant, and + the covariant occurrences of `T` in `Ti` + for `i` in `0, ..., k` where the `i`th type parameter of `C` is + contravariant, + - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, + the union of: + - the contravariant occurrences of `T` in `U` + - the covariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` + the union of: + - the contravariant occurrences of `T` in `U` + - the covariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + +The invariant occurrences of a type `T` in another type `S` are: + - if `S` is `Future` + - the invariant occurrences of `T` in `U` + - if `S` is `FutureOr` + - the invariant occurrencs of `T` in `U` + - if `S` is an interface type `C` + - the union of the invariant occurrences of `T` in `Ti` + for `i` in `0, ..., k` where the `i`th type parameter of `C` is + covariant or contravariant, and + all occurrences of `T` in `Ti` + for `i` in `0, ..., k` where the `i`th type parameter of `C` is + invariant, + - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, + the union of: + - the invariant occurrences of `T` in `U` + - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + - all occurrences of `T` in `Bi` for `i` in `0, ..., k` + - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` + the union of: + - the invariant occurrences of `T` in `U` + - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + - all occurrences of `T` in `Bi` for `i` in `0, ..., k` + +It is a compile-time error if a type parameter declared by a static +extension has a variance modifier. + +*Variance is not relevant to static extensions, because there is no notion +of subsumption. Each usage will be a single call site, and the value of +every type argument associated with an extension method invocation is +statically known at the call site.* + +It is a compile-time error if a type parameter _X_ declared by a type alias +has a variance modifier, unless it is `inout`; or unless it is `out` and +the right hand side of the type alias has only covariant occurrences of +_X_; or unless it is `in` and the right hand side of the type alias has +only contravariant occurrences of _X_. + +*The variance for each type parameter of a type alias is restricted based +on the body of the type alias. Explicit variance modifiers may be used to +document how the type parameter is used on the right hand side, and they +may be used to impose more strict constraints than those implied by the +right hand side.* + +We say that a type parameter _X_ of a type alias _F_ _is +covariant/invariant/contravariant_ if it has the variance modifier +`out`/`inout`/`in`, respectively. We say that it is +_covariant/contravariant_ if it has no variance modifier, and it occurs +only covariantly/contravariantly, respectively, on the right hand side of +`=` in the type alias (*for an old-style type alias, rewrite it to the form +using `=` and then check*). Otherwise (*when _X_ has no modifier, but +occurs invariantly or both covariantly and contravariantly*), we say that +_X_ _is invariant_. + +Let _D_ be the declaration of a class or mixin, and let _X_ be a type +parameter declared by _D_. + +We say that _X_ _is covariant_ if it has no variance modifier or it has the +variance modifier `out`; that it _is invariant_ if it has the variance +modifier `inout`; and that it _is contravariant_ if it has the variance +modifier `in`. + +If _X_ has the variance modifier `out` then it is a compile-time error for +_X_ to occur in a non-covariant position in a member signature in the body +of _D_, except that it is not an error if it occurs in a covariant position +in the type annotation of a covariant formal parameter (*note that this is +a contravariant position in the member signature as a whole*). *For +instance, _X_ can not be the type of a method parameter (unless covariant), +and it can not be the bound of a type parameter of a generic method.* + +If _X_ has the variance modifier `in` then it is a compile-time error for +_X_ to occur in a non-contravariant position in a member signature in the +body of _D_, except that it is not an error if it occurs in a contravariant +position in the type of a covariant formal parameter. *For instance, _X_ +can not be the return type of a method or getter, and it can not be the +bound of a type parameter of a generic method.* + +*If _X_ has the variance modifier `inout` then there are no variance +related restrictions on the positions where it can occur.* + +*For superinterfaces we need slightly stronger rules than the ones that +apply for types in the body of a type declaration.* + +Let _D_ be a class or mixin declaration, let _S_ be a direct superinterface +of _D_, and let _X_ be a type parameter declared by _D_. + +It is a compile-time error if _X_ has no variance modifier and _X_ occurs +in an actual type argument in _S_ such that the corresponding type +parameter has a variance modifier. It is a compile-time error if _X_ has +the modifier `out`, and _X_ occurs in a non-covariant position in _S_. It +is a compile-time error if _X_ has the variance modifier `in`, and _X_ +occurs in a non-contravariant position in _S_. + +*A type parameter with variance modifier `inout` can occur in any position +in a superinterface, and other variance modifiers have constraints such +that if we consider type arguments _Args1_ and _Args2_ passed to _D_ such +that the former produces a subtype, then we also have _S1 <: S2_ where _S1_ +and _S2_ are the corresponding instantiations of _S_.* + +```dart +class A {} +class B implements + A {} + +// B <: B, and hence +// A <: +// A. +``` + +*But a type parameter without a variance modifier can not be used in an +actual type argument for a parameter with a variance modifier, not even +when that modifier is `out`. The reason for this is that it would allow a +subtype to introduce the potential for dynamic errors with a member which +is in the interface of the supertype and considered safe.* + +```dart +abstract class A { + Object foo(); +} + +class B extends A { + // The following declaration would be an error with `class B`, + // so we do not allow it in a subtype of `class A`. + void Function(X) foo() => (X x) {}; +} +``` + +*On the other hand, to ease migration, it _is_ allowed to create the +opposite relationship:* + +```dart +class A { + void foo(X x) {} +} + +class B extends A {} + +main() { + B myB = B(); + ... + myB.foo(42.1); +} +``` + +*In this situation, the invocation `myB.foo(42.1)` is subject to a dynamic +type check (and it will fail if `myB` is still a `B` when that +invocation takes place), but it is statically known at the call site that +`foo` has this property for any subtype of `A`, so we can deal with the +situation statically, e.g., via a lint.* + +*An upcast (like `(myB as A).foo()`) could be used to silence any +diagnostic messages, so a strict rule whereby a member access like +`myB.foo(42.1)` is a compile-time error may not be very helpful in +practice.* + +*Note that the class `B` _can_ be written in such a way that the potential +dynamic type error is eliminated:* + +```dart +class A { + void foo(X x) {} +} + +class B extends A { + void foo(Object? o) {...} +} +``` + +*In this case an invocation of `foo` on a `B` will never incur a dynamic +error due to the run-time type of its argument, which might be a useful +migration strategy in the case where a lot of call sites are flagged by a +lint, especially when `B.foo` is genuinely able to perform its task with +objects whose type is not `X`.* + +*However, in the more likely case where `foo` does require an argument of +type `X`, we do not wish to insist that developers declare an apparently +safe member signature like `void foo(Object?)`, and then throw an exception +in the body of `foo`. That would just eliminate some compile-time errors at +call sites which are actually justified.* + +*If such a method needs to be implemented, the modifier `covariant` must be +used, in order to avoid the compile-time error for member signatures +involving an `out` type parameter:* + +```dart +class A { + void foo(X x) {} +} + +class B extends A { // or `implements`. + void foo(covariant X x) {...} +} +``` + + +### Type Inference + +During downwards inference, a context type + + +## Dynamic Semantics + +The subtype relationship specified in the section on the static analysis +is applied during run-time type tests and type checks. + + +## Migration + +This proposal supports migration of code using dynamically checked +covariance to code where some explicit variance modifiers are used, thus +eliminating the potential for some dynamic type errors. There are two +scenarios. + +Let _legacy class_ denote a generic class that has one or more type +parameters with no variance modifiers. + +If a new class _A_ has no superinterface relationship with any legacy class +(directly or indirectly) then all non-dynamic member accesses to instances +of _A_ and its subtypes will be statically safe. + +*In other words, if the plan is to use explicit variance only with type +declarations that are not "connected to" unsoundly covariant type +parameters then there is no migration.* + +However, there is a need for migration support in the case where an +existing legacy class _B_ is modified such that an explicit variance +modifier is added to one or more of its type parameters. + +In particular, an existing subtype _C_ of _B_ must now add variance +modifiers in order to remain error free, and this may conflict with the +existing member signatures of _C_: + +```dart +// Before the update. +class B {} +class C implements B { + void f(X x) {} +} + +// After the update of `B`. +class B {} +class C implements B { // Error. + void f(X x) {} // If we just make it `C` then this is an error. +} + +// Adjusting `C` to eliminate the errors. +class B {} +class C implements B { + void f(covariant X x) {} +} +``` + +This approach can be used in a scenario where all parts of the program are +migrated to the new language level where explicit variance is supported. + +In the other scenario, some libraries will opt in using a suitable language +level, and others will not. + +If a library _L1_ is at a language level where explicit variance is not +supported (so it is 'opted out') then code in an 'opted in' library _L2_ is +seen from _L1_ as erased, in the sense that (1) the variance modifiers +`out` and `inout` are ignored, and (2) it is a compile-time error to pass a +type argument `T` to a type parameter with variance modifier `in`, unless +`T` is a top type; (3) any type argument `T` passed to an `in` type +parameter in opted-in code is seen in opted-out code as `Object?`. + +Conversely, declarations in _L1_ (opted out) is seen from _L2_ (opted in) +without changes. So class type parameters declared in _L1_ are considered +to be unsoundly covariant by both opted in and opted out code, and +similarly for type aliases used to declare function types. Types of +entities exported from _L1_ to _L2_ are seen as erased (which matters when +_L1_ imports entities from some other opted-in library). From d1bbf58819104221b6cc94ea1f36c92a9eca1c61 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Wed, 23 Sep 2020 14:56:55 +0200 Subject: [PATCH 02/10] WIP --- .../variance/feature-specification.md | 97 +++++++++---------- 1 file changed, 47 insertions(+), 50 deletions(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 3b440bc9c8..3c794347d7 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -14,7 +14,7 @@ Status: Draft ## Summary This document specifies sound and explicit declaration-site -[variance](https://github.com/dart-lang/language/issues/214) +[variance](https://github.com/dart-lang/language/issues/524) in Dart. Issues on topics related to this proposal can be found @@ -60,10 +60,13 @@ The grammar is adjusted as follows: ? ('extends' )? - ::= // New. + ::= // New rule. 'out' | 'inout' | 'in' ``` +`out` and `inout` are added to the set of built-in identifiers (* and `in` +is already a reserved word*). + ## Static Analysis @@ -168,51 +171,39 @@ The invariant occurrences of a type `T` in another type `S` are: - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - all occurrences of `T` in `Bi` for `i` in `0, ..., k` -It is a compile-time error if a type parameter declared by a static -extension has a variance modifier. +It is a compile-time error if a variance modifier is specified for a type +parameter declared by a static extension, a generic function type, a +generic function or method, or a type alias. *Variance is not relevant to static extensions, because there is no notion of subsumption. Each usage will be a single call site, and the value of every type argument associated with an extension method invocation is -statically known at the call site.* - -It is a compile-time error if a type parameter _X_ declared by a type alias -has a variance modifier, unless it is `inout`; or unless it is `out` and -the right hand side of the type alias has only covariant occurrences of -_X_; or unless it is `in` and the right hand side of the type alias has -only contravariant occurrences of _X_. - -*The variance for each type parameter of a type alias is restricted based -on the body of the type alias. Explicit variance modifiers may be used to -document how the type parameter is used on the right hand side, and they -may be used to impose more strict constraints than those implied by the -right hand side.* - -We say that a type parameter _X_ of a type alias _F_ _is -covariant/invariant/contravariant_ if it has the variance modifier -`out`/`inout`/`in`, respectively. We say that it is -_covariant/contravariant_ if it has no variance modifier, and it occurs -only covariantly/contravariantly, respectively, on the right hand side of -`=` in the type alias (*for an old-style type alias, rewrite it to the form -using `=` and then check*). Otherwise (*when _X_ has no modifier, but -occurs invariantly or both covariantly and contravariantly*), we say that -_X_ _is invariant_. +statically known at the call site. Similar reasons apply for functions and +function types. Finally, the variance of a type parameter declared by a +type alias is determined by the usage of that type parameter in the body of +the type alias.* + +We say that a type parameter _X_ of a type alias _F_ _is covariant_ if it +only occurs covariantly in the body of _F_; that it _is contravariant_ if +it occurs contravariantly in the body of _F_ and does not occur covariantly +or invariantly; that it _is invariant_ if it occurs invariantly in the body +of _F_ (*with no constraints on other occurrences*), or if it occurs both +covariantly and contravariantly. + +*In particular, an unused type parameter is considered covariant.* Let _D_ be the declaration of a class or mixin, and let _X_ be a type parameter declared by _D_. -We say that _X_ _is covariant_ if it has no variance modifier or it has the -variance modifier `out`; that it _is invariant_ if it has the variance -modifier `inout`; and that it _is contravariant_ if it has the variance -modifier `in`. - If _X_ has the variance modifier `out` then it is a compile-time error for _X_ to occur in a non-covariant position in a member signature in the body of _D_, except that it is not an error if it occurs in a covariant position -in the type annotation of a covariant formal parameter (*note that this is -a contravariant position in the member signature as a whole*). *For -instance, _X_ can not be the type of a method parameter (unless covariant), -and it can not be the bound of a type parameter of a generic method.* +in the type annotation of a covariant formal parameter (*this is a +contravariant position in the member signature as a whole*). + +*In particular, _X_ can not be the type of a method parameter (unless +covariant), and it can not be the bound of a type parameter of a generic +method.* If _X_ has the variance modifier `in` then it is a compile-time error for _X_ to occur in a non-contravariant position in a member signature in the @@ -255,18 +246,17 @@ class B implements *But a type parameter without a variance modifier can not be used in an actual type argument for a parameter with a variance modifier, not even -when that modifier is `out`. The reason for this is that it would allow a -subtype to introduce the potential for dynamic errors with a member which -is in the interface of the supertype and considered safe.* +when that modifier is `out`. The reason for this is that the sound treatment +of type parameters should not silently change to an unsound treatment +in a subtype.* ```dart abstract class A { Object foo(); } -class B extends A { - // The following declaration would be an error with `class B`, - // so we do not allow it in a subtype of `class A`. +class B extends A { // Error! + // If allowed, `X` could occur contravariantly, which is unsafe. void Function(X) foo() => (X x) {}; } ``` @@ -341,13 +331,21 @@ class B extends A { // or `implements`. ### Type Inference -During downwards inference, a context type +During type inference, downwards resolution produces constraints on type +variables with a variance modifier, rather than fixing them to a specific +value in a partial solution. Upwards resolution will then include those +constraints. + +Detailed rules will be specified in +[inference.md]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md ## Dynamic Semantics +This feature causes the dynamic semantics to change in only one way: The subtype relationship specified in the section on the static analysis -is applied during run-time type tests and type checks. +is different from the subtype relationship without this feature, and the +updated rules are used during run-time type tests and type checks. ## Migration @@ -360,11 +358,11 @@ scenarios. Let _legacy class_ denote a generic class that has one or more type parameters with no variance modifiers. -If a new class _A_ has no superinterface relationship with any legacy class -(directly or indirectly) then all non-dynamic member accesses to instances +If a new class _A_ has no direct or indirect superinterface which is a +legacy class then all non-dynamic member accesses to instances of _A_ and its subtypes will be statically safe. -*In other words, if the plan is to use explicit variance only with type +*In other words, when using sound, explicit variance only with type declarations that are not "connected to" unsoundly covariant type parameters then there is no migration.* @@ -410,9 +408,8 @@ type argument `T` to a type parameter with variance modifier `in`, unless `T` is a top type; (3) any type argument `T` passed to an `in` type parameter in opted-in code is seen in opted-out code as `Object?`. -Conversely, declarations in _L1_ (opted out) is seen from _L2_ (opted in) +Conversely, a declaration in _L1_ (opted out) is seen from _L2_ (opted in) without changes. So class type parameters declared in _L1_ are considered -to be unsoundly covariant by both opted in and opted out code, and -similarly for type aliases used to declare function types. Types of +to be unsoundly covariant by both opted in and opted out code. Types of entities exported from _L1_ to _L2_ are seen as erased (which matters when _L1_ imports entities from some other opted-in library). From a7f914d02f9ca921e7ea88de914398bae6870303 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Fri, 25 Sep 2020 15:12:07 +0200 Subject: [PATCH 03/10] Now allowing legacy/sound parameters to be mixed in subtype relationships --- .../variance/feature-specification.md | 139 ++++++++---------- 1 file changed, 64 insertions(+), 75 deletions(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 3c794347d7..3117308a28 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -213,26 +213,21 @@ can not be the return type of a method or getter, and it can not be the bound of a type parameter of a generic method.* *If _X_ has the variance modifier `inout` then there are no variance -related restrictions on the positions where it can occur.* - -*For superinterfaces we need slightly stronger rules than the ones that -apply for types in the body of a type declaration.* +related restrictions on the positions where it can occur in member +signatures.* Let _D_ be a class or mixin declaration, let _S_ be a direct superinterface -of _D_, and let _X_ be a type parameter declared by _D_. - -It is a compile-time error if _X_ has no variance modifier and _X_ occurs -in an actual type argument in _S_ such that the corresponding type -parameter has a variance modifier. It is a compile-time error if _X_ has -the modifier `out`, and _X_ occurs in a non-covariant position in _S_. It -is a compile-time error if _X_ has the variance modifier `in`, and _X_ -occurs in a non-contravariant position in _S_. - -*A type parameter with variance modifier `inout` can occur in any position -in a superinterface, and other variance modifiers have constraints such -that if we consider type arguments _Args1_ and _Args2_ passed to _D_ such -that the former produces a subtype, then we also have _S1 <: S2_ where _S1_ -and _S2_ are the corresponding instantiations of _S_.* +of _D_, and let _X_ be a type parameter declared by _D_. It is a +compile-time error if _X_ is covariant and _X_ occurs in a non-covariant +position in _S_. It is a compile-time error if _X_ is contravariant, and +_X_ occurs in a non-contravariant position in _S_. In these rules, type +inference of _S_ is assumed to have taken place already. + +*An invariant type parameter can occur in any position in a superinterface. +These constraints on allowed locations for type parameters ensure that if +we consider type arguments _Args1_ and _Args2_ passed to _D_ such that the +former produces a subtype, then we also have _S1 <: S2_ where _S1_ and _S2_ +are the corresponding instantiations of _S_.* ```dart class A {} @@ -244,90 +239,84 @@ class B implements // A. ``` -*But a type parameter without a variance modifier can not be used in an -actual type argument for a parameter with a variance modifier, not even -when that modifier is `out`. The reason for this is that the sound treatment -of type parameters should not silently change to an unsound treatment -in a subtype.* +*In a superinterface, a type parameter without a variance modifier can be +used in an actual type argument for a parameter with a variance modifier, +and vice versa. This creates a subtype hierarchy where sound and unsound +variance is mixed, which is helpful during a transitional period where +sound variance is introduced, or even as a more permanent choice if some +widely used classes (say, `List`) cannot be migrated to use sound +variance. However, it causes dynamic type checks to occur.* ```dart +// Superinterface uses sound variance, subtype uses legacy. + abstract class A { - Object foo(); + X get x; } -class B extends A { // Error! - // If allowed, `X` could occur contravariantly, which is unsafe. - void Function(X) foo() => (X x) {}; +class B implements A { + late X x; +} + +void main() { + B b = B(); + b.x = 3.7; // Dynamic error. } ``` -*On the other hand, to ease migration, it _is_ allowed to create the -opposite relationship:* +*Hence, no additional type safety is obtained when a class using legacy +variance has a supertype which uses sound variance.* ```dart -class A { - void foo(X x) {} +// Superinterface uses legacy covariance, subtype uses sound variance. + +abstract class C { + X x; + C(this.x); } -class B extends A {} +class D extends C { + D(): super((X x) {}); +} -main() { - B myB = B(); - ... - myB.foo(42.1); +void main() { + D d = D(); + d.x(24); // OK. + d.x = (int i) {}; // Dynamic error. } ``` -*In this situation, the invocation `myB.foo(42.1)` is subject to a dynamic -type check (and it will fail if `myB` is still a `B` when that -invocation takes place), but it is statically known at the call site that -`foo` has this property for any subtype of `A`, so we can deal with the -situation statically, e.g., via a lint.* +*The class `D` inherits a setter with argument type `void Function(X)` even +though it is an error to declare such a setter in `D`. It would be easy to +prohibit invocations of that setter on an instance of type `D<...>`, but the +invocation could then be performed using an upcast to `C`, so there is no +real protection against executing such methods on that instance.* -*An upcast (like `(myB as A).foo()`) could be used to silence any -diagnostic messages, so a strict rule whereby a member access like -`myB.foo(42.1)` is a compile-time error may not be very helpful in -practice.* - -*Note that the class `B` _can_ be written in such a way that the potential -dynamic type error is eliminated:* +*Note that the subclass _can_ be written in such a way that the potential +dynamic type error is eliminated, if it is possible to write a useful +implementation with a safe signature:* ```dart -class A { - void foo(X x) {} -} - -class B extends A { - void foo(Object? o) {...} +class SafeD extends C { + set x(void Function(Never) value) { + if (value is void Function(X)) super.x = value; + } } ``` -*In this case an invocation of `foo` on a `B` will never incur a dynamic -error due to the run-time type of its argument, which might be a useful -migration strategy in the case where a lot of call sites are flagged by a -lint, especially when `B.foo` is genuinely able to perform its task with -objects whose type is not `X`.* - -*However, in the more likely case where `foo` does require an argument of -type `X`, we do not wish to insist that developers declare an apparently -safe member signature like `void foo(Object?)`, and then throw an exception -in the body of `foo`. That would just eliminate some compile-time errors at -call sites which are actually justified.* - -*If such a method needs to be implemented, the modifier `covariant` must be -used, in order to avoid the compile-time error for member signatures -involving an `out` type parameter:* +*Otherwise, the modifier `covariant` can be used to avoid the compile-time +error for the member signature:* ```dart -class A { - void foo(X x) {} -} - -class B extends A { // or `implements`. - void foo(covariant X x) {...} +class ExplicitlyUnsafeD extends C { + set x(covariant void Function(X) value) => super.x = value; } ``` +*This makes it possible to declare method implementations with unsafe +signatures, even in the case where the relevant type parameters of the +enclosing class use sound variance.* + ### Type Inference From ecbbb5a0022868027e02bceefe9966591b1cf3b5 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Fri, 25 Sep 2020 15:33:22 +0200 Subject: [PATCH 04/10] Typo fix to markdown link --- accepted/future-releases/variance/feature-specification.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 3117308a28..62ba3a99c4 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -325,7 +325,8 @@ variables with a variance modifier, rather than fixing them to a specific value in a partial solution. Upwards resolution will then include those constraints. -Detailed rules will be specified in +Detailed rules will be specified in [inference.md]. + [inference.md]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md From fdc411634c58aeecc87745fe13b5a887b70c65b6 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Fri, 25 Sep 2020 16:00:34 +0200 Subject: [PATCH 05/10] Revised the migration section --- .../variance/feature-specification.md | 68 ++++--------------- 1 file changed, 14 insertions(+), 54 deletions(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 62ba3a99c4..30750bbf2c 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -341,65 +341,25 @@ updated rules are used during run-time type tests and type checks. ## Migration This proposal supports migration of code using dynamically checked -covariance to code where some explicit variance modifiers are used, thus -eliminating the potential for some dynamic type errors. There are two -scenarios. +covariance to code where some explicit variance modifiers are used, based +on language versions. -Let _legacy class_ denote a generic class that has one or more type -parameters with no variance modifiers. +We use the phrase _legacy library_ to denote a library which is written in +a language version that does not support sound variance. -If a new class _A_ has no direct or indirect superinterface which is a -legacy class then all non-dynamic member accesses to instances -of _A_ and its subtypes will be statically safe. -*In other words, when using sound, explicit variance only with type -declarations that are not "connected to" unsoundly covariant type -parameters then there is no migration.* +### Legacy libraries seen from a soundly variant library -However, there is a need for migration support in the case where an -existing legacy class _B_ is modified such that an explicit variance -modifier is added to one or more of its type parameters. +When a library _L_ with sound variance imports a legacy library _L2_, the +declarations imported from _L2_ are seen in _L_ as if they had been +declared in the language with sound variance. -In particular, an existing subtype _C_ of _B_ must now add variance -modifiers in order to remain error free, and this may conflict with the -existing member signatures of _C_: +*In other words, source code in _L2_ is seen as having variance modifiers +available, but it is simply not using them.* -```dart -// Before the update. -class B {} -class C implements B { - void f(X x) {} -} - -// After the update of `B`. -class B {} -class C implements B { // Error. - void f(X x) {} // If we just make it `C` then this is an error. -} -// Adjusting `C` to eliminate the errors. -class B {} -class C implements B { - void f(covariant X x) {} -} -``` +### Soundly variant libraries seen from a legacy library -This approach can be used in a scenario where all parts of the program are -migrated to the new language level where explicit variance is supported. - -In the other scenario, some libraries will opt in using a suitable language -level, and others will not. - -If a library _L1_ is at a language level where explicit variance is not -supported (so it is 'opted out') then code in an 'opted in' library _L2_ is -seen from _L1_ as erased, in the sense that (1) the variance modifiers -`out` and `inout` are ignored, and (2) it is a compile-time error to pass a -type argument `T` to a type parameter with variance modifier `in`, unless -`T` is a top type; (3) any type argument `T` passed to an `in` type -parameter in opted-in code is seen in opted-out code as `Object?`. - -Conversely, a declaration in _L1_ (opted out) is seen from _L2_ (opted in) -without changes. So class type parameters declared in _L1_ are considered -to be unsoundly covariant by both opted in and opted out code. Types of -entities exported from _L1_ to _L2_ are seen as erased (which matters when -_L1_ imports entities from some other opted-in library). +When a legacy library _L_ imports a library _L2_ with sound variance, the +declarations imported from _L2_ are _legacy erased_. This means that all +variance modifiers in type parameter declarations are removed. From 320ae879a5b2670705db6fcd77bbc22f167c98d9 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Fri, 25 Sep 2020 16:04:40 +0200 Subject: [PATCH 06/10] Added note about issue in need of clarification --- accepted/future-releases/variance/feature-specification.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 30750bbf2c..70995e20fb 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -363,3 +363,8 @@ available, but it is simply not using them.* When a legacy library _L_ imports a library _L2_ with sound variance, the declarations imported from _L2_ are _legacy erased_. This means that all variance modifiers in type parameter declarations are removed. + +*[TODO: This is a source of unsoundness; we probably cannot require that +every type argument passed to a contravariant type parameter in legacy code +must be a top type. Can we generate all the required dynamic checks to +maintain soundness?]* From e8bdb87fe984e1c39e62394807e69e7e6ff0166b Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Sat, 26 Sep 2020 08:53:17 +0200 Subject: [PATCH 07/10] Improved treatment of mixed programs --- .../future-releases/variance/feature-specification.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 70995e20fb..76bccb83aa 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -362,9 +362,9 @@ available, but it is simply not using them.* When a legacy library _L_ imports a library _L2_ with sound variance, the declarations imported from _L2_ are _legacy erased_. This means that all -variance modifiers in type parameter declarations are removed. +variance modifiers in type parameter declarations are ignored. -*[TODO: This is a source of unsoundness; we probably cannot require that -every type argument passed to a contravariant type parameter in legacy code -must be a top type. Can we generate all the required dynamic checks to -maintain soundness?]* +In a mixed program (where both legacy libraries and libraries with sound +variance exist), a dynamic type check is performed on the actual arguments +for each instance method parameter whose declared type contains a +contravariant type variable. From 4682754104ac60316334cdcbfce32624cb708029 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Wed, 30 Sep 2020 12:28:52 +0200 Subject: [PATCH 08/10] Clarified treatment of mixed programs --- .../future-releases/variance/feature-specification.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 76bccb83aa..47be1fc220 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -364,7 +364,10 @@ When a legacy library _L_ imports a library _L2_ with sound variance, the declarations imported from _L2_ are _legacy erased_. This means that all variance modifiers in type parameter declarations are ignored. -In a mixed program (where both legacy libraries and libraries with sound -variance exist), a dynamic type check is performed on the actual arguments -for each instance method parameter whose declared type contains a -contravariant type variable. +*To maintain a sound heap in a mixed program execution (that is, when both +legacy libraries and libraries with sound variance exist), it is then +necessary to perform some type checks at run time. In particular, a +dynamic type check is performed on method calls: The actual argument for +each instance method parameter whose declared type contains a contravariant +type variable. Moreover, a caller-side check is performed on each +expression whose static type contains a contravariant type variable.* From b944a7b8dc1fde648cb5f6e51f85a572f4301c32 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Wed, 30 Sep 2020 12:34:54 +0200 Subject: [PATCH 09/10] Typo --- accepted/future-releases/variance/feature-specification.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 47be1fc220..5037a3e032 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -367,7 +367,7 @@ variance modifiers in type parameter declarations are ignored. *To maintain a sound heap in a mixed program execution (that is, when both legacy libraries and libraries with sound variance exist), it is then necessary to perform some type checks at run time. In particular, a -dynamic type check is performed on method calls: The actual argument for +dynamic type check is performed on method calls, on the actual argument for each instance method parameter whose declared type contains a contravariant type variable. Moreover, a caller-side check is performed on each expression whose static type contains a contravariant type variable.* From 5b1e3c6b5304a1339a072a69e9537a7db8767d72 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Fri, 28 Jan 2022 18:00:33 +0100 Subject: [PATCH 10/10] Review response --- .../variance/feature-specification.md | 309 ++++++++++++------ 1 file changed, 209 insertions(+), 100 deletions(-) diff --git a/accepted/future-releases/variance/feature-specification.md b/accepted/future-releases/variance/feature-specification.md index 5037a3e032..d24f443bf4 100644 --- a/accepted/future-releases/variance/feature-specification.md +++ b/accepted/future-releases/variance/feature-specification.md @@ -95,81 +95,74 @@ as follows: ### Variance Rules -The rules for determining the variance of a position are updated as follows: - -We say that a type parameter of a generic class is _covariant_ if it has no -variance modifier or it has the modifier `out`; we say that it is -_contravariant_ if it has the modifier `in`; and we say that it is -_invariant_ if it has the modifier `inout`. - -The covariant occurrences of a type (schema) `T` in another type (schema) -`S` are: - - - if `S` and `T` are the same type, - - `S` is a covariant occurrence of `T`. - - if `S` is `Future` - - the covariant occurrences of `T` in `U` - - if `S` is `FutureOr` - - the covariant occurrencs of `T` in `U` - - if `S` is an interface type `C` - - the union of the covariant occurrences of `T` in `Ti` - for `i` in `0, ..., k` where the `i`th type parameter of `C` is - covariant, and - the contravariant occurrences of `T` in `Ti` - for `i` in `0, ..., k` where the `i`th type parameter of `C` is - contravariant. - - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, - the union of: - - the covariant occurrences of `T` in `U` - - the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` - the union of: - - the covariant occurrences of `T` in `U` - - the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - -The contravariant occurrences of a type `T` in another type `S` are: - - if `S` is `Future` - - the contravariant occurrences of `T` in `U` - - if `S` is `FutureOr` - - the contravariant occurrencs of `T` in `U` - - if `S` is an interface type `C` - - the union of the contravariant occurrences of `T` in `Ti` - for `i` in `0, ..., k` where the `i`th type parameter of `C` is - covariant, and - the covariant occurrences of `T` in `Ti` - for `i` in `0, ..., k` where the `i`th type parameter of `C` is - contravariant, - - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, - the union of: - - the contravariant occurrences of `T` in `U` - - the covariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` - the union of: - - the contravariant occurrences of `T` in `U` - - the covariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - -The invariant occurrences of a type `T` in another type `S` are: - - if `S` is `Future` - - the invariant occurrences of `T` in `U` - - if `S` is `FutureOr` - - the invariant occurrencs of `T` in `U` - - if `S` is an interface type `C` - - the union of the invariant occurrences of `T` in `Ti` - for `i` in `0, ..., k` where the `i`th type parameter of `C` is - covariant or contravariant, and - all occurrences of `T` in `Ti` - for `i` in `0, ..., k` where the `i`th type parameter of `C` is - invariant, - - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, - the union of: - - the invariant occurrences of `T` in `U` - - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - - all occurrences of `T` in `Bi` for `i` in `0, ..., k` - - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` - the union of: - - the invariant occurrences of `T` in `U` - - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - - all occurrences of `T` in `Bi` for `i` in `0, ..., k` +We say that a type parameter of a generic class, mixin, or enum is +_covariant_ if it has no variance modifier or it has the modifier `out`; we +say that it is _contravariant_ if it has the modifier `in`; and we say that +it is _invariant_ if it has the modifier `inout`. + +The language specification defines what it means for a type to occur +covariantly, contravariantly, or invariantly in another type. No +changes are needed in these definitions. + +However, these definitions rely on the notion that each _position_ in +a type has a specific variance, and those definitions are replaced by +the ones that are given in this section. + +*The position of a type in another type is a property of each occurrence of +the former. For example, the first occurrence of `X` in the type `X +Function(X)` is in a covariant position, and the second occurrence is in a +contravariant position.* + +We say that a type `S` occurs in a covariant position in a type `T` if at +least one of the following conditions is true: + - `T` is `S`. + - `T` is an interface type `C`, `j` is in `1..k`, and: + - the `j`th type parameter of `C` is covariant + and `S` occurs in a covariant position in `Tj`, or + - the `j`th type parameter of `C` is contravariant + and `S` occurs in a contravariant position in `Tj`. + - `T` is `FutureOr` and `S` occurs in a covariant position in `U`. + - `T` is `U Function(T1 x1, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])` and: + - `S` occurs in a covariant position in `U`, or + - `S` occurs in a contravariant position in `Tj` for some `j` in `1..m`. + - `T` is `U Function(T1 x1, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` and: + - `S` occurs in a covariant position in `U`, or + - `S` occurs in a contravariant position in `Tj` for some `j` in `1..m`. + - `T` is `U?` and `S` occurs in a covariant position in `U`. + - `T` is `X & U` and `S` occurs in a covariant position in `U`. + +`S` occurs in a contravariant position in a type `T` if at least one of the +following conditions is true: + - `T` is an interface type `C`, `j` is in `1..k`, and: + - the `j`th type parameter of `C` is covariant + and `S` occurs in a contravariant position in `Tj`, or + - the `j`th type parameter of `C` is contravariant + and `S` occurs in a covariant position in `Tj`. + - `T` is `FutureOr` and `S` occurs in a contravariant position in `U`. + - `T` is `U Function(T1 x1, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])` and: + - `S` occurs in a contravariant position in `U`, or + - `S` occurs in a covariant position in `Tj` for some `j` in `1..m`. + - `T` is `U Function(T1 x1, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` and: + - `S` occurs in a contravariant position in `U`, or + - `S` occurs in a covariant position in `Tj` for some `j` in `1..m`. + - `T` is `U?` and `S` occurs in a contravariant position in `U`. + - `T` is `X & U` and `S` occurs in a contravariant position in `U`. + +`S` occurs in an invariant position in a type `T` if at least one of the +following conditions is true: + - `T` is an interface type `C` and + `S` occurs in an invariant position in `Tj` for some `j` in `1..k`. + - `T` is `FutureOr` and `S` occurs in an invariant position in `U`. + - `T` is `U Function(T1 x1, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])` and: + - `S` occurs in a invariant position in `U`, or + - `S` occurs in a invariant position in `Tj` for some `j` in `1..m`, or + - `S` occurs in `Bj` (*at any position*) for some `j` in `1..k`. + - `T` is `U Function(T1 x1, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` and: + - `S` occurs in a invariant position in `U`, or + - `S` occurs in a invariant position in `Tj` for some `j` in `1..m`, or + - `S` occurs in `Bj` (*at any position*) for some `j` in `1..k`. + - `T` is `U?` and `S` occurs in an invariant position in `U`. + - `T` is `X & U` and `S` occurs in an invariant position in `U`. It is a compile-time error if a variance modifier is specified for a type parameter declared by a static extension, a generic function type, a @@ -183,14 +176,17 @@ function types. Finally, the variance of a type parameter declared by a type alias is determined by the usage of that type parameter in the body of the type alias.* -We say that a type parameter _X_ of a type alias _F_ _is covariant_ if it -only occurs covariantly in the body of _F_; that it _is contravariant_ if -it occurs contravariantly in the body of _F_ and does not occur covariantly -or invariantly; that it _is invariant_ if it occurs invariantly in the body -of _F_ (*with no constraints on other occurrences*), or if it occurs both -covariantly and contravariantly. +*Variance _can_ be used with a generic enum declaration.* -*In particular, an unused type parameter is considered covariant.* +The definition of the variance of a type parameter of a type alias remains +unchanged. + +*In particular, a type parameter _X_ of a type alias _F_ is covariant if it +occurs in covariant positions in the body of _F_, but not in contravariant +nor invariant positions; it is contravariant if it occurs in contravariant +positions in the body of _F_, but in covariant or invariant positions; and +it _is invariant_ if it occurs in invariant positions and/or it occurs +in covariant as well as in contravariant positions.* Let _D_ be the declaration of a class or mixin, and let _X_ be a type parameter declared by _D_. @@ -198,19 +194,19 @@ parameter declared by _D_. If _X_ has the variance modifier `out` then it is a compile-time error for _X_ to occur in a non-covariant position in a member signature in the body of _D_, except that it is not an error if it occurs in a covariant position -in the type annotation of a covariant formal parameter (*this is a +in the type annotation of a formal parameter which is covariant (*this is a contravariant position in the member signature as a whole*). *In particular, _X_ can not be the type of a method parameter (unless -covariant), and it can not be the bound of a type parameter of a generic -method.* +it is covariant). It can never be the bound of a type parameter of a +generic method.* If _X_ has the variance modifier `in` then it is a compile-time error for _X_ to occur in a non-contravariant position in a member signature in the body of _D_, except that it is not an error if it occurs in a contravariant -position in the type of a covariant formal parameter. *For instance, _X_ -can not be the return type of a method or getter, and it can not be the -bound of a type parameter of a generic method.* +position in the type of a formal parameter which is covariant. *For +instance, _X_ can never be the return type of a method or getter, and it can +never be the bound of a type parameter of a generic method.* *If _X_ has the variance modifier `inout` then there are no variance related restrictions on the positions where it can occur in member @@ -218,7 +214,7 @@ signatures.* Let _D_ be a class or mixin declaration, let _S_ be a direct superinterface of _D_, and let _X_ be a type parameter declared by _D_. It is a -compile-time error if _X_ is covariant and _X_ occurs in a non-covariant +compile-time error if _X_ is covariant, and _X_ occurs in a non-covariant position in _S_. It is a compile-time error if _X_ is contravariant, and _X_ occurs in a non-contravariant position in _S_. In these rules, type inference of _S_ is assumed to have taken place already. @@ -301,6 +297,7 @@ class SafeD extends C { set x(void Function(Never) value) { if (value is void Function(X)) super.x = value; } + SafeD(): super((X x) {}); } ``` @@ -309,7 +306,8 @@ error for the member signature:* ```dart class ExplicitlyUnsafeD extends C { - set x(covariant void Function(X) value) => super.x = value; + set x(covariant void Function(X) value); + ExplicitlyUnsafeD(): super((X x) {}); } ``` @@ -338,6 +336,122 @@ is different from the subtype relationship without this feature, and the updated rules are used during run-time type tests and type checks. +### Dynamic Type Checks by Example + +This section is not normative, it explores some consequences of the design +specified in the previous sections. Consider the following declarations: + +```dart +class L { + X m(X x) {} +} + +class Co extends L {} +class Contra extends L {} // Error. +class In extends L {} +``` + +`Co` is allowed, but the implementation of `m` in an instance of `Co` must +perform a dynamic type check on the actual argument, because we could have +a `Co` with static type `Co`. It would be an error to declare `m` +in `Co` with the same signature as in `L`; it is allowed when the method is +inherited from a class where the declaration is not an error, but this also +means that there must be a dynamic type check, just like there must be a +dynamic type check in the implementation of `m` in an instance of `L`. + +`Contra` is an error, because a contravariant type parameter occurs in a +non-contravariant position in a superinterface. + +`In` is allowed, and the implementation of `m` in an instance of `In` must +again perform the dynamic type check. However, this is _also_ true if the +implementation of `m` is copied to `In` (which is not an error) and the +declaration in `L` is made abstract. + +The situation is similar if we use `implements` rather than `extends`, +and write an implementation of `m` in the subtype, adding `covariant` as +needed (including: `Contra` is still an error, no matter how it declares +`m`). + +```dart +class Co2 { + final X x; + Co2(this.x); + X m2() => x; +} + +class Contra2 { + void m2(X x) {} +} + +class In2 { + X m2(X x) => x; +} + +class Lco2 extends Co2 { + Lco2(super.x); +} + +class Lcontra2 extends Contra2 { // Error. + ... // Doesn't matter, it's an error anyway. +} + +class Lin2 extends In2 {} +``` + +`Lco2.m2` does not need any dynamic type checks, it can just be inherited +as is from `Co2`. + +`Lcontra2` is again an error, no matter what's in the body. + +`Lin2` cannot directly inherit `In2.m2`, it needs to have an implicitly +induced stub method which will check the type of the actual argument `x` +and then `return super.m2(x)`. This is necessary because an instance of +`Lin2` could be the value of an expression whose static type is +`Lin2`, and we could then pass `1.5` without any compile-time errors. + +Note also that it is _not_ safe to assign an expression of type `Lin2` +to a variable of type `In2`, because the assigned object could have +dynamic type `Lin2`, which is not a subtype of `In2`. In other +words, with this type of hierarchy, some static superinterfaces may not be +dynamic superinterfaces (which is new). + +If we use `implements` rather than `extends`, we get the following: + +```dart +abstract class Co3 { + X m3(); +} + +class Contra3 { + void m3(X x); +} + +class In3 { + X m3(X x); +} + +class Lco3 implements Co3 { + X x; + Lco3(this.x); + X m3() => x; +} + +class Lcontra3 implements Contra3 { // Error. + ... +} + +class Lin3 extends In3 { + X m3(X x) => x; +} +``` + +`Lco3` needs the usual dynamic type check on the setter `x=`, but no checks +on `m3`. `Lcontra3` is an error. `Lin3.m3` needs a dynamic argument check +because it can be a `Lin3` with static type `Lin3`. Again, +assignment of an expression of type `Lin3` to a variable of type +`In3` requires a dynamic type check. + + ## Migration This proposal supports migration of code using dynamically checked @@ -361,13 +475,8 @@ available, but it is simply not using them.* ### Soundly variant libraries seen from a legacy library When a legacy library _L_ imports a library _L2_ with sound variance, the -declarations imported from _L2_ are _legacy erased_. This means that all -variance modifiers in type parameter declarations are ignored. - -*To maintain a sound heap in a mixed program execution (that is, when both -legacy libraries and libraries with sound variance exist), it is then -necessary to perform some type checks at run time. In particular, a -dynamic type check is performed on method calls, on the actual argument for -each instance method parameter whose declared type contains a contravariant -type variable. Moreover, a caller-side check is performed on each -expression whose static type contains a contravariant type variable.* +subtype relationships will take declaration-site variance into account. + +*In other words, a library that uses an older version of the language +can use declaration-site variance, it just cannot declare types with +declaration-site variance.*