Dynamic Effect Type Inference - #717

Draft

datvo06 wants to merge 17 commits into

effect-typing-engine

Commits on Jul 19, 2026

effect-typing engine (ε): usesof/effectsof + Uses/Computation/Requires + __uses_rule__
datvo06
committed
engine: add effect_type (τ,ε) pairing + check_uses (ε leak checker)
datvo06
committed
fix silent unsoundness: Computation callbacks refuse (loud) on arg inspection
datvo06
committed
scope honesty: infer_annotations gate not wired (validate-if-called, not build-time); document deferred items
datvo06
committed
placement: __uses_rule__ as @final method on Operation, Uses in syntax.py
datvo06
committed
L0 tool governance: static toolsof / reachable_tools (no LLM)
datvo06
committed
fix(governance): reify with interpreter (replace), not handler (merge)
datvo06
committed
L2 checker: check_tools(fn, *allowed) = reachable_tools - allowed
datvo06
committed
L1: Uses-restricted Template.tools (allow-list, default = full capture)
datvo06
committed
resolve P0 #2: demote Computation/Requires to plain read-metadata
datvo06
committed
address cold review: revert .tools restriction; keep static core; upstream-clean docs
datvo06
committed
chore: untrack uv.lock (accidentally swept into an earlier commit; not tracked on master)
datvo06
committed
address whole-branch review: close soundness holes + honest contracts
datvo06
committed
P0-1 follow-up: honest _Opaque boundary + pin the irreducible holes
datvo06
committed
chore: untrack uv.lock again (locally excluded so git add -A won't re-add it)
datvo06
committed
final review nits: honest check_tools docstring + pin the callable(x) hole
datvo06
committed
fix CI lint: mypy + ruff
datvo06
committed