Compute a sound type for "contravariant members"

In response to #296, this issue is a proposal for how to compute a _sound type for devariant members_ of a class type.

For the motivation and some examples, please consult #296.

This proposal simply specifies how to compute a sound type for a class member of the kind that we have called a "contravariant member" in earlier discussions about this topic. At the same time, this proposal introduces the new name _devariant member_ for such members, in order to emphasize that contravariance as well as invariance requires a novel approach when it comes to covariant type parameters, and in case we add support for contravariant type parameters we will need to use a similar approach for covariant and invariant occurrences. In this proposal, it is assumed that a type parameter can be contravariant, because that's a tiny generalization and it might be useful enough to happen.

Note that this proposal specifies how to compute the type of a member as a whole, e.g., both the return type and the type of each formal parameter for a method, but it may be relevant to use just part of such a type. For instance, we may choose to use just the return type of a method obtained as specified here, and then use parameter types obtained differently.

We focus on the approach where the complete signature of each member is specified, and it is then a trivial matter to extract parts of the type as needed, or to compute just the parts which are needed.

For reasons why we might want to do this, please check the discussion at the end.

## Proposal

Let _C_ be a generic class, let _X_ be a type parameter of _C_ which is not declared `invariant` (cf. #214), and let _m_ be a member of the interface of _C_. Let _F_ be the function type of _m_ if _m_ is not a getter, and let _F_ be the return type of _m_ if _m_ is a getter.

*This covers instance variables as well, because an instance variable `T x` implicitly induces a getter and, if not `final`, a setter. Note that nothing is said about constructors, because they are not subject to variance; and nothing is said about static members, because they cannot have type parameters of their enclosing class in their signature.*

We say that _m_ is a _devariant member_ of _C_ with respect to _X_ if and only if

- _X_ is covariant, and _X_ occurs in _F_ in a contravariant position and/or in an invariant position, or
- _X_ is contravariant, and _X_ occurs in _F_ in a covariant position and/or in an invariant position.

Let _m_ be a member of a class _C_. We say that _m_ is a _devariant member_ of _C_ if there exists a type parameter _X_ declared by _C_, such that _m_ is devariant with respect to _X_.

Let _C_ be a generic class and _m_ a member of the interface of _C_. Let _T_ of the form _C<T₁ .. T_s>_ be a parameterized type with no compile-time errors. (*In particular, _C_ has _s_ type parameters and the actual type arguments do not violate the declared bounds.*) Assume that the type variables declared by _C_ are _X₁ .. X_s_.

*The notation _[T₁/X₁ .. T_s/X_s]F_ denotes a non-capturing substitution operation whereby all occurrences of _X_j_ in _F_ are replaced by _T_j_, for all _j_ in 1 .. _s_. We introduce a new substitution operator here, in order to handle devariant members.*

We define the _variance aware substitution_ operator _[T₁,S₁/X₁ .. T_s,S_s/X_s]_var_ as follows: It is non-capturing, just like the regular substitution operator, and it replaces each covariant occurrence of _X_j_ by _T_j_ and each contravariant occurrence of _X_j_ by _S_j_.

If there exists a type parameter _X_j_ which occurs invariantly in _F_, then replace _F_ by the least upper bound of _[Never/X_j]F_ and _[B_j/X_j]F_, where _B_j_ is the declared bound of _X_j_. (*This is a type which is a supertype of all types obtained by choosing a value for _X_j_, and it does not contain _X_j_ itself.*) Repeat this step until no type parameter occurs invariantly in _F_.

For _j_ in 1 .. _s_, if _X_j_ is covariant then let _U_j_ be _T_j_ and let _V_j_ be `Null`; if _X_j_ is contravariant then let _U_j_ be `Object` and let _V_j_ be _T_j_; and if _X_j_ is neither covariant nor contravariant (*in particular, if _X_j_ is declared `invariant`*) then let both _U_j_ and _V_j_ be _T_j_. Then:

- if _m_ is a non-getter member of _C_ then the _function type of m for a receiver of type T_ is _[U₁,V₁/X₁ .. U_s,V_s/X_s]_var F_, where _F_ is the function type of _m_.

- if _m_ is a getter which is a member of _C_ with return type _F_, then the _return type of m for a receiver of type T_ is _[U₁,V₁/X₁ .. U_s,V_s/X_s]_var F_.

In the case where _T_ is of the form _C<invariant? T₁ .. invariant? T_s>_ where one or more of the actual type arguments have been marked as `invariant` (cf. #229), the corresponding member types are computed in the same manner, except that each type parameter which corresponds to an actual type argument marked `invariant` is considered to have no variance (that is, it is not covariant and it is not contravariant).

## Discussion

It is easy to verify that this produces the same type for any non-devariant member as the existing approach (which is directly substituting the actual type arguments for the formal type parameters), that the resulting typing for a devariant member is a supertype of the type which is achieved with the current approach, and also that this is a sound approximation.

The chosen approach for type parameters that occur in an invariant position in the member signature makes the choice to weaken the type to a supertype that does not depend on the type variable. It would also be possible to weaken all function types to `Function` and all non-function type to `Object`, which might be preferable if we consider the least upper bound operation to be a little bit too confusing. This would immediately address the concern that the elimination of type parameters that occur invariantly may not be confluent (so different orderings could produce different results).

We will need to introduce some exceptions, because we are already dealing with the devariance problem in other ways:

For methods that have parameters which are covariant-by-class (e.g., `List.add`), we will probably still check actual arguments according to the type obtained by simple substitution, and rely on a dynamic check of the type of the actual argument in the body of the method. Similarly, we will probably continue to give the tear-off of such a method the same type as today (by simple substitution), and let the thus obtained function object have a reified type which is `Object` for the parameters which are covariant-by-class.

The point is that general function type subtyping and method overriding are different: With a first class function of type `S Function(T)` it is probably common to use a "dummy" function of type `S Function(dynamic)`, or at least a function of type `S Function(T1)` where `T1` is some supertype of `T`, because such a function is already available, and its body "does not need to know everything" about its argument. In contrast, it is probably quite rarely the case that a method accepting an argument of type `T` is overridden by a method accepting an argument of type `dynamic`, or even any supertype `T1` of `T`, because it is not so common to have an overriding method that does not need to know as much about its arguments as the overridden methods did. This means that the statically known argument type for a method _is_ relevant to the call site, even though it is statically known that it is not sound, and even though it is technically possible that the type which is actually required by the callee is some supertype-of-a-subtype (that is, it could be anything whatsoever).

However, the situation where we invoke an instance method that has one or more parameters which are covariant-by-class may be less common in the future, because we would be able to use `invariant` modifiers on type parameter declarations and/or type arguments (#214, #229), and thus eliminate the variance on many more type arguments than what's currently possible. A tear-off of such a receiver would then not have to erase any parameter types to `Object`, because the precise type can be expressed locally and usages can be type checked statically. This would be particularly helpful for method signatures involving invariant occurrences of type variables.

However, for such tear-offs it should be noted that it would be more consistent and it would be sound (that is, there would not be a need for dynamic checks on parameters that are covariant by class in the body of a tear-off) if we used the proposal in this issue to compute the static type of such a tear-off, and we use the actual value of the given type variables to compute the reified type of the function object, and then we use static typing plus an additional entry point ("callAndCheckParameters") of the function object for every invocation which is not statically safe. So it would be nice, if we can tolerate the breakage.

It should also be noted that there is a usability issue connected with these two approaches to typing: Consider the following situation:

```dart
main() {
List xs;
...
xs.add(e); // Static type of `e` is `T`.
}
```

With the current typing, it is a compile-time error if `T` is not assignable to `num`, which means that downcasts to `num` are accepted silently, and so are "upcasts to `num`". The latter is misleading, of course, because the actual dynamic check will be that `e is S` where `S` is some subtype of `num`, so there is no reason to expect this to be a downcast, it's just a cast (for instance, if `S` is `int` and the value of `e` has type `double` then the cast will fail, and it's not a downcast). With `--no-implicit-casts` we will accept arguments whose static type is a subtype of `num` and reject supertypes.

Nevertheless, rejecting `e` with a static type which is unrelated to `num` is _more informative_ than just noting that the statically safe approximation to the actual argument type is `Null`, and anything else than that needs a dynamic check.

This is because we know that the actual type argument `S` for `xs` (which is also the argument type for `add`) is a subtype of `num`, which means that it is known that an argument of type `String` _cannot possibly_ succeed (unless the value is `null`), and for other types it is arguably less likely that a cast from an arbitrary type to another arbitrary type will succeed than it is that a cast between two subtypes of the statically known upper bound of `S` will succeed.

Should we then, somehow, include the type obtained by simple substitution in the static analysis of devariant members? If we consider a receiver `c` with static type `C` then the value returned by its `f` getter will be a function of type `void Function(T1)` for some type `T1` which is a supertype of some type `T2` which is the actual type argument at `C` of the dynamic type of `c`. This is already flexible enough to make it difficult to justify any other typing than one that says "`T1` is a supertype of `Null`". So when it comes to returned results (from getters and methods) it is not likely to be useful to try to use the results from direct substitution (that is, today's typing). It is only the treatment of parameters of instance members which is likely to be more useful when we preserve the results from direct substitution.

This seems to indicate that we could use the types computed as specified here for return types (of getters and methods), and we could consider allowing them to be used for tear-offs of devariant members. (Say, we could allow the tear-off to produce a function object that admits static typing: With no dynamic type checks in the body of the main entry point, and with a reified type which is precisely as declared).

We may then be able to rely on `invariant` modifiers on types to reduce the number of occurrences of devariant method invocations, such that the non-homogeneous treatment of parameters that are covariant-by-class will only play a small role.

Start by reading issue #296 for the motivation and examples, then study this issue's proposal for devariant members and variance-aware substitution. Compare the proposed rules with the existing approach described in the discussion. Done means resolving the language-design questions and determining whether the proposal should be adopted, including its noted exceptions and usability concerns.

Written by the indexing model from the issue text.