necessary information is never considered by inference?

[Stephan Herrmann]

Consider this example:

import java.util.stream.Stream;
import java.util.*;
import static java.util.stream.Collectors.collectingAndThen;
import static java.util.stream.Collectors.toList;
public class X {
	void test(Stream<List<Integer>> stream) {
		stream.collect(collectingAndThen(toList(), Collections::unmodifiableList))
			.remove(0);
	}
}

I fail to see anything in the spec that would let us determine the
return type of the collect(..) invocation. Hence the remove() call
would be unresolvable.

Given that javac does accept the program, I'm wondering what's causing
this discrepancy.

We have two inference variables from the outer invocation, let's write it as:
   <R#0,A#1> <R#0 collect(Collector<? super List<Integer>,A#1,R#0>)
plus four inference variables from the inner invocation:
   <T#2,A#3,R#4,RR#5> Collector<T#2,A#3,RR#5> collectingAndThen(Collector<T#2,A#3,R#4>, Function<R#4,RR#5>)

My question is: how do we get a constraint that would help inference
to find the desired instantiation for R#0.
 From the dependencies / instantiations I see, these are relevant:
   RR#5 = R#0
   R#4  = List<List<Integer>>
There's no dependency between R#0/RR#5 and any other type in sight.

It seems we could only get this connection from inspecting the
method reference Collections::unmodifiableList, from which we *might*
deduce constraints in the following vein (ignoring exact relations):
   List<? extends T#6> ~ R#4
   List<T#6> ~ RR#5
which would probably allow us to correlate R#4 with RR#5.

However, I don't see where the spec would allow me to introduce
such constraints: we're reducing this constraint:
   ⟨collectingAndThen(toList(), Collections::unmodifiableList) → Collector<? super List<Integer>,A#1,R#0>⟩
for this reduction 18.2.1 instructs me to apply 18.5.2 for computing B3.
The problem is: computation of B3 only comprise those parts of 18.5.2 that
never touch the argument expressions, those come into the picture only after.

I made experiments to let 18.2.1 compute B4 instead of B3, this would
nicely produce an "interesting" constraint
   ⟨Collections::unmodifiableList → java.util.function.Function<R#4,RR#5>⟩
but while the outer inference (collect) is still running we don't seem to
be in a position for resolving any inference variables. OTOH, reducing
the constraint with inference variables in these positions yields false
(inexact method reference, whose function type has non-proper parameters).
If I would ignore even that rule I *would* get at least this:
   ⟨List<Object> → RR#5⟩

So, what *does* create the connection between R#4 and RR#5??

thanks,
Stephan

PS: note that the problem does not occur when making the method reference
exact by saying "Collections::<List<Integer>>unmodifiableList".