[gfairbanks]

The overall idea of using your type system to enforce invariants is called typeful programming [1]. The first few sentences of that paper are:

"There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense independent of the language it is embedded in; it adapts equally well to functional, imperative, object-oriented, and algebraic programming, and it is not incompatible with relational and concurrent programming."

[1] Luca Cardelli, Typeful Programming, 1991. http://www.lucacardelli.name/Papers/TypefulProg.pdf

[2] https://news.ycombinator.com/item?id=18872535