I think liquid Haskell is a great example of refinement types?

https://ucsd-progsys.github.io/liquidhaskell/