Javac type inference issue

[Vicente Romero]

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/4afa6e08/attachment-0001.htm>