len :: [a] -> Int
len []     = 0
len (_:xs) = 1 + len xs

--- Returns prefix of length n.
tak :: Int -> [a] -> [a]
tak n l = if n <= 0 then [] else takep n l
 where takep _ []     = []
       takep m (x:xs) = x : tak (m - 1) xs

nth :: [a] -> Int -> a
nth (x:xs) n | n == 0 = x
             | n > 0  = nth xs (n - 1)

nth'nonfail :: [a] -> Int -> Bool
nth'nonfail xs n = n >= 0 && len (tak (n+1) xs) == n+1
-- Alternative non-fail condition, works only for finite lists:
--nth'nonfail xs n = n >= 0 && len xs > n

{-

Inferred non-fail condition when the explicitly state condition is not givens:

nth'nonfail :: [a] -> Int -> Bool
nth'nonfail v1 v2 =
  ((not (null v1)) &&
   (case v1 of
      v3 : v4 -> (v2 == 0) || (not (v2 > 0))
      _ -> True)) &&
   ((not (null v1)) &&
    (case v1 of
      v3 : v4 -> (v2 == 0) || (v2 > 0)
      _ -> True))

This is equivalent to:

nth'nonfail :: [a] -> Int -> Bool
nth'nonfail v1 v2 = not (null v1) && v2 == 0

This is correct but too restrictive.
Hence, providing the less restrictive non-fail condition is useful.

-}