fix(check): harden type checker — occurs check + type schemes#61
Merged
Conversation
unify previously bound a type variable to any type without checking whether the variable occurred inside it, so `'a = 'a -> Int` (or `'a = Echo 'a`) was accepted and made `resolve` recurse forever. Adds `CheckEnv::occurs(id, ty)`, which walks the resolved type through every former (Fun, Dist, List, Set, Option, Map, Result, Tuple, Echo, EchoR), and refuses the binding with a clear error when the variable occurs. 3 new tests (infinite via Fun, infinite via Echo, distinct-vars-still-unify); 41 bet-check tests pass; lib is clippy-clean. First half of the checker-hardening pass; real type schemes (generalise / instantiate at let-boundaries) follow. https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs
…antiate
Replaces the shared-variable pseudo-polymorphism (the module header claimed
let-polymorphism, but the code pinned a single type var across all uses of a
binding) with proper Hindley-Milner generalization:
- new `Scheme { vars, ty }`; env bindings are now schemes. `bind()` still takes
a `Type` and wraps a monomorphic scheme, so its many callers are unchanged;
`bind_scheme()` is added for polymorphic bindings.
- `generalize(ty)` quantifies the type vars free in `ty` but not free in the
environment; `instantiate(scheme)` freshens the quantified vars at each use.
- top-level `Item::Let` generalizes before binding; `Expr::Var` instantiates on
lookup; the recursive-let placeholder reads the scheme body.
- `to_string` is now seeded as `forall a. a -> String` (genuinely polymorphic).
2 new tests (independent instantiation; `to_string` at Int and String in one
scope — the old approximation would reject the second). 43 bet-check tests
pass; lib clippy-clean. Completes the checker-hardening pass (occurs check +
type schemes).
https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs
hyperpolymath
marked this pull request as ready for review
June 14, 2026 16:53
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Harden the
bet-checktype checkerThe follow-up to the echo-types work (and the "harden the checker" item from that session). Two parts:
1. Occurs check (landed) ✅
unifybound a type variable to any type without checking whether the variable occurred inside it — so'a = 'a -> Int(or'a = Echo 'a) was accepted and maderesolverecurse forever. AddedCheckEnv::occurs(id, ty)(walks the resolved type through every former: Fun, Dist, List, Set, Option, Map, Result, Tuple, Echo, EchoR) and bothVarbindings now reject occurrence with a clear error.Fun, infinite viaEcho, distinct-vars-still-unify). 41 bet-check tests pass; lib clippy-clean.2. Real type schemes (in progress) ⏳
Replacing the shared-variable pseudo-polymorphism (the header comment claims "let-polymorphism via generalization at let-boundaries" but the code didn't do it) with proper
generalize/instantiate. Will land as a follow-up commit on this branch.https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs
Generated by Claude Code