[External] : Re: Javac type inference issue

[Vicente Romero]

On 8/28/23 16:01, Attila Kelemen wrote:
> 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.

the compiler is basically doing an upfront capture conversion every time 
it does a subtyping test during inference, this produces the expected 
result for most type pairs but not for all as your test case proves,

Vicente

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