From 7574a3f32a7465cc17539b51aa277b7c62636b8b Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 18 May 2026 10:33:46 +0100
Subject: [PATCH] docs(effects): re-land v1 SPEC rule + effect.ml comment fix
 (Refs #59)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The #207 squash-merge landed only the code commit; the docs commit
(235e161) never reached main, leaving SPEC.adoc §3.4 still showing the
retired Exn[Error] and lib/effect.ml still claiming Throws[E] is 'not
yet threaded' — both now stale/incorrect on main. Re-landing them:

- SPEC.adoc §3.4: Exn[Error] → Throws[E]; new 'Effect inference
  (tracking-only v1)' subsection (catch-less try/? ⇒ Partial; declared
  rows enforced inferred⊆declared; undeclared permissive);
  'Partial by Default' disambiguated from the Partial effect.
- lib/effect.ml: corrected the doc-drift comment (#204 threads
  Throws[E] via name-mangling in Typecheck.lower_effect_expr).

Pure docs/comment; gate unchanged. Refs #59 (closed — lineage only,
do not reopen).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 docs/specs/SPEC.adoc | 31 ++++++++++++++++++++++++++-----
 lib/effect.ml        |  5 +++--
 2 files changed, 29 insertions(+), 7 deletions(-)

diff --git a/docs/specs/SPEC.adoc b/docs/specs/SPEC.adoc
index 167c3617..fbe39de7 100644
--- a/docs/specs/SPEC.adoc
+++ b/docs/specs/SPEC.adoc
@@ -324,11 +324,32 @@ Functions declare effects after `/`:
 ----
 fn pure_fn(x: Int) -> Int / Pure { x + 1 }
 fn io_fn() -> () / IO { println("hello") }
-fn fallible() -> Int / Exn[Error] { throw(Error::new()) }
-fn combined() -> () / IO + Exn[Error] { ... }
-----
-
-*Partial by Default:*
+fn fallible() -> Int / Throws[Error] { throw(Error::new()) }
+fn combined() -> () / IO + Throws[Error] { ... }
+----
+
+The v1 effect-row registry (issue #59) pins five canonical names —
+`IO`, `Async`, `Partial`, `Throws[E]`, `Mut` — plus reserved
+`Random`, `Time`, `Net`. `Throws` is written `Throws[E]` at use
+sites; the type argument is threaded (distinct under unification).
+The lowercase `io`/`state`/`exn` migration aliases and the older
+`Exn` name were retired once the stdlib was renamed to the
+canonical names.
+
+*Effect inference (tracking-only v1):*
+
+- A catch-less `try` — including the `e?` desugar (the `?` operator)
+  — lets failure short-circuit out of the body, so the enclosing
+  function performs `Partial`. A `try` with a `catch` arm handles the
+  failure locally and adds no effect.
+- When a function declares an effect row explicitly, the inferred row
+  must be a subset of the declared one (otherwise an effect-mismatch
+  error is raised). A function with *no* declared row stays permissive
+  under tracking-only v1 — its effects are not yet enforced.
+- Effect *handling* (intercepting/redirecting effects at runtime)
+  remains out of scope; see `docs/guides/effects-migration-stance.adoc`.
+
+*Partial by Default* (termination, distinct from the `Partial` effect):
 
 - Functions are partial by default (may not terminate)
 - `total` functions must provably terminate
diff --git a/lib/effect.ml b/lib/effect.ml
index e0b33f6e..e72b6522 100644
--- a/lib/effect.ml
+++ b/lib/effect.ml
@@ -129,8 +129,9 @@ let string_of_eff (e : eff) : string =
     [docs/guides/effects-migration-stance.adoc]). *)
 
 (** Canonical v1 effect names.  [Throws] is written [Throws[E]] at use
-    sites; the type parameter is carried syntactically but not yet
-    threaded (tracking-only v1). *)
+    sites; the type argument is threaded by [Typecheck.lower_effect_expr]
+    (mangled into the singleton name, so [Throws[A]], [Throws[B]] and
+    bare [Throws] are distinct under effect unification). *)
 let v1_effects = [ "IO"; "Async"; "Partial"; "Throws"; "Mut" ]
 
 (** Reserved for v1.x — recognised so the names are not repurposed, not