Update for GHC8 and (partial) fix of assertion patterns checking #4
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
Mostly changing Eq1 instances to work with transformers-5
…values of the same type
Before this commit assertion patterns are only checked to have the required type. That is not enough, as the value provided in the assertion pattern is used to determine the result type of the clause, so we have to ensure the value provided in the assertion pattern is indeed the only option, otherwise the type checking will become unsound (see src/Dependent/EqAny.sfp for an example). This patch adds checking for the assertion patterns. To achieve this we return new meta variable as the pattern value and save a pair (meta, assertion pattern value) for the later. By the end of clause pattern checking this new meta variable should be solved to exactly the value provided, otherwise it's an error. This fixes all the affected variants EXCEPT Dependent.Monadic, since we rely on the unification to solve the constraint for us.
This patch does the following:
1. Now we have two types of meta variables: Exist and Constraint, the
first to be used to find implicit arguments and stuff like that, while
the second to be used for solving assertion pattern constraints. They
need to be handled differently during the unification process: for
example, it's absolutely legal (and desirable) to instantiate ?meta to
'x' while unifying 'f x' with 'f ?meta' if ?meta is existential (stands
for implicit argument and stuff like that), but it would lead to
undesirable results (like proving injectivity for arbitrary function)
if ?meta comes from the checking of an assertion pattern.
2. Equation constructor now gets an extra Bool argument. It essentially
signals if this equation is good for both constraints and existentials
or only for existentials.
3. equate method also gets an extra Bool argument representing if
current context is ok to solve constraints or only to pick
existentials. There are really only two reasonable two to handle this
argument in the equate implementation:
- pass it to the subsequent Equations if this language construct is
injective
- ignore it and set subsequent Equations flag to False if the
language construct is not guaranteed to be injective (like function
application or record projections)
3. Fix all the variant to compile with the new code. Function
applications, case, record projections and all
quote/continuations/require stuff are made only for existentials (the
latter triple is here mostly because I'm not sure about them and it's
always safe to be conservative).
This fixes the problem with proving arbitrary functions injectivity
everywhere except the Dependent.Monadic variant.
|
@yanok You separated Unification into "solve" and "check" right? |
|
@be5invis not really. It is still just |
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 pull request contains