In the 0.6.2 Lambda spec, a compatibility constraint (ArrayList -> List<alpha>) reduces to a subtyping constraint (ArrayList <: List<alpha>). This does not allow for unchecked conversion (ArrayList <: List<alpha> reduces to false). It is not sound to simply erase the supertype (ArrayList <: List), because there's not always a simple mapping from the type parameters of the subtype to the type parameters of the supertype. Actual compiler behavior -- precisely when an unchecked conversion is allowed -- is poorly-defined.

Solution: Define legal unchecked conversions in terms of inference. Introduce new inference variables when a raw type needs to be unchecked-converted (e.g., ArrayList<beta> <: List<alpha>), and include these variables in the enclosing context.