Iter 14d: remove Term::If as a redundancy

Term::If was semantically a subset of Term::Match on Bool. Per
CLAUDE.md the language must contain no redundancies; two AST nodes
for the same operation produces an authoring decision with no
semantic content and a duplicate codegen path. Removed.

Migration shape (applied to sum, sort, max3 fixtures):
  (if c a b) -> (match c (case (lit-bool true) a) (case _ b))

No schema version bump (per user direction): no third-party consumes
ailang/v0, so version ceremony is pure overhead. Edited AST and
fixtures in place; pinned hashes in hash.rs updated.

Implementer deviation, called out and justified: a tightly-scoped
lower_bool_match helper (~95 LOC) was needed in codegen because
the existing match path rejects i1 scrutinees and Pattern::Lit.
Helper accepts only the canonical two-arm migration shape, errors
on anything else, emits the same br/phi IR Term::If used to. No
generalisation of the ADT-match codegen.

Diff: 13 files, +286/-221 (net +65 LOC). AST got smaller
(one variant gone), form-(A) got smaller (one production gone),
typecheck got smaller (one branch gone). Codegen got slightly
larger by the bool-match helper.

Hash deltas: sum.sum, sort.insert, max3.max, max3.max3 changed.
All other defs (e.g. sum.main, sort.IntList, sort.sort,
sort.print_list, max3.main) kept bit-identical hashes — confirms
canonical-JSON byte format intact.

Verification: 76/76 tests green; sum->55, max3->17, sort->[1,1,2,
3,3,4,5,5,5,6,9] (identical to pre-migration). cargo doc 0 warnings.

Tail-call survey by implementer (informs 14e): print_list
recursions are already in tail position (rhs of seq inside match
arm); map/sort/insert recursions are NOT (constructor-blocked
inside Cons applications). 14e annotation will benefit terminal
recursions; ctor-blocked ones need accumulator-form rewrites in
source, not a compiler-side transform.

Decision 7 added to DESIGN.md. JOURNAL entry has the language-
completion sequence (14d done, 14e tail-calls, 14f GC, 15a stdlib).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

docs/DESIGN.md

@@ -429,6 +429,31 @@ fixtures round-trip identically through `print → parse → canonical
 JSON`; the three hand-written `.ailx` exhibits parse to canonical
 JSON identical to their corresponding `.ail.json` files.
 
+## Decision 7: redundancy removal — `Term::If` is not a primitive
+
+`Term::If { cond, then, else_ }` is semantically a subset of
+`Term::Match` on `Bool`. Per CLAUDE.md the language must contain no
+redundancies; two AST nodes for the same operation produces an
+authoring decision with no semantic content and an extra codegen
+path. Iter 14d removes `Term::If`. Migration shape on the JSON side:
+
+  {"t":"if","cond":C,"then":A,"else":B}
+    →
+  {"t":"match","scrutinee":C,
+    "arms":[
+      {"pat":{"p":"lit","lit":{"kind":"bool","value":true}},"body":A},
+      {"pat":{"p":"wild"},"body":B}]}
+
+The wildcard arm satisfies the typechecker's
+`primitive-needs-wildcard` rule. A future iter may upgrade the
+exhaustiveness check to recognise the `true`+`false` arm pair as
+covering Bool without a wildcard; until then, wildcard is the
+canonical migration target.
+
+No schema version bump (no third-party consumes `ailang/v0`).
+Hash invalidation for the three migrated fixtures (`sum`, `sort`,
+`max3`) is intentional; the new hashes become the new identity.
+
 ## Mangling scheme (Iter 5c)
 
 All AILang functions are mangled to `@ail_<module>_<def>` — even in the
@@ -492,7 +517,6 @@ hashes stay bit-identical.
 { "t": "var", "name": "<id>" }
 { "t": "app", "fn": Term, "args": [Term...] }
 { "t": "let", "name": "<id>", "value": Term, "body": Term }
-{ "t": "if", "cond": Term, "then": Term, "else": Term }
 { "t": "do", "op": "<eff>/<op>", "args": [Term...] }
 { "t": "ctor", "type": "<id>", "ctor": "<id>", "args": [Term...] }
 { "t": "match", "scrutinee": Term, "arms": [Arm...] }
@@ -588,7 +612,9 @@ as iterations land; the JOURNAL records the exact iteration.
 What **is** supported (and used as the smoke test for the pipeline):
 
 - Int, Bool, Unit, **Str** as primitive types.
-- `if`, `let`, function calls, recursion.
+- `let`, function calls, recursion. Bool branching is expressed via
+  `match` on `Bool` with a `(lit-bool true)` arm and a wildcard
+  fallback (Decision 7); there is no separate `if` AST node.
 - Effects on function signatures, with `do op(args)` for direct effect
   ops (`io/print_int`, `io/print_bool`, `io/print_str`).
 - **ADTs + flat pattern matching** (Iter 3). Sub-patterns of a Ctor

docs/JOURNAL.md

@@ -1744,5 +1744,136 @@ this iter cycle, though the architectural pin keeps it
 open for future replacement of `ailang-surface` should
 the form prove inadequate at stdlib scale.
 
