> If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time
This is not entirely true in general. auto is only a best bet. It might not be able to prove something right and will fail. For example, if it has to recurse deeper than 100 constructors. In this case, the user of the function has to provide a proof himself.
See it as a bloom filter. if it doesn't fail, you're sure your function is correctly called. if it does fail, it might still be correctly called but the compiler just didn't have enough time to prove it. In that case a user needs to convince the compiler that he is right.
I don't see the problem here. I said that Idris will reject the program if the proof fails. That's what you're saying too, unless I'm very confused. (It's late, so maybe I am?)
That doesn't contradict the quote that you provided. The quote just says "the compiler will reject the program at compile time [if there's no valid proof]", which is true.
This is not entirely true in general. auto is only a best bet. It might not be able to prove something right and will fail. For example, if it has to recurse deeper than 100 constructors. In this case, the user of the function has to provide a proof himself.
See it as a bloom filter. if it doesn't fail, you're sure your function is correctly called. if it does fail, it might still be correctly called but the compiler just didn't have enough time to prove it. In that case a user needs to convince the compiler that he is right.