Sufficiently advanced type systems can enforce an enormous range of constraints. You can for example create a type for trees enforcing that the tree must be balanced; code that would unbalance a tree will just not compile.