Add reporting of LHS values when error occurs in RHS predicate #1634
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, at least partly, addresses #1633.
In particular, it adds a new case of
TestResult
,failure-exn-satisfies-rhs
, which is used when it a satisfies test where an exception was trigger in the RHS. In those cases, we have a value on the LHS, so we should show it along with the exception. I didn't see tests of this kind of behavior, but please point me if there is a way to do it. The four cases that will trigger the new behavior are:And the new error message looks like:
I noticed, as I was doing this, that there may be other cases where there is more information that could be shown, e.g., if an error is triggered by the refinement of an
is
test, neither the left nor right value is shown, which it seems like they should be:Of course, there are still more variations -- e.g., if the right side of an
is
test errors, the left side value could be shown, etc. Of course, maybe there is a way to make this visible in the stack trace which would subsume all of this? Though with the stack manipulation that's going on, perhaps that is expecting too much.