+## Language-completion sequence (14d → 14f, then stdlib in 15a)
+
+User redirected at the 14d boundary: write the language to
+"finished" before starting on a stdlib. Reasoning:
+authoring a stdlib in an unfinished language wastes work —
+each gap discovered later forces a rewrite of code already
+written. The user also confirmed: **no schema version bump
+needed**. AILang has exactly one consumer (me), so version
+ceremony for compatibility management is pure overhead.
+Edit AST and fixtures in place; pin new hashes where the
+hash regression test demands it.
+
+Updated planning sequence:
+
+- **14d** — remove `Term::If` redundancy. Pure subtraction.
+- **14e** — explicit tail-call annotation (`tail` flag on
+  `Term::App`/`Term::Do`, `musttail` in codegen, tail-position
+  verifier in checker).
+- **14f** — memory management. Currently every ADT allocation
+  leaks. Likely Boehm conservative GC (`GC_malloc` + `-lgc`)
+  for minimum surface change; design pass first.
+- **15a** — first stdlib module (`std_list`).
+
+Deferred (not stdlib-blocking; can land later without
+rewriting code that already exists): records/tuples (use
+ADT pairs), nested patterns (use pyramid `match`), local
+recursive `let` (hoist to top level).
+
+## Iter 14d — `Term::If` removed
+
+Subtraction iter. `Term::If { cond, then, else_ }` was
+semantically a subset of `Term::Match` on `Bool`. CLAUDE.md
+forbids redundancies; two AST nodes for the same operation
+was an authoring decision with no semantic content and a
+duplicate codegen path.
+
+The migration shape was the canonical one named in the
+brief:
+
+```
+(if c a b)  →  (match c (case (lit-bool true) a) (case _ b))
+```
+
+Wildcard arm satisfies the existing `primitive-needs-wildcard`
+rule. A future iter may upgrade exhaustiveness to recognise
+`true`+`false` as covering Bool without a wildcard, but the
+wildcard form works with the current checker and that was
+enough for 14d.
+
+**Implementer dispatch went clean with one documented
+deviation.** Removing the `Term::If` codegen path was not
+sufficient on its own: the existing match codegen rejects
+`i1` (Bool) scrutinees and `Pattern::Lit` patterns — both
+of which the migration shape requires. The implementer
+added a tightly-scoped `lower_bool_match` helper (~95 LOC)
+that handles **only** the two-arm Bool migration shape
+(`(lit-bool true) -> A | _ -> B` or its mirror), errors on
+anything else, and emits the same `br i1`/phi IR the old
+`Term::If` path emitted. No generalisation of the
+ADT-match codegen.
+
+The deviation was the right call. **Lesson for future
+subtraction iters**: when removing a specialised AST node,
+the codegen for the migration target may need a small
+extension. Pre-emptively scope this in the brief next time.
+
+**Diff size**: 13 files, +286/-221 LOC. Net +65 LOC across
+the workspace, but the AST got smaller (one variant gone),
+the form-(A) grammar got smaller (one production gone),
+and the typechecker got smaller (one branch gone). Codegen
+got slightly larger because of the bool-match helper, but
+the alternative was reusing the existing match path and
+generalising it — which would have been a bigger and
+riskier change.
+
+**Hash deltas** (intentional, per Decision 7):
+
+| def | before | after |
+|---|---|---|
+| `sum.sum` | `db33f57cb329935e` | `7f5fe7f72c63a9fd` |
+| `sort.insert` | `697fcb9f30f8633a` | `07ff6ee7db17565d` |
+| `max3.max` | `65c45d6a45dd0a72` | `2aa1576f3fbf5b3d` |
+| `max3.max3` | `624b14429bf302f5` | `c452ec2e36c0af27` |
+
+Untouched defs (e.g. `sum.main`, all `sort.*` except
+`insert`, `sort.IntList`, `sort.print_list`, `max3.main`)
+keep bit-identical hashes. That's the canary that the
+canonical-JSON byte format was not perturbed — only the
+migrated bodies changed identity.
+
+**Verification**: 76/76 tests green (unchanged count; no
+new tests in this iter, by design — subtraction). Manual
+smoke: `sum` → `55`, `max3` → `17`, `sort` → ordered list.
+Identical to pre-migration stdout for all three. `cargo
+doc --no-deps` 0 warnings.
+
+**Tail-call survey from the implementer (gold finding,
+informs 14e).** While reading the migrated fixtures the
+implementer surveyed tail positions. Result:
+
+- `print_list` (in both `sort.ail.json` and
+  `list_map_poly.ail.json`): the recursive call is the
+  rhs of a `seq` which is the body of a match arm —
+  **already in tail position**. TCO would convert these
+  to actual loops.
+- `main` chains: the outer call is in tail position;
+  inner calls are not.
+- `insert`, `sort`, `map`: the recursive calls are
+  **arguments to a `Cons` ctor construction** (e.g.
+  `Cons (f h) (map f t)`). NOT in tail position.
+  Constructor-blocking is the standard ML/Haskell case
+  where TCO does not apply without a CPS transform or an
+  accumulator-form rewrite.
+
+**Implications for 14e.** Adding a `tail` flag to
+`Term::App`/`Do` will work for `print_list`-style
+recursions and for terminal call chains, but **will not**
+help the `map`/`sort`/`insert`-style ctor-blocked
+recursions. Those need either an accumulator-form rewrite
+in the source program (the standard ML/Haskell move) or a
+CPS transform (much more intrusive). 14e ships only the
+annotation + verification; accumulator forms become an
+authoring pattern in the stdlib, not a compiler feature.
+
+This sharpens what 14e can promise: tail-call **wins**
+will be visible in `print_list`-style terminal-recursion
+patterns; `map`/`sort` style stays stack-bounded by depth,
+which makes 14f (GC) the more important iter for handling
+long lists than 14e by itself.
+
+