[openfuture]

This is where linear types and in general quantitative type theory comes into play. Also eagerness / laziness annotations.

Tail recursion is not necessary to annotate imo, but I guess the compiler/linter could maybe complain if it finds recursion it can't do a tail call optimisation for. These kinds of warnings are similar to mutable languages warning about things that are probably bad but sometimes necessary.

[heavenlyblue]

It’s neccessary to annotate tail recursion because you are making it clear to the compiler that your initial assumption about the performance of this function is that it will not explode the stack.

The reason it must be made explicit is because when somebody else comes later on to change that function they may miss the fact that it doesn’t explode only because it’s tail-recursive.

You could of course document the requirement - but why document if you can make it a compiler option? “I don’t want this to compile unless I get the behaviour I expect from it”.

Also as far as I am aware C-style functions can not be tail-recursive because they can not clean up the stack after themselves, thus you can’t support tail-recursion across FFI.