While they aren’t completely mutually exclusive, refactorings like the ones described in here are the killer app of good type systems like in Ocaml and Haskell. You can do some vicious refactorings with pretty solid confidence that the refactoring didn’t break things if you can encode enough information in the type system (which you almost always can do). But this seems to have some usecases that aren’t covered by a good type system as well, which is nice. The main thing that makes me uneasy about this tool is it really depends on hoping you get all cases in production in order to determine if the refactoring is correct. What about infrequently hit paths? This will probably find more bugs than it lets through, but I didn’t see any lip service to that as a limitation of this technique.