Dominance in pattern matching for switch: Spec and Javac inconsistency

[John Rose]

FTR, I approve of not even stepping onto this slippery
slope.  Doing so would seem to promise something of
value to users, a promise they’d probably feel we would
break by the draconian restrictions (with or without
complex case analysis on statically kennable expressions).

Remi, this relates to your offhand comment about guards
which are always true, as in case T x && alwaysTrue(x)
vs. case T (no guard).  Detecting always-true guards is
about the same problem (with no solution) as detecting
equivalent guards.  In particular if G1 and G2 are somehow
provably equivalent then G1==G2 is provably true and
G1!=G2 is provably false.  If G0 is provably true, then
G1 and G1&G0 are provably equivalent, and so on.

Statically, a guard should be treated as a coin flip
independent of every other expression.  (See also
my comment about guards working, in static
analysis, like existential subtypes of the guarded
type.)

— John

> On Sep 6, 2021, at 6:23 AM, Brian Goetz <brian.goetz at oracle.com> wrote:
> 
> 
>> yes,
>> apart that we can detect the case where both guards are identical.
>> 
>> something we currently do not do BTW.
>> 
> 
> That we don't do that now is a deliberate choice.  Even this is stepping onto the slippery slope; the ability to reason about guards falls off a cliff pretty quickly, and I'm not sure that handling the "easy cases" is doing the user a favor, when it risks lulling them into a false sense of confidence.  (We see this all the time with type inference; the better type inference is, the more upset people get when it doesn't read their mind.)
> 
> We could "easily" handle this:
> 
>     case int i && i > 0:
>     case int i && i <= 0;
> 
> (and some languages do.)  But even the short hop to
> 
>     case int i && (i %2) == 0:
>     case int i && (i %2) == 1;
> 
> is harder.  IntelliJ does heroics with abstract interpretation to find these things, which is great for an IDE, but less appropriate for a language spec.  So the question is, if we're going to venture onto that field, where do we draw the line?  Even "you specified exactly the same guard", once you get beyond a purely lexical definition of "same", is going to have holes.
> 
> The danger of attempting something so inherently incomplete is that we will invariably get drawn into a stream of "you do it here, but not there, that's a bug", which leads either to resources invested in low-value extensions, or low-value arguments about why we're not going to take then 342nd step (because, you already took the previous 341!)
> 
> So for now, we've drawn the line at "we're not gonna try"; we can always try harder later, since all that will do is make some switches that were already total but we didn't know it, into "total and we know it."
> 
>