The big innovation there is in realizing that's enough. When I was into language design from 2004-2007, language designers usually assumed people wanted full global type inference. It turns out that local type propagation is an effective 80/20 solution for most practical programming tasks, which opened up a lot of hybrid type systems that would've been far too complex before.