Skip to content

Full type checker implementation#95

Open
purefunctor wants to merge 171 commits intomainfrom
relentless-type-checking
Open

Full type checker implementation#95
purefunctor wants to merge 171 commits intomainfrom
relentless-type-checking

Conversation

@purefunctor
Copy link
Owner

The goal of this branch is to be able to compile the core packages; the compiler-compatbility crate provides a utility that shows compilation errors for each module in the package. There's still a very long journey ahead.

This refactors the error reporting in the checking crate to render local
types eagerly. This is a pre-requisite for creating a diagnostics crate,
which will be used for the LSP's error reporting and integration tests.
This introduces the significant_ranges function in diagnostics::context
to extract the significant ranges in a node. Annotations are attached to
InstanceDeclaration, not InstanceChain; this makes it impossible for the
naive Annotation-stripping approach to work, leading to confusing
offsets during diagnostic reporting.
This improves inference for do statements by using a unification
variable as a stand-in for the innermost expression when emulating
desugard bind/discard expressions. Inferring the pure_expression too
early causes the unification variables we created for the do statement
binders to be solved too eagerly; in the case of 215, the error becomes
associated to `pure "life"` rather than `add a b`.
purefunctor and others added 30 commits February 12, 2026 03:00
This moves generalisation and globalisation for value signatures only
after value equations are checked. This addresses an issue where kind
variables that get solved in the equation body are generalised too early
in the previous implementation.
This demonstrates a current limitation in the type checker where
operators poiinting to kind-polymorphic value groups infer to an
incorrect type. This issue can be addressed by deferring generalisation
for operator declarations, much like it is now for value declarations.
Record patterns that mention different subsets of a row type produced
rows of unequal width in the specialisation matrix, causing a panic in
default_matrix. Normalise all record constructors to the union of labels
before specialising, padding missing labels with wildcard patterns.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant