[interpreter] Fix symbolic local resolution with typeuse #1213
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.
Fixes #1212.
There is a complication here. In order to maintain the malformed/invalid distinction properly, we need to make sure that type definitions are only looked up during parsing when actually needed for computing symbolic indices. Otherwise, we'd turn some syntactically valid, fully desugared programs like the following:
into triggering a syntax error instead of a validation error (due to an undefined type index). My first naive attempt at a fix actually did that and regressed one test expectation from assert_invalid to assert_malformed, which e.g. means that it could not be converted to binary anymore.
Unfortunately, we generally don't know whether the type will be needed until we have seen the full function body and know whether it contains any symbolic local (consider
let
in particular).To address that, the parser now uses a work list to defer looking up the function type (and consecutive index shifts for anonymous binders) until actually needed for computing symbolic indices. In a fully desugared program it is never triggered.
This is a bit ugly, but most implementations probably don't need to care about this distinction. But for the reference interpreter it seems relevant.