types: solve the recursive effect equation exactly instead of widening

[simontreanor]

Fixes #24.

A recursive function of arity >= 2 that performed any effect was rejected outright:

error: effect mismatch: cannot unify ''a -> int -> int with ''a -> int ->{io} int

Arity 1 was fine at any effect, and arity >= 2 was fine while pure — it was the combination that failed, which is the shape of every game loop, REPL, menu and server loop. With no while in the language, recursion is the only way to write a loop at all.

Cause

Not the monomorphic-recursion assumption. Each application in a body performs a fresh latent effect variable into cur_eff, so a recursive call of arity n contributes n of them, and the binding''s own type puts the accumulated body effect on the innermost arrow with the currying arrows pure. unify recurses into the codomain before unifying an arrow''s own effect, so the first equation solved is the innermost one — and it mentions the outer arrows'' variables:

{e6}  ~  {io, e4, e6}

Neither side is a bare variable absent from the other, so it fell through to the conservative widening, which closes every variable involved to the joined label set. That stamped io onto e4 — the outer currying arrow, which only builds a closure and which the binding''s type says is pure. The outer equation was then {io} ~ {}: two closed effects that disagree.

Fix

Effects are an idempotent union, so X = S ∪ X has the exact solution X := S. Solve that case directly — bind the variable to the other side with its own occurrence removed — before falling back to widening, leaving every other variable in the equation open. e4 then stays open and the outer arrow binds it to pure; e6 resolves to {io}, giving ''a -> int ->{io} int.

The effect is not lost, which is the thing worth checking about a fix in this area: fully applying the loop still performs io (a let pure caller is still rejected) and partial application is still pure.

Tests

tests/typecheck.rs — arity-2 recursion with io checks and infers ''a -> int ->{io} int; the effect still leaks out of a full application; partial application is still pure; mutual recursion at arity 2 with io checks. tests/compile.rs — an e2e that the accepted loop actually runs and counts down. All four typecheck tests verified to fail on main.

cargo test green, cargo clippy --all-targets clean, cargo fmt applied. INTERNALS.md gains a short section documenting unify_eff''s solving order, since the case that was missing is not obvious from the code.