Variance #609

daboross · 2020-09-13T06:54:51Z

This contains @super-tuple and my work on rebasing @jackh726's variance work from #520 and implementing the generalizer on top of it.

As mentioned in Zulip, we've been trying to port rustc tests for the generalizer to chalk, in an effort to see what fails. Since we've been failing at this for so long, we decided to just try to write the generalizer instead! We don't fully understand it, but have enough of an idea to write something that hopefully works.

This fails 5 of the existing tests, and that's part of the motivation for opening this now - we aren't sure how to proceed on those. We have not written any new tests for variance nor the generalizer.

The last one we've debugged is dyn_lifetime_bound, which fails because when unifying our generalized value and the original ty value, the code tries to unify a inference var with universe 4, created freshly for our generalized value, with a placeholder with universe 6 - and that fails to pass the OccursCheck. Here's the debug logs we generated for that failed test: https://gist.github.com/daboross/24f1d2310bd86e1d542678c4ebd550e0

jackh726 · 2020-10-08T07:44:06Z

I added the ability to set the variances of adts and fn_defs in tests. E.g.

#[variance(Invariant, Covariant)]
struct Foo<A,B> {}

I didn't add any tests that rely on this, other than a quick lowering success test.

chalk-solve/src/infer/unify.rs

jackh726 · 2020-10-14T22:52:54Z

Did some work on this and rebased.

bors · 2020-10-21T20:24:29Z

☔ The latest upstream changes (presumably #628) made this pull request unmergeable. Please resolve the merge conflicts.

Note that reviewers usually do not review pull requests until merge conflicts are resolved! Once you resolve the conflicts, you should change the labels applied by bors to indicate that your PR is ready for review. Post this as a comment to change the labels:

@rustbot modify labels: +S-waiting-on-review -S-waiting-on-author

daboross · 2020-10-23T02:42:10Z

Thank you for working on this!

I've pushed a rebase onto 30f4a12, and currently figuring out everything that needs to be adjusted to rebase onto #629.

jackh726 · 2020-10-24T02:30:33Z

Rebased this :)

tests/test/unify.rs

tests/test/subtype.rs

chalk-solve/src/infer/unify.rs

nikomatsakis

OK, so, I have been reading the code locally. It seems good. I have to go now. I came here to comment on push_lifetime_eq_goal but I see that @matthewjasper has already made the comments I came here to make. Locally I have a few tests I was toying with adding and I may rebase and/or push those commits tomorrow.

chalk-engine/src/normalize_deep.rs

tests/test/subtype.rs

matthewjasper · 2020-10-31T22:16:57Z

tests/test/subtype.rs

