This morning, I came across this nice post which describes how one can write a very expressive type for filter using singletons. Lets see how one might achieve this with abstract refinements. 23: 24: {-@ LIQUID "--short-names" @-} 25: 26: import Prelude hiding (filter) 27: 28: import Prelude hiding (filter) 29: isPos, isEven, isOdd :: Int -> Maybe Int 30: filter :: (a -> Maybe a) -> [a] -> [a]