Bug ID: JDK-8016195 Lambda Spec: Specify rules for capture in inference

Type: Bug
Component: specification
Sub-Component: language

Priority: P2
Status: Closed
Resolution: Fixed

Submitted: 2013-06-07
Updated: 2014-02-26
Resolved: 2013-09-20

JDK 8
8Fixed

The type of a nested generic method call is the capture of the declared return (Foo<? extends alpha>).  0.6.2 inference rules assert instead that the _uncaptured_ type is a subtype of the target.

Updates to incorporation and resolution: ---- 18.3 When a bound set contains a bound of the form G<��1, ..., ��n> = capture(G<A1, ..., An>), additional bounds or constraints may be inferred. Let P1, ..., Pn represent the type parameters of G, B1, ..., Bn represent the bounds (4.4) of these type parameters, and �� 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). Then for all i (1 �� i �� n): - Where the bounds of Pi are Bi1, ..., Bim, for all j (1 �� j �� m), the bound ��i <: �� Bij is immediately implied. - If Ai is a wildcard of the form ?: -- �� = R implies false -- �� <: R implies �� Bi <: R�� -- R <: �� implies false - If Ai is a wildcard of the form ? extends T: -- �� = R implies false -- If Bi is Object, �� <: R implies ��T <: R�� -- R <: �� implies false - If Ai is a wildcard of the form ? super T: -- �� = R implies false -- �� <: R implies �� Bi <: R�� -- R <: �� implies ��R <: T�� - If Ai is not a wildcard, the bound ��i = Ai is immediately implied. ---- 18.4 An inference variable �� appearing on the left-hand side of a bound of the form G<..., ��, ...> = capture(G<A1, ..., An>) depends on the resolution of every other inference variable mentioned in this bound (on both sides of the = sign). An inference variable �� that does not appear on the left-hand-side of a bound of this form depends on the resolution of an inference variable �� if, where T is either �� or a type that mentions ��, the bound set contains a bound of one of the following forms: ... ... If, for all i (1 �� i �� n), the bound set does not contain a bound of the form G<..., ��i, ...> = capture(G<A1, ..., An>), we first define candidate instantiations, T1, ..., Tn. For all i (1 �� i �� n), define Ti as follows: ... ... Otherwise, a second attempt is made to instantiate { ��1, ..., ��n }, as follows: - Let Z1, ..., Zn be fresh type variables, and �� be the substitution [��1:=Z1, ..., ��n:=Zn]. - For all i, (1 �� i �� n), if ��i has one or more lower bounds, L1, ..., Lk, then define the lower bound of Zi as lub(L1��, ..., Lk��); if not, then Zi has no lower bound. - For all i, (1 �� i �� n), where ��i has upper bounds U1, ..., Uk, then define the upper bound of Zi as glb(L1��, ..., Lk��). If the resulting type variables Z1, ..., Zn have well-formed bounds, then the new bound set is produced by removing all bounds of the form G<..., ��i, ...> = capture(G<A1, ..., An>) (for all i, 1 �� i �� n) and incorporating ��1 = Z1, ..., ��n = Zn. If the result contains the bound false, resolution fails. Otherwise, resolution proceeds by selecting a new set of variables to instantiate (if necessary), as described above.

20-09-2013

Update to Invocation Type Inference in order to provide the "reduction of a nested call" functionality: ---- 18.5.2 - If the invocation is a poly expression, let R be the return type of m, and let S be the invocation's target type. Then one of four cases apply, producing a new bound set, B2: -- If R is void, then a compile-time error occurs; the invocation type of the method is undefined. -- 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> �� S�� is reduced and incorporated, along with the bound G<��1, ..., ��n> = capture(G<A1, ..., An>), into B1. -- If i) S is a primitive type; ii) �� R is an inference variable ��; and iii) exactly one of the primitive wrapper classes mentioned in 5.1.7 is an instantiation, upper bound, or lower bound for �� in B1; then where this wrapper class is W, the constraint formulas ��W �� S�� is reduced and incorporated, along with the bound �� = W, into B1. -- Otherwise, the constraint formula �� R �� S�� is reduced and incorporated into B1.

