Does JLS tell if this program is legal?

[Maurizio Cimadamore]

Hi Stephan,
commments below:

On 21/05/2024 20:49, Stephan Herrmann wrote:
> or a moment I was tempted to challenge the part "if Si and Ti are 
> types (not wildcards)", perhaps also Inner<?> would be a reason not to 
> create that constraint, but I gave up that idea when I discovered the 
> following solution:
>
> * One<X> is a supertype of S / Y (as the 2nd superinterface of Two<X>)
> * One<?> is a supertype of T / One<?> (identity)
> * S1 = X
> * T1 = ?
> * NO new constraint is created
> * inference succeeds to instantiate W#0 = Y
>
> In my understanding the weakness here is in "there *exists* a 
> supertype of S ... (for *some* generic class or interface, G)". Which 
> seems to imply once a compiler finds one witness for the conditions of 
> that supertype, that's the only thing that needs to be looked at for 
> this sentence. In fact, the choice which witness is found by ecj can 
> be toggled by swapping the order of Two's superinterfaces.
>
> Now declaration order is probably a bad thing to decide about 
> accept/reject. So which criterion should be used to select G?
>
> My current implementation draft prefers a "more specific" supertype, 
> which suffices to select One<X> instead of Super<Inner<X>> in this 
> particular case.
>
> Does javac perform an explicit selection in this situation, or does it 
> "just happen" to find the more helpful supertype?

The javac code responsible for this is here:

https://github.com/openjdk/jdk/blob/master/src/jdk.compiler/share/classes/com/sun/tools/javac/comp/Infer.java#L1000

For every pair of upper bounds, we compute the set of _all_ the common 
supertypes, and check them all. So, javac doesn't pick one randomly.

But, as you can see from the code, javac does leave out type equality 
test if either type being tested is a wildcard (as per the JLS text).

The way I read the text is different from the way you read it - I think 
it's a very declarative way to state a rule - e.g. the incorporation 
rule just say that if there exist a pair of super type such and such, 
then a new equality constraint can be derived. Algorithnically, this 
means that _every_ pair of supertype such and such must be considered. I 
think it's a presentation style, and doesn't strike me as an issue in 
the JLS.

Maurizio