Skip to content

Commit 3e3f76a

Browse files
borsbors
committed
Auto merge of #754 - nikomatsakis:issue-727, r=nikomatsakis
we only need to prove things one way Partially addresses #727 (some work is left for future work).
2 parents 1f43e82 + 70b2fdb commit 3e3f76a

File tree

6 files changed

+194
-29
lines changed

6 files changed

+194
-29
lines changed

‎chalk-recursive/src/combine.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ use tracing::debug;
44
use chalk_ir::interner::Interner;
55
use chalk_ir::{ClausePriority, DomainGoal, GenericArg};
66

7+
#[tracing::instrument(level = "Debug", skip(interner))]
78
pub(super) fn with_priorities<I: Interner>(
89
interner: I,
910
domain_goal: &DomainGoal<I>,
@@ -12,7 +13,7 @@ pub(super) fn with_priorities<I: Interner>(
1213
b: Solution<I>,
1314
prio_b: ClausePriority,
1415
) -> (Solution<I>, ClausePriority) {
15-
match (prio_a, prio_b, a, b) {
16+
let result = match (prio_a, prio_b, a, b) {
1617
(ClausePriority::High, ClausePriority::Low, higher, lower)
1718
| (ClausePriority::Low, ClausePriority::High, lower, higher) => {
1819
// if we have a high-priority solution and a low-priority solution,
@@ -34,7 +35,9 @@ pub(super) fn with_priorities<I: Interner>(
3435
}
3536
}
3637
(_, _, a, b) => (a.combine(b, interner), prio_a),
37-
}
38+
};
39+
debug!(?result, "combined result");
40+
result
3841
}
3942

4043
fn calculate_inputs<I: Interner>(

‎chalk-recursive/src/solve.rs

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -154,11 +154,6 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
154154
for program_clause in clauses {
155155
debug_span!("solve_from_clauses", clause = ?program_clause);
156156

157-
// If we have a completely ambiguous answer, it's not going to get better, so stop
158-
if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
159-
return Ok(Solution::Ambig(Guidance::Unknown));
160-
}
161-
162157
let ProgramClauseData(implication) = program_clause.data(self.interner());
163158
let infer = infer.clone();
164159
let subst = subst.clone();
@@ -184,11 +179,19 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
184179
} else {
185180
debug!("Error");
186181
}
182+
183+
if let Some((cur_solution, _)) = &cur_solution {
184+
if cur_solution.is_trivial_and_always_true(self.interner()) {
185+
break;
186+
}
187+
}
187188
}
188189

189190
if let Some((s, _)) = cur_solution {
191+
debug!("solve_from_clauses: result = {:?}", s);
190192
Ok(s)
191193
} else {
194+
debug!("solve_from_clauses: error");
192195
Err(NoSolution)
193196
}
194197
}

‎chalk-solve/src/solve.rs