19-09-2013

Here's what I'd like to do here. We introduce a new kind of "bound" to encode "capture ivars" -- types that we know must be derived by capture, but that we can't generate yet because it makes no sense (at least formally) to have a type variable with to-be-inferred bounds. New kind of bound, a "capture bound": G<��1...��n> = capture(G<...>) If a type argument in the original type is not a wildcard, it still gets a new ivar (for simplicity). Examples: Foo<��> = capture(Foo<? super ��>) Bar<��1, ��2> = capture(Bar<? extends Baz<��>, ?>) Bar<��1, ��2> = capture(Bar<? extends Baz<��>, ��>) --- Reduction of a nested call: - The nested method has return Foo<? extends Bar<��>> - Target is T - Produces bound Foo<��> = capture(Foo<? extends Bar<��>>) (plus all bounds from the nested call) - Produces constraint formula Foo<��> <: T --- Incorporation: Given G<��1...��n> = capture(G<A1 ... An>): - ��i "represents the capture of" Ai (Ai may be a wildcard or a type, and may mention ivars) - wildcardBound(��i), where Ai is a wildcard and the corresponding type parameter has the form Pi extends Bi, is Bi[P1:=��1...Pn:=��n] Then incorporation uses the following additional rules. Where �� represents the capture of an unbound wildcard: �� = T (T not an ivar) --> false �� <: T (T not an ivar) --> wildcardBound(��) <: T T <: �� --> false Where �� represents the capture of '? extends S': �� = T (T not an ivar) --> false �� <: T (T not an ivar), wildcardBound(��) is undefined --> S <: T *** T <: �� --> false Where �� represents the capture of '? super S': �� = T (T not an ivar) --> false �� <: T (T not an ivar) --> wildcardBound(��) <: T T <: �� --> T <: S Where �� represents the capture of a type S: --> ��i = S *** Note: we don't do anything with �� <: T when we have _both_ a use-site and a declaration-site upper bound for ��. This is because we need disjunctive logic: _either_ S <: T _or_ wildcardBound(��) <: T. I've been puzzling over this for awhile, trying to find a way to handle the "easy" cases, but it always seems like a complex mess. I think we're better off simply washing our hands and saying we tried our best rather than diving into the complexity. (Here's a flavor: let's say S <: T reduces to false. Then we _know_ that wildcardBound(��) <: T. Fine. But what if S is an ivar? Does it matter whether S has an eq bound? What if we later discover an eq bound for S that wasn't there when we performed the test, but that would have led to false? What if S <: T doesn't directly reduce to false, but would trigger an incorporation step that ultimately leads to false?) --- Resolution: If �� appears on the LHS of a capture bound, then it depends on all ivars mentioned in that capture bound (on both sides), and nothing else. Otherwise, the existing definition is used to identify dependencies for ��. Resolution of an ivar that appears on the LHS of a capture bound occurs by performing capture, introducing eq bounds for the results, and _discarding_ the capture bound (if we don't discard it, incorporation will immediately infer 'false'). If there are other ivars in the same interdependent set, besides those on the LHS of a capture bound, all the ivars are simultaneously resolved to fresh capture vars. Here's how that might happen (not exactly an everyday occurrence, although maybe there's a simpler example): interface PairList<T> extends List<Pair<T,T>> {} Bound: PairList<alpha> = capture(PairList<? extends Foo<beta>> Constraint: PairList<alpha> <: List<? extends Pair<? extends gamma, ? extends Foo<? extends gamma>>> becomes alpha <: gamma, alpha <: Foo<? extends gamma> alpha <: gamma, Foo<beta> <: Foo<? extends gamma> alpha <: gamma, beta <: gamma Then alpha, beta, and gamma all depend on each other.

02-07-2013