Generic Java type inference is unsound

Dear types researchers,

Bracha, Odersky, Stoutamire and Wadler's Generic Java (OOPSLA 1998) is
an extension of Java to include support for generic types and methods. 
It forms the basis of the Java Specification Request draft specification
`JSR14: Add Generic Types to the Java Programming Language' described


The core of the type checking system was shown to be safe by Igarishi,
Pierce and Wadler (OOPSLA 1999) but the type inference system for
generic method calls was not subjected to formal proof.  In fact, it is
unsound, as demonstrated by the program available at:


This program compiles without error, but produces a ClassCastException
at run time, even though it contains no explicit casts.  (The casts are
produced by the compilation down to JVM bytecode, and should never

This problem has been verified by the JSR14 committee, who are working
on a revised langauge specification.



Alan Jeffrey               http://fpl.cs.depaul.edu/ajeffrey/
CTI, DePaul University, 243 S. Wabash Ave, Chicago 60604, USA