Javac type inference issue

[Attila Kelemen]

What I find the most interesting about this issue is what Rémi showed. If
you change the argument type of listMethod from `List<List<? super T>>` to
`List<? super List<? super T>>`. then the type inferer can find the correct
type assignments. And this looks bizarre to me, because that just looks
like a straight up more difficult problem, yet it is demonstrably not so
for the compiler.

Vicente Romero <vicente.romero at oracle.com> ezt írta (időpont: 2023. aug.
28., H, 20:56):

> very interesting issue, I agree that the compiler could do better here,
> this needs more research, I have been taking a look at the compiler
> internals, it could be that a structural type comparison could be needed
> here. In the mean time I have filed [1]
>
> Thanks,
> Vicente
>
> [1] https://bugs.openjdk.org/browse/JDK-8315134
>
> On 8/28/23 06:59, Maurizio Cimadamore wrote:
>
> This does seem like an issue.
>
> Note that similar code, w/o a method call works:
>
> List<List<? super T1>> res = Arrays.asList(args);
>
> I did some manual calculation of the bounds involved and I got to:
>
> List<? super T1> <: #A = List<? super #T2>
>
> Which seems solvable for:
>
> A = List<? super T2>
> T2 = T1
>
> But the javac error message reveals a capture conversion is being applied
> somewhere:
>
> error: method listMethod in class Test cannot be applied to given types;
> List<List<? super T2>> res = listMethod(Arrays.asList(args));
>                              ^
>   required: List<List<? super T2>>
>   found: List<List<? super T1>>
>   reason: inference variable T has incompatible bounds
>     equality constraints: List<? super CAP#1> // <--------------------------
>     lower bounds: List<? super T1>
>
> Which seems odd - I would have understod if javac tried to capture “args”
> before passing to Arrays::asList - but that’s not what is happening here.
>
> My feeling (confirmed by looking at the internals of the compiler) is that
> javac is applying incorporation to the above set of bounds - and running
> the following check:
>
> List<? super T1> <: List<? super #T2>
>
> The JLS here says that when running the this incorporation step, since
> both types are ? super X wildcards we should just derive:
>
> #T2 <: T1
>
> (e.g. no capture conversion applied).
>
> But that’s not what happens in the compiler implementation (which does a
> straight subtyping check with capture conversion), hence the issue.
>
> Maurizio
>
> On 27/08/2023 15:06, Attila Kelemen wrote:
>
>
>> In case of a capture, the inference does not try to replace the capture
>> by its bound. It's a limitation of the inference which tend to choose the
>> most speciifc type where here, it has to use a less specific type.
>>
>>
> I don't quite understand the step by step "reasoning"  of the type inferer
> here, because naively this is what I would do if I was employed as a full
> time type inferer :). (I'm copying here my code again with some variable
> renaming for easier reference) Suppose I'm a compiler, and I see this:
>
> ```
> <T1> void arrayMethod(List<? super T1>[] args) {
>     listMethod(Arrays.asList(args));
> }
> <T2> void listMethod(List<List<? super T2>> list) { }
> ```
>
> 1. I look at `arrayMethod` and see 2 type variables to infer. One for
> `listMethod` (let's call it #L), and one for `Arrays.asList` (let's call it
> #A).
> 2. The first thing I see is that `Arrays.asList` returns `List<#A>`, and
> it is assigned to `List<List<? super #L>>`. This is easy to satisfy with #A
> = List<? super #L> (and this is actually the only possibility).
> 3. Then I go the next part, and see that args is of course `List<? super
> T1>[]` which must be assigned to `#A[]`, which is again easy to satisfy
> with #A = List<? super T1> (which is the only possibility again).
> 4. So, now I have to satisfy all equalities `#A = List<? super #L>` and
> `#A = List<? super T1>`, which implies that `List<? super #L> = List<?
> super T1>`, which is easy to satisfy by the choice #L = T1 (again, this is
> the only choice).
> 5. So, now I have resolved both variables:` #L = T1`, and `#A = List<?
> super T1>`, and indeed I can validate that this choice will satisfy every
> constraint.
>
> I'm just puzzled here, because sometimes the type inferer can solve much
> more difficult problems, and this seems trivial compared to those.
>
>
>
>> My bad, I should have written List<? super List<? super T>>.
>>
>>
> Surprisingly (to me), that would compile without explicitly specifying the
> type arguments (though of course that is not a type declaration that is
> acceptable for me). What surprises me here is that I would think that this
> would make the job of the type inferer harder, since now it is more
> difficult to find the correct types, since there are more options. Without
> the outer "? super" the inferer would be forced to make the correct type
> assignment (since there is always only one possibility). That is, when you
> write `List<? super List<? super T>`, now you get another fresh type
> variable to satisfy. Namely, you have to pick a type of `? super List<?
> super T>`. While in the other case your only option for this was `List<?
> super T>` (which is the only correct choice even in the `? super` variant.
>
> ​
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/compiler-dev/attachments/20230828/c5292690/attachment-0001.htm>