Coinductive type systems for object-oriented languages