From ef8deb51718b60e65a6d3ebbfc769f4dc5f1726e Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 18 May 2026 09:17:21 +0100 Subject: [PATCH] feat(effects): thread parametric Throws[E] type argument (Refs #59) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit STAGE-B cleanup. lower_effect_expr dropped EffCon type args, so `Throws[MyErr]` collapsed to bare `Throws` — the type parameter the #59 v1 list calls for (`Throws[E]`) was invisible. Now the args are mangled into the effect singleton: `Throws[MyErr]` -> ESingleton "Throws[MyErr]", distinct from `Throws[Other]` and bare `Throws` under the string-equality unification of `eff`. Chosen over growing the `eff` ADT with a parametric variant (which would ripple across every effect operation in effect.ml/unify.ml — disproportionate for this cleanup). The base name is still validated via the v1 registry (`Bogus[E]` is still rejected — verified). Scope: this is effect *tracking* only. AffineScript does not currently *enforce* effect-annotation subsumption at call sites (verified: even `IO` body vs `Mut` decl passes today) — strict effect checking / handler semantics remain the separately-deferred work (migration-stance doc; #59 "tracking alone gives most of the value"). This PR makes the tracked form carry `E`; it does not add enforcement. dune build clean; dune test --force 253/253, zero regression. Refs #59 Co-Authored-By: Claude Opus 4.7 (1M context) --- lib/typecheck.ml | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/lib/typecheck.ml b/lib/typecheck.ml index fb04df11..461b3a99 100644 --- a/lib/typecheck.ml +++ b/lib/typecheck.ml @@ -452,7 +452,22 @@ and lower_effect_expr (ctx : context) (ee : effect_expr) : eff = in match ee with | EffVar { name; _ } -> resolve name - | EffCon ({ name; _ }, _args) -> resolve name + | EffCon ({ name; _ }, args) -> + (* Parametric effect, e.g. `Throws[MyErr]` (issue #59). Effect + *tracking* only: carry the type argument by mangling it into the + singleton name, so `Throws[A]`, `Throws[B]` and bare `Throws` are + distinct under the string-equality unification of `eff` — without + growing the `eff` ADT (which would ripple across every effect + operation). The base name is still validated via `resolve`. *) + (match resolve name with + | ESingleton base when args <> [] -> + let arg_str = + args + |> List.map (fun (TyArg te) -> ty_to_string (lower_type_expr ctx te)) + |> String.concat ", " + in + ESingleton (base ^ "[" ^ arg_str ^ "]") + | other -> other) | EffUnion (e1, e2) -> EUnion [lower_effect_expr ctx e1; lower_effect_expr ctx e2]