> arbitrary properties are very difficult to check in general.

To add to this:

In theory, it is not just difficult, but impossible.

Imagine that the refinement predicate is whether the String/Text encode a (non-)halting Turing machine/Haskell program. Checking it would solve the halting problem. And this predicate is the proof of Rice theorem.[1] (Granted, this may require some sufficiently powerful logic such as first order, not sure if this proof applies to LiquidHaskell.)

In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types.