Subset types, in a completely other context
Heh heh, chasing down a completely other rabbit hole, I came across Refinement Types: "a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types"
The pre-/post-condition approach ties up with Hoare Logic.
There's a program proof tool available for Haskell: LiquidHaskell "refines Haskell's types with logical predicates that let you enforce critical properties at compile time." The type decl and its predicates are inside comments that get pre-processed, to plant the bare decl in its place. The predicates are in a restricted dialect of Predicate Logic, suitable for plugging into a SMT solver that uses subsumption reasoning. The idea seems to be that if it can prove the preconditions follow from the postconditions of the term that supplies the arguments, we don't need a run-time check. This (ideally) pushes run-time checks to the outer edges of your code, rather than needing to be executed inside tight loops (recursion).
This is neat in a functional languages, because we have only arguments and results; there's no iteration, only recursion; there's no flow-of-control with destructive assignment.
Note: The examples on that front page I linked to make extensive use of Haskell's type NonEmpty a = .... type is introducing not a new type, but a type alias/shorthand, with a parameter (a in that example). At a usage site, ... NonEmty b ..., 'macro expand' the RHS of NonEmpty's definition, substituting b (or whatever) for the formal parameter a.
Hmm I might have to reconsider TTM's Inheritance Model. OTOH There doesn't seem to be anything equivalent to Union types. Nor of some uber-type Alpha. The predicates give subsets of a named Haskell type (Int, String, Float, ...); or structured types (List-of-type, Optional-type, tuple-of-types, ...).