> So, it sounds like if you can't provably account for all possible inputs, the compiler will recognise this and throw an error. How? Magic! (And a solver, feed

> So, it sounds like if you can't provably account for all possible inputs, the compiler will recognise this and throw an error. How? Magic! (And a solver, feeding your type constraints into the totality checker, I guess...) That would make many practical, real-world programs noncompilable. Any program which accepts data via API calls, or even reads strings from STDIN, cannot know what values are going to be passed to it before it runs. Compilers cannot predict the future.