Implement instance derivation #81
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 fixes a bug in implicit variable resolution where variables in instance heads are all lowered into Implicit variables rather than becoming Bound.
Following the changes in the previous commit, this adds subtyping and unification rules for Implicit and Bound variables. Previously, instance heads only contained Implicit variables which can be unified trivially.
This removes an erroneous fix now that the lowering properly emits Implicit / Bound variables in the instance head, which means that the `a` in `instance TypeEq a a` now refer to the same logical variable instead of binding `a` twice.
This completely reworks the checking code for types, reducing the number of implicit invariants that using global mutable state introduced.
This commit also changes the instance chain search in the constraint solver to properly consider instances that appear in the files of any Type::Constructor involved in a constraint being solved.
The removal of Variable::Implicit uncovered a bug in instance checking where promote_type began throwing an escaped skolem error in previously valid types. Variable::Implicit was excluded from this check, and it turns out that the instance head checking was producing invalid ones. Instance head checking would use ShiftImplicit to correctly adjust the levels after generalisation. The problem was that in instance member checking, this was not applied; thus, the unification of Implicit and Bound exposed the issue through promote_type.
This commit implements coercion for `f <~> g` given that `f a <~> g a` can be solved. See the try_higher_kinded_coercion function for details.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
No description provided.