Is rethrow in multi-catch formally defined?

Why is throw e allowed, but not throw a, in the following case?

  void test() {
    try {
      System.out.println();
    } catch (Error | RuntimeException e) {
      var a = e;
      //throw a; unreported exception Throwable; must be caught or declared to be thrown
      throw e;
    }
  }

All of this intuitively makes sense, but from JLS 14.20

A multi-catch clause can be thought of as a sequence of uni-catch clauses. That is, a catch clause where the type of the exception parameter is denoted as a union D1|D2|...|Dn is equivalent to a sequence of n catch clauses where the types of the exception parameters are class types D1, D2, ..., Dn respectively. In the Block of each of the n catch clauses, the declared type of the exception parameter is lub(D1, D2, ..., Dn).

Since lub(Error,RuntimeException) is Throwable, the code above should be equivalent to:

    try {
      System.out.println();
    } catch (Error e) {
      Throwable lub = e;
      throw lub;
    } catch (RuntimeException e) {
      Throwable lub = e;
      throw lub;
    }

(which obviously doesn't compile)

Moreover, the type of the a is the type of e "when treated as if it did not appear in an assignment context" (JLS 14.4.1), but as shown above it's not the same as the type of e.

Is there anything I've overlooked?

Edit: this is not a duplicate of Why is it legal to re-throw a Throwable in certain cases, without declaring it? because this question is specific to multi-catch (which isn't discussed there) and arises due to a misunderstanding of a specific fragment of the JLS that addresses multi-catch. The answers provided in this question helped me to connect the dots :)

Solution

This is described in 11.2.2. This basically boils down to "exception parameters in catch (...) are a special case".

Our goal is to show throw e; compiles. We start with this line in 11.2.3:

It is a compile-time error if a method or constructor body can throw some exception class E when E is a checked exception class and E is not a subclass of some class declared in the throws clause of the method or constructor.

So we want to show that the try statement in test cannot throw Throwable. Note that "can throw" in this context is a rigorously defined term. According to 11.2.2,

A try statement can throw an exception class E iff either:

The try block can throw E, [...]

Some catch block of the try statement can throw E and either no finally block is present or the finally block can complete normally; or

A finally block is present and can throw E.

Only the second point is relevant here. Let's show that the catch block cannot throw Throwable. Namely, throw e; cannot throw Throwable.

A throw statement whose thrown expression is a final or effectively final exception parameter of a catch clause C can throw an exception class E iff:

E is an exception class that the try block of the try statement which declares C can throw; and

E is assignment compatible with any of C's catchable exception classes; and

E is not assignment compatible with any of the catchable exception classes of the catch clauses declared to the left of C in the same try statement.

throw e; here immediately fails the first bullet point, so we can conclude that throw e; cannot throw Throwable.

If it were throw a;, then the above doesn't apply, but another clause does:

A throw statement whose thrown expression has static type E and is not a final or effectively final exception parameter can throw E or any exception class that the thrown expression can throw.