The Dangers of Termination in Haskell

The design of the internal language and of our proof of type safety accommodate this. But there are two dangerous things with termination. One is what you said that your compiler might not terminate with. That's assuming it is OK. And then termination might cause inconsistencies. It's not a problem, but again, it means that we have this extra step at runtime essentially checking the termination of our proofs. Because they do need to terminate. We can check them later. You come up at once and then you just take the proofs and you assume it, right?