Sounds great! And very close to what I was thinking about.

What's your IDE?

> The type information is simply “stored” in the plain-text source code itself, as type declarations/annotations.

Yes, I think that's the right way to do it. I do believe that there needs to be some way to tell the difference between these three cases:

1. I put the type information there, that's really what I intended

2. The system put the type information there and I okayed it

3. This is what the system currently thinks, no human interaction

However, I believe this just from thinking about it, without having used such a system, so I may be completely wrong.

My background is also dynamically typed systems like Smalltalk, so the state of having no static type information available is also acceptable.