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.
It's a standard assert, so whatever happens on assertion failure normally happens here, too. This is orthogonal to refinement types - they are concerned with whether the check is made or not (ie. with them you cannot accidentally forget to write that assert). The check failing is a runtime concern (similar to dynamic cast failure), the type system has nothing to do with that.
