The idea of trying to move subset types forward is interesting. Using an SMT solver [0] you can move quite a bit forward. Otherwise, generally, you're talking a

The idea of trying to move subset types forward is interesting. Using an SMT solver [0] you can move quite a bit forward. Otherwise, generally, you're talking about associating a dictionary of pre- and post-conditions with a type (e.g., Weekday is a new nominal type isomorphic with Day, but it also has an associated dict containing checks that it's within Mon-Fri). Carrying that dict around has been well-solved by Haskell's typeclass compilation machinery and then it's just a matter of inserting the checks at the right times and not more often, I suppose. [0] http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/