Mostly because, per my reading (as an admitted Haskell dabbler and not fluent), it looks like a variation on a theme rather than a totally different thing. It seems to be a more consistent and refined (har har) way of doing the same thing as the first link, and still has a dynamic check (at least in one form,
refine vs
refineTH) just like the smart constructors.
But also because we got derailed from my initial point and context.
> Pre/post conditions are complementary to a type system.
Do you disagree or agree with this statement? Because you never addressed it either.
> They can ensure logical properties that may not be encodable in your underlying type system
Note the "may", because that's important. I didn't say that there were no languages in which my example could be encoded in the type system. And maybe it wasn't the best example, but the point itself was that there is no type system (that I'm aware of, not even Idris as far as I know) which can prove in its static type system every piece of logic about a program. This means that some properties of the system will end up being checked (if you bother to) at runtime and not at compile time. That's where pre/post conditions are useful, they contain information (and in a more deliberate form in cases like the Clojure example) about the properties of the system that are hard or impossible to encode directly in the type system.
Different type systems (both static and dynamic) let you express more or less with them, which reduces the need/desire to have checks like these in your program. But I seriously doubt that any mainstream language will ever totally remove their utility, as complements to the rest of the type system.