Do extension types follow their representation type in being always-exhaustive?

[eernstg]

[Edit: The language team decided that the answer is yes.]

The pattern feature specification defines the notion of an always-exhaustive type and specifies that a switch statement must be checked for exhaustiveness when the static type of the scrutinee is always-exhaustive.

Exhaustiveness properties of patterns involving extension types is achieved by taking the extension type erasure of all the relevant types, as specified [here](https://github.com/dart-lang/language/blob/main/accepted/future-releases/extension-types/feature-specification.md#:~:text=V%3E.empty()\).-,An%20extension%20type%20V,-(which%20may%20include).

The intention behind that paragraph in the extension type feature specification was that extension type erasure should apply to all aspects of exhaustiveness, but it has not been spelled out that the matched value type should be extension type erased as well.

If we do that then it follows that a switch statement must be checked for exhaustiveness when the static type of the scrutinee is an extension type whose erasure is always-exhaustive.

The conceptual justification would be that extension types should only be used in association with pattern matching in the case where it is OK to adopt the extension type (that is, casting from the representation type or a subtype to the extension type). We can have other devices (say, lints) to check that this is OK in the first place. Assuming that it is OK, it seems reasonable to me to say that the property of being always-exhaustive should also be allowed to propagate from the representation type to the extension type.

@dart-lang/language-team, WDYT?

[lrhn]

I'll say "no" as default, "yes" if the extension type implements a sealed class type.

And that's still work caveats.

If the extension type implements an enum type (or bool), it'll be tested as that. That's the easy case, because we know there are no subclasses.

If it implements a sealed type, then it matters how.
If it writes implements SealedType and the representation type is SealedType, then yes.

If the representation type is not SealedType, then no. Having a subclass of a sealed class as representation type, and implementing the sealed type, is a way to create a wrapped alternative to a sealed type direct subclass. It doesn't represent the entire sealed type hierarchy.

If it's not all of the sealed type, because of generics, then probably still yes.
Say there is an Option<T>/Value<T>/None sealed class hierarchy. If an extension type only applies to Option<int>... then that's still a sealed sub-hierarchy. Maybe.

If it doesn't implement the SealedType interface, then no, it's not telling you that it's exhaustive. Don't assume what the representation type is.

If it implements the desired type, but doesn't do it directly, say it implements another extension type which does, then it should probably count.

So the representation type is the sealed class, or an instantiation of it, and the extension type implements that sealed class' interface, then inheriting "must be exhaustive" is ok. Otherwise I wouldn't.

(But this is really just another example showing that "must be exhaustive" types is a hack, a heuristic trying to guess what the user might want absent of any signs of intent, and what we should really have is switches that must always be exhaustive. Possibly with an easy opt-out to get a switch which is not assumed to be exhaustive, and doesn't have to be. Then the author chooses the exhaustiveness of every switch, and all we have to do is validate.

Or in short: "always exhaustive" is bad because it's type based, but types don't always imply intent. I don't want to add it to an extension type that didn't ask for it. The ones that ask for it, are ones that extend and implement the sealed type itself, ones that are extending the sealed type with more members.)

[eernstg]

in short: "always exhaustive" is bad because it's type based, but types don't always imply intent.

My starting point is usually that we should set out from an assumption that a type implies a certain amount of intent, in addition to being a "technical" specification (for instance, that an object representation needs to contain a certain amount of storage in order to have the specified state, which is a kind of information that could be identical for many different types with very different intent). For starters, we do not know the intent, but we need to make sure that it does not get ignored gratuitously.

For this reason I'm usually arguing that we should not erase an extension type and proceed to use the representation type, unless there is a good enough reason to do so.

In this particular case I do think we have a reason: We're considering exhaustiveness.

In general, extension types don't have any guarantees about being exhaustive based on anything other than a catch-all case. In particular, extension types do not have the ability to specify exhaustiveness (we don't have a notion of sealed extension types). They basically can't specify exhaustiveness properties independently of the representation type because the actual exhaustiveness is fully determined by run-time properties, that is, it is fully determined by the extension type erasure.

So we can't even introduce sealed extension types or similar notions unless they will just repeat something which can be shown to hold for the extension type erasure in the first place (and, conversely, the only thing a sealed modifier could really do would be to deny knowledge about a specific actual exhaustiveness property which is known for the erasure, but which has (intentionally?) been kept away from the extension type itself.

Note that we have already decided a while ago that exhaustiveness relative to a given matched value type and set of cases is determined based on the extension type erasure. The only question which is on the table here is whether we should also let the status of being 'always-exhaustive' propagate back from the erasure to the extension type, and this is only used for (1) switch statements (not expressions), to determine (2) whether the switch statement must be exhaustive.

So if we refuse to do this then we gain exactly one thing: The ability to let a non-exhaustive switch statement go under the radar if it has a scrutinee whose type is an extension type and a representation type which is always-exhaustive. I'm not sure that's a net positive.

It isn't going to matter for the exhaustiveness analysis (the result will be the same with and without this behavior), it just turns off the exhaustiveness analysis for these particular switch statements. It doesn't matter whether each case uses the erasure or the extension type (or some intermediate form with a mixture of extension types and non-extension types), the outcome of the exhaustiveness analysis will be the same. It is only about the scrutinee, and it won't ever make anything safer, it just makes scrutinees with an extension type somewhat dangerous (an obvious thing to lint).

