Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration.  On this approach, we write recursive functions by coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to the result type of the recursion.  Subdata of the input data are available at type R only, not at the original datatype.  This allows us to make explicit recursive calls, but only on subdata.