Well, to answer my own question, the lub can't be a pure function of the input types if that means it will lose information which it cannot afford to lose. As long as there are types which have one behavior before erasure and a different, incompatible behavior after (like Array[Nothing] and Array[Object]) then there's no way to avoid awareness of this when performing type computation. Otherwise it's like throwing a few divide-by-zeros into your proofs.