Dominance in pattern matching for switch: Spec and Javac inconsistency

[forax at univ-mlv.fr]

----- Original Message -----
> From: "John Rose" <john.r.rose at oracle.com>
> To: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "Jesper Steen Møller" <jesper at selskabet.org>, "Ilyas Selimov" <ilyas.selimov at jetbrains.com>, "amber-spec-experts"
> <amber-spec-experts at openjdk.java.net>
> Sent: Samedi 4 Septembre 2021 20:09:24
> Subject: Re: Dominance in pattern matching for switch: Spec and Javac inconsistency

> On Sep 3, 2021, at 7:00 AM, forax at univ-mlv.fr wrote:
>> 
>> 
>> but a guarded switch dominates it's prefix,
>> e.eg
>>   case Integer i && foo(i) dominates case Integer.
>> 
>> But there is no rule between a guarded pattern like case Integer i && foo(i) and
>> case 1, so they can appear in any order.
>> 
> 
> Surely that’s a simple oversight.
> 
> FWIW, it would be possible to convert reasoning about value-set
> inclusion to reasoning about type dominance, in this case, by
> simulating T x && g(x) as an existential type (? extends T).
> 
> I think that simulation has the right properties for guards,
> which is that (a) no two guards denote the same static value
> set and (b) any guarded value set is a subset (possibly improper)
> of the corresponding unguarded value set.

yes,
apart that we can detect the case where both guards are identical.

something we currently do not do BTW.

Rémi