---

For the concrete use cases:

If the extension type implements an enum type (or bool), it'll be tested as that.

We'd need to adjust the specification in order to get that behavior. (The current behavior in DartPad based on Dart SDK 3.3.0-238.0.dev is to consider the switch as exhaustive with and without implements iff it is exhaustive using the erasure for all types).

If it writes implements SealedType and the representation type is SealedType, then yes.

I'm recommending that the always-exhaustive status is obtained from the extension type erasure, with or without implements Whatever. The case where the erasure is a direct subinterface of the sealed type is not special, and it isn't always-exhaustive unless that subinterface is itself always-exhaustive (e.g., because it is sealed or enum).

Say there is an Option<T>/Value<T>/None sealed class hierarchy [where Option<T> is also the representation type of an extension type ET<T>]

In that case I would certainly expect ET<T> to be always-exhaustive because Option<T> is always-exhaustive. It is perhaps possible that ET is intended to play a role which is conceptually totally unrelated to the optionality which is the obvious interpretation of Option<T>/Value<T>/None, but I find it unlikely.

So, apart from the general arguments given above (which are applicable to all classes, independently of their conceptual role and responsibilities), I also think this is very likely to be a use case where it is highly useful and meaningful to say that ET<T> is also always-exhaustive.

If it doesn't implement the SealedType interface, then no, it's not telling you that it's exhaustive. Don't assume what the representation type is.

This is at the core of my reasoning: We are switching on that SealedType which very likely involves directly querying its run-time type. This implies that we have already decided that it's OK to violate that thin, compile-time only encapsulation which is provided by an extension type.

We will have lints and stuff to help developers avoid that kind of query in the first place, but here we have it and then we might as well perform the analysis which takes the run-time type into account because that's what we will test, anyway.

[lrhn]

We can also just make all extension type switches "always exhaustive".

It's the way I'd like to go with switches in general, and to say that a switch statement with an extension type as matched value type must always be exhaustive, is not breaking.
The only side-effect is that every such switch statement which isn't otherwise exhaustive must have an empty case _: or default: at the end. That's the same as a switch expression on the same type would require.

So, my issue is that I don't think "must exhaust"-types is really a well-behaving concept to begin with, it's ad-hoc'ed on top of our existing ad-hoc enums-must-be-exhausted rule, which was based on user-requests, not language design. The language doesn't care. It's an attempt to guess "the user probably wants to exhaust this type, because they can".

I'd loathe to add more cases where we try to infer whether something should be exhausted or not, every time risking making a mistake because the type author has no way to control it, when it's derived from choices you're likely to make for other reasons (except sealed, that's only there for exhaustiveness). For extension types, your choice of representation type is for other reasons than exhaustiveness.
You can't have an enum which doesn't need to be exhausted, not even if you want to. And now, you can't even have an extension type on bool? which mustn't necessarily be exhausted, even if you don't think it's necessary.

So, I suggest either allowing sealed extension type, which must be exhausted, and non-sealed extension types don't need to,
or making all extension type switch statements "always exhaustive".

If every switch must be exhaustive, nothing needs to be special-cased, and the author doesn't have to worry about whether their extension type must be exhausted or not - because it always must.
(But it might be better to make all switches exhaustive then, as a breaking change which is trivially and automatically migratable, because then it won't be the same kind of breaking change to convert a final class into an extension type.)

We can add a switch! (expr) { ... } which doesn't need to be exhaustive, if we really want to avoid default: /* do nothing */, but I doubt it's worth it.

[eernstg]

The language team just decided (Jan 3, 2024) that we should indeed let the property of being always-exhaustive for an extension type follow the same property of the corresponding extension type erasure.

This seems to be the behavior which is already implemented, in which case there is no implementation effort:

// Does not have `implements bool`.
extension type Bool(bool b) {}

void main() {
  switch (Bool(true)) {
    case true: print('Got true!');
  }
}

This program has an error at switch which shows that the type Bool is considered to be always-exhaustive (as it should, because the erasure bool is always-exhaustive).

[eernstg]

@sgrekhov, I think this implies that a couple of co19 PRs can be unblocked?

[sgrekhov]

@sgrekhov, I think this implies that a couple of co19 PRs can be unblocked?

I think so! I'll check

[sgrekhov]

@eernstg does the decision that was made by the language team affect #3534 as well?

[eernstg]

No, the question about flow analysis hasn't been resolved yet.

We should be able to get good coverage anyway by ensuring that the flow analysis doesn't cause tests to fail. That is, some switch statements will be able to complete normally according to the flow analysis, even though they are exhaustive and will be recognized as such if we change the scrutinee type such that, for example, switch (ET(myBool)) { case .... } becomes switch (myBool) { case .... }. We could then change switch (ET(myBool)) { case .... } to something like switch (ET(myBool).it /*TODO: remove .it when #3534 is settled*/) { case .... }. This means that we can test exactly the rule handled in #3534 by performing that removal, and the test should succeed today with the extra .it.

Please double-check, but something like that should work. ;-)

[eernstg]

Closing: The specification is updated in #3568, and tests and implementation is handled from there.