Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix sum type declaration collision #1277

Merged
merged 9 commits into from
Dec 1, 2023
Merged

Fix sum type declaration collision #1277

merged 9 commits into from
Dec 1, 2023

Conversation

shonfeder
Copy link
Contributor

@shonfeder shonfeder commented Nov 29, 2023

Closes #1277

The implementation of the isDefined constraint was producing invalid type inferences in the presence of row types with the same labels coordinated with incompatible types.

The problem was that the isDefined constraint was being solved before other constraints that would have narrowed the type thru substitutions that would have prevented the ambiguity (e.g., by unifying thru the equality constraints induced by operator annotations). This fix takes the very simple course of introducing an ordering over constraints that places isDefined constraints lasts, and sorts constraints prior to solving.

A more robust solution should be considered if we encounter similar problems with constraint order again. Alternatives might include:

  • Make the typing context available in our typing ruled and dispensing with the isDefined constraint.
  • Support some form of back-tracking in our constraint solver to ensure we find the MGU consistent with a commutative conjunction constraint.
  • Introduce disjunctive constraints and define isDefined using it.

Review by commit is probably helpful here, as some incidental cleanup is included and explained in the commit messages.


  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality
  • Feature table on README.md updated for any listed functionality

@shonfeder shonfeder force-pushed the 1275/sum-type-collision branch 2 times, most recently from c0815ea to 6731617 Compare November 29, 2023 22:26
@shonfeder shonfeder changed the title WIP: Fix sum type declaration collision Fix sum type declaration collision Nov 29, 2023
@shonfeder shonfeder requested a review from bugarela November 29, 2023 23:13
@shonfeder shonfeder force-pushed the 1275/sum-type-collision branch from 3f666f9 to 607af5c Compare November 29, 2023 23:16
Shon Feder added 9 commits November 30, 2023 09:48
Our parser and IR has the convention that the declaration

def f(x) = y

Gets represented as

def f = (x) => y

And in the IR, we expect both the representation of the declaration and
the representation of the lambda to have the same source ID.  We had not
been following this convention in the generation of variant
constructors, and that is corrected here.
Closes #1275

Since we don't do any backtracking in our constraint solving, the order
in which the are solved is important. In particular, if we solve
`isDefined` constraints before solving equality constraints, we can end
up unifying a free variable with a variable in the first discovered
defined type, rather than finding the most specific type that can unify
with the given schema.

This change defines an order over constraints, based on their kind, and
uses that to sort the constraints before they are solved.
This reverts commit 3158e29.

Apparently the example in the IR I was following is incorrect :)
This reverts commit dc4eb2a.
@shonfeder shonfeder force-pushed the 1275/sum-type-collision branch from 607af5c to d95b299 Compare December 1, 2023 00:43
@shonfeder shonfeder enabled auto-merge December 1, 2023 00:43
@shonfeder shonfeder requested a review from bugarela December 1, 2023 00:43
@shonfeder shonfeder mentioned this pull request Dec 1, 2023
4 tasks
Copy link
Collaborator

@bugarela bugarela left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great!

@shonfeder shonfeder merged commit 5fbfcd2 into main Dec 1, 2023
15 checks passed
@shonfeder shonfeder deleted the 1275/sum-type-collision branch December 1, 2023 10:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants