Do extension types support statically checked variance?

[eernstg]

Thanks to @sgrekhov for raising this issue! Currently, extension types are specified such that it is an error for a type variable declared by an extension type to occur in a non-covariant position in the representation type. This is required for soundness:

extension type E<X>(void Function(X) func) {} // Error, but pretend that we'd allow it.

Y upcast<X extends Y, Y>(X x) => x; // Return includes upcast, should not need dynamic check.

void main() {
  E<int> eInt = E((int i) {});
  E<num> eNum = upcast(eInt); // OK, but it violates soundness!
}

This would be a soundness violation because eNum.func has static type void Function(num) and run-time type void Function(int), and the latter is not a subtype of the former. In short, extension types already behave as if they have the modifier out on every type parameter, because it would otherwise give rise to soundness violations.

It seems obvious that this could be generalized such that an upcoming variance feature could be used with extension types. For example:

extension type E<in X>(void Function(X) func) {} // OK (future generalization).

Y upcast<X extends Y, Y>(X x) => x;

void main() {
  E<int> eInt = E((int i) {});
  E<num> eNum = upcast(eInt); // Compile-time error, `Y extends X` not satisfied.
}

We would then make it explicit that extension types do admit statically checked variance modifiers, and a type parameter with no such modifier is implicitly out (and that subsumes the current compile-time error involving variance).

@dart-lang/language-team, WDYT?

[lrhn]

Type parameters of an extension type must be used covariantly today, in the representation type and superinterfaces, because the parameter is (unsafely) covariant by default, and the representation type must co-variate with the extension type. We want E<T> <: E<S> to imply R<T> <: R<S>, where R<X> is the representation type of E<X>, otherwise the extension type erasure isn't sound.

If we can specify other variances, then I don't see a reason the type variables can't be used at that variance only, subject to all the usual requirements of where they can then be used. As long as the variance implies the subtyping of representation types, that's what we need for soundness.