[nerdponx]

I'm actually not sure about that. I think the Javascript compiler target also lacks full TCO. The Idris 2 compiler itself I think does not perform this optimization, because the Scheme reference backend does it already. I might be wrong about that, but I remember several active unresolved discussions on this topic in the community last year. I haven't been involved actively in it for several months, so my memory might be wrong.

[dunham]

The javascript back end handles mutually recursive tail calls. It finds connected components and rewrites them to use a trampoline-like thing. There is a nice explanation of how it works at the top of the file:

https://github.com/idris-lang/Idris2/blob/main/src/Compiler/...

One could argue that it's not "full" TCO, but it does cover a lot of use-cases. That rewrites to NamedCExp, so it could be reused by other backends.

The Java backend seems to be doing its own thing. There aren't a lot of comments or documentation in that repository, but I do see evidence that it's doing something interesting in src/Compiler/Jvm/Optimizer.idr:

    Pure $ if shouldTrampoline && hasNonSelfTailCall tailCallCategory
      then trampolineExpression True inlinedAndTailRecursionMarkedExpr
      else inlinedAndTailRecursionMarkedExpr