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.
You can annotate the program in ways to make the compiler see that a parameter is actually getting smaller.