or, the code below:

-----

{-@ LIQUID "--no-termination" @-}

module Nat255 where

-- | Define a predicate for valid integers

{-@ predicate IsValid X = 0 <= X && X < 255 @-}

-- | Use the predicate to define a refinement type (subset) of valid integers

{-@ type Valid = {v:Int | IsValid v}        @-}

-- | A function that checks whether a given Int is indeed valid

{-@ isValid   :: n:Int -> {v:Bool | Prop v <=> IsValid n} @-}

isValid n     = 0 <= n && n < (255 :: Int)

-- | A function that can only be called with Valid Ints.

{-@ workWithValidNumber :: Valid -> IO () @-} 

workWithValidNumber n = putStrLn $ "This is a valid number" ++ show (n :: Int)

-- | This is fine...

ok    = workWithValidNumber 12

-- | ... But this is not.        

notOk = workWithValidNumber 257

-- | Finally the top level loop that inputs a number, tests it 

--   and calls `workWithValidNumber` if the number is valid.

loop = do putStrLn "Enter Number between 0 and 255"

          n <- readLn :: IO Int

          if isValid n

             then workWithValidNumber n

             else putStrLn "Humph, bad input, try again!" >> loop