[hwayne]

> is supposed to mean exactly. If your predicate makes some data invalid, it's just not representable in the refined type.

Author here. It's representable; the type checker has to prove it never happens in practice. This requires very different techniques from typechecking constructive types. Liquid Haskell shells out to Z3, which can return "unknown" as an answer in addition to "sat" or "unsat".

(There's actually a fourth option, which is that Z3 runs forever, but I think LH does a bunch of clever design to avoid that case.)

You can also `assume` that refinements are satisfied without proving them, in which case they can be violated at runtime. This would be impossible if the invalid data was unrepresentable.

Other approaches to refinement types, such as the original ML paper [0], implemented them constructively and didn't have this problem.

[0]: https://www.cs.cmu.edu/~fp/papers/pldi91.pdf