Is Well-Founded recursion safe?

Question

In the question about non-termination With clauses obscuring termination an answer suggests to recourse to <-wellFounded.

I looked at the definition of <-wellFounded before, and it strikes me there is a --safe in OPTIONS. Is it meant to work without this option? That is, is using --safe some optimisation, or is it working around some fundamental problem? So in this case we just delegate the termination problem to a function marked as "safe"?

Answer 1

It is completely safe. --safe holds a module to a stricter standard than default. It does not mean that something is unsafe, it means that something is safe. Using well-founded recursion from any module, safe or not, will not introduce non-termination. Termination is rather strongly baked into the inductive definition of accessibility.