Provable distinctness is a tool used by cast checking (5.5.1) to decide if two sets of type arguments are compatible.  Intuitively, two type arguments are "provably distinct" no object can ever exist that is an instance of both parameterizations.

The JLS rules are as follows:

- If both type arguments are non-variable types, they are provably distinct if they are different types.

- Otherwise, map wildcards and type variables to their upper bounds, and then test whether their erasures are related classes or interfaces (that is, one erased type is a subtype of the other).

This is unsound: there are clearly objects that have both types List<? extends Runnable> and List<? extends Cloneable>. And there may, in fact, be objects that have both types List<Class<String>> and List<Class<X>>, even though these would be considered provably distinct. (Compare List<String> and List<X>, which are not considered provably distinct.)

In addition, there are a lot of types that are logically disjoint but these rules don't detect it. The use of erasure is especially strange, and discards a lot of information (see JDK-8033709).

As an alternative, we already have a fairly sophisticated system for determining constraints on type variables -- type inference (JLS 18). These tools could be fairly directly utilized to provide a more accurate definition of provable distinctness.