Complete coinductive subtyping for abstract compilation of object-oriented languages