Why is this invalid Java? Type of ternary operator output

Check out this code.

// Print object and recurse if iterable
private static void deep_print(Object o) {
  System.out.println(o.getClass().toString() + ", " + o.toString());

  boolean iter = false;
  Iterable<?> i1 = null;
  Object[] i2 = null;

  if (o instanceof Iterable<?>) {
    iter = true;
    i1 = (Iterable<?>) o;
  } else if (o instanceof Object[]) {
    iter = true;
    i2 = (Object[]) o;
  }

  if (iter) {
    for (Object o_ : i2 == null ? i1 : i2) deep_print(o_); // ERROR: Can only iterate over an array or an instance of java.lang.Iterable
  }

I know how to solve it. I just want to know why it happens. Shouldn't the compiler simply check all the possible outputs?

The static result type of the expression (i2 == null) ? i1 : i2 is the common ancestor of i1 and i2 which is Object. A for statement requires the static type of the expression to be either an Iterable or an array type. That is not the case, so you get a compilation error.

Now if you are asking why doesn't the compiler deduce that (i2 == null) ? i1 : i2 will always be an array or an Iterable:

1. The Java language specification (JLS) does not allow this.
2. If the JLS did allow it (but not require it) then different compilers would behave differently, depending on how good they were at theorem proving. BAD.
3. If the JLS required it, then the compiler has to incorporate a sophisticated theorem prover^`1 (BAD SLOW), and you run into the "minor inconvenience" of solving the Halting Problem² (BAD BAD BAD).
4. In actual fact the compiler needs to know which of the two kinds of type the expression has because it needs to generate different code in each case.

Hypothetically, if the Java type system was a bit different, this particular case could be handled better. Specifically, if Java supported algebraic data types then it would be possible to declare o as being "either an object array or an iterable" ... and the for loop would be type-checkable.

^{1 - Suppose that o had been initialized as o = (x * x < 0) ? new Object() : new Object[0]. Determining that that will always result in an Object[] instance entails a small proof involving the fact that the square of a (real) number is not negative. That's a simple example, it is possible to construct arbitrarily complicated examples requiring arbitrary difficult proofs.}

^{2 - The Halting Problem is mathematically proven to be an incomputable function. In other words, there exist functions where it is mathematically impossible to prove whether or not they terminate.}