AILang/design/contracts/tail-calls.md

Tail calls

Decision 8: explicit, verified tail calls

For an LLM author, recursion is the natural iteration form (\n. if n == 0 then () else loop(n-1) is what I reach for, not a for-loop). Without a tail-call guarantee, every recursive program has a silent stack-depth ceiling that no compile-time diagnostic warns about. That is exactly the class of correctness hazard the language exists to eliminate.

Solution: explicit, verified tail calls.

• AST. Term::App { fn, args, tail: bool } and Term::Do { op, args, tail: bool } gain a tail flag, serde-defaulting to false so existing fixtures load with tail: false and their hashes stay bit-identical.
• Typecheck. A new pass verify_tail_positions(fn_body) runs after the main type-check. It walks the body with an is_tail_context: bool threaded down. The flag is true at the start, true for the body of every Term::Match arm, true for the right operand of Term::Seq, true for the body of Term::Let, true for the body of Term::Lam (each Lam opens its own tail scope). The flag is false for: args of any App/Do/Ctor, scrutinee of Match, left of Seq, condition of Let-bound expression. When the walker visits an App { tail: true } or Do { tail: true }, the flag must be true at that visit; otherwise emit diagnostic tail-call-not-in-tail-position.
• Codegen. Emit musttail call (LLVM IR) for marked calls instead of plain call. LLVM rejects at IR-verification time if the call cannot physically be a tail call (calling convention mismatch, signature divergence, etc.). The reject surfaces as a hard build error, not a silent runtime surprise.
• Form (A). Two new keywords: tail-app, tail-do. Productions are positional analogues of app/do with tail: true set on the resulting term. EBNF gains 2 lines; total production count goes from ~28 to ~30, still inside the constraint-1 budget.

What this does NOT promise. Per the tail-call survey of existing fixtures, many existing recursive calls are not in tail position because they are arguments to constructor calls (e.g. Cons (f h) (map f t)). The current pipeline adds annotation + verification; it does not add a CPS transform or accumulator-form rewrite. Programs whose recursion is constructor-blocked will continue to be stack-bounded by recursion depth. The canonical authoring pattern in such cases is to write the accumulator-form variant (map_acc, fold_left, etc.) explicitly. The stdlib ships both forms where relevant.

Migration of existing fixtures is partial: only print_list-style terminal recursions get marked. The constructor-blocked recursions in map, sort, insert remain unmarked — they cannot benefit from musttail without a source-level rewrite.

Ratified by: crates/ailang-check/src/lib.rs.