On Sep 3, 2021, at 7:00 AM, fo...@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.