Piotr Szturmaj:
These are refinement types (I call them 'views') and I have half-written DIP for this. However, I doubt that it will be accepted.
I'll be quite interested by such DIP. Even if your DIP will be refused, it could still produce several useful consequences.
Bye, bearophile
