Overall this looks very interesting - I always thought more could have been done with RPython, but there was never any documentation for it. I do have some nits though:

> The following silly example happily passes mypy

In fairness that's because Mypy is shit. Pyright catches this mistake.

> As such, we need to treat Python type checkers more like linters than actual theorem provers

Again I think this is true of Mypy but Pyright is much closer to a sound type checker.

> redshifting

This is just constant propagation isn't it? C compilers have been doing this for decades. I don't think we need a silly new term for it. Let's not cause another "tree shaking" situation.

> So far, this is not different than usual constant folding, with the difference that it's guaranteed to happen. What makes it more powerful is the ability to mark some functions as @blue.

That's not different. It's just constant folding with C++'s `consteval`. And @blue is an absolutely abysmal name.

It would be much clearer if @blue were changed to @consteval or @comptime (either's good I think), and you just call it "compile time evaluation" or "constant propagation" instead of "redshifting".