Full type checker implementation #95
Open
Conversation
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
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`.
|
🚢 🇮🇹 |
When a constrained class method like `apply` is passed as an argument to a function expecting a higher-rank type, the constraint was leaking into unification because `subtype_with_mode` with `ElaborationMode::No` does not peel constraints. Skolemise forall and collect given constraints on the expected side, then instantiate and collect wanted constraints on the inferred side, before comparing the unwrapped body types. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
match_given_instances required functional dependencies to cover stuck unification variable positions before accepting a match. This gate is correct for instance matching but wrong for given constraints, which are authoritative as they come from signatures and superclass elaboration. The bug surfaced as a spurious NoInstanceFound when a where binding used superclass methods like pure from Applicative while the outer function only had a deeper constraint like MonadRec. The binding's type variable hadn't unified with the outer skolem yet, making the position stuck, and the functional dependency check rejected it. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This adds the check_derive_members phase, which implements constraint solving and implementation generation based on the result of check_derive_heads. This introduces symmetry with check_instance_heads where a user-defined instance head's constraints are solved in check_instance_members where they're actually used. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Similar to class members 5c9d9fa, synonym bodies need to be shifted to align with the current scope. We use the current size of the scope as an offset because synonym bodies are originally bound starting at 0. This commit also updates class member shifting to use the size of the current scope for symmetry.
This commit adds missing cases in match_type, match_given_type, and can_unify. It also changes the approach from pattern matching deeply against the Type::Application, to reconstructing a Type::Application from the Type::Function to unify against.
Add a parallel `classes` map alongside `types` in ResolvedLocals, ResolvedExports, and ResolvedImport. Classes are routed exclusively into `classes`, non-class types into `types`. The lowering phase uses context-aware lookup: an `in_constraint` flag propagates through TypeConstrained and TypeApplicationChain so that TypeConstructor tries class resolution first in constraint position, falling back to type resolution. The checking phase's PrimLookup and known-type collectors use dedicated class lookups for class items (Partial, Add, Warn, Coercible, etc.). LSP consumers (completion, definition, hover, references, symbols) iterate and look up both types and classes. This fixes the conflict where Prim.Row.Cons (a class) and Prim.RowList.Cons (a data type) occupied the same map, reducing the record package compatibility errors from 39 to 3. Co-authored-by: Amp <amp@ampcode.com>
This adds implication-based constraint solving to replace the local constraint solving that was being done in let binding groups. This potentially enables future extensions to the language like GADTs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-Authored-By: Amp <amp@ampcode.com>
When a type synonym's kind signature has more function arrows than the definition has parameters, the excess arrows belong to the result kind. Previously, both check_signature_like and infer_synonym_application required an exact match between arrow count and parameter count, which rejected these synonyms with TypeSignatureVariableMismatch and PartialSynonymApplication errors respectively. The fix folds excess kind arrows back into the result kind during signature checking, and applies excess arguments as regular type applications after synonym expansion. See test 309 for examples. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The previous implementation was susceptible to level conflicts because of synonym expansion, which can introduce variables while we're also performing substitutions. This commit refactors the algorithm to only perform substitution once we encounter a non-Forall type post-expansion.
This implements a proper checking rule for guarded expressions to fix the erroneous implementation which overwrote types instead of unifying.
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.
The goal of this branch is to be able to compile the core packages; the
compiler-compatbilitycrate provides a utility that shows compilation errors for each module in the package. There's still a very long journey ahead.