Java SE > Java SE Specifications > Java Language Specification
Table of Contents
A variety of compile-time analyses require reasoning about types that are not yet known. Principal among these are generic method applicability testing (§18.5.1) and generic method invocation type inference (§18.5.2). In general, we refer to the process of reasoning about unknown types as type inference.
At a high level, type inference can be decomposed into three processes:
Reduction takes a compatibility assertion about an expression or type, called a constraint formula, and reduces it to a set of bounds on inference variables. Often, a constraint formula reduces to other constraint formulas, which must be recursively reduced. A procedure is followed to identify these additional constraint formulas and, ultimately, to express via a bound set the conditions under which the choices for inferred types would render each constraint formula true.
Incorporation maintains a set of inference variable bounds, ensuring that these are consistent as new bounds are added. Because the bounds on one variable can sometimes impact the possible choices for another variable, this process propagates bounds between such interdependent variables.
Resolution examines the bounds on an inference variable and determines an instantiation that is compatible with those bounds. It also decides the order in which interdependent inference variables are to be resolved.
These processes interact closely: reduction can trigger incorporation; incorporation may lead to further reduction; and resolution may cause further incorporation.
§18.1 more precisely defines the concepts used as intermediate results and the notation used to express them.
§18.2 describes reduction in detail.
§18.3 describes incorporation in detail.
§18.4 describes resolution in detail.
§18.5 defines how these inference tools are used to solve certain compile-time analysis problems.
In comparison to the Java SE 7 Edition of The Java® Language Specification, important changes to inference include:
Adding support for lambda expressions and method references as method invocation arguments.
Generalizing to define inference in terms of poly expressions, which may not have well-defined types until after inference is complete. This has the notable effect of improving inference for nested generic method and diamond constructor invocations.
Describing how inference is used to handle wildcard-parameterized functional interface target types and most specific method analysis.
Clarifying the distinction between invocation applicability testing (which involves only the invocation arguments) and invocation type inference (which incorporates a target type).
Delaying resolution of all inference variables, even those with lower bounds, until invocation type inference, in order to get better results.
Improving inference behavior for interdependent (or self-dependent) variables.
Eliminating bugs and potential sources of confusion. This revision more carefully and precisely handles the distinction between specific conversion contexts and subtyping, and describes reduction by paralleling the corresponding non-inference relations. Where there are intentional departures from the non-inference relations, these are explicitly identified as such.
Laying a foundation for future evolution: enhancements to or new applications of inference will be easier to integrate into the specification.
This section defines inference variables, constraint formulas, and bounds, as the terms will be used throughout this chapter. It also presents notation.
Inference variables are meta-variables for types - that is, they are special names that allow abstract reasoning about types. To distinguish them from type variables, inference variables are represented with Greek letters, principally α.
The term "type" is used loosely in this chapter to include type-like syntax that contains inference variables. The term proper type excludes such "types" that mention inference variables. Assertions that involve inference variables are assertions about every proper type that can be produced by replacing each inference variable with a proper type.
Constraint formulas are assertions of compatibility or subtyping that may involve inference variables. The formulas may take one of the following forms:
‹Expression → T›: An expression is compatible in a loose invocation context with type T (§5.3).
‹S → T›: A type S is compatible in a loose invocation context with type T (§5.3).
‹S <: T›: A reference type S is a
subtype of a reference type T
(§4.10).
‹S <= T›: A type argument S is
contained by a type argument T
(§4.5.1).
‹S = T›: A type S is the same as a type T (§4.3.4), or a type argument S is the same as type argument T.
‹LambdaExpression →throws T›: The checked
exceptions thrown by the body of the LambdaExpression are
declared by the throws clause of the function type derived
from T.
‹MethodReference →throws T›: The checked
exceptions thrown by the referenced method are declared by the
throws clause of the function type derived from T.
Examples of constraint formulas:
From Collections.singleton("hi"),
we have the constraint formula ‹"hi"
→ α›. Through reduction, this will become the
constraint formula: ‹String <:
α›.
From Arrays.asList(1, 2.0),
we have the constraint formulas ‹1 →
α› and ‹2.0 →
α›. Through reduction, these will become the
constraint formulas ‹int → α› and
‹double → α›, and then ‹Integer
<: α› and ‹Double <:
α›.
From the target type of the constructor
invocation List<Thread> lt = new
ArrayList<>(), we have the constraint formula
‹ArrayList<α>
→ List<Thread>›. Through
reduction, this will become the constraint formula
‹α <= Thread›, and then
‹α = Thread›.
During the inference process, a set of bounds on inference variables is maintained. A bound has one of the following forms:
S = T, where at least one of S or T is an inference variable: S is the same as T.
S <: T, where at least one of S or T is an
inference variable: S is a subtype of T.
G<α1, ..., αn> =
capture(G<A1, ..., An>): The variables
α1, ..., αn represent the result of capture
conversion (§5.1.10) applied to
G<A1, ..., An> (where A1, ..., An may be
types or wildcards and may mention inference variables).
throws α: The inference variable α appears in a
throws clause.
A bound is satisfied by an inference variable substitution if, after applying the substitution, the assertion is true. The bound false can never be satisfied.
Some
bounds relate an inference variable to a proper type. Let T be a
proper type. Given a bound of the form α = T or T = α,
we say T is an instantiation of α.
Similarly, given a bound of the form α <: T, we say T
is a proper upper bound of α, and given a
bound of the form T <: α, we say T is
a proper lower bound of α.
Other
bounds relate two inference variables, or an inference variable to a
type that contains inference variables. Such bounds, of the form S =
T or S <: T, are called
dependencies.
A bound
of the form G<α1, ..., αn> =
capture(G<A1, ..., An>) indicates that α1,
..., αn are placeholders for the results of capture
conversion. This is necessary because capture conversion can only be
performed on a proper type, and the inference variables in A1, ...,
An may not yet be resolved.
A bound
of the form throws α is purely informational: it directs
resolution to optimize the instantiation of α so that, if
possible, it is not a checked exception type.
An important intermediate result of inference is a bound set. It is sometimes convenient to refer to an empty bound set with the symbol true; this is merely out of convenience, and the two are interchangeable.
Examples of bound sets:
{ α = String } contains a single bound,
instantiating α as String.
{ Integer <: α, Double
<: α, α <: Object } describes two
proper lower bounds and one proper upper bound for
α.
{ α
<: Iterable<?>, β <:
Object, α
<: List<β> }
describes a proper upper bound for each of α and β,
along with a dependency between them.
{ } contains no bounds nor dependencies, and can be referred to as true.
{ false } expresses the fact that no satisfactory instantiation exists.
When inference begins, a bound set is typically generated from a list of type parameter declarations P1, ..., Pp and associated inference variables α1, ..., αp. Such a bound set is generated as follows. For each l (1 ≤ l ≤ p):
If
Pl has no TypeBound, the
bound αl <: Object appears
in the set.
Otherwise, for each type T delimited by & in
the TypeBound, the bound αl <:
T[P1:=α1, ..., Pp:=αp] appears
in the set; if this results in no proper upper bounds for
αl (only dependencies), then the bound αl <:
Object also appears in the set.
Reduction is the process by which a set of constraint formulas (§18.1.2) is simplified to produce a bound set (§18.1.3).
Each constraint formula is considered in turn. The rules in this section specify how the formula is reduced to one or both of:
Reduction completes when no further constraint formulas remain to be reduced.
The results of a reduction step are always soundness-preserving: if an inference variable instantiation satisfies the reduced constraints and bounds, it will also satisfy the original constraint. On the other hand, reduction is not completeness-preserving: there may exist inference variable instantiations that satisfy the original constraint but do not satisfy a reduced constraint or bound. This is due to inherent limitations of the algorithm, along with a desire to avoid undue complexity. One effect is that there are expressions for which type argument inference fails to find a solution, but that can be well-typed if the programmer explicitly inserts appropriate types.
A constraint formula of the form ‹Expression → T› is reduced as follows:
If T is a proper type, the constraint reduces to true if the expression is compatible in a loose invocation context with T (§5.3), and false otherwise.
Otherwise, if the expression is a standalone expression (§15.2) of type S, the constraint reduces to ‹S → T›.
Otherwise, the expression is a poly expression (§15.2). The result depends on the form of the expression:
If the expression is a parenthesized expression of the form
( Expression' ), the constraint reduces to
‹Expression' → T›.
If the expression is a class instance creation expression or a method invocation expression, the constraint reduces to the bound set B3 which would be used to determine the expression's compatibility with target type T, as defined in §18.5.2.1. (For a class instance creation expression, the corresponding "method" used for inference is defined in §15.9.3.)
This bound set may contain new inference variables, as well as dependencies between these new variables and the inference variables in T.
If the expression is a conditional expression of the form
e1 ? e2 : e3, the constraint reduces to two
constraint formulas, ‹e2 → T› and
‹e3 → T›.
If the expression is a lambda expression or a method reference expression, the result is specified below.
By treating nested generic method invocations as poly expressions, we improve the behavior of inference for nested invocations. For example, the following is illegal in Java SE 7 but legal in Java SE 8:
ProcessBuilder b = new ProcessBuilder(Collections.emptyList()); // ProcessBuilder's constructor expects a List<String>
When both the outer and the nested invocation require inference, the problem is more difficult. For example:
List<String> ls = new ArrayList<>(Collections.emptyList());
Our approach is to "lift" the bounds inferred for
the nested invocation (simply { α <: Object } in the
case of emptyList) into the outer inference process
(in this case, trying to infer β where the constructor is for
type ArrayList<β>). We also
infer dependencies between the nested inference variables and the
outer inference variables (the constraint
‹List<α>
→ Collection<β>›
would reduce to the dependency α = β). In this way,
resolution of the inference variables in the nested invocation can
wait until additional information can be inferred from the outer
invocation (based on the assignment target, β = String).
A constraint formula of the form ‹LambdaExpression → T›, where T mentions at least one inference variable, is reduced as follows:
If T is not a functional interface type (§9.8), the constraint reduces to false.
Otherwise, let T' be the ground target type derived from
T, as specified in §15.27.3. If
§18.5.3 is used to derive a functional
interface type which is parameterized, then the test that
F<A'1, ..., A'm> is a subtype of
F<A1, ..., Am> is not performed (instead, it
is asserted with a constraint formula below). Let the target
function type for the lambda expression be the function type of
T'. Then:
If no valid function type can be found, the constraint reduces to false.
Otherwise, the congruence of LambdaExpression with the target function type is asserted as follows:
If the number of lambda parameters differs from the number of parameter types of the function type, the constraint reduces to false.
If the lambda expression is implicitly typed and one or more of the function type's parameter types is not a proper type, the constraint reduces to false.
This condition never arises in practice, due to the handling of implicitly typed lambda expressions in §18.5.1 and the substitution applied to the target type in §18.5.2.2.
If the function type's result is void and the lambda
body is neither a statement expression nor a
void-compatible block, the constraint reduces to
false.
If the function type's result is not void and the
lambda body is a block that is not value-compatible, the
constraint reduces to false.
Otherwise, the constraint reduces to all of the following constraint formulas:
If the lambda parameters have explicitly declared types
F1, ..., Fn and the function type has parameter types
G1, ..., Gn, then (i) for all i (1 ≤ i
≤ n), ‹Fi = Gi›, and (ii)
‹T' <: T›.
If the function type's return type is a (non-void) type
R, assume the lambda's parameter types are the same as the
function type's parameter types. Then:
If R is a proper type, and if the lambda body or some result expression in the lambda body is not compatible in an assignment context with R, then false.
Otherwise, if R is not a proper type, then where the
lambda body has the form Expression, the constraint
‹Expression → R›; or where the
lambda body is a block with result expressions e1,
..., em, for all i (1 ≤ i ≤ m),
‹ei → R›.
The key piece of information to derive from a compatibility constraint involving a lambda expression is the set of bounds on inference variables appearing in the target function type's return type. This is crucial, because functional interfaces are often generic, and many methods operating on these types are generic, too.
In the simplest case, a lambda expression may simply provide a lower bound for an inference variable:
<T> List<T> makeThree(Factory<T> factory) { ... }
String s = makeThree(() -> "abc").get(2);
In more complex cases, a result expression may be a poly expression - perhaps even another lambda expression - and so the inference variable might be passed through multiple constraint formulas with different target types before a bound is produced.
Most of the work described in this section precedes assertions about the result expressions; its purpose is to derive the lambda expression's function type, and to check for expressions that are clearly disqualified from compatibility.
We do not attempt to produce
bounds on inference variables that appear in the target function
type's throws clause. This is because exception containment is not
part of compatibility (§15.27.3) - in particular,
it must not influence method applicability
(§18.5.1). However, we do
get bounds on these variables later, because invocation type inference
(§18.5.2.2) produces exception containment
constraint formulas (§18.2.5).
Note that if the target type is an inference variable, or if the target type's parameter types contain inference variables, we produce false. During invocation type inference (§18.5.2.2), extra substitutions are performed in order to instantiate these inference variables, thus avoiding this scenario. (In other words, reduction will, in practice, never be "invoked" with a target type of one of these forms.)
Finally, note that the result expressions of a
lambda expression are required by §15.27.3 to be
compatible in an assignment context with the target type's return
type, R. If R is a proper type, such as Byte derived
from Function, then
assignability is easy enough to test, and reduction does so above. If
R is not a proper type, such as α derived from
<α,Byte>Function, then we
make the simplifying assumption above that loose invocation
compatibility will be sufficient. The difference between assignment
compatibility and loose invocation compatibility is that only
assignment allows narrowing of constant expressions, such
as <String,α>Byte b = 100;. Consequently, our simplifying
assumption is not completeness-preserving: given target return type
α and an integer literal result expression
100, it is conceivable that α could be
instantiated to Byte, but reduction will not in fact produce such a
bound.
A constraint formula of the form ‹MethodReference → T›, where T mentions at least one inference variable, is reduced as follows:
If T is not a functional interface type, or if T is a functional interface type that does not have a function type (§9.9), the constraint reduces to false.
Otherwise, if there does not exist a potentially applicable method for the method reference when targeting T, the constraint reduces to false.
Otherwise, if the method reference is exact (§15.13.1), then let P1, ..., Pn be the parameter types of the function type of T, and let F1, ..., Fk be the parameter types of the potentially applicable method. The constraint reduces to a new set of constraints, as follows:
In the special case where n = k+1, the parameter
of type P1 is to act as the target reference of the
invocation. The method reference expression necessarily has
the form ReferenceType ::
[TypeArguments] Identifier. The constraint
reduces to ‹P1 <: ReferenceType› and,
for all i (2 ≤ i ≤ n), ‹Pi
→ Fi-1›.
In all other cases, n = k, and the constraint reduces to, for all i (1 ≤ i ≤ n), ‹Pi → Fi›.
If the function type's result is not void, let R be its
return type. Then, if the result of the potentially
applicable compile-time declaration is void, the
constraint reduces to false. Otherwise, the constraint
reduces to ‹R' → R›, where R' is the
result of applying capture conversion
(§5.1.10) to the return type of the
potentially applicable compile-time declaration.
Otherwise, the method reference is inexact, and:
If one or more of the function type's parameter types is not a proper type, the constraint reduces to false.
This condition never arises in practice, due to the handling of inexact method references in §18.5.1 and the substitution applied to the target type in §18.5.2.2.
Otherwise, a search for a compile-time declaration is performed, as specified in §15.13.1. If there is no compile-time declaration for the method reference, the constraint reduces to false. Otherwise, there is a compile-time declaration, and: (let R be the result of the function type)
Otherwise, if the method reference expression elides TypeArguments, and the compile-time declaration is a generic method, and the return type of the compile-time declaration mentions at least one of the method's type parameters, then:
If R mentions one of the type parameters of the function type, the constraint reduces to false.
In this case, a constraint in terms of R might lead an inference variable to be bound by an out-of-scope type variable. Since instantiating an inference variable with an out-of-scope type variable is nonsensical, we prefer to avoid the situation by giving up immediately whenever the possibility arises. This simplification is not completeness-preserving.
If R does not mention one of the type parameters of the function type, then the constraint reduces to the bound set B3 which would be used to determine the method reference's compatibility when targeting the return type of the function type, as defined in §18.5.2.1. B3 may contain new inference variables, as well as dependencies between these new variables and the inference variables in T.
The strategy used to determine a return type for a generic referenced method follows the pattern used earlier in this section for generic method invocations. This may involve "lifting" bounds into the outer context and inferring dependencies between the two sets of inference variables.
Otherwise, let R' be the result of applying capture
conversion (§5.1.10) to the return
type of the invocation type (§15.12.2.6)
of the compile-time declaration.
If R' is void, the constraint reduces to false;
otherwise, the constraint reduces to ‹R' →
R›.
A constraint formula of the form ‹S → T› is reduced as follows:
If S and T are proper types, the constraint reduces to true if S is compatible in a loose invocation context with T (§5.3), and false otherwise.
Otherwise, if S is a primitive type, let S' be the result of applying boxing conversion (§5.1.7) to S. Then the constraint reduces to ‹S' → T›.
Otherwise, if T is a primitive type, let T' be the result of applying boxing conversion (§5.1.7) to T. Then the constraint reduces to ‹S = T'›.
Otherwise, if T is a parameterized type of the form
G<T1, ..., Tn>, and there exists no type of
the form G<...> that is a supertype of S, but
the raw type G is a supertype of S, then the constraint
reduces to true.
Otherwise, if T is an array type of the form G<T1,
..., Tn>[]k, and
there exists no type of the form
G<...>[]k
that is a supertype of S, but the raw type
G[]k is a supertype of S,
then the constraint reduces to true. (The notation
[]k indicates an array type
of k dimensions.)
The fourth and fifth cases are implicit uses of unchecked conversion (§5.1.9). These, along with any use of unchecked conversion in the first case, may result in compile-time unchecked warnings, and may influence a method's invocation type (§15.12.2.6).
Boxing T to T' is not
completeness-preserving; for example, if T were long, S might be
instantiated to Integer, which is not a subtype of Long but could
be unboxed and then widened to long. We avoid this problem in most
cases by giving special treatment to inference-variable return types
that we know are already constrained to be certain boxed primitive
types; see §18.5.2.1.
Similarly, the treatment of unchecked conversion sacrifices completeness in cases in which T is not a parameterized type (for example, if T is an inference variable). It is not usually clear in such situations whether the unchecked conversion is necessary or not. Since unchecked conversions introduce unchecked warnings, inference prefers to avoid them unless it is clearly necessary.
A
constraint formula of the form ‹S <: T› is
reduced as follows:
If S and T are proper types, the constraint reduces to true if S is a subtype of T (§4.10), and false otherwise.
Otherwise, if S is the null type, the constraint reduces to true.
Otherwise, if T is the null type, the constraint reduces to false.
Otherwise, if S is an inference variable, α, the
constraint reduces to the bound α <: T.
Otherwise, if T is an inference variable, α, the
constraint reduces to the bound S <: α.
Otherwise, the constraint is reduced according to the form of T:
If T is a parameterized class or interface type, or an
inner class type of a parameterized class or interface type
(directly or indirectly), let A1, ..., An be the type
arguments of T. Among the supertypes of S, a
corresponding class or interface type is identified, with
type arguments B1, ..., Bn. If no such type exists, the
constraint reduces to false. Otherwise, the constraint
reduces to the following new constraints: for all i (1
≤ i ≤ n), ‹Bi <=
Ai›.
If T is any other class or interface type, then the constraint reduces to true if T is among the supertypes of S, and false otherwise.
If T is an array type, T'[], then among the
supertypes of S that are array types, a most specific type
is identified, S'[] (this may be S
itself). If no such array type exists, the constraint
reduces to false. Otherwise:
If T is an intersection type, I1 & ... & In,
the constraint reduces to the following new constraints: for
all i (1 ≤ i ≤ n), ‹S
<: Ii›.
A
constraint formula of the form ‹S <= T›, where
S and T are type arguments (§4.5.1), is
reduced as follows:
A constraint formula of the form ‹S = T›, where S and T are types, is reduced as follows:
If S and T are proper types, the constraint reduces to true if S is the same as T (§4.3.4), and false otherwise.
Otherwise, if S or T is the null type, the constraint reduces to false.
Otherwise, if S is an inference variable, α, and T is not a primitive type, the constraint reduces to the bound α = T.
Otherwise, if T is an inference variable, α, and S is not a primitive type, the constraint reduces to the bound S = α.
Otherwise, if S and T are class or interface types with the same erasure, where S has type arguments B1, ..., Bn and T has type arguments A1, ..., An, the constraint reduces to the following new constraints: for all i (1 ≤ i ≤ n), ‹Bi = Ai›.
Otherwise, if S and T are array types, S'[]
and T'[], the constraint reduces to
‹S' = T'›.
Otherwise, if S and T are intersection types, a correspondence between the elements of S and the elements of T is established. An element of S, Si, corresponds to an element of T, Tj, if Si and Tj are either the same type, or both parameterizations of the same generic class or interface, or both array types.
If each element of S corresponds to exactly one element of T, and vice versa, then the constraint reduces to the following new constraints: for each element Si of S and the corresponding element Tj of T, ‹Si = Tj›. If not, the constraint reduces to false.
This rule does not accommodate inference variables appearing directly as elements of an intersection type (rather than nested in a parameterized type). Due to the restrictions on type parameter declarations (§4.4), such intersection types do not arise in practice.
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'›.
A constraint formula of the form ‹LambdaExpression →throws T› is reduced as follows:
If T is not a functional interface type (§9.8), the constraint reduces to false.
Otherwise, let the target function type for the lambda expression be determined as specified in §15.27.3. If no valid function type can be found, the constraint reduces to false.
Otherwise, if the lambda expression is implicitly typed, and one or more of the function type's parameter types is not a proper type, the constraint reduces to false.
This condition never arises in practice, due to the substitution applied to the target type in §18.5.2.2.
Otherwise, if the function type's return type is neither void
nor a proper type, the constraint reduces to false.
This condition never arises in practice, due to the substitution applied to the target type in §18.5.2.2.
Otherwise, let E1, ..., En be the types in the function
type's throws clause that are not proper
types. If the lambda expression is implicitly typed, let its
parameter types be the function type's parameter types. If the
lambda body is a poly expression or a block containing a poly
result expression, let the targeted return type be the function
type's return type. Let X1, ..., Xm be the checked exception
types that the lambda body can throw
(§11.2). Then there are two cases:
If n = 0 (the function type's throws clause
consists only of proper types), then if there exists some
i (1 ≤ i ≤ m) such that Xi is not a
subtype of any proper type in the throws clause, the
constraint reduces to false; otherwise, the constraint
reduces to true.
If n > 0, the constraint reduces to a set of
subtyping constraints: for all i (1 ≤ i ≤
m), if Xi is not a subtype of any proper type in the
throws clause, then the constraints include, for all
j (1 ≤ j ≤ n), ‹Xi <:
Ej›. In addition, for all j (1 ≤ j
≤ n), the constraint reduces to the bound throws
Ej.
A constraint formula of the form ‹MethodReference →throws T› is reduced as follows:
If T is not a functional interface type, or if T is a functional interface type but does not have a function type (§9.9), the constraint reduces to false.
Otherwise, let the target function type for the method reference expression be the function type of T. If the method reference is inexact (§15.13.1) and one or more of the function type's parameter types is not a proper type, the constraint reduces to false.
Otherwise, if the method reference is inexact and the function
type's result is neither void nor a proper type, the
constraint reduces to false.
Otherwise, let E1, ..., En be the types in the function
type's throws clause that are not proper
types. Let X1, ..., Xm be the checked exceptions in the
throws clause of the invocation type of the method reference's
compile-time declaration (§15.13.2) (as
derived from the function type's parameter types and return
type). Then there are two cases:
If n = 0 (the function type's throws clause
consists only of proper types), then if there exists some
i (1 ≤ i ≤ m) such that Xi is not a
subtype of any proper type in the throws clause, the
constraint reduces to false; otherwise, the constraint
reduces to true.
If n > 0, the constraint reduces to a set of
subtyping constraints: for all i (1 ≤ i ≤
m), if Xi is not a subtype of any proper type in the
throws clause, then the constraints include, for all
j (1 ≤ j ≤ n), ‹Xi <:
Ej›. In addition, for all j (1 ≤ j
≤ n), the constraint reduces to the bound throws
Ej.
Constraints on checked exceptions are handled separately from constraints on return types, because return type compatibility influences applicability of methods (§18.5.1), while exceptions only influence the invocation type after overload resolution is complete (§18.5.2). This could be simplified by including exception compatibility in the definition of lambda expression compatibility (§15.27.3), but this would lead to possibly surprising cases in which exceptions that can be thrown by an explicitly typed lambda body change overload resolution.
The exceptions thrown by a lambda body cannot be
determined until (i) the parameter types of the lambda are known, and
(ii) the target type of result expressions in the body is known. (The
second requirement is to account for generic method invocations in
which, for example, the same type parameter appears in the return type
and the throws clause.) Hence, we require both of these, as derived
from the target type T, to be proper types.
One consequence is that lambda expressions returned from other lambda expressions cannot generate constraints from their thrown exceptions. These constraints can only be generated from top-level lambda expressions.
Note that the handling of the case in which more
than one inference variable appears in a function type's throws
clause is not completeness-preserving. Either variable may, on its
own, satisfy the constraint that each checked exception be declared,
but we cannot be sure which one is intended. So, for predictability,
we constrain them both.
As bound sets are generated and grown during inference, it is possible that new bounds can be inferred based on the assertions of the original bounds. The process of incorporation identifies these new bounds and adds them to the bound set.
Incorporation can happen in two scenarios. One scenario is that the bound set contains complementary pairs of bounds; this implies new constraint formulas, as specified in §18.3.1. The other scenario is that the bound set contains a bound involving capture conversion; this implies new bounds and may imply new constraint formulas, as specified in §18.3.2. In both scenarios, any new constraint formulas are reduced, and any new bounds are added to the bound set. This may trigger further incorporation; ultimately, the set will reach a fixed point and no further bounds can be inferred.
If incorporation of a bound set has reached a fixed point, and the set does not contain the bound false, then the bound set has the following properties:
For each combination of a proper lower bound L and a proper
upper bound U of an inference variable, L <:
U.
If every inference variable mentioned by a bound has an instantiation, the bound is satisfied by the corresponding substitution.
Given a dependency α = β, every bound of α matches a bound of β, and vice versa.
Given a dependency α <: β, every lower bound
of α is a lower bound of β, and every upper bound of
β is an upper bound of α.
The assertion that incorporation reaches a fixed point oversimplifies the matter slightly. Building on the work of Kennedy and Pierce, On Decidability of Nominal Subtyping with Variance, this property can be proven by making the argument that the set of types that may appear in the bound set is finite. The argument relies on two assumptions:
New capture variables are not generated when reducing subtyping constraints (§18.2.3).
Expansive inheritance paths are not pursued.
This specification does not currently guarantee these properties (it is imprecise about the handling of wildcards when reducing subtyping constraints, and does not detect expansive inheritance paths), but may do so in a future version. (This is not a new problem: the Java subtyping algorithm is also at risk of non-termination.)
(In this section, S and T are inference variables or types, and U is a proper type. For conciseness, a bound of the form α = T may also match a bound of the form T = α.)
When a bound set contains a pair of bounds that match one of the following rules, a new constraint formula is implied:
When a bound set contains a pair of bounds α <: S and
α <: T, and there exists a supertype of S of the form
G<S1, ..., Sn> and a supertype of T of the form
G<T1, ..., Tn> (for some generic class or
interface, G), then for all i (1 ≤ i ≤ n), if
Si and Ti are types (not wildcards), the constraint formula
‹Si = Ti› is implied.
When a
bound set contains a bound of the form G<α1, ...,
αn> = capture(G<A1, ..., An>), new
bounds are implied and new constraint formulas may be implied, as
follows.
Let P1,
..., Pn represent the type parameters of G and let B1, ..., Bn
represent the bounds of these type parameters. Let θ represent
the substitution [P1:=α1, ..., Pn:=αn].
Let R be a type that is not an inference
variable (but is not necessarily a proper type).
A set of bounds on α1, ..., αn is implied, generated from the declared bounds of P1, ..., Pn as specified in §18.1.3.
In addition, for all i (1 ≤ i ≤ n):
Given a bound set that does not contain the bound false, a subset of the inference variables mentioned by the bound set may be resolved. This means that a satisfactory instantiation may be added to the set for each inference variable, until all the requested variables have instantiations.
Dependencies in the bound set may require that the variables be resolved in a particular order, or that additional variables be resolved. Dependencies are specified as follows:
Given a bound of one of the following forms, where T is either an inference variable β or a type that mentions β:
If α appears on the left-hand side of another bound of the
form G<..., α, ...> =
capture(G<...>), then β depends on the
resolution of α. Otherwise, α depends on the
resolution of β.
An inference variable α appearing on the left-hand side of
a bound of the form G<..., α, ...> =
capture(G<...>) depends on the resolution of
every other inference variable mentioned in this bound (on both
sides of the = sign).
An inference variable α depends on the resolution of an inference variable β if there exists an inference variable γ such that α depends on the resolution of γ and γ depends on the resolution of β.
An inference variable α depends on the resolution of itself.
Given a set of inference variables to resolve, let V be the union of this set and all variables upon which the resolution of at least one variable in this set depends.
If every variable in V has an instantiation, then resolution succeeds and this procedure terminates.
Otherwise, let { α1, ..., αn } be a non-empty subset of uninstantiated variables in V such that (i) for all i (1 ≤ i ≤ n), if αi depends on the resolution of a variable β, then either β has an instantiation or there is some j such that β = αj; and (ii) there exists no non-empty proper subset of { α1, ..., αn } with this property. Resolution proceeds by generating an instantiation for each of α1, ..., αn based on the bounds in the bound set:
If the bound set does not contain a bound of the form
G<..., αi, ...> =
capture(G<...>) for all i (1 ≤ i
≤ n), then a candidate instantiation Ti is defined
for each αi:
If αi has one or more proper
lower bounds, L1, ..., Lk, then Ti = lub(L1, ...,
Lk) (§4.10.4).
Otherwise, if the bound set contains throws αi, and
each proper upper bound of αi is a supertype of
RuntimeException, then Ti = RuntimeException.
Otherwise, where αi has proper upper bounds U1, ..., Uk, Ti = glb(U1, ..., Uk) (§5.1.10).
The bounds α1 = T1, ..., αn = Tn are incorporated with the current bound set.
If the result does not contain the bound false, then the result becomes the new bound set, and resolution proceeds by selecting a new set of variables to instantiate (if necessary), as described above.
Otherwise, the result contains the bound false, so a second attempt is made to instantiate { α1, ..., αn } by performing the step below.
If the bound set contains a bound of the form G<...,
αi, ...> = capture(G<...>) for some
i (1 ≤ i ≤ n), or;
If the bound set produced in the step above contains the bound false;
then let Y1, ..., Yn be fresh type variables whose bounds are as follows:
For all i (1 ≤ i ≤ n), if αi
has one or more proper lower bounds
L1, ..., Lk, then let the lower bound of Yi be
lub(L1, ..., Lk); if not, then Yi has no lower
bound.
For all i (1 ≤ i ≤ n), where αi
has upper bounds U1, ..., Uk, let the upper bound of
Yi be glb(U1 θ, ..., Uk θ), where θ is
the substitution [α1:=Y1, ..., αn:=Yn].
If the type variables Y1, ..., Yn do not have well-formed bounds (that is, a lower bound is not a subtype of an upper bound, or an intersection type is inconsistent), then resolution fails.
Otherwise, for all i (1 ≤ i ≤ n), all
bounds of the form G<..., αi, ...> =
capture(G<...>) are removed from the current
bound set, and the bounds α1 = Y1, ..., αn = Yn
are incorporated.
If the result does not contain the bound false, then the result becomes the new bound set, and resolution proceeds by selecting a new set of variables to instantiate (if necessary), as described above.
Otherwise, the result contains the bound false, and resolution fails.
The first method of instantiating an inference variable derives the instantiation from that variable's bounds. Sometimes, however, complex dependencies mean that the result is not within the variable's bounds. In that case, a different method of instantiation is performed, analogous to capture conversion (§5.1.10): fresh type variables are introduced, with bounds derived from the bounds of the inference variables. Note that the lower bounds of these "capture" variables are computed using only proper types: this is important in order to avoid attempts to perform typing computations on uninstantiated type variables.
Using the inference processes defined above, the following analyses are performed at compile time.
Given a
method invocation that provides no explicit type arguments, the
process to determine whether a potentially applicable generic method
m is applicable is as follows:
Where P1, ..., Pp (p ≥ 1) are the type parameters
of m, let α1, ..., αp be inference variables, and
let θ be the substitution [P1:=α1, ...,
Pp:=αp].
An initial bound set, B0, is generated from the declared bounds of P1, ..., Pp, as described in §18.1.3.
For all i (1 ≤ i ≤ p), if Pi appears in
the throws clause of m, then the bound throws αi is
implied. These bounds, if any, are incorporated with B0 to
produce a new bound set, B1.
A set of constraint formulas, C, is generated as follows.
Let F1, ..., Fn be the formal parameter types of m, and
let e1, ..., ek be the actual argument expressions of the
invocation. Then:
To test for applicability by strict invocation:
If k ≠ n, or if there exists an i (1
≤ i ≤ n) such that ei is pertinent to
applicability (§15.12.2.2) and either
(i) ei is a standalone expression of a primitive type but
Fi is a reference type, or (ii) Fi is a primitive type
but ei is not a standalone expression of a primitive type;
then the method is not applicable and there is no need to
proceed with inference.
Otherwise, C includes, for all i (1 ≤ i
≤ k) where ei is pertinent to applicability,
‹ei → Fi θ›.
To test for applicability by loose invocation:
If k ≠ n, the method is not applicable and there is no need to proceed with inference.
Otherwise, C includes, for all i (1 ≤ i
≤ k) where ei is pertinent to applicability,
‹ei → Fi θ›.
To test for applicability by variable arity invocation:
Let F'1, ..., F'k be the first k variable
arity parameter types of m
(§15.12.2.4). C includes, for all
i (1 ≤ i ≤ k) where ei is pertinent
to applicability, ‹ei → F'i
θ›.
C is reduced (§18.2) and the resulting bounds are incorporated with B1 to produce a new bound set, B2.
Finally, the method m is applicable if B2 does not contain
the bound false and resolution of all the inference
variables in B2 succeeds (§18.4).
Consider the following method invocation and assignment:
List<Number> ln = Arrays.asList(1, 2.0);
A most specific applicable method for the invocation must be identified as described in §15.12. The only potentially applicable method (§15.12.2.1) is declared as follows:
public static <T> List<T> asList(T... a)
Trivially (because of its arity), this method is neither applicable by strict invocation (§15.12.2.2) nor applicable by loose invocation (§15.12.2.3). But since there are no other candidates, in a third phase the method is checked for applicability by variable arity invocation.
The initial bound set, B, is a trivial upper bound for a single inference variable, α:
{ α <: Object }
The initial constraint formula set is as follows:
{ ‹1 → α›,
‹2.0 → α› }
These are reduced to a new bound set, B1:
{ α <: Object,
Integer <: α,
Double <: α }
Then, to test whether the method is applicable, we attempt to resolve these bounds. We succeed, producing the rather complex instantiation
α = Number & Comparable<?
extends Number & Comparable<?>>
We have thus demonstrated that the method is applicable; since no other candidates exist, it is the most specific applicable method. Still, the type of the method invocation, and its compatibility with the target type in the assignment, is not determined until further inference can occur, as described in the next section.
Given a method invocation expression that provides no explicit type
arguments, and a corresponding most specific applicable generic method
m, the process to infer the invocation type
(§15.12.2.6) of the chosen method may require
resolving additional constraints, both to assert compatibility with a
target type and to assert validity of the method invocation's argument
expressions.
It is important to note that multiple "rounds" of inference are involved in finding the type of a method invocation. This is necessary, for example, to allow a target type to influence the type of the invocation without allowing it to influence the choice of an applicable method. The first round (§18.5.1) produces a bound set and tests that a resolution exists, but does not commit to that resolution. Subsequent rounds reduce additional constraints until a final resolution step determines the "real" type of the expression.
If the method invocation expression is a poly expression (§15.12), its compatibility with a target type T is determined as follows.
If the method invocation expression appears in a strict invocation context and T is a primitive type, the expression is not compatible with T.
Let B2 be the bound set produced by reduction in order to
demonstrate that m is applicable in §18.5.1.
(While it was necessary in §18.5.1 to demonstrate that the inference variables in B2 could be resolved, in order to establish applicability, the instantiations produced by this resolution step are not considered part of B2.)
Let B3 be the bound set derived from B2 as follows.
Let R be the return type of m,
and let θ be the substitution [P1:=α1, ...,
Pp:=αp] defined in §18.5.1
to replace the type parameters of m with inference variables,
and let T be the invocation's target type. Then:
If unchecked conversion was necessary for the method to be applicable during constraint set reduction in §18.5.1, the constraint formula ‹|R| → T› is reduced and incorporated with B2.
Otherwise, if R θ is a parameterized type,
G<A1, ..., An>, and one of A1, ...,
An is a wildcard, then, for fresh inference variables
β1, ..., βn, the constraint formula
‹G<β1, ..., βn> →
T› is reduced and incorporated, along with the bound
G<β1, ..., βn> =
capture(G<A1, ..., An>), with
B2.
Otherwise, if R θ is an inference variable α, and one of the following is true:
T is a reference type, but is not a
wildcard-parameterized type, and either (i) B2 contains
a bound of one of the forms α = S or S
<: α, where S is a wildcard-parameterized
type, or (ii) B2 contains two bounds of the forms S1
<: α and S2 <: α, where S1
and S2 have supertypes that are two different
parameterizations of the same generic class or
interface.
T is a parameterization of a generic class or
interface, G, and B2 contains a bound of one of the
forms α = S or S <: α, where
there exists no type of the form G<...>
that is a supertype of S, but the raw type
|G<...>| is a supertype of S.
T is a primitive type, and one of the primitive wrapper classes mentioned in §5.1.7 is an instantiation, upper bound, or lower bound for α in B2.
then α is resolved in B2, and where the capture of the resulting instantiation of α is U, the constraint formula ‹U → T› is reduced and incorporated with B2.
Otherwise, the constraint formula ‹R θ → T› is reduced and incorporated with B2.
The method invocation expression is compatible with T if B3 does not contain the bound false and resolution of all the inference variables in B3 succeeds (§18.4).
Consider the example from the previous section:
List<Number>ln = Arrays.asList(1, 2.0);
The most specific applicable method was identified as:
public static<T>List<T>asList(T... a)
In order to complete type-checking of the method
invocation, we must determine whether it is compatible with its target
type, List.
<Number>
The bound set used to demonstrate applicability in the previous section, B2, was:
{ α <: Object,
Integer <: α,
Double <: α }
The new constraint formula set is as follows:
{ ‹List → <α>List› }
<Number>
This compatibility constraint produces an equality bound for α, which is included in the new bound set, B3:
{ α <: Object,
Integer <: α,
Double <: α,
α = Number }
These bounds are trivially resolved:
α = Number
Finally, we perform a substitution on the declared
return type of asList to determine that the method
invocation has type List;
clearly, this is compatible with the target type.
<Number>
This inference strategy is different than the Java
SE 7 Edition of The Java® Language Specification, which would have instantiated α based
on its lower bounds (before even considering the invocation's target
type), as we did in the previous section. This would result in a type
error, since the resulting type is not a subtype
of List.
<Number>
Under various special circumstances, based on the bounds appearing in B2, we eagerly resolve an inference variable that appears as the return type of the invocation. This is to avoid unfortunate situations in which the usual constraint, ‹R θ → T›, is not completeness-preserving. It is, unfortunately, possible that by eagerly resolving the variable, we are unable to make use of bounds that would be inferred later. It is also possible that, in some cases, bounds that will later be inferred from the invocation arguments (such as implicitly typed lambda expressions) would have caused a different outcome if they had been present in B2. Despite these limitations, the strategy allows for reasonable outcomes in typical use cases, and is backwards compatible with the algorithm in the Java SE 7 Edition of The Java® Language Specification.
The invocation type for the chosen method is determined after considering additional constraints that may be implied by the argument expressions of the method invocation expression, as follows:
If the method invocation expression is a poly expression, let B3 be the bound set generated in §18.5.2.1 to demonstrate compatibility with the actual target type of the method invocation.
If the method invocation expression is not a poly expression,
let B3 be the same as the bound set produced by reduction in
order to demonstrate that m is applicable in
§18.5.1.
(While it was necessary in §18.5.1 and §18.5.2.1 to demonstrate that the inference variables in the bound set could be resolved, the instantiations produced by these resolution steps are not considered part of B3.)
A set of constraint formulas, C, is generated as follows.
Let e1, ..., ek be the actual argument expressions of the
method invocation expression.
If m is applicable by strict or loose invocation, let F1,
..., Fk be the formal parameter types of m; if m is
applicable by variable arity invocation, let F1, ..., Fk the
first k variable arity parameter types of m
(§15.12.2.4).
Let θ be the substitution [P1:=α1, ...,
Pp:=αp] defined in §18.5.1
to replace the type parameters of m with inference
variables.
If ei is not pertinent to applicability, C contains
‹ei → Fi θ›.
Additional constraints may be included, depending on the
form of ei:
If ei is a LambdaExpression,
C contains ‹LambdaExpression →throws Fi θ›,
and the lambda body is searched for additional constraints:
For a block lambda body, the search is applied recursively to each result expression.
For a poly class instance creation expression or a poly method invocation expression , C contains all the constraint formulas that would appear in the set C generated by §18.5.2 when inferring the poly expression's invocation type.
For a parenthesized expression, the search is applied recursively to the contained expression.
For a conditional expression, the search is applied recursively to the second and third operands.
For a lambda expression, the search is applied recursively to the lambda body.
If ei is a MethodReference,
C contains ‹MethodReference →throws Fi θ›.
If ei is a poly class instance creation expression or
a poly method invocation expression, C contains all
the constraint formulas that would appear in the set C
generated by §18.5.2 when inferring
the poly expression's invocation type.
If ei is a parenthesized expression,
these rules are applied recursively to the contained expression.
If ei is a conditional expression,
these rules are applied recursively to the second and third operands.
While C is not empty, the following process is repeated, starting with the bound set B3 and accumulating new bounds into a "current" bound set, ultimately producing a new bound set, B4:
A subset of constraints is selected in C, satisfying the property that, for each constraint, no input variable can influence an output variable of another constraint in C. The terms input variable and output variable are defined below. An inference variable α can influence an inference variable β if α depends on the resolution of β (§18.4), or vice versa; or if there exists a third inference variable γ such that α can influence γ and γ can influence β.
If this subset is empty, then there is a cycle (or cycles) in the graph of dependencies between constraints. In this case, the constraints in C that participate in a dependency cycle (or cycles) and do not depend on any constraints outside of the cycle (or cycles) are considered. A single constraint is selected from these considered constraints, as follows:
If any of the considered constraints have the form ‹Expression → T›, then the selected constraint is the considered constraint of this form that contains the expression to the left (§3.5) of the expression of every other considered constraint of this form.
If no considered constraint has the form ‹Expression → T›, then the selected constraint is the considered constraint that contains the expression to the left of the expression of every other considered constraint.
The input variables α1, ..., αm of all the selected constraint(s) are resolved.
Where T1, ..., Tm are the instantiations of α1,
..., αm, the substitution [α1:=T1, ...,
αm:=Tm] is applied to every constraint.
The constraint(s) resulting from substitution are reduced and incorporated with the current bound set.
Finally, if B4 does not contain the bound false, the inference variables in B4 are resolved.
If resolution succeeds with instantiations T1, ..., Tp for
inference variables α1, ..., αp, let θ' be
the substitution [P1:=T1, ..., Pp:=Tp]. Then:
If unchecked conversion was necessary for the method to be
applicable during constraint set reduction in
§18.5.1, then the parameter types of
the invocation type of m are obtained by applying
θ' to the parameter types of m's type, and the
return type and thrown types of the invocation type of m
are given by the erasure of the return type and thrown types
of m's type.
If unchecked conversion was not necessary for the method to
be applicable, then the invocation type of m is obtained
by applying θ' to the type of m.
If B4 contains the bound false, or if resolution fails, then a compile-time error occurs.
The process of reducing additional argument constraints may require carefully ordering constraint formulas of the forms ‹Expression → T›, ‹LambdaExpression →throws T›, and ‹MethodReference →throws T›. To facilitate this ordering, the input variables of these constraints are defined as follows:
If T is an inference variable, it is the (only) input variable.
If T is a functional interface type, and a function type
can be derived from T (§15.27.3),
then the input variables include (i) if the lambda expression
is implicitly typed, the inference variables mentioned by
the function type's parameter types; and (ii) if the function
type's return type, R, is not void, then for each result
expression e in the lambda body (or for the body itself if
it is an expression), the input variables of ‹e
→ R›.
For ‹LambdaExpression →throws T›:
If T is an inference variable, it is the (only) input variable.
If T is a functional interface type, and a function type can be derived, as described in §15.27.3, the input variables include (i) if the lambda expression is implicitly typed, the inference variables mentioned by the function type's parameter types; and (ii) the inference variables mentioned by the function type's return type.
If T is an inference variable, it is the (only) input variable.
If T is a functional interface type with a function type, and if the method reference is inexact (§15.13.1), the input variables are the inference variables mentioned by the function type's parameter types.
For ‹MethodReference →throws T›:
If T is an inference variable, it is the (only) input variable.
If T is a functional interface type with a function type, and if the method reference is inexact (§15.13.1), the input variables are the inference variables mentioned by the function type's parameter types and the function type's return type.
For ‹Expression → T›, if Expression is a parenthesized expression:
Where the contained expression of Expression is Expression', the input variables are the input variables of ‹Expression' → T›.
For ‹ConditionalExpression → T›:
Where the conditional expression has the form e1 ? e2
: e3, the input variables are the input variables of
‹e2 → T› and ‹e3 →
T›.
For all other constraint formulas, there are no input variables.
The output variables of these constraints are all inference variables mentioned by the type on the right-hand side of the constraint, T, that are not input variables.
Where a lambda expression with explicit parameter types P1, ...,
Pn targets a functional interface type F<A1, ...,
Am> with at least one wildcard type argument, then a
parameterization of F may be derived as the ground target type of
the lambda expression as follows.
Let Q1, ..., Qk be the parameter types of the function type of the
type F<α1, ..., αm>, where α1, ...,
αm are fresh inference variables.
If n ≠ k, no valid parameterization exists. Otherwise, a set of constraint formulas is formed with, for all i (1 ≤ i ≤ n), ‹Pi = Qi›. This constraint formula set is reduced to form the bound set B.
If B contains the bound false, no valid parameterization
exists. Otherwise, a new parameterization of the functional interface
type, F<A'1, ..., A'm>, is constructed as
follows, for 1 ≤ i ≤ m:
If B contains an instantiation (§18.1.3) for αi, T, then A'i = T.
If F<A'1, ..., A'm> is not a well-formed
type (that is, the type arguments are not within their bounds), or if
F<A'1, ..., A'm> is not a subtype of
F<A1, ..., Am>, no valid parameterization
exists. Otherwise, the inferred parameterization is either
F<A'1, ..., A'm>, if all the type
arguments are types, or the non-wildcard parameterization
(§9.9) of F<A'1, ...,
A'm>, if one or more type arguments are still
wildcards.
In order to determine the function type of a wildcard-parameterized functional interface, we have to "instantiate" the wildcard type arguments with specific types. The "default" approach is to simply replace the wildcards with their bounds, as described in §9.8, but this produces spurious errors in cases where a lambda expression has explicit parameter types that do not correspond to the wildcard bounds. For example:
Predicate<? super Integer> p = (Number n) -> n.equals(23);The lambda expression is
a Predicate<Number>, which is a subtype
of Predicate<? super Integer> but
not Predicate<Integer>. The analysis in this
section is used to infer that Number is an
appropriate choice for the type argument
to Predicate.
That said, the analysis here, while described in terms of general type inference, is intentionally quite simple. The only constraints are equality constraints, which means that reduction amounts to simple pattern matching. A more powerful strategy might also infer constraints from the body of the lambda expression. But, given possible interactions with inference for surrounding and/or nested generic method invocations, this would introduce a lot of extra complexity.
When testing that one applicable method is more specific than another (§15.12.2.5), where the second method is generic, it is necessary to test whether some instantiation of the second method's type parameters can be inferred to make the first method more specific than the second.
Let m1 be the first method and m2 be the second method. Where m2
has type parameters P1, ..., Pp, let α1, ..., αp be
inference variables, and let θ be the substitution
[P1:=α1, ..., Pp:=αp].
Let e1, ..., ek be the argument expressions of the corresponding
invocation. Then:
If m1 and m2 are applicable by strict or loose invocation
(§15.12.2.2,
§15.12.2.3), then let S1, ..., Sk be
the formal parameter types of m1, and let T1, ..., Tk be
the result of θ applied to the formal parameter types of
m2.
If m1 and m2 are applicable by variable arity invocation
(§15.12.2.4), then let S1, ..., Sk be
the first k variable arity parameter types of m1, and let
T1, ..., Tk be the result of θ applied to the first
k variable arity parameter types of m2.
Note that no substitution is applied to S1, ...,
Sk; even if m1 is generic, the type parameters of m1 are treated
as type variables, not inference variables.
The process to determine if m1 is more specific than m2 is as
follows:
First, an initial bound set, B, is generated from the declared bounds of P1, ..., Pp, as specified in §18.1.3.
Second, for all i (1 ≤ i ≤ k), a set of constraint formulas or bounds is generated.
If Ti is a proper type, the result is true if Si is
more specific than Ti for ei
(§15.12.2.5), and false
otherwise. (Note that Si is always a proper type.)
Otherwise, if Si and Ti are not both functional interface
types, the constraint formula ‹Si <: Ti›
is generated.
Otherwise, if the interface of Si is a superinterface or a
subinterface of the interface of Ti (or, where Si or Ti is
an intersection type, some interface of Si is a superinterface
or a subinterface of some interface of Ti), the constraint
formula ‹Si <: Ti› is generated.
Otherwise, let MTS be the function type of the capture of Si, let MTS' be the function type of Si (without capture), and let MTT be the function type of Ti. If MTS and MTT have a different number of formal parameters or type parameters, or if MTS and MTS' do not have the same type parameters (§8.4.4), the result is false. Otherwise, the following constraint formulas or bounds are generated from the type parameters, formal parameter types, and return types of MTS and MTT:
Let A1, ..., An be the type parameters of MTS, and let B1, ..., Bn be the type parameters of MTT.
Let θ' be the substitution [B1:=A1, ...,
Bn:=An]. Then, for all j (1 ≤ j
≤ n):
If the bound Aj mentions one of A1, ..., An, and the bound of Bj is not a proper type, then producing an equality constraint would raise the possibility of an inference variable being bounded by an out-of-scope type variable. Since instantiating an inference variable with an out-of-scope type variable is nonsensical, we prefer to avoid the situation by giving up immediately whenever the possibility arises. This simplification is not completeness-preserving. (The same comment applies to the treatment of formal parameter types and return types below.)
Let U1, ..., Uk be the formal parameter types of MTS, and let V1, ..., Vk be the formal parameter types of MTT. Then, for all j (1 ≤ j ≤ k):
Let RS be the return type of MTS, and let RT be the return type of MTT. Then:
If RS mentions one of A1, ..., An, and RT is not a proper type, false.
Otherwise, if ei is an explicitly typed lambda expression:
Otherwise, if RS and RT are functional interface
types, and ei has at least one result expression,
then for each result expression in ei, this entire
second step is repeated to infer constraints under
which RS is more specific than RT θ' for
the given result expression.
Otherwise, if RS is a primitive type and RT is not,
and ei has at least one result expression,
and each result expression of ei is a standalone
expression (§15.2) of a primitive
type, true.
Otherwise, if RT is a primitive type and RS is not,
and ei has at least one result expression,
and each result expression of ei is either a
standalone expression of a reference type or a poly
expression, true.
Otherwise, if ei is a parenthesized expression, these
rules for constraints derived from RS and RT are
applied recursively for the contained expression.
Otherwise, if ei is a conditional expression, these
rules for constraints derived from RS and RT are
applied recursively for each of the second and third operands.
Third, if m2 is applicable by variable arity invocation and
has k+1 parameters, then where Sk+1 is the k+1'th
variable arity parameter type of m1 and Tk+1 is the
result of θ applied to the k+1'th variable arity
parameter type of m2, the constraint ‹Sk+1
<: Tk+1› is generated.
Fourth, the generated bounds and constraint formulas are reduced and incorporated with B to produce a bound set B'.
If B' does not contain the bound false, and
resolution of all the inference variables in B' succeeds,
then m1 is more specific than m2.