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 astype inference.
At a high level, type inference can be decomposed into three processes:
Reduction takes a compatibility assertion about an expression or type, called aconstraint formula, and reduces it to a set ofbounds oninference variables. Often, a constraint formula reduces toother 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 aninstantiation 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 ofTheJava® 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 untilafter 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 definesinference variables,constraint formulas, andbounds, as the terms will be used throughout this chapter. It also presents notation.
Inference variables aremeta-variables for types - that is, they are special names that allow abstract reasoning about types. To distinguish them fromtype 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 termproper 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 typeT (§5.3).
‹S→T›: A typeS is compatible in a loose invocation context with typeT (§5.3).
‹S<:T›: A reference typeS is a subtype of a reference typeT (§4.10).
‹S<=T›: A type argumentS is contained by a type argumentT (§4.5.1).
‹S =T›: A typeS is the same as a typeT (§4.3.4), or a type argumentS is the same as type argumentT.
‹LambdaExpression→throwsT›: The checked exceptions thrown by the body of theLambdaExpression are declared by thethrows clause of the function type derived fromT.
‹MethodReference→throwsT›: The checked exceptions thrown by the referenced method are declared by thethrows clause of the function type derived fromT.
Examples of constraint formulas:
FromCollections.singleton("hi"), we have the constraint formula ‹"hi"→α›. Through reduction, this will become the constraint formula: ‹String<:α›.
FromArrays.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 invocationList<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 ofbounds on inference variables is maintained. A bound has one of the following forms:
S =T, where at least one ofS orT is an inference variable:S is the same asT.
S<:T, where at least one ofS orT is an inference variable:S is a subtype ofT.
G<α1, ...,αn> = capture(G<A1, ...,An>): The variablesα1, ...,αn represent the result of capture conversion (§5.1.10) applied toG<A1, ...,An> (whereA1, ...,An may be types or wildcards and may mention inference variables).
A bound issatisfied by an inference variable substitution if, after applying the substitution, the assertion is true. The boundfalse can never be satisfied.
Some bounds relate an inference variable to a proper type. LetT be a proper type. Given a bound of the formα =T orT =α, we sayT is aninstantiation ofα. Similarly, given a bound of the formα<:T, we sayT is aproper upper bound ofα, and given a bound of the formT<:α, we sayT is aproper lower bound ofα.
Other bounds relate two inference variables, or an inference variable to a type that contains inference variables. Such bounds, of the formS =T orS<:T, are calleddependencies.
A bound of the formG<α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 inA1, ...,An may not yet be resolved.
A bound of the formthrowsα 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 abound set. It is sometimes convenient to refer to anempty bound set with the symboltrue; this is merely out of convenience, and the two are interchangeable.
Examples of bound sets:
{α =String } contains a single bound, instantiatingα asString.
{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 astrue.
{false } expresses the fact that no satisfactory instantiation exists.
When inference begins, a bound set is typically generated from a list of type parameter declarationsP1, ...,Pp and associated inference variablesα1, ...,αp. Such a bound set is constructed as follows. For eachl (1≤l≤p):
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 alwayssoundness-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 notcompleteness-preserving: there may exist inference variable instantiations that satisfy the original constraint butdo 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:
IfT is a proper type, the constraint reduces totrue if the expression is compatible in a loose invocation context withT (§5.3), andfalse otherwise.
Otherwise, if the expression is a standalone expression (§15.2) of typeS, 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 setB3 which would be used to determine the expression's invocation type when targetingT, as defined in§18.5.2. (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 inT.
If the expression is a conditional expression of the forme1?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>
Whenboth 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 ofemptyList) into the outer inference process (in this case, trying to inferβ where the constructor is for typeArrayList<β>). 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›, whereT mentions at least one inference variable, is reduced as follows:
IfT is not a functional interface type (§9.8), the constraint reduces tofalse.
Otherwise, letT' be the ground target type derived fromT, as specified in§15.27.3. If§18.5.3 is used to derive a functional interface type which is parameterized, then the test thatF<A'1, ...,A'm> is a subtype ofF<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 ofT'. Then:
If no valid function type can be found, the constraint reduces tofalse.
Otherwise, the congruence ofLambdaExpression 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 tofalse.
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 tofalse.
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.
If the function type's result isvoid and the lambda body is neither a statement expression nor a void-compatible block, the constraint reduces tofalse.
If the function type's result is notvoid and the lambda body is a block that is not value-compatible, the constraint reduces tofalse.
Otherwise, the constraint reduces to all of the following constraint formulas:
If the lambda parameters have explicitly declared typesF1, ...,Fn and the function type has parameter typesG1, ...,Gn, then i) for alli (1≤i≤n), ‹Fi =Gi›, and ii) ‹T'<:T›.
If the function type's return type is a (non-void) typeR, assume the lambda's parameter types are the same as the function type's parameter types. Then:
IfR is a proper type, and if the lambda body or some result expression in the lambda body is not compatible in an assignment context withR, thenfalse.
Otherwise, ifR is not a proper type, then where the lambda body has the formExpression, the constraint ‹Expression→R›; or where the lambda body is a block with result expressionse1, ...,em, for alli (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 donot attempt to produce bounds on inference variables that appear in the target function type'sthrows 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, wedo get bounds on these variables later, because invocation type inference (§18.5.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 producefalse. During invocation type inference (§18.5.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. IfR is a proper type, such asByte derived fromFunction, then assignability is easy enough to test, and reduction does so above. IfR 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 expression100, it is conceivable thatα could be instantiated toByte, but reduction will not in fact produce such a bound.
A constraint formula of the form ‹MethodReference→T›, whereT mentions at least one inference variable, is reduced as follows:
IfT is not a functional interface type, or ifT is a functional interface type that does not have a function type (§9.9), the constraint reduces tofalse.
Otherwise, if there does not exist a potentially applicable method for the method reference when targetingT, the constraint reduces tofalse.
Otherwise, if the method reference is exact (§15.13.1), then letP1, ...,Pn be the parameter types of the function type ofT, and letF1, ...,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 wheren =k+1, the parameter of typeP1 is to act as the target reference of the invocation. The method reference expression necessarily has the formReferenceType:: [TypeArguments] Identifier. The constraint reduces to ‹P1<:ReferenceType› and, for alli (2≤i≤n), ‹Pi→Fi-1›.
In all other cases,n =k, and the constraint reduces to, for alli (1≤i≤n), ‹Pi→Fi›.
If the function type's result is notvoid, letR be its return type. Then, if the result of the potentially applicable compile-time declaration isvoid, the constraint reduces tofalse. Otherwise, the constraint reduces to ‹R'→R›, whereR' 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 tofalse.
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.
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 tofalse. Otherwise, there is a compile-time declaration, and:
If the result of the function type isvoid, the constraint reduces totrue.
Otherwise, if the method reference expression elidesTypeArguments, 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 the constraint reduces to the bound setB3 which would be used to determine the method reference's invocation type when targeting the return type of the function type, as defined in§18.5.2.B3 may contain new inference variables, as well as dependencies between these new variables and the inference variables inT.
Otherwise, letR be the return type of the function type, and letR' 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. IfR' isvoid, the constraint reduces tofalse; otherwise, the constraint reduces to ‹R'→R›.
The strategy used to determine a return type for a generic referenced method follows the same pattern as for generic method invocations (§18.2.1). This may involve "lifting" bounds into the outer context and inferring dependencies between the two sets of inference variables.
A constraint formula of the form ‹S→T› is reduced as follows:
IfS andT are proper types, the constraint reduces totrue ifS is compatible in a loose invocation context withT (§5.3), andfalse otherwise.
Otherwise, ifS is a primitive type, letS' be the result of applying boxing conversion (§5.1.7) toS. Then the constraint reduces to ‹S'→T›.
Otherwise, ifT is a primitive type, letT' be the result of applying boxing conversion (§5.1.7) toT. Then the constraint reduces to ‹S =T'›.
Otherwise, ifT is a parameterized type of the formG<T1, ...,Tn>, and there exists no type of the formG<...> that is a supertype ofS, but the raw typeG is a supertype ofS, then the constraint reduces totrue.
Otherwise, ifT is an array type of the formG<T1, ...,Tn>[]k, and there exists no type of the formG<...>[]k that is a supertype ofS, but the raw typeG[]k is a supertype ofS, then the constraint reduces totrue. (The notation[]k indicates an array type ofk 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).
BoxingT toT' is not completeness-preserving; for example, ifT werelong,S might be instantiated toInteger, which is not a subtype ofLong but could be unboxed and then widened tolong. 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.
Similarly, the treatment of unchecked conversion sacrifices completeness in cases in whichT is not a parameterized type (for example, ifT 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:
IfS andT are proper types, the constraint reduces totrue ifS is a subtype ofT (§4.10), andfalse otherwise.
Otherwise, ifS is the null type, the constraint reduces totrue.
Otherwise, ifT is the null type, the constraint reduces tofalse.
Otherwise, ifS is an inference variable,α, the constraint reduces to the boundα<:T.
Otherwise, ifT is an inference variable,α, the constraint reduces to the boundS<:α.
Otherwise, the constraint is reduced according to the form ofT:
IfT is a parameterized class or interface type, or an inner class type of a parameterized class or interface type (directly or indirectly), letA1, ...,An be the type arguments ofT. Among the supertypes ofS, a corresponding class or interface type is identified, with type argumentsB1, ...,Bn. If no such type exists, the constraint reduces tofalse. Otherwise, the constraint reduces to the following new constraints: for alli (1≤i≤n), ‹Bi<=Ai›.
IfT is any other class or interface type, then the constraint reduces totrue ifT is among the supertypes ofS, andfalse otherwise.
IfT is an array type,T'[], then among the supertypes ofS that are array types, a most specific type is identified,S'[] (this may beS itself). If no such array type exists, the constraint reduces tofalse. Otherwise:
IfT is an intersection type,I1& ...&In, the constraint reduces to the following new constraints: for alli (1≤i≤n), ‹S<:Ii›.
A constraint formula of the form ‹S<=T›, whereS andT are type arguments (§4.5.1), is reduced as follows:
A constraint formula of the form ‹S =T›, whereS andT are types, is reduced as follows:
IfS andT are proper types, the constraint reduces totrue ifS is the same asT (§4.3.4), andfalse otherwise.
Otherwise, ifS orT is the null type, the constraint reduces tofalse.
Otherwise, ifS is an inference variable,α, andT is not a primitive type, the constraint reduces to the boundα =T.
Otherwise, ifT is an inference variable,α, andS is not a primitive type, the constraint reduces to the boundS =α.
Otherwise, ifS andT are class or interface types with the same erasure, whereS has type argumentsB1, ...,Bn andT has type argumentsA1, ...,An, the constraint reduces to the following new constraints: for alli (1≤i≤n), ‹Bi =Ai›.
Otherwise, ifS andT are array types,S'[] andT'[], the constraint reduces to ‹S' =T'›.
Note that we do not address intersection types above, because it is impossible for reduction to encounter an intersection type that is not a proper type.
A constraint formula of the form ‹S =T›, whereS andT are type arguments (§4.5.1), is reduced as follows:
IfS andT are types, the constraint is reduced as described above.
IfS has the form? andT has the form?, the constraint reduces totrue.
IfS has the form? andT has the form?extendsT', the constraint reduces to ‹Object =T'›.
IfS has the form?extendsS' andT has the form?, the constraint reduces to ‹S' =Object›.
IfS has the form?extendsS' andT has the form?extendsT', the constraint reduces to ‹S' =T'›.
IfS has the form?superS' andT has the form?superT', the constraint reduces to ‹S' =T'›.
A constraint formula of the form ‹LambdaExpression→throwsT› is reduced as follows:
IfT is not a functional interface type (§9.8), the constraint reduces tofalse.
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 tofalse.
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 tofalse.
This condition never arises in practice, due to the substitution applied to the target type in§18.5.2.
Otherwise, if the function type's return type is neithervoid nor a proper type, the constraint reduces tofalse.
This condition never arises in practice, due to the substitution applied to the target type in§18.5.2.
Otherwise, letE1, ...,En be the types in the function type'sthrows clause that arenot 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. LetX1, ...,Xm be the checked exception types that the lambda body can throw (§11.2). Then there are two cases:
Ifn =0 (the function type'sthrows clause consists only of proper types), then if there exists somei (1≤i≤m) such thatXi is not a subtype of any proper type in thethrows clause, the constraint reduces tofalse; otherwise, the constraint reduces totrue.
Ifn >0, the constraint reduces to a set of subtyping constraints: for alli (1≤i≤m), ifXi is not a subtype of any proper type in thethrows clause, then the constraints include, for allj (1≤j≤n), ‹Xi<:Ej›. In addition, for allj (1≤j≤n), the constraint reduces to the boundthrowsEj.
A constraint formula of the form ‹MethodReference→throwsT› is reduced as follows:
IfT is not a functional interface type, or ifT is a functional interface type but does not have a function type (§9.9), the constraint reduces tofalse.
Otherwise, let the target function type for the method reference expression be the function type ofT. 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 tofalse.
Otherwise, if the method reference is inexact and the function type's result is neithervoid nor a proper type, the constraint reduces tofalse.
Otherwise, letE1, ...,En be the types in the function type'sthrows clause that arenot proper types. LetX1, ...,Xm be the checked exceptions in thethrows 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:
Ifn =0 (the function type'sthrows clause consists only of proper types), then if there exists somei (1≤i≤m) such thatXi is not a subtype of any proper type in thethrows clause, the constraint reduces tofalse; otherwise, the constraint reduces totrue.
Ifn >0, the constraint reduces to a set of subtyping constraints: for alli (1≤i≤m), ifXi is not a subtype of any proper type in thethrows clause, then the constraints include, for allj (1≤j≤n), ‹Xi<:Ej›. In addition, for allj (1≤j≤n), the constraint reduces to the boundthrowsEj.
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 thethrows clause.) Hence, we require both of these, as derived from the target typeT, to be proper types.
One consequence is that lambda expressions returned fromother 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'sthrows 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 constructed and grown during inference, it is possible that new bounds can be inferred based on the assertions of the original bounds. The process ofincorporation 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 boundfalse, then the bound set has the following properties:
For each combination of a proper lower boundL and a proper upper boundU 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 andT are inference variables or types, andU is a proper type. For conciseness, a bound of the formα =T may also match a bound of the formT =α.)
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 ofS of the formG<S1, ...,Sn> and a supertype ofT of the formG<T1, ...,Tn> (for some generic class or interface,G), then for alli (1≤i≤n), ifSi andTi are types (not wildcards), the constraint formula ‹Si =Ti› is implied.
When a bound set contains a bound of the formG<α1, ...,αn> = capture(G<A1, ...,An>), new bounds are implied and new constraint formulas may be implied, as follows.
LetP1, ...,Pn represent the type parameters ofG and letB1, ...,Bn represent the bounds of these type parameters. Letθ represent the substitution[P1:=α1, ...,Pn:=αn]. LetR be a type that isnot an inference variable (but is not necessarily a proper type).
A set of bounds onα1, ...,αn is implied, constructed from the declared bounds ofP1, ...,Pn as specified in§18.1.3.
In addition, for alli (1≤i≤n):
Given a bound set that does not contain the boundfalse, a subset of the inference variables mentioned by the bound set may beresolved. 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, whereT is either an inference variableβ or a type that mentionsβ:
Ifα appears on the left-hand side of another bound of the formG<...,α, ...> = 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 formG<...,α, ...> = 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β.
Given a set of inference variables to resolve, letV 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 inV has an instantiation, then resolution succeeds and this procedure terminates.
Otherwise, let {α1, ...,αn } be a non-empty subset of uninstantiated variables inV such that i) for alli (1≤i≤n), ifαi depends on the resolution of a variableβ, then eitherβ has an instantiation or there is somej 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 formG<...,αi, ...> = capture(G<...>) for alli (1≤i≤n), then a candidate instantiationTi is defined for eachαi:
Ifαi has one or moreproper lower bounds,L1, ...,Lk, thenTi = lub(L1, ...,Lk) (§4.10.4).
Otherwise, if the bound set containsthrowsαi, and the proper upper bounds ofαi are, at most,Exception,Throwable, andObject, thenTi =RuntimeException.
Otherwise, whereαi hasproper upper boundsU1, ...,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 boundfalse, 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 boundfalse, so a second attempt is made to instantiate {α1, ...,αn } by performing the step below.
If the bound set contains a bound of the formG<...,αi, ...> = capture(G<...>) for somei (1≤i≤n), or;
If the bound set produced in the step above contains the boundfalse;
then letY1, ...,Yn be fresh type variables whose bounds are as follows:
For alli (1≤i≤n), ifαi has one or moreproper lower boundsL1, ...,Lk, then let the lower bound ofYi be lub(L1, ...,Lk); if not, thenYi has no lower bound.
For alli (1≤i≤n), whereαi has upper boundsU1, ...,Uk, let the upper bound ofYi be glb(U1θ, ...,Ukθ), whereθ is the substitution[α1:=Y1, ...,αn:=Yn].
If the type variablesY1, ...,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 alli (1≤i≤n), all bounds of the formG<...,α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 boundfalse, 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 boundfalse, 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 methodm is applicable is as follows:
WhereP1, ...,Pp (p≥ 1) are the type parameters ofm, letα1, ...,αp be inference variables, and letθ be the substitution[P1:=α1, ...,Pp:=αp].
An initial bound set,B0, is constructed from the declared bounds ofP1, ...,Pp, as described in§18.1.3.
For alli (1≤i≤p), ifPi appears in thethrows clause ofm, then the boundthrowsαi is implied. These bounds, if any, are incorporated withB0 to produce a new bound set,B1.
A set of constraint formulas,C, is constructed as follows.
LetF1, ...,Fn be the formal parameter types ofm, and lete1, ...,ek be the actual argument expressions of the invocation. Then:
To test forapplicability by strict invocation:
Ifk≠n, or if there exists ani (1≤i≤n) such thatei is pertinent to applicability (§15.12.2.2) and either i)ei is a standalone expression of a primitive type butFi is a reference type, or ii)Fi is a primitive type butei 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 alli (1≤i≤k) whereei is pertinent to applicability, ‹ei→Fiθ›.
To test forapplicability by loose invocation:
Ifk≠n, the method is not applicable and there is no need to proceed with inference.
Otherwise,C includes, for alli (1≤i≤k) whereei is pertinent to applicability, ‹ei→Fiθ›.
To test forapplicability by variable arity invocation:
LetF'1, ...,F'k be the firstk variable arity parameter types ofm (§15.12.2.4).C includes, for alli (1≤i≤k) whereei is pertinent to applicability, ‹ei→F'iθ›.
C is reduced (§18.2) and the resulting bounds are incorporated withB1 to produce a new bound set,B2.
Finally, the methodm is applicable ifB2 does not contain the boundfalse and resolution of all the inference variables inB2 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 that provides no explicit type arguments, and a corresponding most specific applicable generic methodm, the process to infer the invocation type (§15.12.2.6) of the chosen method is as follows:
Letθ be the substitution[P1:=α1, ...,Pp:=αp] defined in§18.5.1 to replace the type parameters ofm with inference variables.
LetB2 be the bound set produced by reduction in order to demonstrate thatm is applicable in§18.5.1. (While it was necessary in§18.5.1 to demonstrate that the inference variables inB2 could be resolved, in order to establish applicability, the instantiations produced by this resolution step arenot considered part ofB2.)
If the invocation is not a poly expression, let the bound setB3 be the same asB2.
If the invocation is a poly expression, let the bound setB3 be derived fromB2 as follows. LetR be the return type ofm, letT be the invocation's target type, and 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 withB2.
Otherwise, ifRθ is a parameterized type,G<A1, ...,An>, and one ofA1, ...,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 boundG<β1, ...,βn> = capture(G<A1, ...,An>), withB2.
Otherwise, ifRθ 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 orS<:α, whereS is a wildcard-parameterized type, or ii)B2 contains two bounds of the formsS1<:α andS2<:α, whereS1 andS2 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, andB2 contains a bound of one of the formsα =S orS<:α, where there exists no type of the formG<...> that is a supertype ofS, but the raw type |G<...>| is a supertype ofS.
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α inB2.
thenα is resolved inB2, and where the capture of the resulting instantiation ofα isU, the constraint formula ‹U→T› is reduced and incorporated withB2.
Otherwise, the constraint formula ‹Rθ→T› is reduced and incorporated withB2.
A set of constraint formulas,C, is constructed as follows.
Lete1, ...,ek be the actual argument expressions of the invocation. Ifm is applicable by strict or loose invocation, letF1, ...,Fk be the formal parameter types ofm; ifm is applicable by variable arity invocation, letF1, ...,Fk the firstk variable arity parameter types ofm (§15.12.2.4). Then:
For alli (1≤i≤k), ifei is not pertinent to applicability,C contains ‹ei→Fiθ›.
For alli (1≤i≤k), additional constraints may be included, depending on the form ofei:
Ifei is aLambdaExpression,C contains ‹LambdaExpression→throwsFiθ›.
In addition, 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 (§15.9) or a poly method invocation expression (§15.12),C contains all the constraint formulas that would appear in the setC 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.
Ifei is aMethodReference,C contains ‹MethodReference→throwsFiθ›.
Ifei is a poly class instance creation expression (§15.9) or a poly method invocation expression (§15.12),C contains all the constraint formulas that would appear in the setC generated by§18.5.2 when inferring the poly expression's invocation type.
Ifei is a parenthesized expression, these rules are applied recursively to the contained expression.
Ifei is a conditional expression, these rules are applied recursively to the second and third operands.
WhileC is not empty, the following process is repeated, starting with the bound setB3 and accumulating new bounds into a "current" bound set, ultimately producing a new bound set,B4:
A subset of constraints is selected inC, satisfying the property that, for each constraint, no input variable can influence an output variable of another constraint inC. The termsinput variable andoutput 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, all constraints are considered that participate in a dependency cycle (or cycles) and do not depend on any constraints outside of the cycle (or cycles). A single constraint is selected from the 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.
WhereT1, ...,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, ifB4 does not contain the boundfalse, the inference variables inB4 are resolved.
If resolution succeeds with instantiationsT1, ...,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 ofm are obtained by applyingθ' to the parameter types ofm's type, and the return type and thrown types of the invocation type ofm are given by the erasure of the return type and thrown types ofm's type.
If unchecked conversion was not necessary for the method to be applicable, then the invocation type ofm is obtained by applyingθ' to the type ofm.
IfB4 contains the boundfalse, or if resolution fails, then a compile-time error occurs.
Invocation type inference may require carefully sequencing the reduction of constraint formulas of the forms ‹Expression→T›, ‹LambdaExpression→throwsT›, and ‹MethodReference→throwsT›. To facilitate this sequencing, theinput variables of these constraints are defined as follows:
IfT is an inference variable, it is the (only) input variable.
IfT is a functional interface type, and a function type can be derived fromT (§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 notvoid, then for each result expressione in the lambda body (or for the body itself if it is an expression), the input variables of ‹e→R›.
For ‹LambdaExpression→throwsT›:
IfT is an inference variable, it is the (only) input variable.
IfT 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.
IfT is an inference variable, it is the (only) input variable.
IfT 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→throwsT›:
IfT is an inference variable, it is the (only) input variable.
IfT 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›, ifExpression is a parenthesized expression:
Where the contained expression ofExpression isExpression', the input variables are the input variables of ‹Expression'→T›.
For ‹ConditionalExpression→T›:
Where the conditional expression has the forme1?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.
Theoutput 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.
It is important to note that two "rounds" of inference are involved in finding the type of a method invocation. This is necessary 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 produces a bound set and tests that a resolution exists, but does not commit to that resolution. The second round reduces additional constraints and then performs a second resolution, this time "for real".
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 ofasList to determine that the method invocation has typeList; clearly, this is compatible with the target type.<Number>
This inference strategy is different than the Java SE 7 Edition ofTheJava® 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 ofList.<Number>
Under various special circumstances, based on the bounds appearing inB2, 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 inB2. 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 ofTheJava® Language Specification.
Where a lambda expression with explicit parameter typesP1, ...,Pn targets a functional interface typeF<A1, ...,Am> with at least one wildcard type argument, then a parameterization ofF may be derived as the ground target type of the lambda expression as follows.
LetQ1, ...,Qk be the parameter types of the function type of the typeF<α1, ...,αm>, whereα1, ...,αm are fresh inference variables.
Ifn≠k, no valid parameterization exists. Otherwise, a set of constraint formulas is formed with, for alli (1≤i≤n), ‹Pi =Qi›. This constraint formula set is reduced to form the bound setB.
IfB contains the boundfalse, 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:
IfB contains an instantiation (§18.1.3) forαi,T, thenA'i =T.
IfF<A'1, ...,A'm> is not a well-formed type (that is, the type arguments are not within their bounds), or ifF<A'1, ...,A'm> is not a subtype ofF<A1, ...,Am>, no valid parameterization exists. Otherwise, the inferred parameterization is eitherF<A'1, ...,A'm>, if all the type arguments are types, or the non-wildcard parameterization (§9.9) ofF<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 donot correspond to the wildcard bounds. For example:
Predicate<? super Integer> p = (Number n)-> n.equals(23);The lambda expression is aPredicate<Number>, which is a subtype ofPredicate<? super Integer> but notPredicate<Integer>. The analysis in this section is used to infer thatNumber is an appropriate choice for the type argument toPredicate.
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 ismore 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.
Letm1 be the first method andm2 be the second method. Wherem2 has type parametersP1, ...,Pp, letα1, ...,αp be inference variables, and letθ be the substitution[P1:=α1, ...,Pp:=αp].
Lete1, ...,ek be the argument expressions of the corresponding invocation. Then:
Ifm1 andm2 are applicable by strict or loose invocation (§15.12.2.2,§15.12.2.3), then letS1, ...,Sk be the formal parameter types ofm1, and letT1, ...,Tk be the result ofθ applied to the formal parameter types ofm2.
Ifm1 andm2 are applicable by variable arity invocation (§15.12.2.4), then letS1, ...,Sk be the firstk variable arity parameter types ofm1, and letT1, ...,Tk be the result ofθ applied to the firstk variable arity parameter types ofm2.
Note that no substitution is applied toS1, ...,Sk; even ifm1 is generic, the type parameters ofm1 are treated as type variables, not inference variables.
The process to determine ifm1 is more specific thanm2 is as follows:
First, an initial bound set,B, is constructed from the declared bounds ofP1, ...,Pp, as specified in§18.1.3.
Second, for alli (1≤i≤k), a set of constraint formulas or bounds is generated.
IfTi is a proper type, the result istrue ifSi is more specific thanTi forei (§15.12.2.5), andfalse otherwise. (Note thatSi is always a proper type.)
Otherwise, ifTi is not a functional interface type, the constraint formula ‹Si<:Ti› is generated.
Otherwise,Ti is a parameterization of a functional interface,I. It must be determined whetherSi satisfies the following five conditions:
Si is not a superinterface ofI, nor a parameterization of a superinterface ofI.
Si is not a subinterface ofI, nor a parameterization of a subinterface ofI.
IfSi is an intersection type, at least one element of the intersection is not a superinterface ofI, nor a parameterization of a superinterface ofI.
IfSi is an intersection type, no element of the intersection is a subinterface ofI, nor a parameterization of a subinterface ofI.
If all five conditions are true, then the following constraint formulas or bounds are generated (whereU1 ...Uk andR1 are the parameter types and return type of the function type of the capture ofSi, andV1 ...Vk andR2 are the parameter types and return type of the function type ofTi):
Ifei is an explicitly typed lambda expression:
Otherwise, ifR1 andR2 are functional interface types, and neither interface is a subinterface of the other, andei has at least one result expression, then these rules are applied recursively toR1 andR2, for each result expression inei.
Otherwise, ifR1 is a primitive type andR2 is not, andei has at least one result expression, and each result expression ofei is a standalone expression (§15.2) of a primitive type,true.
Otherwise, ifR2 is a primitive type andR1 is not, andei has at least one result expression, and each result expression ofei is either a standalone expression of a reference type or a poly expression,true.
Ifei is a parenthesized expression, these rules are applied recursively to the contained expression.
Ifei is a conditional expression, these rules are applied recursively to each of the second and third operands.
If the five constraints onSi are not satisfied, the constraint formula ‹Si<:Ti› is generated instead.
Third, ifm2 is applicable by variable arity invocation and hask+1 parameters, then whereSk+1 is thek+1'th variable arity parameter type ofm1 andTk+1 is the result ofθ applied to thek+1'th variable arity parameter type ofm2, the constraint ‹Sk+1<:Tk+1› is generated.
Fourth, the generated bounds and constraint formulas are reduced and incorporated withB to produce a bound setB'.
IfB' does not contain the boundfalse, and resolution of all the inference variables inB' succeeds, thenm1 is more specific thanm2.