fix: Ensure that the constraints are checked and propagated fully #4798
Conversation
Only the root variable knows which kinds it is constrained by as we remove them and combine them when two variables are unified
Else we aren't able to reliably lookup all constraints for a variable as they may be spread out over multiple (otherwise unified) variables.
| @@ -182,6 +182,28 @@ pub fn equal( | |||
| }) | |||
| } | |||
|
|
|||
| pub fn subsume( | |||
There was a problem hiding this comment.
What is the intent of the name subsume? Is this related to subtyping somehow? My understanding of your changes was that we are propagating the constraints to the root type. Is root type the supertype in this context? I had assumed that the root type was just the root type variable where all its sub type variables are all equal to it and we have a convention to associate the constraints with the root type.
There was a problem hiding this comment.
What is the intent of the name subsume? Is this related to subtyping somehow?
Yes, this change is for fix: Don't cause errors in default argument checking due to label requirements. I needed to change the check to use subsumption, else the default value (a string literal) would not get treated as a label and cause an error as the function required a label to be passed. It should probably have been a separate PR as it is a different change from fully checking the constraints fully.
Is root type the supertype in this context?
No. If multiple variables are unified the root is the variable that names the entire set.
Say you unify like this
A <> B
B <> C
D <> E
The set A, B, C may have the root A while D, E has the root E. Querying the root for B or C returns A in both cases which lets us know that they are unified while querying it for D will yield E so we know it is in a disjoint set from B, C (and A). Which variable in a set that ends up as the root is arbitrary and just a by product of how https://en.wikipedia.org/wiki/Disjoint-set_data_structure is implemented.
Specifically in this change I made sure that add a constraint on, for example, B (which has A as the root) we actually record the constraint on A. Before, when we added the constraint on B explicitly inference did not know that A and C were also constrained by this (hence lost).
There was a problem hiding this comment.
Thanks for the explanation, helps clarify.
…is bound by Only the root variable knows which kinds it is constrained by as we remove them and combine them when two variables are unified
Fixed. Messed up the cherry-pick/rebase and dropped the test and a change. |
fix: Always query the root variable for the constraint it is bound by
Only the root variable knows which kinds it is constrained by as we remove them and combine
them when two variables are unified
fix: Don't cause errors in default argument checking due to label requirements
fix: Always add constraints to the root variable
Else we aren't able to reliably lookup all constraints for a variable as they
may be spread out over multiple (otherwise unified) variables.
Extracted from #4776