On type system, type equality and type containment

Recently after fixing [1], it was clear that the compiler wasn't implementing an important part of the JLS8, in particular this part related to

wildcards equality at §18.2.4:


A constraint formula of the form ‹ S = T ›, where S and T are type arguments (§4.5.1),

is reduced as follows:

If S and T are types, the constraint is reduced as described above.

If S has the form ? and T has the form ? , the constraint reduces to true.

If S has the form ? and T has the form ? extends T' , the constraint reduces to ‹ Object = T' ›.

If S has the form ? extends S' and T has the form ? , the constraint reduces to ‹ S' = Object ›.

If S has the form ? extends S' and T has the form ? extends T' , the constraint reduces to ‹ S' = T' ›.

If S has the form ? super S' and T has the form ? super T' , the constraint reduces to ‹ S' = T' ›.

Otherwise, the constraint reduces to false.


This meant that the compiler implementation managed to provide the right output to a number of regression and JCK tests without actually implementing

a part of the spec, probably for years!!! This called my attention and after some research I focused on 3 aspects of the type system implementation:


IMO type containment implementation was supplying the correct output for the cases related to the missing implementation of §18.2.4, at least for most cases.

But then this implies that something wasn't right in the implementations of type equality, type containment or in the interaction between them.


Are these types the same? is not the question, the question is if they are strictly or loosely the same

Type equality verification is implemented in the compiler using two visitors at class Types: isSameTypeStrict and isSameTypeLoose. I lack the background

to know when this duality first appear of if it was there since the first implementation of the type system. The thing is that it would be desirable, if possible,

to have just one implementation of the type equality check. The fact that a section of JLS8 §18.2.4 wasn't implemented at all made me suppose that this

was probably a missing part toward that goal; that probably other parts of the specification are not fully or correctly implemented and that this lack of

synchronization created the need for this duality. At least I considered interesting investigating to which point this duality was really needed and necessary.


Stressing the strict-loose duality

In order to check to what extend the strict-loose duality was necessary I started by removing as much invocations to the loose visitor as possible. In general it

seems like the loose visitor is very used in javac, 70+ times. There are some cases that clearly don't need a loose check and use it. So the first step was to

remove as much invocations of the loose visitor as possible. The result of this experiment was a patch that led to the removal of most of the invocations, to less than 5.

Of these remaining uses, there is a special one at the 'containsType' visitor at class Types. This visitor in used by method containsType(Type, Type) which checks if

the first argument contains the second. Removing this invocation provokes a cascade of issues. So let's move the focus to javac's type containment implementation.


Type containment and it's implementation

Type containment is defined in the JLS8 at §4.5.1. From there we can read:


A type argument T1 is said to contain another type argument T2, written T2 <= T1,

if the set of types denoted by T2 is provably a subset of the set of types denoted

by T1 under the reflexive and transitive closure of the following rules (where <:

denotes subtyping (§4.10)):


? extends T <= ? extends S if T <: S

? extends T <= ?

? super T <= ? super S if S <: T

? super T <= ?

? super T <= ? extends Object

T <= T

T <= ? extends T

T <= ? super T


But this is not the only place where the JLS8 mentions type containment. At §18.2.3, we have:


A constraint formula of the form ‹ S <= T ›, where S and T are type arguments

(§4.5.1), is reduced as follows:

If T is a type:

If S is a type, the constraint reduces to ‹ S = T ›.

If S is a wildcard, the constraint reduces to false.

If T is a wildcard of the form ? , the constraint reduces to true.

If T is a wildcard of the form ? extends T' :

If S is a type, the constraint reduces to ‹ S <: T' ›.

If S is a wildcard of the form ? , the constraint reduces to ‹ Object <: T' ›.

If S is a wildcard of the form ? extends S' , the constraint reduces to ‹ S' <: T' ›.

If S is a wildcard of the form ? super S' , the constraint reduces to ‹ Object= T' ›.

If T is a wildcard of the form ? super T' :

If S is a type, the constraint reduces to ‹ T' <: S ›.

If S is a wildcard of the form ? super S' , the constraint reduces to ‹ T' <: S' ›.

Otherwise, the constraint reduces to false.


Putting everything together, reordering and using the most general version of a rule when more than one is available, we get the following set of rules:


  1. T <= S if T = S; this one implies that T <= T

  2. T <= ?; for completeness as this rule can be inferred from ? extends T <= ? and T <= ? extends T, implying that T <= ?

  3. ? extends T <= ?

  4. ? super T <= ?

  5. T <= ? extends S if T <: S; this one implies that T <= ? extends T

  6. ? extends T <= ? extends S if T <: S; this one implies that ? <= ? extends S if Object <: S

  7. ? super T <= ? extends S if S = Object; this one implies that ? super T <= ? extends Object

  8. T <= ? super S if S <: T; this implies that T <= ? super T

  9. ? super T <= ? super S if S <: T


But are all these rules correctly implemented in javac? After giving it a try with vanilla javac, we can check that for rules I and II, the compiler behaves

as expected. For rule III, we found the special case of ? extends Object <= ? and ? <= ? extends Object as expected. For other cases the compiler

behaves as expected.


No surprises for rules IV, V, VI, VII, and IX. In the case of rule VIII, we have that these rules hold for javac:


Object <= ? super Object

? super Object <= Object


this implies that Object is equal to ? super Object, this seems wrong. I don't know if this is one of the areas for which javac has decided to go for a more

flexible approach than the one defined by the specification or if this is just a bug, more likely. Unfortunately this is not the only case for which javac and

the specification differs. The other case I have found is when we enter into the world of captured types. I found that these rules hold for javac:


capture of ? <= ?

capture of ? super T <= ? super T

capture of ? extends T <= ? extends T


Again this doesn't appear explicitly in the specification, IMO this is another case in which javac has gone for a more 'flexible', another bug?, but not

specified approach.


The dependency between type containment and the type equality loose visitor

As it can be seen from the type containment rules if two types are equal then they contain each other. Right now this is expressed in javac

by an invocation to the type equality loose visitor. I tried to change this into an invocation to the type equality strict visitor. By doing this and after several

tests I discovered the incongruence between the specification and the compiler in the type containment area. I believe that if it's possible to use the strict

visitor from the type containment implementation then we can eliminate the strict-loose type equality visitors' duality in the compiler. This should add more

clarity to our type system and pave the way for future improvements in the area.


I have done many experiments, not commented here. I haven't included any patch in order to focus the discussion on the javac-specification incongruence

but if there is interest I can provide the patches I have been working with. I believe that there is a lot of room for cleaning, improving, even for a JEP not for 9

of course, which I can write using part of this material but as there are incongruences between javac and the specification it's hard to make decisions

before we have a clear idea of what the right behavior of the compiler should be.


I'm greedy for comments :)


[1] https://bugs.openjdk.java.net/browse/JDK-8159970