Alright, we're now good with both checker framework and nullaway.

Yep, Just Works™. Very cool, thank you. :)

So, I'm thinking this maybe could work better / more accurately in that with the current enforceNullSafety it pretty much assuming that enforceNullSafety = true the record is in a @NullMarked scope [with the scope based on class then package then module etc annotated with @NullMarked].

That is, if code is using jspecify then there is @NullMarked and @NullUnmarked on the module/package/class to control the scope of "it should be NonNull or Null unspecified by default". This PR is currently working / passing with the assumption that enforceNullSafety = true matches when the record is in a @NullMarked scope.

That is, currently there isn't code in the annotation processor to traverse up the enclosed types (class -> package -> module) looking for a @NullMarked or @NullUnmarked and using that to determine the NonNull'ness of a component of a record (and instead the code just uses the enforceNullSafety flag and assumes that matches what the jspecify scope has defined).

I'm pondering if it would be better if the enforceNullSafety was removed completely and instead if a record component isn't explicitly defined as NonNull or Nullable then:

• Traverse up to the record type and look for @NullMarked or @NullUnmarked, if neither are present then ...
• If the record is enclosed in another class traverse up to that class and look for @NullMarked or @NullUnmarked
• Traverse up to the package and look for @NullMarked or @NullUnmarked, if neither are present then ...
• Traverse to the module and look for @NullMarked or @NullUnmarked

Nb: Packages are not enclosed by "parent" packages.

Class members are enclosed by classes, which may be enclosed by other class members or classes. and top-level classes are enclosed by packages, which may be enclosed by modules.

I'm pondering if it would be better

why not both?

We can probably also try to annotation process those nullmark annotations

in any case we can add that as a fast followup, this PR is getting pretty big.

So, I'm thinking this maybe could work better / more accurately [...]

Yeah, that sounds right. Checker Framework presently supports neither annotation and NullAway has only experimental support for them (and the default happens to be acceptable for my use cases) so I have not experimented with those combinations.

why not both?

I suppose because enforceNullSafety runs somewhat counter to @NullMarked and @NullUnmarked, needlessly expanding the surface area and complexifying both the implementation and the usage, compared to an alternate with strict adherence to the annotations (presumably with some default -- does JSpecify suggest a default?). But either way, it is indeed something that can be built on top.

why not both?

I suppose because...

I'm thinking more along the lines of somebody who doesn't use static null analysis and wants the builders to enforce non-null at runtime anyway. this option would be useful for them.

Traverse up to the record type and look for @NullMarked or @NullUnmarked, if neither are present then .

hmm, yeah wasn't that hard to add