module Foo where import Language.Haskell.Liquid.Prelude {-@ gpp :: Monad m => m {v:Int|v>=0} -> m {v:Int|v>0} @-} gpp :: Monad m => m Int -> m Int gpp z = do x <- z return $ liquidAssert (x >= 0) (x)