Solve unsolved class constraints during whnf #61
Merged
Conversation
This file contains 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 requires some changes to the normalisation machinery and to the elaborator. * The whnf function is now parameterised by how it should handle unsolved class constraints. When typechecking, this parameter is the class instance elaborator. * The class instance elaborator is now parameterised by what it should do with constraints it still didn't manage to solve. When normalising, we want to keep the constraints as the `UnsolvedConstraint` global, since it allows the type of the constraint to contain bound variables. When generalising, we want to (like before) make the constraints `Exist` metavars, such that they are picked up as free vars that can be generalised. Fixes #48. The elaboration during normalisation will not take into account local constraints (e.g. stemming from `MyClass a =>` constraints in a type signature), but I believe this is not necessary since those constraints are still unknown and will not reduce further anyway. So I think it's OK to leave those for the full elaboration pass. (I might be wrong though...)
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.
This requires some changes to the normalisation machinery and to the
elaborator.
unsolved class constraints. When typechecking, this parameter is the
class instance elaborator.
do with constraints it still didn't manage to solve. When normalising,
we want to keep the constraints as the
UnsolvedConstraintglobal,since it allows the type of the constraint to contain bound variables.
When generalising, we want to (like before) make the constraints
Existmetavars, such that they are picked up as free vars that can be
generalised.
Fixes #48.
The elaboration during normalisation will not take into account local
constraints (e.g. stemming from
MyClass a =>constraints in a typesignature), but I believe this is not necessary since those constraints
are still unknown and will not reduce further anyway. So I think it's OK
to leave those for the full elaboration pass. (I might be wrong
though...)