An experiment in type inference and verification by abstract interpretation