The notion of ThisType has been proposed to promote typesafe reuse of binary methods and recently extended to mutually recursive definitions. It is well-known, however, that ThisType does not match with subtyping well. In the current type systems, type safety is guaranteed by the sacrifice of subtyping, hence dynamic dispatch. In this paper, we propose two mechanisms, namely, nonheritable methods and local exactization to remedy the mismatch between ThisType and subtyping. We rigorously prove their safety by modeling them in a small calculus. Categories and Subject Descriptors D.3.1 [Programing Languages]: Formal Definitions and Theory; D.3.2 [Programming Languages]: Language Classifications—Object-oriented languages; D.3.3 [Programming Languages]: Language Constructs and Features—Classes and objects; Polymorphism; F.3.3 [Logics and Meaning of Programs]: Studies of Program Constructs—Objectoriented constructs; Type structure General Terms Design, Languages, Theory Keywords b...