This note describes how I would like to approach the “soft type challenge” in Isabelle. It collects ideas that emerged in discussions with many people including Jeremy Avigad, John Matthews, Tobias Nipkow, Larry Paulson, Andreas Schropp, and Makarius Wenzel. Some of these ideas were previously summarized by notes by Larry Paulson (in 2007) and Jeremy Avigad (in May 2010). Here, I am trying to be more specific and concrete where possible, and to outline a concrete research program. Note: This direction of research has not been continued so far.