I think that if I were building a system that worked this way, automatically-inserted type declarations would be distinguished somehow (preferably in a way that

I think that if I were building a system that worked this way, automatically-inserted type declarations would be distinguished somehow (preferably in a way that in good text editors just appears as different formatting), and then when you change the function to return "wow" the compiler/linter/magic-type-annotator will see that the only things that need updating are ones it inserted itself, and just do it. If you edit any of those automatically-inserted type declarations, though, they're fixed and doing things that violates them becomes a type error rather than an auto-rewriting opportunity.