Anyway, Type checking is essentially an application of set theory : (I did no search in te literature for this, It is just my perception). When I say š (+) :: Num a => a -> a -> a . I mean that (+) takes two elements of the set of Num typeclass and return another. This is in principle a weak restriction, because many functions do it as well, for example (*). š
A propery check or a contract would be much more restrictive and thus would detect much more program errors. But it seems that no other language but haskell took this set theoreticalšanalysisšso exhaustively, and without it, a property check is like detecting microscopic cracks in nuclear waste vessel without first making sure that the cover has been sealed.