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.