Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?