> The way that the value floats through the system is checked statically, and the program can (and should) be designed so that the value with the appropriate type cannot be constructed unsafely.

Except that in the first example from the first link you sent me, there is no static guarantee that the inputs to the constructor are valid, thus the error branch (it would be unnecessary if static guarantees could be made regarding the use of the constructor). And that was my point, that you still end up with dynamic checks on the values which is where pre/post conditions step in to cover what static typing cannot (or, again, cannot easily in mainstream languages, which would not be Haskell).