Figure out how JDK 21 record patterns interact with nullability annotations

[msridhar]

Consider the following code using a record pattern:

class Records {
  record Rec(Object fst, @Nullable Object snd) {}
  void ex(Object obj) {
    if (obj instanceof Rec(Object f, @Nullable Object s)) {
      s.toString(); // possible NPE
    }
  }
}

It seems clear NullAway should report an error on the dereference above. What if the code is written as follows?

  void ex(Object obj) {
    if (obj instanceof Rec(Object f, Object s)) {
      s.toString(); // possible NPE
    }
  }

Here I think the error should be reported in the pattern itself: if the code explicitly writes Object s, the top-level nullability annotation should match the record declaration. Finally, if var is used:

  void ex(Object obj) {
    if (obj instanceof Rec(var f, var s)) {
      s.toString(); // possible NPE
    }
  }

Here I think we should infer the type of s to be @Nullable Object. I think all of the above also holds for uses of record patterns in switch cases.