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.

Sign up for GitHub

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

we only need to prove things one way #754

Merged
merged 6 commits into from
Apr 12, 2022
Merged

we only need to prove things one way #754

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f979cd1
start of a fix for rust-lang/chalk#727
nikomatsakis Mar 10, 2022
d55a9a2
mark the failing test as "WIP"
nikomatsakis Mar 10, 2022
2e759c1
fix tests
nikomatsakis Mar 16, 2022
a5083eb
add a fast path
nikomatsakis Mar 16, 2022
502d989
extend SLG solver with a similar optimization
nikomatsakis Mar 18, 2022
70b2fdb
Revert "extend SLG solver with a similar optimization"
nikomatsakis Apr 12, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions tests/test/misc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -749,7 +749,7 @@ fn empty_definite_guidance() {
} yields[SolverChoice::slg_default()] {
expect![["Unique"]]
} yields[SolverChoice::recursive_default()] {
expect![["Ambiguous; suggested substitution []"]]
expect![[r#"Unique"#]]
}
}
}
Expand Down Expand Up @@ -812,8 +812,10 @@ fn env_bound_vars() {
WellFormed(&'a ())
}
}
} yields {
} yields[SolverChoice::slg_default()] {
expect![["Ambiguous; definite substitution for<?U0> { [?0 := '^0.0] }"]]
} yields[SolverChoice::recursive_default()] {
expect![[r#"Unique; for<?U0> { substitution [?0 := '^0.0] }"#]]
nikomatsakis marked this conversation as resolved.
Show resolved Hide resolved
}
goal {
exists<'a> {
Expand Down Expand Up @@ -841,7 +843,7 @@ fn recursive_hang() {
} yields[SolverChoice::slg_default()] {
expect![["Ambiguous; definite substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
} yields[SolverChoice::recursive_default()] {
expect![["Ambiguous; suggested substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
expect![[r#"Ambiguous; no inference guidance"#]]
}
Comment on lines 843 to 847
Copy link
Member

Choose a reason for hiding this comment

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

And here?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

These are, I believe, equivalent. That substitution is an "identity substitution", so it's not very useful guidance. I looked into why this was coming about -- it's because I removed the (erroneous) "early exit" that was causing us to bail out early. What we now do is bail out because we see ?T: '?a for some unknown ?T and we can't make progress (in fact, we could see that it's in the environment, but the code doesn't do that today).

Comment on lines 843 to 847
Copy link
Member

Choose a reason for hiding this comment

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

The fact these are still different bothers me. Also, SLG is still given the identity solution as "ambiguous", which is somewhat at odds with what the aggregate hack is saying, right?

}
}
4 changes: 2 additions & 2 deletions tests/test/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -394,11 +394,11 @@ fn solve_aggregated(
.expect("Test requires at least one solver");
for (i, other) in tail.iter().enumerate() {
println!(
"\ncomparing solvers:\n\tleft: {:?}\n\tright: {:?}\n",
"\ncomparing solvers:\n\texpected: {:?}\n\tactual: {:?}\n",
&choices[0],
&choices[i + 1]
);
assert_same(head, other);
assert_same(other, head);
}

expected.assert_eq(head);
Expand Down