Left subtyping argument must be captured

Per JLS 4.10.2, a subtyping test that involves indentifying the direct supertypes of a wildcard-parameterized type must capture the type before performing a substitution:

"The direct supertypes of the type C<T1,...,Tn>, where Ti (1 ≤ i ≤ n) is a type, are D<U1 θ,...,Uk θ>, where:
• D<U1,...,Uk> is a direct supertype of C<F1,...,Fn>, and θ is the substitution [F1:=T1,...,Fn:=Tn].
• C<S1,...,Sn> where Si contains Ti (§4.5.1) for 1 ≤ i ≤ n.

"The direct supertypes of the type C<R1,...,Rn>, where at least one of the Ri (1 ≤ i ≤ n) is a wildcard type argument, are the direct supertypes of C<X1,...,Xn>, where C<X1,...,Xn> is the result of applying capture conversion (§5.1.10) to C<R1,...,Rn>."

javac does not do this; as a result, unsound results are permitted. The following program compiles without error and crashes at runtime because the subtyping implementation allows C<?> <: A<Box<?>>.

public class WildSubstitution {

static class Box<T> {
 private T val;
 public Box(T val) { this.val = val; }
 public T get() { return val; }
 public void set(T val) { this.val = val; }
}

interface A<T> { T get(); void set(T arg); }
interface B<T> extends A<T> {}
interface C<S> extends A<Box<S>> {}

static class D implements B<String> {
 String s;
 public String get() { return s; }
 public void set(String s) { this.s = s; }
}

static class E implements C<String> {
 Box<String> b;
 public Box<String> get() { return b; }
 public void set(Box<String> arg) { b = arg; }
}

public static void main(String... args) {
 // B<?> <: A<?> is true
 Box<D> b1 = new Box<D>(new D());
 Box<? extends B<?>> b2 = b1;
 Box<? extends A<?>> b3 = b2;

 // C<?> <: A<Box<?>> is false
 Box<E> b4 = new Box<E>(new E());
 Box<? extends C<?>> b5 = b4;
 Box<? extends A<Box<?>>> b6 = b5;

 b6.get().set(new Box<Integer>(10));
 String s = b4.get().get().get();
}

}