Clarify the void allowlist wrt [] and []= (#4454)

This PR adds a clarification to the `void` allowlist, specifying explicitly that `e1` can have type `void` in the case where `e0[e1]` is encountered and the statically known operator `[]` of `e1` has a parameter whose type is `void`, and similarly for `e0[e1] = e2` where both `e1` and `e2` can have type `void` when the corresponding formal parameters have type `void`. It also clarifies that the same rule applies to setters. Finally, it clarifies the item about local variable / parameter assignments.

This PR also changes the word 'parameter' to 'argument' in the same item, in a location where it is clearly intended to refer to an actual argument, not a formal parameter.

See also dart-lang/sdk#57071.

Author: eernstg

specification/dartLangSpec.tex

@@ -41,6 +41,10 @@
 % version of the language which will actually be specified by the next stable
 % release of this document.
 %
+% Jul 2025
+% - Clarify that operator `[]` and `[]=` are included in the `void` allowlist
+%   rule about formal parameters of type `void`, and so are setters.
+%
 % May 2025
 % - Add `s?.length` as a constant expression in the case where `s` satisfies
 %   some requirements.
@@ -22873,7 +22877,7 @@ \subsection{Type Void}
   may have type \VOID.
   \rationale{Usages of that variable are constrained.}
 \item
-  An actual parameter expression corresponding to a formal parameter
+  An actual argument expression corresponding to a formal parameter
   whose statically known type annotation is \VOID{}
   may have type \VOID.
   \rationale{%
@@ -22882,14 +22886,28 @@ \subsection{Type Void}
     See the discussion about soundness below
     (\ref{voidSoundness}).%
   }
+  This rule also applies to the operators \code{[]} and \code{[]=}.
+  \commentary{%
+    For example, $e_1$ and $e_2$ may have type \VOID{}
+    in an expression of the form \code{$e_0$[$e_1$] = $e_2$}
+    when the parameters of the statically known operator \code{[]=}
+    both have type \VOID{}.%
+  }
+  Finally, this rule also applies to setters.
+  \commentary{%
+    For example, with an expression of the form \code{$e_1$ = $e_2$}
+    which denotes a setter invocation whose
+    statically known parameter type is \VOID,
+    $e_2$ may have type \VOID{}.%
+  }
 \item
   In an expression of the form \code{$e_1$\,=\,$e_2$}
-  where $e_1$ is an \synt{assignableExpression}
-  denoting a variable or formal parameter of type \VOID,
+  where $e_1$ is an \synt{assignableExpression} denoting a local variable
+  \commentary{(which can also be a formal parameter)}
+  of type \VOID,
   $e_2$ may have type \VOID.
   \rationale{%
-    Usages of that variable or formal parameter
-    are statically expected to be constrained by having type \VOID.
+    Usages of that variable are constrained because it has type \VOID.
     See the discussion about soundness below
     (\ref{voidSoundness}).%
   }