The definition of "provably distinct" type arguments does not account for intersection types.  For example, if X extends Foo & Bar, is C<X> provably distinct from C<Bar>?

There is also some vagueness about what it means to perform "capture conversion, if necessary", and confusion about what the supertypes of a wildcard-parameterized type are (see 5.5.1).

(For context, the only meaningful impact of the "provably distinct" definition is in deciding which casts are allowed.)