Listing the sub-types that exhaust a sealed type

[lrhn]

We should ensure that the set of subtypes which exhaust a sealed type is predictable and computable.

(TL;DR: We should ignore non-implementable mixins with a sealed class as an on type from the types we care about for exhaustiveness of that sealed class. We should compute a set of public types that can exhaust a sealed type for documentation purposes. Possible algorithm provided.)

We have an algorithm for checking whether a sealed type has been exhausted by a switch.

Generally, a sealed type has a number of subtypes, so that if you check an object whose static type is the sealed type against every one of those subtypes, at least one of them is guaranteed to match. Checking all of them "exhausts" the supertype.
(Instead of checking against the subtype directly, you might also be able to exhaust the subtype using multiple checks tjat again ensures that if the value has that subtype, it will be matched by at least one switch case. Checking a type directly is the easiest way to exhaust that type, some types allow other ways too, like sealed types and enums.)

There can potentially be many ways to exhaust a sealed type, but to be usable, a sealed type should communicate to users a set of subtypes they need to check in order to achieve an exhaustive switch.

We want that set of subtypes to be predictable, both to the author and to users, at least in non-pathological cases.
(It's probably OK that things get weird if you do things that makes the sealed class effectively unusable anyway, but for any reasonable use-case, the author and users should see the same declarations and make the same conclusion about which types to check for.)

It would be nice if that set (or a set) is computable, because it would be useful for the DartDoc for a sealed type to list the exhausting subtypes specially.
Most of the time, that will just be the immediate subtypes of a sealed class, but we need to be sure we handle non-trivial cases too.

Do we need a concept of public exhaustive subtypes, separate from local exhaustive subtypes?

Example:

sealed class S {}
sealed class _Base extends S {}
class A implements S {}
class B extends _Base implements S {}
class C extends _Base implements S {}

Here the type _Base and A exhausts S, but nobody outside of this library cares. They need to know that A, B and C exhaust S, and they never never need to hear about _Base.

A minimal set of public subtypes which exhaust a sealed public supertype seems to be the most useful and actionable information for users. It might differ from the local types that can exhaust the sealed type (but should still be sufficient inside the declaring library.)

Which means that we may want to be able to compute the set of public subtypes for documentation purposes.

Non-trivial cases

It's all about mixins.

mixin _M {}
sealed class S {}
class A extends S with _M {}
class B extends S with _M {}
class C extends S {}

Here we'd expect S to be exhausted by A, B and C.
However, A and B are not "immediate subclasses" of S, they are subclasses of C with _M. (See #2830 for why C with _M should be sealed, in which case A and B exhaust each of their C with _Ms.)

@munificent Will _M and C exhaust S locally, or will the algorithm only consider actual subtypes?

That case is "easy" because _M is private, and maybe because M is not a subtype of S.

Example:

mixin M implements S {} // public
sealed class S {}
class A extends S with M {}
class B extends S with M {}
class C extends S {}

In this case, the exhausting subclasses need to be C and M, because M is public and therefore someone, somewhere can create a new instantiable subclass of M, which is a subclass of S not declared in this library. An instance of such a class will be an S and M, but checking A, B and C alone is not guaranteed to exhaust all values of type S.
So M needs to be checked in order to exhaust all possible values of type S. And then A and B are no longer necessary to check, they're included in the necessary M check.

That case was also clear because M was a public, subclassable subtype of S.

Example:

mixin _M implements S {} // private
sealed class S {}
class A extends S with _M {}
class B extends S with _M {}
class C extends S {}

In this case, the exhausting subclasses probably still need to be C and _M, because even though _M is private, that doesn't prove that the type of _M is not accessible elsewhere. There might be a typedef M = _M;.

We can try to check whether the private type escapes in a way that makes it subclassable, but then we need to ensure that we are clever enough to detect all possible leaks. Possibly possible, but complicated. Let's assume that leak-detection is not viable, so being a private declaration is not helping us in any way.

Then nobody outside of this library can exhaust S, which is a concerning consequence for using what looks like a very reasonable private implementation choice.

The issue is that we have an abstract private sub-classable subtype of S which is not a subtype of any of the public subtypes, one we plan to ensure is only ever used in a concrete class which is a subtype of one of the public subtypes of S. That ensures that no instance of _M will not also be an instance of one of A, B or C.
We just can't easily prove that intent, and we can't specify it.

One approach is to use a mixin on type instead of just implements:

Example

mixin _M on S {}  // `on` clause relation is special!
sealed class S {}
class A extends S with _M {}
class B extends S with _M {}
class C extends S {}

Again, we have the problem that _M can be implemented, so if it leaks, A, B and C are not exhaustive for S, and we must assume that it can leak.

Then try:

base mixin _M on S {}  // `on` clause relation is special!
sealed class S {}
class A extends S with _M {}
class B extends S with _M {}
class C extends S {}

Here we might have a case. There can be no concrete subclass of _M which is not also a concrete subclass of another subclass of S. Which means that any subtype of _M is either a subtype of another subtype of S, it it's a mixin application on S itself, which means it's inside the same library as S, in which that declaration's type can be used as part of the public exhausting set.

Do we need to treat non-implementable mixins on the sealed type specially in some way?

Here _M is a subtype of S, but we don't want to include it in the set of exhausting subtypes of _S. We probably can get away with that because there can be no objects implementing _M which do not also implement at least one other subclass of _S, so _M is not needed in a minimal set of exhausting subtypes.

So A, B and C are enough to exhaust S because they exhaust _M, because there cannot be an _M which is not one of A, B or C (or a new subclass of S which would then be included in the exhausting set).

We need to figure out precisely when that logic applies. A mixin being non-implementable (base/final/sealed) and on S may be sufficient.
(That also explains why it's not a problem that a mixin in a nother library has on S for a sealed S. That mixin cannot be implemented, and then the mixin in another library doesn't matter for exhaustability, because such a mixin doesn't matter in any library.)

That also explains why this example is sound:

library lib1;
import "lib2.dart";

sealed class S {}
class A extends S with M {}
class B extends S with M {}
class C extends S {}

and

library lib2;
import "lib1.dart";

base mixin M on S {}

class D extends C with M {}

The classes A and B implement M, but M is an ignorable mixin wrt. exhaustiveness, even in another library,
so S is exhausted by A, B and C, the closest (public) subtypes to S declared in lib1.

(Whether lib2 can use switch (s) {case C c: ...; case M m => ...} to exhaust S depends on what the algorithm does, but we won't document M as one of the types to use, because it's not declared in the same library as S.)

Proposal

Define the set of exhausting subtypes of a sealed type S in library L as the set, EXHAUST(S), of proper subtypes of S declared in L which are not non-implementable mixin declarations with S as on type, and which
do not have a supertype which is itself in EXHAUST(S)

(Start with the set of all proper subtypes of S declared in L. Remove all unimplementable mixins with S as an on type. Then remove all types which still have a supertype in the remaining set.)

If the exhaustiveness algorithm needs to find a a set of subtypes that exhausts a sealed type, this should be that set.
(If the algorithm works directly from declarations, it's still a set that the library author can use to exhaust the type.)

Then we define the public exhausting subtypes of a sealed S in library L, EXHAUST_pub(S) as the proper subtypes of S declared in L, P, s.t.:

• P ∈ EXHAUST(S) and
  • P is public, or
  • P is not sealed, or
  • P is sealed and EXHAUST_pub(P) is empty.
• or there exists R in EXHAUST(S), R is private and sealed and P ∈ EXHAUST_pub(R);

If this set contains a private name, then the sealed type has a subtype which is private and is either not sealed, or has no public subtypes. In that case, that type cannot be exhausted from outside the library.

This is the set of types we should show in DartDoc. If it contains a private declaration, we should probably just say that the type cannot be exhausted without a wildcard pattern/default case, and list subtypes normally.

WDYT?

@leafpetersen @munificent @kallentu @eernstg @stereotype441 @natebosch @jakemac53

[eernstg]

I'd prefer an approach which uses the graph properties strictly and ignores the distinction between private and non-private declarations.

We would then rely on propagation in order to confirm that any particular set of types will exhaust a given sealed type. For example:

// Introduce exhaustiveness.
sealed class A {}

// Unrelated stuff, allowed but makes no difference.
mixin UM {}
base mixin _UM {}

// A is exhausted by `{B1, B2, _B3}`.
final class B1 extends A with UM, _UM {}
class B2 implements A {}
sealed mixin _B3 on A {} // Propagate exhaustiveness.

// _B3 is exhausted by `{C1, C2}`.
base class C1 implements B1, _B3 {}
interface class C2 extends B2 with _B3 {}

A is exhausted by the first "generation" after A, namely {B1, B2, _B3}, and _B3 is exhausted by the next generation after _B3, namely {C1, C2}.

The point is that we're only using the notion of 'direct declared superinterface' to detect that the direct subinterfaces of A are B2 and _B3 (those are trivial), plus B1 (which has A as an indirect superinterface because the mixin application A & UM & _UM is the direct superclass, and then we have A & UM, and finally A, but it has A as a direct declared superinterface because the mixin applications are not 'declared').

So we don't have a complex EXHAUST function, we just check the superinterface graph and walk down as far as possible from each sealed class to a predecessor whose path back to the sealed class has exactly one edge that counts: That's the exhaustive set.

graph BT;
    C1[base C1] -.-> B1[final B1]
    C1 -.-> _B3
    B1 --x AUM_UM[A & UM & _UM]
    AUM_UM --> _UM([base _UM])
    AUM_UM --x AUM[A & UM]
    AUM --> A[sealed A]
    AUM -.-> UM([UM])
    C2[interface C2] --x B2_B3
    B2_B3[B2 & _B3] --> B2
    B2_B3 -.-> _B3([sealed _B3])
    B2 -.-> A
    _B3 -.-> A

Loading

It is then up to various tools (e.g., DartDoc) to use this basic notion of exhaustive sets to compute a set which is exhaustive based on propagation, e.g., {B1, B2, C1, C2}, satisfying whatever additional criteria may be applicable for the given purpose (e.g., eliminate private declarations, or make it as fine-grained as possible, or whatever).

[lrhn]

Using "direct declared superinterface" risks depending on syntactic accidents.
Take:

sealed class S {}
class A extends S {}
class B extends A implements S {}

Here both A and B have S as directly declared superinterface, but for B it's an accident, since B is also getting S from another source.

So maybe restrict the levels to to class having S only as a directly declared superinterface, meaning that it has S as a directly declared superinterface, and also that no other directly declared superinterface (so which is not S itself) has S as a superinterface.

That would discount B because while it has S as directly declared superinterface, it also has A as directly declared superinterface, and A has S as a proper superinterface.

It also brings us back to

sealed class S {}
base mixin _M on S {}
class A extends S with _M {}
class B extends S {}

Here M has S as directly declared superinterface, but the types A and B still exhaust all instances of S.
Non-implementable mixins do not contribute instances by themselves.

[eernstg]

Using "direct declared superinterface" risks depending on syntactic accidents.

sealed class S {}
class A extends S {}
class B extends A implements S {}

Ah, good catch! The algorithm I mentioned will produce a set of types which is (easily provably) exhausting the sealed type by means of direct declared subinterfaces, but it is possible that some types in that set are related (like B <: A). This means that the set will still be exhaustive if we remove every type which is a subtype of any other type in the set.

We need to perform this reduction after each sealedness propagation operation: In my example here, {B1, B2, _B3} will exhaust A, and cannot be reduced, and {C1, C2} will exhaust _B3, and cannot be reduced, but by propagation we can also exhaust A by {B1, B2, C1, C2}, and this set can be reduced to {B1, B2, C2}.

I think this reduction step is needed, because we probably won't have any graph-shape based rule which will tell us from first principles to remove C1 when we exhaust A with propagation through _B3, it's much simpler to say that we compute a set of types and then we reduce it by eliminating subtypes (and we just don't care how C1 was made redundant by propagation that turned {B1, B2, _B3} into {B1, B2, C1, C2}).

Considering the other example:

Here M has S as directly declared superinterface, but the types A and B still exhaust all instances of S.

sealed class S {}
base mixin _M on S {}
base class A extends S with _M {}
class B extends S {}

The 'direct declared' criterion would say that S is exhausted by {_M, A, B} which is then reduced to {_M, B}. If we wish to compute an exhaustive set that doesn't include _M (because it's private, or because we can prove that there are no instances of type _M that aren't also instances of type A) then we could make an attempt to propagate. However, _M isn't sealed. So if we have a leak (like typedef M = _M;) then we could have declarations in other libraries implementing _M, and it wouldn't be correct to try to propagate _M into {A}.

We could consider "auto sealing" every non-leaking private type. However, I'd actually prefer the more explicit approach where we don't compute the sealedness property, we always require an explicit sealed keyword in order to get that status, for every declared type.

[lrhn]

If we wish to compute an exhaustive set that doesn't include _M (because it's private, or because we can prove that there are no instances of type _M that aren't also instances of type A)

It's the latter. A non-implementable mixin with S as on-type will never be necessary to exhaust S. There can be no instances of that mixin that are not also instances of another subtype of S. An instance is an instance of a class.
A class can only have a mixin as superinterface if it implements it (which is assumed impossible) or it implements a mixin application of that mixin, and that mixin application class will a subtype of S.

If the mixin can be implemented (interface or no modifier), then it doesn't matter that it's also mixin, it's being an interface that makes it impossible to know all the subtypes locally, without an escape analysis which I also don't want to have to do.

[eernstg]

There can be no instances of that mixin that are not also instances of another subtype of S

A similar argument would be applicable for any abstract class, but we probably wouldn't force developers to use case B1Impl():, .. case BkImpl(): just because we think B shouldn't be listed as a member of the exhaustive set because there are no instances.

[Edit:] Ah, it isn't necessarily another subtype of S. But it is still not obvious that we want to reason about the existence of instances, because it might be useful to have a case on a type that does not have direct instances.

Also, what's going to stop base class C implements _M {}?

[lrhn]

Mixins are unique in that they cannot create objects themselves, and cannot be simply subtyped into something which can create objects, at least not if they can't be implemented.
They have to be applied to a superclass before they become classes. And either that superclass, or the mixin application class itself, will be a better representative for exhausting instance of subtypes of that than the mixin.

Nothing stops the same library from doing base class C implements _M, but then we can treat C as the class exhausting the instances that are created by subclasses of C, and can still ignore M.
There will still be no instances that are subtypes of S and _M which are not also subtypes of another sub-type of S declared in the same library.

(If we had an abstract class which could never be subclassed into something that can create values, we could also ignore it from exhaustion checks. It's just not a particularly useful thing to have, so we don't have language support for declaring or detecting that. But it is why we can ignore the valid subtype Never in exhaustion checks, because we know it's empty.)

[eernstg]

I just don't see a good reason why we should ignore a pseudo-non-implementable mixin when we're computing exhaustive sets of types for a given sealed type.

sealed class S {}

// "Normal" cases.
class B1 extends S {}
class B2 implements S {}

// We actually want clients to use this as a type.
base mixin NiceInterface on S {}

// `NiceInterface` has a bunch of implementations. Clients shouldn't care which one they got.
base class Impl1 implements NiceInterface {}
base class Impl2 extends B1 with NiceInterface {} // In some cases we also want the methods.
...
base class ImplN implements NiceInterface {}

I don't see why it should be impossible to recognize that S is exhausted by {B1, B2, NiceInterface}, just because we have a rule which says that the exhaustive set is {B1, B2, Impl1 ... ImplN}. Consider also the case where some or all of the Impl classes are private.

How does it help anybody if we're trying really really hard to eliminate that mixin from the exhaustive set?

[lrhn]

The situation I want to avoid is having:

sealed class S {}

// "Normal" cases.
class B1 extends S {}
class B2 implements S {}

base mixin NiceInterface on S {}

class C extends B2 with NiceInterface  {}

and somehow end up thinking that you need to exhaust B1, B2 and NiceInterface in order to exhaust S.
You don't, B1 and B2 is enough, because every sub-class of S implements at least one of those.
Because NiceInterface is base, we known that no other library can implement it, and if another library mixes it in,
it must do so on a type which is already a subtype of S. Therefore NiceInterface cannot be used to introduce a new subspace for S outside of this library.

I don't know (and don't understand) how the exhaustiveness checking algorithm actually works, but I think it needs to decide, somehow, which subspaces of a sealed type needs to be exhausted in order to exhaust the type itself.
I don't want NiceInterface to end up in that set unnecessarily.

[eernstg]

It's true that the reduction step that I mentioned (delete every type from the exhaustive set which is a subtype of some other type in the set) is needed in order to reduce {B1, B2, C} to {B1, B2}. No problem.

However, the algorithm I proposed won't create that set, it will create {B1, B2, NiceInterface}, which might be exactly what you want.

However, if you have a specific reason why you want to eliminate NiceInterface from the set then you can do that if it is marked sealed: Just compute the next generation after NiceInterface, remove NiceInterface and add the next generation to the exhaustive set, and reduce the set. Still no problem.

(But if NiceInterface is not sealed then I'm not so sure it is a good idea to try to exhaust it, even in the case where that's possible based on the precise source code at the time. What makes you think that result won't change over time?)

I think [the exhaustiveness algorithm] needs to decide, somehow, which
subspaces of a sealed type needs to be exhausted in order to exhaust the type itself.

I don't think it needs to do that in a general sense, I think it's fine if it can determine whether or not any given set of types is exhaustive. The algorithm must definitely be able to recognize that {B1, B2, NiceInterface} is exhaustive if that's what the developer has chosen to switch on, but it should also recognize all those sets which are created by propagation.

This can be done (assuming the algorithm I mentioned) by (1) noting that the static type of the matched object is a sealed type S declared in a library L; (2) find all sealed types in L which are subtypes of S, transitively; (3) compute the exhaustive sets for each of those; (4) gather the types being tested in the switch as the set Tested; (5) for every sealed type Sj where Tested already contains the entire exhaustive set for Sj, add Sj to Tested; iterate this step until stable; (6) check that S is a member of Tested.

I don't see a need for this algorithm to try to avoid any particular nodes in the graph (mixin or not, implementable or not, private or not). This would simply introduce complexity that doesn't help anyone.

A quite different task is documentation: Telling developers what they need to include when they want to switch over a given sealed type. In this case it does make sense to avoid private classes and perhaps some others, but that's a pragmatic matter, and it is possible that we will rely on human judgment in order to determine what the best exhaustive set is, based on the superinterface graph but also on the meaning and purpose of each of those classes.

In other words, it might be a task which is best done manually in some non-trivial situations to specify in the DartDoc of S that the recommended way to exhaust S is to cover the types {B1, B2, B3, B4, C1, C2}, or whatever it is. If a developer wants to use {B1, B2, B3, B4, M} (where M is a sealed mixin exhausted by C1 and C2) then the exhaustiveness check should of course also be able to recognize that {B1, B2, B3, B4, M} exhausts S, and it's not actually necessary to use the "official" exhaustive set {B1, B2, B3, B4, C1, C2} if that other exhaustive set fits the given purpose better.

[munificent]

I think you may be overthinking this, which is my fault because the proposal is totally silent on this question (oops) and the exhaustiveness prototype sidesteps it by only modeling a simplified abstract subset of the type system.

The exhaustiveness checker does not need a set of exhaustive subtypes that are disjoint. It is totally fine with them overlapping in various ways and (I believe!) the algorithm will sort it all out correctly, automagically. So I don't think we need any notion of a "minimal" set of exhaustive types.

Looking at Erik's example:

// Introduce exhaustiveness.
sealed class A {}

// Unrelated stuff, allowed but makes no difference.
mixin UM {}
base mixin _UM {}

// A is exhausted by `{B1, B2, _B3}`.
final class B1 extends A with UM, _UM {}
class B2 implements A {}
sealed mixin _B3 on A {} // Propagate exhaustiveness.

// _B3 is exhausted by `{C1, C2}`.
base class C1 implements B1, _B3 {}
interface class C2 extends B2 with _B3 {}

As Lasse suggests, I think we want to ignore mixin applications when considering the direct subtypes of a sealed type. So the hierarchy of subtypes as far as sealed is concerned would be (here parentheses mean "is marked sealed"):

     (A)
    / | \
   /  |  \
  B1 B2 (_B3)
         / \
        C1 C2

The sealed subtypes of A are B1, B2, and _B3. The sealed subtypes of _B3 are C1 and C2.

We don't need to flatten that graph down so that the subtypes of A are B1, B2, C1, C2. We just leave it as is. If you're matching on a value of type A, the exhaustiveness checker will require you to cover B1, B2, and _B3. But it understands that even though you can't say _B3 from outside of the library, because it's marked sealed too, you can cover it with C1 and C2.

Another example:

sealed class S {}
class A extends S {}
class B extends A implements S {}

Here, the sealed hierarchy is:

 (S)
 / \
A   B

So you have to cover both A and B. But the exhaustiveness checker understands that because B is a subtype of A, if you cover A then you've covered B too. Both types are still considered the direct subtypes of S, but the exhaustiveness checker won't have any problems with it.

It works sort of like this. Say you have a switch like:

S s = ...
switch (s) {
  case A _: ...
}

Because the matched value type is a sealed type, it essentially expands it out into two separate switches for each subtype:

S s = ...
switch (s as A) { // Narrow the matched value type.
  case A _: ...
}

switch (s as B) { // Narrow the matched value type.
  case A _: ...
}

It knows, because S is sealed, that if both of those switches are exhaustive over their respective narrower types, then the original switch is sealed too. Note that both switches get all of the cases from the original. So then it dutifully trucks through the first switch and sees that, yes case A _ does indeed cover the entire matched value type A, so that one is fine. And then it proceeds to the next and sees that case A _ also matches every instance of the other matched value type B because B is a subtype of A. So that one's good too. Therefore the original switch is exhaustive.

So, in general, overlapping hierarchies shouldn't cause any problems. In fact, the prototype has tests for funny things like:

//    (A)
//    / \
//  (B) (C)
//  / \ / \
// D   E   F
sealed class A {}
sealed class B implements A {}
sealed class C implements A {}
class D implements B {}
class E implements B, C {} // <-- !
class F implements C {}

And it understands that these switches are all exhaustive:

A a = ...

// Easy.
switch (a) {
  case B _:
  case C _:
}

// Medium.
switch (a) {
  case D _:
  case E _:
  case F _:
}

// Hard!
switch (a) {
  case B _:
  case F _:
}

If we had an abstract class which could never be subclassed into something that can create values, we could also ignore it from exhaustion checks. It's just not a particularly useful thing to have, so we don't have language support for declaring or detecting that.

We will have it soon:

abstract final class C {}

I don't know (and don't understand) how the exhaustiveness checking algorithm actually works, but I think it needs to decide, somehow, which subspaces of a sealed type needs to be exhausted in order to exhaust the type itself.

The two algorithms handle it a little differently. But the basic way to think about it is when a case matches only a subtype of the matched value type, it's not really helpful. If you have:

class A {} // Not sealed.
class B extends A {}
class C extends A {}

switch (A()) {
  case B _: ...
  case C _: ...
}

Those cases match some stuff, probably, but as far as exhaustiveness checking is concerned, they're useless. Cases that may match don't help prove exhaustiveness. Only cases that must match are useful, because they prove that no value can escape it. (That's also why cases with guards don't help with exhaustiveness.)

What sealing does is let you bifurcate the matched value's type into a set of subtypes—that may or may not be disjoint!—and then try them independently. That's useful because (and only because) when the matched value's type gets narrower, it means you're more likely to have a case whose type is a supertype of the matched value. Those are the case types that are useful because a case whose type is a supertype of the matched value always matches.

In the previous example, if we mark A as sealed, then it lets the exhaustiveness checker now treat that one switch as if you'd written:

switch (A() as B) {
  case B _: ...
  case C _: ...
}

switch (A() as C) {
  case B _: ...
  case C _: ...
}

And now we know that the first case must match in the first switch and the second case much match in the second switch. Therefore, the original switch is exhaustive too.

It took me a long time to wrap my head around this, because functional languages don't have subtyping so exhaustiveness checking is always disjoint. Therefore cases either always match or never match. Subtyping means you need to think about cases that may or must match. And it's only the latter that are useful.

I didn't follow everything in the comments about private base mixin declarations, but I'll try to think about that more.

[eernstg]

As Lasse suggests, I think we want to ignore mixin applications when considering the direct subtypes of a sealed type.

Right. We get the same effect with the rule that I mentioned. In short, in a given superinterface graph containing a sealed class/mixin S, the direct subtypes of S is the set of nodes at the beginning of the longest paths reaching S with exactly one edge that counts (and an edge that doesn't count is an edge that ends in a mixin application).

In particular, a mixin application is never included in the set of direct subinterfaces of any denotable class, because a mixin application is never a leaf node in the graph, and every predecessor of a mixin application AM is connected to AM by an edge that doesn't count (so the path from AM is never the longest one).

We can't outright ignore mixin applications in the graph, because they introduce subtyping relations. But it is probably possible to cluster some nodes. For example, class B extends A with M1 .. Mk {...} would have one node for B and all the mixin applications, and that node would have superinterface edges to A and to M1 .. Mk and so on, following the definition of what a mixin application means.

The sealed subtypes of A are B1, B2, and _B3. The sealed subtypes of _B3 are C1 and C2.

That's great! This is exactly the kind of approach I'd prefer: No exceptions, no unnecessary complexity. And we have no problems detecting that {B1, B2, C1, C2} exhausts A, and if we have C1 <: B2 then we can reduce the set and conclude that {B1, B2, C2} is also exhaustive.

[lrhn]

For the record: We want to ignore anonymous mixin applications. That's most of them, but we cannot ignore:

mixin M {}
sealed class S {}
class A = S with M;

Here A is a mixin application, but it's also a publicly visible and extensible immediate subclass of S.

(Named mixin applications. There are dozens of them!)

[eernstg]

Right, I'd treat class A = S with M; as the same thing as class A extends S with M {}, because <mixinApplicationClass> (the one with =) actually creates a nominally unique type per declaration:

class S {}
mixin M {}
class A1 = S with M;
class A2 = S with M;

void main() {
  // A1 a1 = A2(); // Compile-time error.
  print(identical(A1, A2)); // 'false'.
}

So S with M is the mixin application (and in general we can have several, as in S with M1, .. Mk), and every class declaration (with or without =) creates a new class where the superclass may be a mixin application, but the class itself is not.

[lrhn]

If we're going to nitpick (and by golly, I will!), the class A1 of class A1 = S with M; is a mixin application class. It's not equivalent to class A1 extends S with M {} because the superclass of the former is S, the superclass of the latter is S-with-M.

(And it is possible to tell the difference in a few corner cases.)

[munificent]

Tangential:

(And it is possible to tell the difference in a few corner cases.)

I can honestly never remember what they are. Can someone remind me why we even have the class A = S with M; syntax instead of just having users write class A extends S with M {}? I understand conceptually that they are different things. But what is the concrete motivating use case where a user would need the former and the latter wouldn't do?

[lrhn]

I can't say why we added the syntax class C = S with M implements I1, I2;, but I like it and use it occasionally.

The underlying idea of a mixin is that it describes the implementation difference between a superclass and a subclass.
A subclass is always a superclass with a mixin and possibly adding some new interfaces.
Writing class C extends S { ... } is applying the literal mixin {...} to the superclass S.
The syntax class C = S with M; is the primitive operation for applying a named mixin. We could also have used class C extends S with M; as syntax instead (and honestly, we probably should have).

I'd use class C = S with M; when adding an empty body seems unnecessary. The "overhead" of adding one more class to the hierarchy is small, but it is still unnecessary.
That one extra layer can affect our LUB computations, because it depends on distance-to-Object. (I'd blame LUB for that, not mixins.)

It's convenient to have the basic mixin-application operation in the language. That means that we can tell people that
class C = S with M1, M2 { ... } can be desugared to:

class _$S_M1 = S with M1;
class _$S_M1_M2 = $S_M1 with M2;
class C extends _$S_M1_M2 with { ... }

Having a fundamental operation that you can't express directly is always annoying.

The case where you can really tell the difference is:

mixin _M { ... something ..., no fields. }
class C = Object with _M;

Here C is a class, can be instantiated, and has a const constructor (mixin application forwards constructors, const constructors as const if the mixin has no fields).
It can (could) also be used as a mixin since it declares no constructor, and has Object as superclass.

There was no other way to create a declaration that could be used as a superclass, a mixin, and have a const constructor.

In Dart 3.0, you'll just write mixin class C { const C(); ... something ... }. Much better!
(That was one of the reasons I wanted to allow "trivial constructors" in mixin classes.)

[munificent]

I've updated the spec for exhaustiveness (#2948) and it now defines how sealed types are expanded. Given that, I think this can be closed since there's no other work to do. Feel free to re-open, though, if you think the spec should be changed.