Well, if the compiler will also report error for recursive calls not in tail position...
There are strategies to prove various things about recursive calls. See Ada/Spark's explanation for Rule 17.2 in [1].
I'm not familiar with Coq and Agda, but I believe they allow recursive calls if they can prove termination, though "termination" may be different than "using too much stack".
As a rule of thumb, they permit recursion where one parameter "obviously" is getting smaller each time, with a base case at 0 or the empty list or whatever.
You can annotate the program in ways to make the compiler see that a parameter is actually getting smaller.
There are strategies to prove various things about recursive calls. See Ada/Spark's explanation for Rule 17.2 in [1].
I'm not familiar with Coq and Agda, but I believe they allow recursive calls if they can prove termination, though "termination" may be different than "using too much stack".
[1] http://www.spark-2014.org/entries/detail/misra-c-2012-vs-spa...