I guess the only natural way would be to have operations send you back to the Base type, and then have a `TryInto(v: Base) -> Result<Refined>` function that would verify the predicate and allow you getting back into the refined type.
Maybe some operations can be proved to stay within the refined type, like adding natural numbers, but that's something that the used would need to provide as a function allowing that under assertions or some proof that the compiler can verify and trust.
Maybe some operations can be proved to stay within the refined type, like adding natural numbers, but that's something that the used would need to provide as a function allowing that under assertions or some proof that the compiler can verify and trust.