I noticed an apparent hole in the way in which subtyping rules deal with intersection types. Consider the following example

class Test {
   static interface I {}

   static class C2 extends C1 implements I {}

   static class C3 extends C1 implements I {}

   public <T> T m1(T t1, T t2) { return t1; }

   public void test(C2 c2, C3 c3) {
       m1(c2, c3);         }
}

In this case T is inferred to be the intersection type C1&I. If we look at the subtyping rules for intersection types, it's not clear, however, that either C2 or C3 are subtypes of the type C1 & I. This relation should hold, since otherwise it would mean that we are inferring a type that make the selected method unapplicable (since actuals are not subtypes of formals). Any idea on how to fix this?

Currently we only know that the supertypes of an intersection type C&I1&I2 ... &In are C, I1, I2 ... In, respectively.
It seems sensible to say that a classtype CT is a subtype of an intersection type C&I1&I2 ... &In iff CT <:  C &&  CT  <:  I1 ...  &&  CT  <:  In.
however this is not stated in the JLS

Fixing this is crucial in order to properly implement method applicability as described in 15.12.2.2:

"The method m is applicable by subtyping if and only if both of the following conditions hold:

    * For 1in, either:
          o Ai is a subtype (§4.10) of Si (Ai <: Si) or
          o Ai is convertible to some type Ci by unchecked conversion (§5.1.9), and Ci <: Si. 
    * If m is a generic method as described above then Ul <: Bl[R1 = U1, ..., Rp = Up], 1lp. "

As types U1, U2 ... Un are inferred types that might be intersection types. It's quite common to end up with a subtyping test of the kind:

A<T> <: A<? extends B&C> that leads to:
T <: B&C (should be OK if T extends/implements both B and C)
A further problem with intersection types is that they allow a type of the form I<T1> & I<T2> where I is an interface type and T1, T2 are two unrelated types. This can be exploited to produce unpredictable results:

interface B<X> { public X m(); }

class C implements B<String> {}

class A<X extends C> {
   X x;

   A<? extends B<Integer>> b = null; // bound of the captured type var is B<Integer>&C, i.e. B<Integer>&B<String>
   Integer o = b.x.m();  // which m()? - compiles with Eclipse
   String o = b.x.m();  // which m()? - doesn't compile with Eclipse
}

Type variables already require that "The erasures of all constituent types of a bound must be pairwise different, or a compiler-time error occurs." But since intersection types "arise from the process of capture conversion", we should be clear about their form too. JLS 4.9 should say: "The constituent type expressions of an intersection type must be pairwise provably distinct, or a compile-time error occurs."