Nada Amin and Ross Tate recently published an excellent paper pointing out a soundness hole they found in the Java and Scala type systems. The actual mechanics of the bug are pretty close to an issue that comes up in type systems for functional languages, so I'm going to have a go at explaining it from that point of view (I still highly recommend reading the original paper, though).

In OCaml, you can write the type of equality witnesses, whose values represent evidence that two types are the same:

type ('a, 'b) eq = Refl : ('a, 'a) eq

(There's nothing OCaml-specific here except the syntax: the same type exists in Haskell, and both are a less powerful version of the equality types in dependently-typed languages)

The type ('a, 'b) eq takes two parameters 'a and 'b, but you can only make values of this type (Refl) when you know that the two parameters are equal. So, a value of type ('a, 'b) eq is evidence that 'a and 'b are the same type.

You can use this evidence to convert an 'a to a 'b:

let cast (type a) (type b) (eq : (a, b) eq) (x : a) : b=
  match eq with Refl -> x

To cast x from an a to a b, we match on eq (applying our evidence that a and b are the same type), then return x which we now know to be of type b, since b = a.

For this to be type safe, we need to know that Refl is really the only way of coming up with a value of type ('a, 'b) eq. If we are able to construct a value of type, say, (int, string) eq, then type safety breaks:

# let lies : (int, string) eq = Obj.magic 0;;
val lies : (int, string) eq = Refl
# cast lies 42;;
Segmentation fault

OCaml's type safety relies on not being able to construct an (int, string) eq (at least, without using the unsafe intrinsics in Obj).

Amin and Tate follow the same path, starting with something that looks like the ('a, 'b) eq type:

static class Constrain<A, B extends A> {}

There are two differences from ('a, 'b) eq. First, instead of equality, this talks about subtyping (B extends A rather than B = A). This difference isn't terribly important here, since B extends A is enough information to cast B to A.

The second difference is deeper: because this class exposes the B extends A constraint, we can't even talk about the type Constraint<Integer, String>. With OCaml's ('a, 'b) eq type, there is always a type (t1, t2) eq regardless of what t1 and t2 are. This separates the proposition (t1, t2) eq, which is a sentence saying "t1 and t2 are equal", from the proof Refl, which is evidence that the sentence is actually true.

Constrain<A, B> doesn't give us that, because in Java Constrain<A, B> is not even a type unless we already know that B extends A. It's a type error in Java to write a function taking a parameter of type Constrain<Integer, String>, because we don't know that String extends Integer. By constrast, such a function is perfectly fine in OCaml, but it can never be called because you'll never be able to supply a suitable argument (without using unsafe functions like Obj.magic).

Amin and Tate find a nice way around this, using the type:

Constrain<U, ? super T>

This is a type regardless of what U and T are. In particular, Constrain<Integer, ? super String> is a type. But since we can only have a Constrain<U, ? super T> if the ? extends U, then we must have T extends ? extends U, so having an instance of this type implies that T extends U.

It's even possible to write the cast function that applies this evidence to turn a T into a U, although we have to jump through a few more hoops than the OCaml version does:

static <T, U> U cast(Constrain<U, ? super T> eq, T t) {
  return new Bind<U>().upcast(eq, t);
}
static class Bind<A> {
  <B extends A> A upcast(Constrain<A, B> constrain, B b) {
    return b;
  }
}

(The exact code needed to make cast typecheck varies by compiler version. I've adapted some code from Figure 1. of the paper, but they give a few versions that work on different compilers).

By itself, there's nothing problematic about this function. It's able to turn a T into a U, but only if you provide a Constrain<U, ? super T>. We should only be able to come up with one of those if T is in fact a subtype of T, so this seems just as safe as the cast function in OCaml.

The trouble is that Java types have more values than they should: null is a value of every reference type, and null will happily act as evidence for lies:

String zero = cast(null, 0);

Running this, we get fireworks, without using any unsafe features:

Exception in thread "main" java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
	at Unsound.main(Unsound.java:12)

(The explosion is a bit less dramatic than in OCaml, because the JVM doesn't actually trust the javac compiler's type checking of generics, and inserts dynamic class checks in generic code. So, the effect is that we see a ClassCastException in a program containing no casts, rather than a segfault).