Exhaustiveness mixing sealed type and enum

[Gavin Bierman]

Hi Rémi,

On 2 Jun 2021, at 11:42, Remi Forax <forax at univ-mlv.fr<mailto:forax at univ-mlv.fr>> wrote:

Do we agree that the code below defines an exhaustive switch so no default is necessary ?

sealed interface List permits Cons, Nil { }
record Cons(String value, Object next) implements List { }
enum Nil implements List { NIL }

int size(List list) {
 return switch(list) {
   case Cons cons -> 1 + size(cons.next);
   case Nil.NIL -> 0
 };
}


You are quite right, this should work. I have fixed up the spec to address this. The new definition looks like this:

A switch block covers a type T if one of the following is true:

  *   T names an enum class E and all of the enum constants of E appear as constant switch label elements in the switch block.
  *   T supports a sealed class or interface C, and the switch block covers all of the permitted direct subclasses and subinterfaces of C.
  *   A switch label in the switch block has a pattern case label element p where the pattern p is total for T (14.30.3).
  *   There is a default switch label in the switch block.

A switch statement or expression is exhaustive if the switch block covers the type of the selector expression. (Neat, huh?)

What is this notion of “supports a sealed class or interface” in the second bulletpoint I hear you ask? It’s actually to address another problem you raised in a different mailing list:

  sealed interface Vehicle {}
  record Car(String owner, String color) implements Vehicle {}
  record Bus(String owner) implements Vehicle {}

  public static void example2() {
    var vehicles = List.of(
        new Car("Bob", "red"),
        new Bus("Ana")
    );
    for(var vehicle: vehicles) {
      switch(vehicle) {
        case Car car -> System.out.println("car !");
        case Bus bus -> System.out.println("bus !");
        //default -> throw new AssertionError();
      }
    }
  }


PatternMatching101.java:25: error: the switch statement does not cover all possible input values
      switch(vehicle) {

The reason this doesn’t behave as you expected is is that the inferred type for vehicle is not Vehicle but an intersection type! Previously the spec didn’t deal with this, it only asked if the type of the selector expression was a sealed class/interface on the nose. We need to be a little more flexible. So we define the following:

A type T supports a sealed class or interface C if and only if one of the following holds:

  *   T is a class type that names C, and the class C is both sealed and abstract.
  *   T is an interface type that names C, and the interface C is sealed.
  *   T is a type variable, and its bound supports C.
  *   T is an intersection type T1 & ... & Tn, and a type Ti supports C (1 ≤ i ≤ n).

This is what the second bulletpoint for the “covers” relation uses. This ensures that your vehicle example works as expected as well.

The compiler will be updated to match this spec shortly.

Thanks for the feedback.
Gavin

PS: Latest version of the spec available, as always, at: http://cr.openjdk.java.net/~gbierman/jep406/latest

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210608/8e978036/attachment.htm>