The key word in "automatic simplification" is "automatic". The feature loses value if a human has to intervene to specify which functions to inline or to continue inlining. Imagine how worthless `go fmt` would be if it prompted the user to confirm every change to the source code
Compilers like LLVM and GCC use heuristics not human intervention. For inlining a common heuristic is the size of the function. So we inline (even recursive functions) until the function becomes larger than a certain threshold. The threshold can be specified by a human (-finline-limit), but I believe that is rarely done.
This isn't compiling though; it's normalising. A heuristic like function size is useful when optimising a Turing-complete language since (a) we have to rely on some heuristic and (b) smaller binaries are generally more efficient, all else being equal, so we should avoid a size blow up regardless of what we're optimising for (speed, size, memory, etc.).
In the case of normalising a non-Turing-complete language, we (a) don't need any heuristics, beta-reduction is a complete and correct strategy and (b) things like the size of a function are useless at telling us whether we've reached a normal form. In fact, I would imagine that normal forms of real Dhall programs are generally much bigger than the programs themselves, since one of the main reasons to use a language like Dhall is to reduce repetition. Also, your heuristic is heavily dependent on the evaluation order: if we have a program like this:
On the other hand, an evaluation strategy like call-by-value will evaluate big-thing, resulting in some arbitrarily large value (which may cause your heuristic to halt); then it will create 1000000 duplicates of that value (again, causing a size-based heuristic to halt); then finally it will evaluate the functions and discard the big, duplicate expression:
You do if you want to reach a normal form. Note that the author isn't talking about compiling or optimising, they're talking about normalising. I don't know of a Turing-complete language where we can ask to normalise some arbitrary expression including going 'under a lambda' (i.e. performing partial application, etc. inside function invocations; what you refer to as 'inlining'). The closest I can think of is expanding Lisp macros, but they're already a "compile time" transformation so I'm not sure how comparable they are (although of course Lisp can interleave compilation with evaluation!)
The place where using a non-Turing complete language actually matters is in constructive proofs where it's common to write a function without running it. This can be used to show that a value can be constructed in principle, even if it's not a practical program because it would take billions of years.
But practical programming is about writing programs that we actually want to run. The distinction between "takes far too long" and "hangs forever" is unimportant because real-world tasks have at least an informal deadline: how long the user is willing to wait. And most performance testing is done by actually running programs, not via static analysis alone, because we want to know how fast the code is on real-world hardware.
This particular language is something you'd use to generate large, repetitive configurations. It makes sense for that use case that you'd want to make sure all macros can be expanded. But you don't have to prove this statically, because you can actually run the program and look at what it generates. Doing config file generation using a Turing-complete language would also work fine; if you accidentally create an infinite loop (or just very slow code), you can hit control-C and fix the bug.
For the purposes of evaluation, it's still an improvement to have a total language. As I mentioned in another thread, using a totality checker is like wearing seatbelts: it doesn't protect against everything, but it's still a huge improvement.
