The way I wish things worked:
Programmers code with three types of constraints: soft cast, hard cast, and unsafe cast. Soft cast is a runtime assertion that the constraint isn't violated, hard cast is a "do not compile unless you can prove that this constraint isn't violated" and unsafe cast is a "check at compile time to make sure you cannot provide a counterexample, but do not include a runtime check". Hard cast will be rarely used, for obvious reasons.
Compiler propagates known values / constraints forwards as much as possible, and propagates constraints backwards as much as possible. Note that this generally already happens as part of compiler optimizations. If at any point any value violates a constraint, error out and provide a "constraint trace" of what caused the violation.
After this step, the compiler looks at all unknown-at-compile time variables and randomly (or rather, pseudo-randomly, maybe seeded with the md6 of the file or something to be deterministic) generates and tests values (along with some common values - note that this could be integrated with a test framework built into the language!), ensuring that no constraints are violated. (There are a bunch of optimizations here that I'm not going to mention.) If any constraints are, error out with the variables required to violate the constraint and the values assigned to them.