Schemes leave closed

A Scheme leaves the unifier that minted it only if it is closed — every variable in its body is either ground or bound by the quantifier (or is a cyclic-binding root, which the ∀-prefix carries as a μ-equation, or a marked weak residual, below). A scheme that still mentions a residual variable — one free in the minting unifier — must not cross out of that unifier’s lifetime.

This is hard, not stylistic, because quantification is nominal-by-listing over unifier root ids (type-inference): the quantifier is a Vec of u32-tagged variable ids, and a free id is meaningful only relative to the union-find that minted it. A run’s unifier dies with the run and the next run’s ids restart at zero. An open scheme imported into a fresh unifier therefore silently aliases that unifier’s variables — type corruption that no check catches, not an error that surfaces.

Closure is enforced where schemes are minted for exit, by generalising against the empty TyEnv: with no environment to subtract, generalize quantifies every residual variable and resolves the body against the final unifier (core/src/typecheck/generalize.rs). Two sites mint:

• the top-level Bind-node annotation, where each statement’s scheme rides the IR into the evaluator (typecheck::annotate);
• the alias arm stored on the persistent handler frame at install (typecheck::alias_arm_scheme).

Every other carrier only transports what those two closed: the build-time prelude bake carries the schemes on the annotated prelude’s Define phrases (typecheck::bake_prelude), read back by SessionSchemes::from_prelude, and the seed’s scope tables carry the installed (value, scheme) pairs to a sealed child engine (seed::table::SerialBinding).

A weak residual is the one variable a scheme may carry unquantified, because it is marked: Scheme.weak lists it, seed_env re-seeds each listed variable as a fresh weak variable of the next unifier — with the kind it had, so a residual refuses in the next unit what it refused in its own — and a Define scheme is settled before it is stored, so no foreign id is ever read (a-let-generalises-what-is-not-weak).

One consequence: α-equivalence is not quotiented. Scheme’s PartialEq is derived, hence structural on the listed ids, so two schemes minted by different unifier runs compare unequal even when they denote the same ∀-type. Scheme comparisons must stay within one unifier run, or go through Scheme’s Display (core/src/ty/fmt.rs), which renames the prefix to canonical Greek letters before comparing.

See session-scheme-continuity for the decision this rule serves, and type-inference for how the prefix is represented.