We seem to lean toward allowing covariant return types and contravariant parameter types (in the nullness dimension). These are ordinary contractual refinements [EDIT: strengthenings]
I want to discuss backward refinements [EDIT: contractual weakenings]: covariant parameters and contravariant returns. Surprisingly, I'm going to claim these are also valid.
Scenario A: Foo.bar() has a non-nullable return type. SubFoo.bar() should not return null in any case, but for whatever reason, its author has decided to do so and no one will change their mind. (This situation could also arise from Foo changing after the fact.)
From jspecify's point of view, I think that @Nullable is the only correct way to annotate the return type of SubFoo.bar(), and the user should absolutely do so. That way, at least consumers who happen to have the static type SubFoo will behave correctly, and that is better than nothing.
From the "what our annotations mean as specification" perspective, there is nothing wrong here. It's just that from the "preventing bugs" perspective, any reasonable checker is going to want to issue a warning on SubFoo.bar(), explaining that it risks causing an NPE for anyone using SubFoo via its Foo supertype, and strongly recommending against doing this. It should also suggest considering modifying Foo itself, but we have to realize that such decisions tend to be made more on annoyance equilibrium than on correctness.
(I would hope that if the user just changed the SubFoo.bar() return type but left the code alone, they would get louder/worse errors for that, as that's the worst case.)
Scenario B: a covariant parameter type. Foo promises to accept null, SubFoo doesn't want to. Perhaps this case is slightly different: SubFoo has the option of just still declaring @Nullable, since it's allowed to throw NPE or any other exception for any reason it wants to. However, it still shouldn't, because it's withholding useful information from the callers who happen to have the SubFoo static type. So I think it works out similarly the Scenario A anyway.
We seem to lean toward allowing covariant return types and contravariant parameter types (in the nullness dimension). These are ordinary contractual refinements [EDIT: strengthenings]
I want to discuss backward refinements [EDIT: contractual weakenings]: covariant parameters and contravariant returns. Surprisingly, I'm going to claim these are also valid.
Scenario A:
Foo.bar()has a non-nullable return type.SubFoo.bar()should not return null in any case, but for whatever reason, its author has decided to do so and no one will change their mind. (This situation could also arise fromFoochanging after the fact.)From jspecify's point of view, I think that
@Nullableis the only correct way to annotate the return type ofSubFoo.bar(), and the user should absolutely do so. That way, at least consumers who happen to have the static typeSubFoowill behave correctly, and that is better than nothing.From the "what our annotations mean as specification" perspective, there is nothing wrong here. It's just that from the "preventing bugs" perspective, any reasonable checker is going to want to issue a warning on
SubFoo.bar(), explaining that it risks causing an NPE for anyone usingSubFoovia itsFoosupertype, and strongly recommending against doing this. It should also suggest considering modifyingFooitself, but we have to realize that such decisions tend to be made more on annoyance equilibrium than on correctness.(I would hope that if the user just changed the
SubFoo.bar()return type but left the code alone, they would get louder/worse errors for that, as that's the worst case.)Scenario B: a covariant parameter type. Foo promises to accept null, SubFoo doesn't want to. Perhaps this case is slightly different: SubFoo has the option of just still declaring
@Nullable, since it's allowed to throw NPE or any other exception for any reason it wants to. However, it still shouldn't, because it's withholding useful information from the callers who happen to have theSubFoostatic type. So I think it works out similarly the Scenario A anyway.