docs(effects): re-land v1 SPEC rule + effect.ml comment (#207 follow-up, Refs #59)

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

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