Unsoundness in exhaustiveness with on clauses

[lrhn]

See dart-lang/sdk#53221 for context.

The gist is that

sealed class S {}
mixin M on S {}
class C extends S {}
class F implements M {}

is not prohibited by the specifications, and they also don't count M towards exhausting S, so

int i = switch (F() as S) {C _ => throw "Not this"};

should be allowed, as currently written, and have who-knows-what behavior.

Current behavior is:

• CFE disallows program, counts M as needed for exhausting S.
• Analyzer: Accepts program.

We can either:

• Count M towards exhausting S, by including on-types in the list of dependencies that count. Or because that's generally useless,
• allow M to be excluded from exhaustiveness, but then enforce that it's not implementable in any way:
  • We keep the current exhaustiveness rules about which types count twards exhaustiveness, which exclude mixins with only an on reference to the sealed class, only extends, implements and with clauses count.
  • We add the following restrictions on mixin ... on SealedClass and its uses:
    • It's a compile-time error if a mixin declaration M has a sealed (necessarily class) declaration S as
      a declared on type, M does not have S as a declared interface, and M is not marked base.
    • It's a compile-time error if any declaration has a mixin declaration M as declared interface, M has a sealed
      declaration S as declared on type, and M does not have S as a declared interface. (Even inside the same
      library. Really, only inside the same library, otherwise the "implementing a base type" error should take precedence.)

If we do count M towards exhauting S, we should allow M to be declared sealed (or implicitly count it as sealed, so that it's possible to exhaust M using all the classes of the form class F extends S with M {}.

[eernstg]

We can either count M towards exhausting S, by including on-types in the list of dependencies that count.

We should do that. Implementing the type introduced a mixin is a perfectly meaningful and well-defined relationship. Also, the CFE already does it. (I'm surprised that I must have overlooked the fact that it wasn't already included.)

that's generally useless

That's purely an opinion with no technical basis. It's a bit like claiming that it doesn't rain on a very rainy day: You might like that thought, but you're going to get wet anyway if you take a walk. ;-)

[munificent]

This doesn't mention the on clause, so an on S does not introduce a subtype that is part of space that exhausts the sealed type, so matching M should not be needed to exhaust S above.

Yes, that was a deliberate design choice. Some related discussion here.

That could also be sound, since an on S does introduce a subtype, but it's a subtype which only really works if it is mixed in on another concrete type which otherwise implements S, which means it should be a subtype of one of the "real" subtypes of the sealed type.

Yes, that was exactly the intent. Every instance of a mixin will also be an instance of some subtype of the mixin. If it's a mixin whose on clause is a sealed type, then any instance of that mixin should be an instance of a subtype of some other known subtype of the sealed type.

However, I can't find a rule against implementing M from above from another library (it's not marked base), or from the same library, which means that it's possible to create an instance of a subtype of S which is not a subtype of C1 or C2, which means that the exhaustiveness is not sound if it doesn't include M.

