00cc056 (or at least that's the main code)

I no longer remember all the context for this one, and it probably would be wise for me to make sure that the change is even still necessary. (I suspect that it is, if only to avoid warnings for using <?> with a type parameter whose bound is "unspecified nullness." But if that's the only fallout from reverting this change, we could probably do so.)

Anyway, the basic idea seems to be to stop treating wildcards as if they have a bound that matches the corresponding type parameters'. I think this is part of CF's approach to wildcards (which they use instead of capture conversion). I think we get away without it because of our own handling of that, which is in jspecify/jspecify-reference-checker@15e9517#diff-ce82a59b06d0d82bfc6d06835d1b06ac15619bc3a71617d32189d041f02ca9c0R399 and possibly other places.

Changes from

• 5fc6c28
• and handling of verbose generics (didn't track down commit that removed that code, yet).

(as opposed to on their bounds)

• 1db27ba
• 235b632

As the latter commit explains, I quite possibly could have done this in our TypeAnnotator if I'd been thinking. That way, we wouldn't need to modify CF.

That said, this change isn't too important, since we already report an error for such annotations. But if they appear in unchecked code or if users suppress the error, it would be nice for them to still have no effect.

f3e9f21

Note that that links to jspecify/jspecify-reference-checker@2bab27e, which describes another problem solved by that commit. It doesn't seem that "not inheriting annotations" is necessarily a sufficient fix for that problem in general, but it works here. More to the point, if we someday restore inheriting annotations, we'll still need a way to avoid the recursion. (The linked commit does discuss some other options.)

These commits:

• 763b130
• 2e3deb7
• 0843fc5

Add a new showTypes option used by the conformance tests.

See how we can generalize LSP support to output the same information and adapt the conformance tests to the changed format.

28089b9

Obviously this is minor, and obviously it is sometimes nice to be able to suppress only a more fine-grained category. For the moment, though, I am erred on the side of making the output shorter and making it clear how to suppress. If we end up wanting to stick with that approach, we'd want to upstream.

There may be other ways around this: Maybe we'd plug in our own Messager that munges the default message.

(Note that it is not sufficient to define a single message key, nullness=%s, and then use it for all errors we report. That's because CF itself issues errors with its own keys.)

At the moment, we're probably just going to disable them entirely: #19. But it could make sense to make this configurable through a flag.

ff45ce7

As noted in that commit, we may end up wanting to support it after all.

If so, then we have a different task ahead of us: Figure out if CF's behavior for "the Ordering.min/max case" (discussed in the commit message) qualifies as a bug, and either make CF's logic accommodate our subtyping logic or make our subtyping logic work around what it needs to.

And actually, we might need to do one of those anyway: It might be possible to produce a new failure in our prototype checker by changing the code to compare E[] and F[] using a subtype check instead of an equality check. Presumably we'd do that by writing a sample that uses the return type instead of a parameter.

It may be that the CF difficulty is here:

https://github.com/typetools/checker-framework/blob/fd0abaa8b8fea775aaf71057d93d9415355b665e/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java#L1387

CF calls createType, but it probably it is not "adapting the formal parameter types of N to the the type parameters of M." (It's probably also not applying defaulting rules -- a separate issue that may also be worth a look at some point.)

Changes in 0a0904f

Both eisop and typetools have several changes in this area, so let's see whether any of this will be necessary.

c5f5118

The upstream code is essentially implementing GLB, anyway, only by using isSubtype.

(It turned out to be nice that I had had to migrate from MultiGraphQualifierHierarchy to ElementQualifierHierarchy: That had forced me to implement greatestLowerBound myself instead of inheriting an implementation that would likely have had the same problem as the CFAbstractValue code.)

But! CFAbstractValue has a concept of a "backup." Still, I'm hoping that we could preserve that by upstreaming a slightly less aggressive version of the above commit: We would still verify that a <: b or vice versa. But then, instead of inserting whichever one we detect to be the subtype first, we would still insert greatestLowerBound(a, b). That would be equivalent to the existing code for reasonable type systems, but it would still work for our unreasonable type system :)

ddec8ff

I should type more here, but for now, see the description of that commit. See also the usage in jspecify/jspecify-reference-checker@2237cda

ad7d132

Unless I got confused, both that and -AassumePure/-AassumeSideEffectFree are necessary in order to get the results I'm hoping for.

When we look to upstream this, we should try the obvious alternative to my blunt approach: Instead of hardcoding if (true), make sure to propagate the value of allowNonDeterministic (which we always set to true and I don't think any framework code calls) to recursive fromNode and fromTree calls. Perhaps CF would even consider it a bug that they don't do this at present -- but I'm unsure, since I haven't thought through all the implications of undoing our purity/side-effect-free assumption.

https://github.com/jspecify/checker-framework/blame/2eea6f8242391624def3818289abc44c1ec4ae0b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java#L562

This ignores parts of the checks in visitParameterizedType and notes that the check seems weird.

Steps:

• investigate whether the EISOP behavior makes sense or needs adjusting,
• investigate what different behavior the jspecify-reference-checker needs,
• address by either adjusting upstream in general or adding a new helper method to allow downstream adjustment.

So far, I've opened issues only for changes that I've suspected we absolutely need to make to CF in order to make our checker work.

But there are plenty of places in which our checker could be cleaner (read: less hacky) if we made additional changes to CF. Just to pick the most recent example, I can't imagine that anyone would feel great about how I default type-variable usages only conditionally. Perhaps CF could have native support for this. [update: I backed out my hack because it was -- who could have guessed? :) -- buggy. And I have replaced it with another upstreaming proposal, #7. But the general point stands. To offer a new example, I present another fragile-looking hack.]

But some of our needs make little sense to 99% of CF checkers. So, as with many of the changes we've already made in this CF fork, we may find it hard to argue for supporting them upstream. Still, it would be nice to eventually look into the possibility of replacing hacks with CF changes: Hacks often break somewhere down the line.

Understand what this change achieved and see whether it is still necessary. If it is, find a way to upstream.

(different from #9)

• Include class name along with method name: b7cd35c
• Plug in arbitrary information (but perhaps my current approach is overly general): 508185c [edit: used by jspecify/nullness-checker-for-checker-framework@9a44397 for ternaries], with perhaps more to come in the future

9ab109c

I assume that we don't really need to upstream this: The built-in CF nullness checker reports a full error for cases like casting from @Nullable Object to int. It might well always do this in cases that are actually unsafe (although then... why issue a warning?). (The built-in CF nullness checker also doesn't report an error, so perhaps it takes some action to short-circuit the cast.unsafe check.) Presumably we could do the same. But for now, I made cast.unsafe an error in our copy.

fd977fe

I suspect that there will ultimately be no need to upstream this: The types of enum constants should matter only in implementation code, so it can be covered by dataflow analysis once we implement that.

Usage: jspecify/jspecify-reference-checker@ad33cbd

Understand changes to

• fixupBoundAnnotations from d1aba1c, related to #4
• getErased from ef726d7
• supertypesFromElement from 0a2de06

For each PR (and post-merge), add a job to run tests (maybe just conformance tests?) for the reference checker.

That way we can know whether the reference checker needs to be updated for any given change in this repo.

d1aba1c

CF already lets us override the TypeVariableSubstitutor, and we do so.

But our larger changes to substitution rules require changes to behavior even "before" substitution occurs. Notable, @NullnessUnspecified T (which is how we currently represent the type of a plain T when it appears in non-null-aware code) does not always have a nullness of "unspecified." That's because, if the type is instantiated with T set to a nullable type, the result must be @Nullable T. Therefore, it's not guaranteed safe to, e.g., dereference a value of type @NullnessUnspecified T, even in "lenient mode."

To upstream our current changes, we probably need to add methods to AnnotatedTypeFactory for the fixupBoundAnnotations methods in AnnotatedTypeMirror and for AsSuperVisitor to call.

Additionally, though, note that these changes do not make sense in isolation. They may invalidate assumptions in other parts of CF, so perhaps other code should be updated, too. (For example, is any of this related to jspecify/jspecify-reference-checker@89725d4#diff-ce82a59b06d0d82bfc6d06835d1b06ac15619bc3a71617d32189d041f02ca9c0R351? Or maybe that's caused by some other change I've made? Or maybe it will go away once we have dataflow implemented?) Or maybe the changes are just too weird to upstream without significantly more work, which we'd have to discuss.

Links:

• see "assumed parametric nullness" in https://docs.google.com/document/d/15NND5nBxMkZ-Us6wz3Pfbt4ODIaWaJ6JDs4w6h9kUaY/edit#heading=h.u8phmghg96wr
• https://jspecify.dev/tsttcpw.html#augmented-type-of-a-type-usage-in-code
• https://jspecify.dev/tsttcpw.html#substitution

Big changes to the ATF https://github.com/jspecify/checker-framework/blame/2eea6f8242391624def3818289abc44c1ec4ae0b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java#L5017 which come from 2e588e7

c24904e

At first glance, this looks straightforward (though it should come with a test). However, note that we change the value of boundType: Previously, it would match the type parameter's bound type (UPPER or UNBOUNDED, as the case may be). But in our commit, it is always UNBOUNDED. This may change behavior of existing code.

One possibility is to track "wildcard-site unboundedness" as a separate bit, used only to trigger our new UNBOUNDED_WILDCARD_UPPER_BOUND, while leaving boundType untouched to preserve existing behavior.

Usage: jspecify/jspecify-reference-checker@94bf778#diff-ce82a59b06d0d82bfc6d06835d1b06ac15619bc3a71617d32189d041f02ca9c0R541

(The only way I found to set this default was to modify the Checker Framework itself. In particular, I wasn't able to employ an approach like I did in jspecify/jspecify-reference-checker@8e46bea#diff-ce82a59b06d0d82bfc6d06835d1b06ac15619bc3a71617d32189d041f02ca9c0R288: IIUC, that code jumps between usages and declarations, so it can't track whether the wildcard itself appears in null-aware or non-null-aware code. Thus, it can't apply different defaults for the two cases.)

That should pick up at least a couple improvements:

• better support for T extends @Nullable Object
• an easier way to support package-level annotations that don't affect subpackages

I may be forgetting others.