@GuardSatisfied on array elements

The Lock Checker forbids using @GuardSatisfied on an array element type; you get a warning message such as:

GuardSatisfiedArray.java:7: error: [guardsatisfied.location.disallowed] @GuardSatisfied annotations are only allowed on method return types, receivers and parameters.
    void bar(@GuardSatisfied Object[] args) {
             ^
1 error

I believe that @GuardSatisfied should be permitted on all components of a return or formal parameter type. This includes array element types.

I don't remember a theoretical reason why @GuardSatisfied is not permitted on non-top-level components -- that is, I don't see a type loophole.

There is a test case in file checker/tests/lock/GuardSatisfiedArray.java .

Start with checker/tests/lock/GuardSatisfiedArray.java and run the Lock Checker test that demonstrates the current diagnostic. Trace the Lock Checker handling of @GuardSatisfied locations and determine how array element types are rejected. Done means the test permits @GuardSatisfied on array elements of return or formal parameter types without emitting the disallowed-location error.