+        } yields {
+            "Unique;substitution [], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }]"


This doesn't look right, these constraints are not solvable.

But these are? This just says that 'a == 'b

These are placeholders, so relating them is an error. The requirements here should be !1_0: '?0, !1_1: ?0, '!2_0: '?1, '!2_0: '?2 (the same as subtyping in both directions).

But we have allowed unifying placeholders? (On master, here is unification, here an example where two lifetime placeholders are equated).

yes, but region inference will error on such constraints.

matthewjasper · 2020-10-31T22:32:18Z

chalk-solve/src/infer/unify.rs

            let a_universal = self.table.instantiate_binders_universally(interner, a);
            let b_existential = self.table.instantiate_binders_existentially(interner, b);
-            Zip::zip_with(self, &a_universal, &b_existential)?;
+            Zip::zip_with(self, variance, &a_universal, &b_existential)?;


Suggested change

Zip::zip_with(self, variance, &a_universal, &b_existential)?;

Zip::zip_with(self, Variance::Contravariant, &a_universal, &b_existential)?;

(And Covariant below). This is required for the tests I've commented on to give the correct results.

Is Contravariant here right? I don't think so, since this also covers the Invariant case.

In the invariant case this if uses Contravariant and the other one uses Covariant. This is required so that T == U is the same as T <: U and U <: T.

super-tuple · 2020-11-01T00:00:59Z

Thank you for the comments!

We've found and fixed a bug where relate_ty_ty was incorrectly inverting the variance by re-ordering the parameters when passing them into relate_var_ty, and we've added additional tests to catch similar inversion bugs.

We haven't looked at the FnPointer problem yet.

chalk-solve/src/infer/unify.rs

jackh726 · 2020-11-01T00:31:46Z

chalk-solve/src/infer/unify.rs

            let a_universal = self.table.instantiate_binders_universally(interner, a);
            let b_existential = self.table.instantiate_binders_existentially(interner, b);
-            Zip::zip_with(self, &a_universal, &b_existential)?;
+            Zip::zip_with(self, variance, &a_universal, &b_existential)?;


Is Contravariant here right? I don't think so, since this also covers the Invariant case.

jackh726 · 2020-11-01T00:34:07Z

tests/test/subtype.rs

+        } yields {
+            "Unique;substitution [], lifetime constraints [\
+            InEnvironment { environment: Env([]), goal: '!1_0: '!1_1 }, \
+            InEnvironment { environment: Env([]), goal: '!1_1: '!1_0 }]"


But these are? This just says that 'a == 'b

tests/test/subtype.rs

super-tuple · 2020-11-01T06:31:45Z

We found another bug, which was caused by inconsistent use of push_lifetime_outlives_goals. Specifically, the code that relates lifetimes in structs assumed the function behaved the opposite way to what it was doing. We updated the function to behave the way the struct code expected (which we believe is more intuitive), and then updated the code that relates references to work with the inverted behavior. In more detail, we updated push_lifetime_outlives_goals to say that a is a subtype of b, and therefore when called with covariant, it pushes constraints that a outlives b. We also had to fix an incorrect test case once we'd fixed the bug.

We also applied the code quality suggestions Jack Huey made, and removed some duplicate tests.

Additionally, we looked at the constraints emitted by fn_lifetime_variance_with_return_type, and I don't think any of them are wrong although I don't know whether the output is meaningful. I think this PR is ready for review.

matthewjasper · 2020-11-01T10:29:25Z

The lifetime variance was correct as it was. It is a bit strange that Contravariant is the "normal" variance for lifetimes, but it is what rustc is using.

jackh726 · 2020-11-01T21:48:14Z

I reverted the lifetime variance change and made relate_binders zip with Contravariant and Covariant

bors · 2020-11-08T03:02:04Z

☔ The latest upstream changes (presumably #650) made this pull request unmergeable. Please resolve the merge conflicts.

Note that reviewers usually do not review pull requests until merge conflicts are resolved! Once you resolve the conflicts, you should change the labels applied by bors to indicate that your PR is ready for review. Post this as a comment to change the labels:

@rustbot modify labels: +S-waiting-on-review -S-waiting-on-author

nikomatsakis · 2020-11-10T21:01:04Z

r=me but it needs a rebase!

Merge of the following 17 commits by Jack Huey: Remove Zip impl for Substitution and add zip_substs Add unification database fn_def_variance and adt_variance Use actual variances when zipping Introduce FnSubst to wrap Fn subst logic Just use self.variance WIP begin adding subtypegoal Pass ambient variance to zip_substs no with_local_variance, instead zip_with calls xform Relate alias to ty rename unify to relate Start adding subtype tests Fail if trying to subtype to inference vars Use Variances not Vec<Variance> Some renames Review comments

This implements the rough equivalent of the rustc Generalizer in the chalk variance code. This needs significant refactoring, and does not yet pass all tests, however it implements all core functionality. We don't fully understand the Generalizer, and this thus most likely contains errors. Co-authored-by: Super Tuple <supertuple@gmail.com>

Co-authored-by: David Ross <daboross@daboross.net>

Added tests that verify that the generalizer works and outputs the correct constraints, and tests that verify variance is being handled correctly. Co-authored-by: David Ross <daboross@daboross.net>

This changes NormalizeDeep to normalize unified inference variables without values to the same 'root' inference variable, and fixes the normalize_deep::test::infer test. The change is necessary to accomodate the generalizer, which commonly creates new inference variables and then unifies them with old ones. This has no functional change, but would have broken normalization without this new behavior. Co-authored-by: David Ross <daboross@daboross.net>

These are just a few test cases not tested. Co-authored-by: David Ross <daboross@daboross.net>

These mirror the test cases we just added, but relating directly to an InferenceVar so that we directly test the generalizer dealing with recursing into each type. Co-authored-by: David Ross <daboross@daboross.net>

Co-authored-by: David Ross <daboross@daboross.net>

Tuples should always be covariant over their inner types. Co-authored-by: David Ross <daboross@daboross.net>

relate_ty_ty was ignoring the order in which the var and ty were passed in when matching a var and a ty. This mean't if the var was passed in second, the variance would be incorrectly inverted because the parameters were swapped around. We fixed this by inverting the variance if the var is on the right side, and added a test case for the issue. We also had to switch the order we pass the value + generalized value into relate_ty_ty, since the previous incorrect ordering was hidden by the bug. Co-authored-by: David Ross <daboross@daboross.net>

This addresses a previous TODO comment asking for further explanation with said further explanation. Co-authored-by: David Ross <daboross@daboross.net>

Expanding on our earlier bugfix, we've added additional tests where the generalized inference var is on the left side. This will help catch any bugs where the variance or the parameters inadvertantly get flipped. Co-authored-by: David Ross <daboross@daboross.net>

The code that relates Adt's was using `push_lifetime_outlives_goals` in a way that assumed it would push a outlives b when the variance is covariant. The code that relates two references assumed that it would push a constraint b outlives a when the variance was covariant. This latter behavior was what the function actually did, despite its name implying the opposite. This commit changes the behavior of `push_lifetime_outlives_goals` to push a outlives b when the variance is covariant, and updates the code that relates references. We also updated an incorrect test case where a reference was used in a struct. This test case would have failed (because `push_lifetime_outlives_goals` was inverted), but the constraints in the expected output were also incorrectly inverted. The output of two additional test cases also were updated because the constraints were emitted in a different order after making the update. Co-authored-by: David Ross <daboross@daboross.net>

Refactored some of the logic for relating inference vars with types into `relate_var_ty`. This allowed us to massively simplify the code in `relate_ty_ty` that calls `relate_var_ty`. Co-authored-by: David Ross <daboross@daboross.net>

This test was originally unique, but we accidentally duplicated it with tests now in subtype.rs. Further, when attempting to fix PR comments on this test, we actually fixed them on the other tests. Co-authored-by: David Ross <daboross@daboross.net>

This reverts commit d5b0ffc.

jackh726 · 2020-11-10T21:56:08Z

@bors r=nikomatsakis

bors · 2020-11-10T21:56:10Z

📌 Commit dfb510a has been approved by nikomatsakis

bors · 2020-11-10T21:56:20Z

⌛ Testing commit dfb510a with merge 944fce6...

bors · 2020-11-10T22:03:26Z

☀️ Test successful - checks-actions
Approved by: nikomatsakis
Pushing 944fce6 to master...

super-tuple force-pushed the subtype-variance-and-goal-writer branch from 6ad79a2 to cd44491 Compare October 4, 2020 05:37

daboross force-pushed the subtype-variance-and-goal-writer branch from 841de64 to d11b470 Compare October 11, 2020 06:02

matthewjasper reviewed Oct 11, 2020

View reviewed changes

chalk-solve/src/infer/unify.rs Outdated Show resolved Hide resolved

jackh726 force-pushed the subtype-variance-and-goal-writer branch from 3635351 to a206730 Compare October 14, 2020 22:52

jackh726 mentioned this pull request Oct 15, 2020

Add Variance and use it for zip #520

Closed

daboross force-pushed the subtype-variance-and-goal-writer branch from 7b17f8a to 893e8db Compare October 23, 2020 02:42

jackh726 force-pushed the subtype-variance-and-goal-writer branch from 893e8db to 7967679 Compare October 24, 2020 02:29

matthewjasper reviewed Oct 26, 2020

View reviewed changes

tests/test/unify.rs Outdated Show resolved Hide resolved

tests/test/subtype.rs Outdated Show resolved Hide resolved

chalk-solve/src/infer/unify.rs Outdated Show resolved Hide resolved

chalk-solve/src/infer/unify.rs Outdated Show resolved Hide resolved

nikomatsakis reviewed Oct 26, 2020

View reviewed changes

chalk-engine/src/normalize_deep.rs Outdated Show resolved Hide resolved

super-tuple force-pushed the subtype-variance-and-goal-writer branch from cc95d4e to 2d82a43 Compare October 31, 2020 19:20

jackh726 reviewed Oct 31, 2020

View reviewed changes

tests/test/subtype.rs Outdated Show resolved Hide resolved

tests/test/subtype.rs Outdated Show resolved Hide resolved

tests/test/subtype.rs Outdated Show resolved Hide resolved

tests/test/subtype.rs Show resolved Hide resolved

matthewjasper reviewed Oct 31, 2020

View reviewed changes

jackh726 reviewed Nov 1, 2020

View reviewed changes

tests/test/subtype.rs Outdated Show resolved Hide resolved

super-tuple force-pushed the subtype-variance-and-goal-writer branch from 23f4ebb to 7474fd4 Compare November 1, 2020 06:13

daboross marked this pull request as ready for review November 1, 2020 06:31

nikomatsakis approved these changes Nov 9, 2020

View reviewed changes

jackh726 and others added 2 commits November 10, 2020 16:38

jackh726 and others added 20 commits November 10, 2020 16:38

Rebase fix

8e3b1cf

Fix unify_lifetime_var

2794bd5

Fix struct_lifetime_variance test

f4957f0

Fix lifetime variance and change name

55bd1aa

Fix lifetime outlives log message

3f0f85f

Co-authored-by: David Ross <daboross@daboross.net>

Add variance and generalizer tests

ecf20dc

Added tests that verify that the generalizer works and outputs the correct constraints, and tests that verify variance is being handled correctly. Co-authored-by: David Ross <daboross@daboross.net>

Fix incorrect test cases

0b8da85

These are just a few test cases not tested. Co-authored-by: David Ross <daboross@daboross.net>

Add test cases for generalizer recursing into things

6216d80

These mirror the test cases we just added, but relating directly to an InferenceVar so that we directly test the generalizer dealing with recursing into each type. Co-authored-by: David Ross <daboross@daboross.net>

Clean up test cases

24168e3

Co-authored-by: David Ross <daboross@daboross.net>

Fix tuples being invariant

7fc9755

Tuples should always be covariant over their inner types. Co-authored-by: David Ross <daboross@daboross.net>

Improve comments

37c8340

This addresses a previous TODO comment asking for further explanation with said further explanation. Co-authored-by: David Ross <daboross@daboross.net>

Apply suggestions from code review

c9dfb7f

Refactored some of the logic for relating inference vars with types into `relate_var_ty`. This allowed us to massively simplify the code in `relate_ty_ty` that calls `relate_var_ty`. Co-authored-by: David Ross <daboross@daboross.net>

Remove duplicate test

7b15b1d

This test was originally unique, but we accidentally duplicated it with tests now in subtype.rs. Further, when attempting to fix PR comments on this test, we actually fixed them on the other tests. Co-authored-by: David Ross <daboross@daboross.net>

Revert "Fix incosistent usage of push_lifetime_outlives"

c2136ba

This reverts commit d5b0ffc.

Relate with contravariant and covariant

b5cd4d3

Use recursive_default (rebase)

dfb510a

jackh726 force-pushed the subtype-variance-and-goal-writer branch from 3ed4270 to dfb510a Compare November 10, 2020 21:46

bors merged commit 944fce6 into rust-lang:master Nov 10, 2020

bors mentioned this pull request Nov 10, 2020

Pass canonical goals to program clauses code in SLG solver #624

Merged

daboross deleted the subtype-variance-and-goal-writer branch November 11, 2020 03:46

flodiebold mentioned this pull request Nov 27, 2020

Regression with unification within fn (?) #658

Closed

jackh726 mentioned this pull request Dec 11, 2020

subtyping and type equality #418

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Variance #609

Variance #609

daboross commented Sep 13, 2020

jackh726 commented Oct 8, 2020 •

edited

Loading

jackh726 commented Oct 14, 2020

bors commented Oct 21, 2020

daboross commented Oct 23, 2020

jackh726 commented Oct 24, 2020

nikomatsakis left a comment

matthewjasper Oct 31, 2020

jackh726 Nov 1, 2020

matthewjasper Nov 1, 2020

jackh726 Nov 1, 2020

matthewjasper Nov 1, 2020

matthewjasper Oct 31, 2020

jackh726 Nov 1, 2020

matthewjasper Nov 1, 2020

super-tuple commented Nov 1, 2020

jackh726 Nov 1, 2020

jackh726 Nov 1, 2020

super-tuple commented Nov 1, 2020

matthewjasper commented Nov 1, 2020

jackh726 commented Nov 1, 2020

bors commented Nov 8, 2020

nikomatsakis commented Nov 10, 2020

jackh726 commented Nov 10, 2020

bors commented Nov 10, 2020

bors commented Nov 10, 2020

bors commented Nov 10, 2020

	Zip::zip_with(self, variance, &a_universal, &b_existential)?;
	Zip::zip_with(self, Variance::Contravariant, &a_universal, &b_existential)?;

Variance #609

Variance #609

Conversation

daboross commented Sep 13, 2020

jackh726 commented Oct 8, 2020 • edited Loading

jackh726 commented Oct 14, 2020

bors commented Oct 21, 2020

daboross commented Oct 23, 2020

jackh726 commented Oct 24, 2020

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

super-tuple commented Nov 1, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

super-tuple commented Nov 1, 2020

matthewjasper commented Nov 1, 2020

jackh726 commented Nov 1, 2020

bors commented Nov 8, 2020

nikomatsakis commented Nov 10, 2020

jackh726 commented Nov 10, 2020

bors commented Nov 10, 2020

bors commented Nov 10, 2020

bors commented Nov 10, 2020

jackh726 commented Oct 8, 2020 •

edited

Loading