Oops! I think we overlooked this case. :(

So, we can go one of two ways:

• Allow M to not be counted as a subtype for exhaustiveness, but then not allow implementing it, even inside the same library.
• Count M towards exhaustiveness.

The second choice is easier, and safer.

The first choice is tempting because it does allow some more complex class hierarchies without requiring seemingly pointless cases to be exhaustive. But the additional complexity is worrisome. It will be very confusing whenever users run into it, and it's hard for me to imagine that the use cases it allows will be common or very compelling.

Could we maybe say that a mixin with an on clause on a sealed is counted for exhaustiveness unless the mixin is also marked base?

If that doesn't plug the hole, I think we should just take the second choice.

[lrhn]

Oops! I think we overlooked this case. :(

Not entirely sure, I'm pretty certain I considered it at some point. Maybe I just thought it was already in, so I forgot to add it in the next rewrite.

Could we maybe say that a mixin with an on clause on a sealed is counted for exhaustiveness unless the mixin is also marked base?

I can work with that.

We still need to prevent implements Mixin in the same library, but that's a simpler rule than looking at whether it also implements the sealed class.
I think most mixins-on-sealed-class will be private anyway, for use in the subclasses. Likely directly as class C12 extends Sealed with _Mixin1, _Mixin2 {}.

What do we do if the mixin has implements Sealed as well, should it count or not? (I'd be fine with "not". If it's base, then it doesn't count towards exhaustiveness, and nobody can implement it. If not, it counts, and everybody can implement it. Using implements S as a trigger is artificial, but then, so is using base, both are using something that has an existing meaning, and piggy-backing a second meaning on top. That makes it impossible to separate the two.)

What if you could put sealed on a mixin? In that case, it must be on another sealed type, cannot be implemented, and doesn't count towards exhausting the on-type, because it's considered included in that sealed-ness.
(Also artificial, but doesn't use an existing valid syntax.)

[munificent]

All of that makes me think we should just stick with option 2. The set of people that are doing all of:

1. Authoring sealed classes.
2. Authoring mixins.
3. Authoring mixins with on clauses.
4. Authoring mixins with on clauses that are sealed classes.

Must be very very small. I can't see it justifying a lot of extra feature complexity in order to eliminate slightly redundant-seeming switch cases when they do this. It's probably simpler and better to just say that the on clause introduces another subtype for purposes of exhaustiveness checking.

[lrhn]

There is another option: Disallowing having a sealed class as on type.

Then we have more time to figure out what the use cases we want to support are, without being bound to a bad decision.

[munificent]

That works for me too.

[eernstg]

The language team decided to handle this by including on clauses during exhaustiveness computation, and a breaking change was approved. A request for implementation of this behavior has been filed as dart-lang/sdk#53390.

[lrhn]

I'm reopening this issue, because I don't think the chosen approach is good enough.

TL;DR: I suggest just disallowing a sealed type as a mixin on type. If we find a way to make it work, then we can allow it, but the way we "allow" it today is causing more problems than it's solving. (The latter, IMO, being "none".)

The chosen approach is to count a mixin with a sealed class as an on type as one of the immediate subtypes of the sealed class which are needed to exahust the sealed class.

However, it will be impossible to exhaust the sealed class using actual concrete subtypes.

The following works and is exhaustive:

sealed class S {}
final class B extends S {}
base mixin M on S {}
final class C extends S with M {}
final class D extends B with M {}

void foo(S value) {
  print(switch (value) {
    B _ => "B",
    M _ => "M",
  });
}
void main() {
  foo(B());
  foo(C());
  foo(D());
}

This switch is exhaustive, because it checks for all immediate subtypes of S: B and M.

The class C is not an immediate subclass of S, even if it directy extends S, because it's a subclass of M which is also a subclass of S. The longest path to the sealed class should have length 1 for a class to be considere an immediate subclass. So C is not "immediate enough". (Same goes for the anonymous S&M, because it implements M, it's not immediate. It might actually be considered sealed as currently specified, because an anonymous mixin application inherits being sealed from the superclass, but exahusting S&M doesn't exhaust anything else, so it doesn't matter.)

The class D doesn't mention directly S at all, so nobody expected that to be an immediate subclass of S.

In any case, that switch is probably not what anyone wants to write for two reasons:

• They actually wanted C to count towards exhaustiveness directly, and would like to match C instead of just M.
• And if not, they definitely wanted C to exhaust M.

That is, they would want:

void bar(S value) {
  print(switch (value) {
    C _ => "C",
    B _ => "B",
  });
}

to be exhaustive, which it isn't.
The switch does not exhaust M. It doesn't directly match M, and M is not sealed (mixins cannot be declared sealed), so even if C had been the only direct subclass of M, it wouldn't exhaust M. (It isn't, D is another direct subclass of M.)

All in all, to exhaust S, you have to directly test for M. That is, on the face, reasonable since it is a direct subclass of the sealed class, but I claim that it is never what anyone actually wants.

What they want isn't currently possible. If we keep allowing on S, we'll be in a worse position for actually solving the problem in the future (whether by allowing M to be declared sealed, or by not counting M as an immediate sublass of S and requiring it to be base, which also closes the unsoundness-hole of implementing M, and then C would be an immediate subclass of S for exhaustiveness, since it's a subclass of S and it has no other more-immediate superclass.)

But if we don't do either of these today, we should disallow on S to keep our options open.