Yeah, anything you assert has to be proved at runtime. Liquid Haskell just a) checks your assertions are consistent with the type returned and b) avoids you having to check again.

You could theoretically remove all the unnecessary checks by hand, but it’s tricky.