Skip to content

Commit 9f8a6ed

Browse files
feat(effects): thread parametric Throws[E] type argument (Refs #59) (#204)
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) <noreply@anthropic.com>
1 parent ad50525 commit 9f8a6ed

1 file changed

Lines changed: 16 additions & 1 deletion

File tree

lib/typecheck.ml

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -452,7 +452,22 @@ and lower_effect_expr (ctx : context) (ee : effect_expr) : eff =
452452
in
453453
match ee with
454454
| EffVar { name; _ } -> resolve name
455-
| EffCon ({ name; _ }, _args) -> resolve name
455+
| EffCon ({ name; _ }, args) ->
456+
(* Parametric effect, e.g. `Throws[MyErr]` (issue #59). Effect
457+
*tracking* only: carry the type argument by mangling it into the
458+
singleton name, so `Throws[A]`, `Throws[B]` and bare `Throws` are
459+
distinct under the string-equality unification of `eff` — without
460+
growing the `eff` ADT (which would ripple across every effect
461+
operation). The base name is still validated via `resolve`. *)
462+
(match resolve name with
463+
| ESingleton base when args <> [] ->
464+
let arg_str =
465+
args
466+
|> List.map (fun (TyArg te) -> ty_to_string (lower_type_expr ctx te))
467+
|> String.concat ", "
468+
in
469+
ESingleton (base ^ "[" ^ arg_str ^ "]")
470+
| other -> other)
456471
| EffUnion (e1, e2) ->
457472
EUnion [lower_effect_expr ctx e1; lower_effect_expr ctx e2]
458473

0 commit comments

Comments
 (0)