-- Factorial function fails on negative numbers:
fac :: Int -> Int
fac n | n == 0 = 1
      | n > 0  = n * fac (n - 1)

-- Reads a number and call `fac` after checking it:
facIO :: IO ()
facIO = do
  putStr "Input some non-negative integer: "
  mbn <- fmap readInt getLine
  case mbn of Just n | n >= 0 -> print (fac n)
              _               -> facIO

-- Reads an integer from a string.
readInt :: String -> Maybe Int
readInt s = case reads s of [(n,"")] -> Just n
                            _        -> Nothing

-- The tool to verify Curry operations as non-failing can be installed by
--
--     > cypm install verify-non-fail
--
-- If `~/.cpm/bin` is in the path, programs can be verified as non-failing
-- (provided that the SMT solver Z3 is installed) by
--
--     > curry-calltypes FacIO
-- 
-- In this case, the following non-fail condition for `fac` is inferred:
--
-- fac'nonfail v1 = (v1 == 0) || (v1 > 0)
--
-- Since the argument is checked in operation `facIO`, this operation
-- is verified as non-failing.