[yakshaving_jgt]

Sorry, I should have been clearer. I was referring to the Template Haskell part of that refinement types library, where the construction of values can indeed be statically checked at compile time.

> > Pre/post conditions are complementary to a type system.

> Do you disagree or agree with this statement? Because you never addressed it either.

I agree with it. I write web applications in Haskell for a living, and the very nature of web applications is that most values coming into the system are not known until runtime. It is not a reasonable design goal to want every possible value in the system to be verified at compile time. However, it is valuable to be able to statically verify the relationships between functions and values as those values — once they have been parsed at runtime into a more principled type — move through the system.