One of the benefits of refinement types is that they allow optimizations that otherwise wouldn't be possible. If the code is just a single function where the data flow is obvious, the compiler can automatically infer bounds for integers and other things and optimize the code based on those – for example not adding bounds checks on accesses it knows will never fail. However, if the computed value is stored in memory somewhere, and then accessed later in another part of the code, these inferred bounds are not transferred with the value. A way to solve this is to make the bounds explicit by refinement types, but to be able to benefit from that, also the compiler must know that those bounds exist.
The way to do this is to add an unchecked assert to every place where the value is dereferenced/extracted/etc. Something like this:
fn deref(&self) -> &Self::Target {
unsafe { hint::assert_unchecked(P::test(&self.0)); }
&self.0
}In a real implementation, it'd be better to have a debug_assert if bounds checks are present, and assert_unchecked only if they are not.
For this to be safe, a few things must be true:
- There must be no safe way to construct a refined value without the test being invoked
- The predicate test must be consistent so it will always return the same output for the same input
- The value must not have interior mutability so it could change to not satisfy the test anymore
Since obviously there might be bugs in such an implementation, not everyone is going to want there to be unsafe optimization that is very niche. That means the feature should be configurable via a cargo feature, and probably not enabled by default.
One of the benefits of refinement types is that they allow optimizations that otherwise wouldn't be possible. If the code is just a single function where the data flow is obvious, the compiler can automatically infer bounds for integers and other things and optimize the code based on those – for example not adding bounds checks on accesses it knows will never fail. However, if the computed value is stored in memory somewhere, and then accessed later in another part of the code, these inferred bounds are not transferred with the value. A way to solve this is to make the bounds explicit by refinement types, but to be able to benefit from that, also the compiler must know that those bounds exist.
The way to do this is to add an unchecked assert to every place where the value is dereferenced/extracted/etc. Something like this:
In a real implementation, it'd be better to have a
debug_assertif bounds checks are present, andassert_uncheckedonly if they are not.For this to be safe, a few things must be true:
Since obviously there might be bugs in such an implementation, not everyone is going to want there to be unsafe optimization that is very niche. That means the feature should be configurable via a cargo feature, and probably not enabled by default.