Sounds overcomplicated. I've seen any number of fancy not-exactly-type-systems and they always end up having crazy edge cases, whereas a plain type system does exactly what you expected (and, crucially, does it in an understandable way) and scales arbitrarily far. Having the type system work the same way in the REPL and the rest of the language is important for that.
I guess then you'd need another mechanism for dealing with re-defining APIs in incompatible ways within the REPL. It's a pretty common use case for REPLs to play around with APIs and temporarily break them.
The best alternative is to keep a map of all of the definitions with broken type checks, and refuse to generate new machine code/bytecode as long as that map is non-empty, and keep using the older definitions until again get back to a sound state of the world.
GHC's REPL supports turning type errors into crashes when the ill-typed expression is used, which lets you test one part of code while another part is broken.
I think you can even extend that to compiled code, for an authentic "it crashed in production" experience.
