Exhaustiveness mixing sealed type and enum

[forax at univ-mlv.fr]

> De: "Gavin Bierman" <gavin.bierman at oracle.com>
> À: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Mercredi 9 Juin 2021 17:08:17
> Objet: Re: Exhaustiveness mixing sealed type and enum

> Ahem,

> Actually, now I come to think about it - whilst your example enabled me to clean
> up the notions of coverage and exhaustiveness - I overlooked that your example
> still will not work because of the way that switch deals with case constants.

For whatever reason, in my mind it was Ok to mix constants and type patterns ... sorry for that. 

> In the Java 16 spec, it says first:

>> The type of the selector expression must be char, byte, short, int, Character,
>> Byte, Short, Integer, String, or an enum type (§8.9), or a compile-time error
>> occurs.

> And then:

>> The switch block of a switch statement or a switch expression is compatible with
>> the type of the selector expression, T, if both of the following are true:

>        * If T is not an enum type, then every case constant associated with the switch
>         block is assignment compatible with T (§5.2).
>        * If T is an enum type, then every case constant associated with the switch
>         block is an enum constant of type T.
> The important thing to realise is that these rules are driven by the type of the
> selector expression, not the case constant. Whilst these have been re-jigged in
> the draft 17 spec, the semantic content has been preserved for compatibility
> reasons.

> Back to a simplified version of your example:

> List l = ...
> switch(l) {
> case Nil.NIL -> ...
> default -> ...
> }

> Using the existing rules, this has to fail as List is not an enum type.

> So, what to do? We could add another rule for checking compatibility of a case
> label with the selector expression, along the lines of:

>> - If the type of e is not an enum type, char, byte, short, int, Character, Byte,
>> Short, Integer, or String, then e is downcast convertible to the type of c.

I don't think you should restrict the type here, i think it should also work for any static final fields by example, 
so something more like 

- If e is a constant, then e is downcast convertible to the type of c. 

> But that is quite a change to Java. We’d now be able to write things like:

> Object o = …
> switch(o) {
> case “Hello” -> ...
> case Nil.NIL -> ...
> default -> ...
> }

It's not that rare to have code that say, if it's this instance of that instance do that, otherwise if it's that type do this, etc. 
By example, JSON values are a mix between the constants null, true and false and instances of classes String, Double, JSONArray, JSONObject. 

> And code like:

> switch(o) {
> case Nil.NIL -> ...
> }

> would typecheck only if o is downcast compatible to Nil but NOT if it is
> actually of type Nil! Confusing? Potentially!

I think you mean the opposite, if o is typed Nil, because NIL is the only value of the enum Nil, the switch is correct while if o is a super type of Nil, then the switch accept more possible instances that just Nil.NIL so the switch does not typecheck without a default or a total pattern. 

> But I think actually we need a bigger chat about constants, both on this matter
> and how constants and patterns should co-exist more generally. I propose we
> table this for the second preview of this feature.

I agree. 

> (But the improved definitions of coverage and exhaustiveness stay as I stated
> them yesterday!)

yes ! 

> Thanks,
> Gavin

regards, 
Rémi