If one link of an @Implies chain is bad, are the following links still followed?

[cpovirk]

For example (from #240 (comment)), what if one link is bad because it implies an annotation with a required element?

@interface One {}

@Implies(One.class)
@interface Two {
  String somethingRequired();
}

@Implies(Two.class)
@interface Three {}

@Three void foo();

We already know (from #240) that foo() is not considered to have @Two "present." Should it also not be considered to have @One "present?"

That would be justified by a rule that a chain of implication stops entirely at an unrecognized edge.

We could imagine other variants of this, too, like one that involves a difference in @Target. (I forget whether we have a proper writeup of that somewhere, but I see I linked #34 (comment) in a discussion of it previously, so let's go with that.)

@Target(METHOD)
@interface One {}

@Implies(One.class)
@Target(FIELD)
@interface Two {}

@Implies(Two.class)
@Target({FIELD, METHOD})
@interface Three {}

@Three void foo();

As in the previous example, the question is whether foo() is considered to have @One "present."

[cpovirk]

(Ugh, I was going to post a short followup, but it's become long. Maybe I can come up with another post that will be short.)

In thinking about this, I've been thinking in terms of two subtly different categories of badness:

1. "This implication link is bad."
2. "The annotation added by this implication link is bad."

By "This implication link is bad," I mean something like my first example above: @Implies(Two.class) is itself bogus (because @Two has required elements). We can tell that just by looking at the declarations of @One and @Two.

By "The annotation added by this implication link is bad," I mean something like this:

@Implies(Nullable.class)
@interface MyNullable

@MyNullable @NonNull String s;

In that case, the abstract idea that @MyNullable implies @Nullable is fine. The problem arises only at the use site, when @MyNullable @NonNull creates a conflict.

I had been focused on the first category when I wrote my initial post, but we should figure out if it actually makes sense to treat the categories separately.

Returning to my initial post: My second example from that post is... at least mostly like the first one, but I can tweak the example to make it more distinct:

@Target({MODULE, METHOD})
@interface One {}

@Implies(One.class)
@Target({MODULE, FIELD})
@interface Two {}

@Implies(Two.class)
@Target({MODULE, FIELD, METHOD})
@interface Three {}

@Three void foo();

In this new example, there's nothing wrong with any individual implication edge or even with the implication chain as a whole. (I mean, I think we're OK with having an annotation be applicable to more locations than the annotation it implies is, right? as long as there's some overlap, in the broad sense of "overlap" permitted by #124?) But if we were to evaluate the @Target values in the context of the particular usage on foo(), then we'd find that we encounter a step at which we're looking at whether @Two is present on foo(), concluding "no, because its @Target is wrong," and yet maybe still following its implication edge to @One and concluding that @One is present. It's weird for @One to be present but the annotation that implied it not to be, but that could already happen in other cases if we did something like #259 (comment).)

For that matter, we can produce that case without appealing to multiple @Implies steps or @Target differences at all:

@Target(TYPE_USE)
@interface ApplicableToLocalVariables {}

@Implies(ApplicableToLocalVariables.class)
@Target(TYPE_USE)
@interface NotApplicableToLocalVariables {}

void foo() {
  @NotApplicableToLocalVariables String s;
}

That's pretty perverse, especially since JSpecify cannot know in general whether a particular annotation is applicable to top-level local-variable types or not. (#136 could help with that particular case, but it wouldn't cover other cases we care about, like outer types and primitives. Maybe this also relates to the kevinb9n goal of distinguishing @NonNull Outer.Inner from @Nullable Outer.Inner, with the former being redundant and the latter being worse than that? Or maybe, again, this is just not a path we want to go down.)

[cpovirk]

Without thinking about this in great detail (ha!), I'm inclined to aim for the same kind simplicity as proposed in #311:

We'd start by following every @Implies link (or perhaps almost every @Implies link) to collect all the annotations in the resulting graph. After that, we'd check for @Target mismatches and conflicts, removing only the problem annotations (and not extending the removal to anything that they imply that is free of mismatches and conflicts).

The main remaining question to me at that point is the original one: If @Implies(Foo.class) is bad because Foo has a required element, do we stop following the chain there, or do we continue? I'm somewhat inclined to say that we stop there: A tool's first step would naturally be to collect "what all the annotations and their element values are," so we'd be asking it to track a @Foo annotation that is missing its required element. But I would have to imagine that tools still could track that if we wanted. Maybe they'd even tell us that that's simpler than stopping following the chain. I don't think we have reason to care too much either way, so my leaning is toward whatever seems simplest to specify and implement.