Lines changed: 40 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -44,30 +44,43 @@ impl<I: Interner> Solution<I> {
4444
/// There are multiple candidate solutions, which may or may not agree on
4545
/// the values for existential variables; attempt to combine them. This
4646
/// operation does not depend on the order of its arguments.
47-
//
48-
// This actually isn't as precise as it could be, in two ways:
49-
//
50-
// a. It might be that while there are multiple distinct candidates, they
51-
// all agree about *some things*. To be maximally precise, we would
52-
// compute the intersection of what they agree on. It's not clear though
53-
// that this is actually what we want Rust's inference to do, and it's
54-
// certainly not what it does today.
55-
//
56-
// b. There might also be an ambiguous candidate and a successful candidate,
57-
// both with the same refined-goal. In that case, we could probably claim
58-
// success, since if the conditions of the ambiguous candidate were met,
59-
// we know the success would apply. Example: `?0: Clone` yields ambiguous
60-
// candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
61-
// Clone`.
62-
//
63-
// But you get the idea.
47+
///
48+
/// This actually isn't as precise as it could be, in two ways:
49+
///
50+
/// a. It might be that while there are multiple distinct candidates, they
51+
/// all agree about *some things*. To be maximally precise, we would
52+
/// compute the intersection of what they agree on. It's not clear though
53+
/// that this is actually what we want Rust's inference to do, and it's
54+
/// certainly not what it does today.
55+
///
56+
/// b. There might also be an ambiguous candidate and a successful candidate,
57+
/// both with the same refined-goal. In that case, we could probably claim
58+
/// success, since if the conditions of the ambiguous candidate were met,
59+
/// we know the success would apply. Example: `?0: Clone` yields ambiguous
60+
/// candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
61+
/// Clone`.
62+
///
63+
/// But you get the idea.
6464
pub fn combine(self, other: Solution<I>, interner: I) -> Solution<I> {
6565
use self::Guidance::*;
6666

6767
if self == other {
6868
return self;
6969
}
7070

71+
// Special case hack: if one solution is "true" without any constraints,
72+
// that is always the combined result.
73+
//
74+
// This is not as general as it could be: ideally, if we had one solution
75+
// that is Unique with a simpler substitution than the other one, or region constraints
76+
// which are a subset, we'd combine them.
77+
if self.is_trivial_and_always_true(interner) {
78+
return self;
79+
}
80+
if other.is_trivial_and_always_true(interner) {
81+
return other;
82+
}
83+
7184
debug!(
7285
"combine {} with {}",
7386
self.display(interner),
@@ -88,6 +101,16 @@ impl<I: Interner> Solution<I> {
88101
Solution::Ambig(guidance)
89102
}
90103

104+
pub fn is_trivial_and_always_true(&self, interner: I) -> bool {
105+
match self {
106+
Solution::Unique(constrained_subst) => {
107+
constrained_subst.value.subst.is_identity_subst(interner)
108+
&& constrained_subst.value.constraints.is_empty(interner)
109+
}
110+
Solution::Ambig(_) => false,
111+
}
112+
}
113+
91114
/// View this solution purely in terms of type inference guidance
92115
pub fn into_guidance(self) -> Guidance<I> {
93116
match self {

‎tests/test/ambiguity_issue_727.rs

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
use super::*;
2+
3+
#[test]
4+
fn issue_727_1() {
5+
test!(
6+
program {
7+
#[upstream] #[non_enumerable] #[lang(sized)]
8+
trait Sized {}
9+
10+
#[non_enumerable] #[object_safe]
11+
trait Database {}
12+
13+
#[non_enumerable]
14+
trait QueryGroup
15+
where
16+
Self: Sized,
17+
{
18+
type DynDb: Database + HasQueryGroup<Self>;
19+
}
20+
21+
#[non_enumerable] #[object_safe]
22+
trait HasQueryGroup<G>
23+
where
24+
Self: Database,
25+
G: QueryGroup,
26+
G: Sized,
27+
{ }
28+
29+
#[non_enumerable] #[object_safe]
30+
trait HelloWorld
31+
where
32+
Self: HasQueryGroup<HelloWorldStorage>,
33+
{ }
34+
35+
struct HelloWorldStorage {}
36+
37+
impl QueryGroup for HelloWorldStorage {
38+
type DynDb = dyn HelloWorld + 'static;
39+
}
40+
impl<DB> HelloWorld for DB
41+
where
42+
DB: Database,
43+
DB: HasQueryGroup<HelloWorldStorage>,
44+
DB: Sized,
45+
{ }
46+
}
47+
48+
goal {
49+
forall<T> {
50+
if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); FromEnv(T: Sized)) {
51+
T: HelloWorld
52+
}
53+
}
54+
} yields[SolverChoice::slg_default()] { // ok
55+
expect![["Unique"]]
56+
} yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
57+
expect![["Unique"]]
58+
}
59+
);
60+
}
61+
62+
#[test]
63+
fn issue_727_2() {
64+
test!(
65+
program {
66+
#[non_enumerable] #[object_safe]
67+
trait Database {}
68+
69+
#[non_enumerable]
70+
trait QueryGroup
71+
{
72+
type DynDb: Database + HasQueryGroup<Self>;
73+
}
74+
75+
#[non_enumerable] #[object_safe]
76+
trait HasQueryGroup<G>
77+
where
78+
Self: Database,
79+
G: QueryGroup,
80+
{ }
81+
82+
struct HelloWorldStorage {}
83+
84+
impl QueryGroup for HelloWorldStorage {
85+
type DynDb = dyn HasQueryGroup<HelloWorldStorage> + 'static;
86+
}
87+
}
88+
89+
goal {
90+
forall<T> {
91+
if (FromEnv(T: HasQueryGroup<HelloWorldStorage>)) {
92+
T: Database
93+
}
94+
}
95+
} yields[SolverChoice::slg_default()] {
96+
expect![["Unique"]]
97+
} yields[SolverChoice::recursive_default()] {
98+
expect![[r#"Ambiguous; no inference guidance"#]] // FIXME rust-lang/chalk#727
99+
}
100+
);
101+
}
102+
103+
#[test]
104+
fn issue_727_3() {
105+
test!(
106+
program {
107+
#[non_enumerable]
108+
trait Database {}
109+
110+
#[non_enumerable]
111+
trait HasQueryGroup<G>
112+
where
113+
Self: Database,
114+
{ }
115+
116+
struct HelloWorldStorage {}
117+
118+
impl Database for HelloWorldStorage { }
119+
}
120+
121+
goal {
122+
forall<T, S> {
123+
if (FromEnv(HelloWorldStorage: HasQueryGroup<T>); FromEnv(HelloWorldStorage: HasQueryGroup<S>)) {
124+
HelloWorldStorage: Database
125+
}
126+
}
127+
} yields[SolverChoice::slg_default()] {
128+
expect![["Unique"]]
129+
} yields[SolverChoice::recursive_default()] {
130+
expect![["Unique"]]
131+
}
132+
);
133+
}

‎tests/test/misc.rs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -749,7 +749,7 @@ fn empty_definite_guidance() {
749749
} yields[SolverChoice::slg_default()] {
750750
expect![["Unique"]]
751751
} yields[SolverChoice::recursive_default()] {
752-
expect![["Ambiguous; suggested substitution []"]]
752+
expect![[r#"Unique"#]]
753753
}
754754
}
755755
}
@@ -812,8 +812,10 @@ fn env_bound_vars() {
812812
WellFormed(&'a ())
813813
}
814814
}
815-
} yields {
815+
} yields[SolverChoice::slg_default()] {
816816
expect![["Ambiguous; definite substitution for<?U0> { [?0 := '^0.0] }"]]
817+
} yields[SolverChoice::recursive_default()] {
818+
expect![[r#"Unique; for<?U0> { substitution [?0 := '^0.0] }"#]]
817819
}
818820
goal {
819821
exists<'a> {
@@ -841,7 +843,7 @@ fn recursive_hang() {
841843
} yields[SolverChoice::slg_default()] {
842844
expect![["Ambiguous; definite substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
843845
} yields[SolverChoice::recursive_default()] {
844-
expect![["Ambiguous; suggested substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
846+
expect![[r#"Ambiguous; no inference guidance"#]]
845847
}
846848
}
847849
}

‎tests/test/mod.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -394,16 +394,17 @@ fn solve_aggregated(
394394
.expect("Test requires at least one solver");
395395
for (i, other) in tail.iter().enumerate() {
396396
println!(
397-
"\ncomparing solvers:\n\tleft: {:?}\n\tright: {:?}\n",
397+
"\ncomparing solvers:\n\texpected: {:?}\n\tactual: {:?}\n",
398398
&choices[0],
399399
&choices[i + 1]
400400
);
401-
assert_same(head, other);
401+
assert_same(other, head);
402402
}
403403

404404
expected.assert_eq(head);
405405
}
406406

407+
mod ambiguity_issue_727;
407408
mod arrays;
408409
mod auto_traits;
409410
mod closures;

0 commit comments

Comments
 (0)