Note the "codata" and also note that "main" is marked as "partial". Only the total subset of Idris is non-TC.

Note also the use of Fuel -- this is to provide "fuel" for the computation, but it's a data structure which can only decrease in 'size' -- which is used by the compiler to prove totality (termination).

("codata" is a way to model 'infinite' computations as data structures.)