A very interesting idea! A couple of functional languages use "when" in a similar way to introduce pattern-matching guards, but I haven't used any languages which support such a general facility for type declarations, though I suspect some dependently-typed languages do. I suppose that at least you would need to limit the condition to terminating computations to be able to verify it at compile time, and perhaps restrict mutation somewhat. (p : S) => { p.x ← 0 } would have to be illegal, for example, though (p : S) => { (p.x, p.y) ← (3, 4) } might be permitted.

These are called refinement types (https://en.wikipedia.org/wiki/Refinement_type).

Provable termination isn’t strictly necessary I think, because compile-time evaluation, or metaprogramming in general, is usually Turing-complete anyway.