Dear Alexander, FWIW, this sort of thing is quite straightforward with LiquidHaskell: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1418064183.hs 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