From 56e076b2ca3bd90c8a927a0caabaf507b06e70c3 Mon Sep 17 00:00:00 2001
From: Brummel <mould@mycelium.de>
Date: Tue, 2 Jun 2026 11:16:49 +0200
Subject: [PATCH] docs(contracts): make 0012 tail-context list code-exhaustive
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The §Typecheck enumeration in 0012-tail-calls.md presented the
tail-position rule as exhaustive ("The flag is `false` for: ...") but
omitted `Term::If` entirely — even though `verify_tail_positions`
propagates `is_tail` into both `If` branches (ailang-check/src/lib.rs),
and 0012's own motivating example (`if n == 0 then () else loop(n-1)`)
relies on the `else` branch being a tail position.

Restate the rule by principle (a sub-term is in tail position iff it is
the value of the whole expression) and enumerate the actual checker's
arms: `If` branches, `Match` arms, `Seq` right, `Let`/`LetRec`
in-clause, `Lam` body, and the identity/`Loop` propagators; every
argument position (incl. `If` condition, `Recur`/`New` args) is
non-tail. Matches the present `verify_tail_positions` walker.
---
 design/contracts/0012-tail-calls.md | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/design/contracts/0012-tail-calls.md b/design/contracts/0012-tail-calls.md
index 54c88e7..0eb523d 100644
--- a/design/contracts/0012-tail-calls.md
+++ b/design/contracts/0012-tail-calls.md
@@ -19,12 +19,17 @@ Solution: explicit, verified tail calls.
 - **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
+  the start and propagates to every sub-term that is the value of
+  the whole expression: the body of every `Term::Match` arm, both
+  branches of `Term::If`, the right operand of `Term::Seq`, the
+  body of `Term::Let` and the in-clause of `Term::LetRec`, and the
+  body of `Term::Lam` (each Lam opens its own tail scope); the
+  identity nodes `Term::Clone` / `Term::ReuseAs` and a `Term::Loop`
+  body propagate the enclosing flag unchanged. The flag is `false`
+  for every argument position: args of any
+  `App`/`Do`/`Ctor`/`Recur`/`New`, the scrutinee of `Match`, the
+  condition of `If`, the left operand of `Seq`, and the value of a
+  `Let`/`LetRec` binding. 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`.