Report a generic nullability mismatch as a marked diff of the two types - #1828

Why

In JSpecify mode, passing a List<?> to Collection.addAll in @NullMarked code was reported as incompatible types: List<?> cannot be converted to Collection<? extends Object> (List<?> is a subtype of Collection<?>). The report is correct: an unbounded wildcard takes the upper bound of the type variable it instantiates, and E of List has a @Nullable Object bound in the JSpecify JDK model, while ? extends Object requires a non-null element. Nothing in the message said so, and the parenthetical read as a contradiction (#1822).

The shape of the message was the wider problem. It printed the two types in full and left the reader to diff two strings, which is hopeless once the difference is a @Nullable three levels down, and it named at most one position out of however many failed.

What

The diagnostic is rebuilt around the positions where the two types differ in nullness. A parallel traversal of the target and the source records every such position, as the smallest pair of nodes that still differs, and the message is rendered from that list: a summary, both types with a caret under each position at fault, one entry per position naming it in words, and the types to write instead.

The summary line names the difference, not the types. It begins incompatible nullability:, so the leading text of every generic nullness diagnostic changes; the two types move into the found: and required: lines below. With one difference the summary states it (found @Nullable Object, required Object); with several it states how many. It says found/required rather than calling one unassignable to the other because the difference runs both ways: a type argument the source states outright has to match, so List<String> fails against List<@Nullable String> as surely as the reverse. That direction is the one a reader can misread as a false subtype claim, since every String is a @Nullable String, so there the line opens a type argument must match exactly.

The caret marks the smallest node that still differs, @Nullable String rather than the Collection<@Nullable String> around it, and it is drawn on both types. Where the position is one the source does not print, as with the bound an unbounded wildcard leaves implicit, the caret stays on the wildcard and a note: line says which type parameter the bound is inherited from. That note is what #1822 was missing. Which node of the source as written a caret belongs under has two answers, since the comparison views the source as the target's supertype: where that view is the same class, the position is the same position, and where it is another class, only a node the substitution carried over rather than rebuilt can be pointed at. Where neither answers, the view is printed as found as and carries the carets, so a caret always marks a type the check actually compared. A note there states the bound and stops: naming the type parameter it came from would mean naming a declaration the message does not print, and answering in coordinates of its own, so path: Base type argument B would stand beside type parameter S of Sub and read as a contradiction. Where the wildcard does stand at a position of the type the reader wrote, the note still names the parameter, which is what makes the message in #1822 readable.

A path: line names the position in words, as Map type argument V -> List type argument E -> wildcard upper bound -> Collection type argument E, and wraps at its separators for a deeply nested type. It is the channel that survives when the caret does not: a message pasted through a chat client, re-indented by a log collector, or read by a tool that never had the columns.

Every failing position is reported, numbered where there is more than one, up to five, after which the message says how many are left. The old message named one and left the rest for the next compile. A single mismatch and a numbered entry carry the same fields in the same order, so a reader who has learned one message has learned the other.

Two repairs are offered, and each is checked before it is offered. The source type rewritten with explicit wildcard bounds, as before; and the required type carrying the source's nullness, which is new. The second is a claim about which side of a contract is wrong, so it comes with two limits: it appears only where the required type is written at the diagnostic itself, as it is in a variable declaration, and it only ever adds @Nullable. At a call the required type comes from a signature somewhere else, and proposing an edit to it would be a guess at what that signature is for; taking a @Nullable away would be a guess of the same kind about a contract the author stated on purpose. A candidate is also withheld where printing it would drop a type-use annotation, since the printer shows @Nullable and nothing else: that costs a described type nothing and costs a pasted one whatever was left out. Both candidates are passed to subtypeParameterNullability, the predicate that rejected the assignment, and both must be denotable, since a type the check accepts may still print capture of ?, which no declaration may contain.

The format is written down where the next reporter will look. The rendering lives in NullabilityMismatchMessage, whose class comment states the contract a message follows: the four words it uses, the rule for the first line, when a caret is drawn and when it is declined, and what each of the two repairs presumes. A reporter that adopts the format inherits those rules; one that builds its own message text is not bound by them and reads worse for it. GenericsChecks ends the change 161 lines shorter than it started, having lost the old message machinery and gained none of the new.

Where the traversal locates no difference, which is what a ? super containment failure looks like from here, the message falls back to incompatible types: A cannot be converted to B with the subtype relation, as before.

Two mechanisms are worth naming for review. The target is traversed as the reader wrote it, so a position in it is a path, and the same path tells the printer where to draw the caret; the source is viewed as the target's supertype at every level, which is a type the reader never wrote, so the source node is carried by identity and located in the printed source afterwards. And javac's WildcardType.bound is overwritten by each substitution during asSuper, so the type parameter named in a note is found by the wildcard's position in the source rather than through that field, which after viewing List<?> as a Collection names E of an intermediate supertype.

A type variable is explained rather than printed twice. #1834 makes the check reject a Box<T> declared with T extends @Nullable Object where a Box<? extends Object> is required. The traversal that finds the differing positions judged such a variable by its use site, found no difference, and left the reporter with the fallback text, so the reader was told only that two types were incompatible. It now takes the same step the check takes: the caret stays on the T they wrote, found names the bound the variable was declared with, and a note says the nullness comes from there. A use that states its own nullness keeps it and gets no note, since the printed @Nullable T already says what the note would.

Examples

The issue's own case, where writing the bound out repairs the assignment:

incompatible nullability: found @Nullable Object, required Object
    found:    List<?>
                   ^
    required: Collection<? extends Object>
                                   ^^^^^^
    path: Collection type argument E -> wildcard upper bound
    note: the source ? has no explicit upper bound, so its upper bound is inherited from type
          parameter E of List
    did you mean List<? extends Object>?

A difference nested four levels down, where the caret does the work no prose can:

incompatible nullability: found @Nullable String, required String
    found:    Map<? extends Object, List<? extends Collection<@Nullable String>>>
                                                              ^^^^^^^^^^^^^^^^
    required: Map<? extends Object, List<? extends Collection<String>>>
                                                              ^^^^^^
    path: Map type argument V -> List type argument E -> wildcard upper bound
          -> Collection type argument E

Two positions at fault, one of them a concrete type argument that no wildcard bound explains:

incompatible nullability: 2 mismatches between source and target types
    found:    Map<?, @Nullable String>
                  ^  ^^^^^^^^^^^^^^^^
                  1  2
    required: Map<? extends Object, String>
                            ^^^^^^  ^^^^^^
                            1       2

    1. path: Map type argument K -> wildcard upper bound
       found:    @Nullable Object
       required: Object
       note: the source ? has no explicit upper bound, so its upper bound is inherited from type
             parameter K of Map

    2. path: Map type argument V
       found:    @Nullable String
       required: String

The source viewed as the supertype it was compared against, where the type as written shows nothing:

incompatible nullability: found @Nullable Object, required Object
    found:    Sub<?>
    found as: Base<?>
                   ^
    required: Base<?>
                   ^
    path: Base type argument B -> wildcard upper bound
    note: the source wildcard has an implicit @Nullable Object upper bound

A variable declaration, where the required type is written at the diagnostic and the reader can change either side:

incompatible nullability: found @Nullable String, required String
    found:    Map<? extends String, @Nullable String>
                                    ^^^^^^^^^^^^^^^^
    required: Map<? extends Object, String>
                                    ^^^^^^
    path: Map type argument V
    consider changing the required type to:
      Map<? extends Object, @Nullable String>

Verification

WildcardTests holds 118 tests, 53 of them added here, covering the rendering and both repair decisions: the caret at the smallest differing node, in a nested type argument, an array element and an enclosing type; a source instance that fills two type arguments, and one the comparison reached in a view of the source; the numbering, and the cut-off at five with the count of the rest; a source repair withdrawn for an explicit-bound mismatch, for bounds differing below the top level, for a concrete type argument, for an unrewritable ? super, for a candidate holding a capture, and for one whose printed form would drop a type-use annotation; a required-type repair offered at a variable declaration and withheld at a call, in the direction that would drop a @Nullable, and where printing it would drop an annotation. Nine tests declare the type a repair suggests in the same source and assert it draws no diagnostic, one for each shape of repair the message offers; the tests that pin a repair only as message text rely on that coverage rather than repeating it. Every test named for the absence of a repair asserts that absence rather than stopping short of it.

Thirteen deliberate breakages were run against the suite, each failing the test named for it:

About a hundred expectations across the JSpecify suites changed with the message text; :nullaway:test and :nullaway:buildWithNullAway pass.

Scope

This branch is stacked on #1834, which makes the check reject the type-variable case this message then explains. Until that merges, the diff here carries its commit as well; the two touch different files apart from the tests they share.

The incompatible types message is shared by the assignment, return, and parameter reporters, and all three carry the new rendering. The ternary, method-reference, and override reporters build their own messages and are unchanged, so a List<?> in one of those positions still gets the old text; those reporters have their own mechanics and their own diagnostics, and a separate pull request will bring them across.

The message text is not API, but anything matching on it, such as a golden-output test in a downstream build, sees incompatible nullability: where it saw incompatible types:.

Three branches have no test because no input was found that reaches them: the class-type requirement on the bound to write out, in rewriteWithExplicitBounds; three of the four node kinds isDenotable rejects; and the root position in mismatchDetail, which would print path: the type itself, since a nullness difference at the root of the two types is reported by another check before this one is reached. All three are recorded in the code rather than claimed as covered.

Fixes #1822