Taking a step back for a moment, I think there are two distinct issues here:
- What’s the correct behavior for type checkers?
- How do we make it easy for users to express what they want checked?
Right now, I believe the answer to the first one is “the type checker is correct for the case on-hand, and there are x other ways to express it depending on your intent”
The latter has been a larger ongoing recurring topic with a lot of concerns. Variance and API boundaries not being “Easy” was definitely brought up there, and I think this is a real thing we need to address.
I’m not sure I agree with a protocol with a single method defined as effort, but I have a feeling that effort here is less the protocol itself, and more the process to determining it was needed and why. If that’s accurate, I think a more productive way forward would be pushing type checkers to have built-in explanations for what caused specific variance to be determined. This is a not-uncommon pain point in the type system, and even those with experience in it or experience with similar, yet different languages (With slightly different concerns) get surprised by the effects of it at times.