It's because `Integer` is an insufficiently specific type to ensure that the value expression is well formed. If you really wanted to, you could prove that `add` is well-formed in Haskell and Haskell-likes: https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...