Empowering union and intersection types with integrated subtyping