(but is in fact correct that Java's type system isn't entirely sound, I forget the details, but I believe array element type variance is one of the soundness hole.)