[23] exhaustiveness signalling difference between javac and ecj

[mpalat]

Given,

	public class X  {
	    public static int foo(Integer myInt) {
	        return switch (myInt) {
	            case int i  -> i;
	            default -> 0;
	        };
	    }
	
	    public static void main(String argv[]) {
	    	Integer i = 100;
	    	System.out.println(X.foo(i) == i);
	    }
	}  

ecj bails out with the error:
"Switch case cannot have both unconditional pattern and default label"
while javac compiles.

Further, spec says -
Section 5.7.2 says - "Unconditional exactness is used at compile time to check the dominance of one pattern over another in a switch block (14.11.1), and whether a switch block as a whole is exhaustive (14.11.1.1)."

and also, includes "a boxing conversion" for unconditionally exact. However, this is an unboxing condition [from Integer to int] and not a boxing conversion -and hence not unconditionally exact. and hence it looks like ecj should allow this - ie, should not consider "case int i" as covering Integer.
But, what could be a value of myInt such that default is taken instead of case int i? @stephan-herrmann any thoughts on this?

[stephan-herrmann]

But, what could be a value of myInt such that default is taken instead of case int i? @stephan-herrmann any thoughts on this?

null ?

[mpalat]

But, what could be a value of myInt such that default is taken instead of case int i? @stephan-herrmann any thoughts on this?

null ?

@stephan-herrmann, I expected this question :)
null anyway is not covered by default. Still, even if I add null
case int i -> i;
case null -> -1;
default -> 0;
now also similar behaviour difference between javac and ecj - javac accepts, ecj doesn't. Between int i and null, now all the cases are covered, I believe? can you think of a case where default case will be exercised?

[stephan-herrmann]

Firstly this seems to apply (14.11.1.1):

A set of case elements, CE, covers a type T if one of the following cases applies:

• ...
• CE contains a type pattern with a primitive type P, and T is the wrapper class for the primitive type W, and the conversion from type W to type P is unconditionally exact (5.7.2).

Thus case int i indeed covers type Integer (with W->P being the identity conversion int->int), but "covers" doesn't imply "unconditional", so default should be allowed.

While the difference between "covers" and "unconditional" seems indeed to be null, 14.11.1.2, OTOH, explicitly states that default does not apply to null.

This sounds like the spec is saying:

• because null is possible default is allowed
• but default does not match null.

There are other places in the spec saying "A default label is permitted, but not required, when ...", so the spec "prefers" unnecessary default over omission of a necessary one. While in the case of switches over enum or a sealed type an "unnecessary" default might protect for future additions, type Integer will never contain any value that is neither convertible to int or null.

Sounds like a good question for the EG ...

but for now ecj needs to be corrected.

[stephan-herrmann]

@mpalat for the fix I had to provide a more precise implementation of TypePattern.isUnconditional() but then I wondered, if any implementation other than return false; is needed in any other class of the Pattern hierarchy. See 14.30.3

Additionally, I'm surprised that the definition of "unconditional" doesn't seem to consider presence of a guard. Did you find a connection between these somewhere? Or is that supposed to be evident from the word "unconditional"?

[mpalat]

@mpalat for the fix I had to provide a more precise implementation of TypePattern.isUnconditional() but then I wondered, if any implementation other than return false; is needed in any other class of the Pattern hierarchy. See 14.30.3
Thanks @stephan-herrmann for the fix!

Additionally, I'm surprised that the definition of "unconditional" doesn't seem to consider presence of a guard. Did you find a connection between these somewhere? Or is that supposed to be evident from the word "unconditional"?

I see the following statement in section 14.11.1 which provides a connection between unguarded and unconditional:
"A default label or a case null, default label is dominated if there is a preceding unguarded case label in the switch block with a case pattern p where p is unconditional for the type of the selector expression (14.30.3).

A case label with a case pattern that is unconditional for the type of the selector expression will, as the name suggests, match every value and so behave like a default label. A switch block can not have more than one switch label that acts like a default."
Hence we may deduce that such a case label will cover the type.

That said, the following is not spelt out explicitly in case of guarded pattern, but may have to be deduced:

• when true [ie condition is the constant true] - easy to deduce and we can consider this as unconditional

[thinking wild :) - more involved cases - when the conditional covers all possibilities ie eg: all values of ints are covered - we may not be able to do this analysis at compile time - these are anyway not expected to be spelt out in spec]

[mpalat]

Sounds like a good question for the EG ...

Yes, believe so.

[stephan-herrmann]

I see the following statement in section 14.11.1 which provides a connection between unguarded and unconditional:
"A default label or a case null, default label is dominated if there is a preceding unguarded case label in the switch block with a case pattern p where p is unconditional for the type of the selector expression (14.30.3).

So, in this situation JLS requires that a case be both unguarged and unconditional, suggesting that these are independent concepts.

Ergo: isUnconditional() should not look at isUnguarded() but leave that check to callers.

[stephan-herrmann]

For posterity: our concept of a "total pattern" (SwitchStatement.TotalPattern) is not explicit in the spec, it seems to be a short-hand for saying "unguarded and unconditional".

This should not be confused with Pattern.isTotalTypeNode, which corresponds to coversType() only.

"... A case label with a case pattern that is unconditional for the type of the selector expression will, as the name suggests, match every value and so behave like a default label. A switch block can not have more than one switch label that acts like a default."

In 14.11.1 this sentence is typeset in italics, which implies that it only serves to explain a situation that should already be defined by other parts of the spec (it's "non-normative"). This might indicate that the errors we report via ProblemReporter.duplicateTotalPattern() are only secondary errors, following another error from the normative part of the spec. In fact, all tests in our suite that report through duplicateTotalPattern() additionally report on the same line:

This case label is dominated by one of the preceding case labels

I'm removing duplicateTotalPattern() which then allows me to introduce the following separation of concerns:

• CaseStatement.resolveCasePattern will no longer report any conflicts with other cases, only record information about the current case (SwitchStatement.Exhaustive, SwitchStatement.TotalPattern, Pattern.isTotalTypeNode)
• all conflict detection already happens within SwitchStatement.resolve()
  • via caseStmt.resolveCase() we check default/total conflicts with a preceding case (where I'm renaming flagDuplicateDefault() to checkDuplicateDefault() to signal that the final checks for duplicates happen inside, not by the caller.
  • inner loop over j performs pairwise comparison to detect dominance and fully redundant duplicates (reportDuplicateCase())

[stephan-herrmann]

Closed via #2925