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 branch adds debugging information to saw-core typechecking errors. It adds a new constructor to the
TCError
data structure, calledErrorTerm
, which keeps track of the term in which an error resides. The error message displays this term to provide context to the error. This means that instead of messages likeWe will now produce error messages of the form
There are several avenues for potentially improving this feature if needbe:
ErrorTerm
controllable by a debugging flagErrorTerm
, check the size of the term; if it is so big that printing the term would not be useful, consider eliding the term, possibly printing its typeErrorTerm
for a different set of terms. Currently it will be raised for any expression called viatypeInferComplete
, which skips many recursive cases that calltypeInfer
.