Hi
Indeed, if Catch or ESC or similar tools can handle such specifications it would be great. However I suspect that the translation you gave is different from what I wanted. I consider a function buggy, if it implements 'const' considerably more complicated than just saying 'const'. :-) That is, I only want to reject a function if it _always_ returns the empty list. Your 'filterNonEmpty' is rejected whenever _some_ arguments yield the empty list.
Yes, but someone redefined your problem as the above one, which I can solve :-) For your original problem, Catch is entirely unsuitable. ESC/Haskell would be my preferred method of solving this within Haskell, but I'm not sure if it has existentials or not. I could imagine writing something like: filter :: {f: exists x. f x == True} -> {True} -> {True} filter :: (a -> Bool) -> [a] -> [a] Thanks Neil