New type hole inference #1872
Draft
New type hole inference #1872
Conversation
This file contains hidden or 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
Matched product and list functions now produce constraints. Added todos for other matched functions since it's unclear how they work at the moment. Commented out type join prov joining as the implementation of that needs to be deliberated.
Tried adding subsumption constraints where it makes sense, but the current goal is compiling. Also added constraint generation for ap.
All references to existing provenances now compile. Their correctness will need to bre re-evaluated at a later date. Adds a Prov file with some convenience functions for working with provenances. Fixes the grammar class provenance stuff by making argument properly optional, as well as adding utils for the matched types.
Join provenance will be emitted in a type join of two provenance of different origin.
… into new-type-hole-inference
The original solver would wipeout holes when refining solutions. This resulted in loss of possible types. To resolve this, holes now dominate over concrete types (i.e. the opposite behavior to before). Fixed a bug where the PTS deps would have q, instead of p.
This type projector supports only a single type and has no interactivity right now
Typed hole projectors now allow clicking through multiple types. The types are loaded lazily, so all options are generated only when the hole is clicked on.
resolved by adding subsumption constraints to pat
…, solution gen filters out bad tuples The naive duplicate detection algorithm was causing issues with valid constraints gettings filtered out. This is because checking if types are equal does not consider provenances for uniqueness Solution generation filters out tuples that have duplicate labels (which are byproducts of the solving)
matched forall was not producing the correct constraint in all cases, and typeap was missing the forall constraints it should be generated for the function it is applied to
this caused a bug where the type being passed in one would be incorrectly constrained to the body of a forall
this fixes bugs where the same provenance would become constrained to multiple unrelated things across statics
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.
A WIP, updated implementation of type hole inference.