Dominance in pattern matching for switch: Spec and Javac inconsistency
John Rose
john.r.rose at oracle.com
Sat Sep 4 18:09:24 UTC 2021
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.
More information about the amber-spec-experts
mailing list