Generic Java type inference is unsound

To: Types List <types@cis.upenn.edu>
Subject: Generic Java type inference is unsound
From: Alan Jeffrey <ajeffrey@cs.depaul.edu>
Date: 17 Dec 2001 13:18:22 -0600

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
at:

  http://www.jcp.org/jsr/detail/14.jsp

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:

  http://fpl.cs.depaul.edu/Problem.java

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
fail.)

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

Cheers,

Alan.

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