Bug fixes to the modules system. #959
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 fixes #796. It also fixes the @bboston7's example on #883, but not the original example in #883. The issue there is that `asdf` function generates a constraint only involving the module parameter. Normally we don't try to solve constraint that don't mention a schema's parameters, because they can always be solved "later", and hopefully with more things instantiated. The weird thing in this case is that the schema adds *local" constraint to the module parameters, but we end up ignoring these.
When checking a signature we try to solve sub-goals that mention any of the variables mentioned in the signature's assumptions. We do this because these assumptions are local, and if the assumption is not solved in the current context, we may not be able to solve it later. This is OK if the goal does not contain free variables. If it does, things are a bit flaky as we may reject some programs and accept others depending on in what order things happened to be instnatiated
|
This should now fix #883 in its entirety |
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 fixes #796.
It also fixes the @bboston7's example on #883, but not the original
example in #883. The issue there is that
asdffunction generatesa constraint only involving the module parameter.
Normally we don't try to solve constraint that don't mention a schema's
parameters, because they can always be solved "later", and hopefully with
more things instantiated.
The weird thing in this case is that the schema adds *local" constraint to
the module parameters, but we end up ignoring these.