[voxcogitatio]

Of course human error applies here too; But it's much simpler to get one type right than to use the type in the right way everywhere. Per example: The Red-Black-Tree implementation mentioned in the examples. If we define a tree that cannot be unbalanced, we can skip all explicit checks for whether the tree is balanced, thus eliminating a source for errors (forgetting/bungling the balance checks) and also increasing productivity (since we don't need to write the balance checks in the first place).