]>
Commit | Line | Data |
---|---|---|
f9f354fc | 1 | use crate::coherence::{CoherenceError, CoherenceSolver}; |
f035d41b | 2 | use crate::debug_span; |
f9f354fc | 3 | use crate::ext::*; |
f035d41b | 4 | use crate::rust_ir::*; |
f9f354fc XL |
5 | use crate::{goal_builder::GoalBuilder, Solution}; |
6 | use chalk_ir::cast::*; | |
7 | use chalk_ir::fold::shift::Shift; | |
8 | use chalk_ir::interner::Interner; | |
9 | use chalk_ir::*; | |
f9f354fc | 10 | use itertools::Itertools; |
f035d41b | 11 | use tracing::{debug, instrument}; |
f9f354fc XL |
12 | |
13 | impl<I: Interner> CoherenceSolver<'_, I> { | |
14 | pub(super) fn visit_specializations_of_trait( | |
15 | &self, | |
16 | mut record_specialization: impl FnMut(ImplId<I>, ImplId<I>), | |
17 | ) -> Result<(), CoherenceError<I>> { | |
18 | // Ignore impls for marker traits as they are allowed to overlap. | |
19 | let trait_datum = self.db.trait_datum(self.trait_id); | |
20 | if trait_datum.flags.marker { | |
21 | return Ok(()); | |
22 | } | |
23 | ||
24 | // Iterate over every pair of impls for the same trait. | |
25 | let impls = self.db.local_impls_to_coherence_check(self.trait_id); | |
26 | for (l_id, r_id) in impls.into_iter().tuple_combinations() { | |
27 | let lhs = &self.db.impl_datum(l_id); | |
28 | let rhs = &self.db.impl_datum(r_id); | |
29 | ||
30 | // Two negative impls never overlap. | |
31 | if !lhs.is_positive() && !rhs.is_positive() { | |
32 | continue; | |
33 | } | |
34 | ||
35 | // Check if the impls overlap, then if they do, check if one specializes | |
36 | // the other. Note that specialization can only run one way - if both | |
37 | // specialization checks return *either* true or false, that's an error. | |
38 | if !self.disjoint(lhs, rhs) { | |
39 | match (self.specializes(l_id, r_id), self.specializes(r_id, l_id)) { | |
40 | (true, false) => record_specialization(l_id, r_id), | |
41 | (false, true) => record_specialization(r_id, l_id), | |
42 | (_, _) => { | |
3dfed10e | 43 | return Err(CoherenceError::OverlappingImpls(self.trait_id)); |
f9f354fc XL |
44 | } |
45 | } | |
46 | } | |
47 | } | |
48 | ||
49 | Ok(()) | |
50 | } | |
51 | ||
52 | // Test if the set of types that these two impls apply to overlap. If the test succeeds, these | |
53 | // two impls are disjoint. | |
54 | // | |
55 | // We combine the binders of the two impls & treat them as existential quantifiers. Then we | |
56 | // attempt to unify the input types to the trait provided by each impl, as well as prove that | |
57 | // the where clauses from both impls all hold. At the end, we apply the `compatible` modality | |
58 | // and negate the query. Negating the query means that we are asking chalk to prove that no | |
59 | // such overlapping impl exists. By applying `compatible { G }`, chalk attempts to prove that | |
60 | // "there exists a compatible world where G is provable." When we negate compatible, it turns | |
61 | // into the statement "for all compatible worlds, G is not provable." This is exactly what we | |
62 | // want since we want to ensure that there is no overlap in *all* compatible worlds, not just | |
63 | // that there is no overlap in *some* compatible world. | |
64 | // | |
65 | // Examples: | |
66 | // | |
67 | // Impls: | |
68 | // impl<T> Foo for T { } // rhs | |
69 | // impl Foo for i32 { } // lhs | |
70 | // Generates: | |
71 | // not { compatible { exists<T> { exists<> { T = i32 } } } } | |
72 | // | |
73 | // Impls: | |
74 | // impl<T1, U> Foo<T1> for Vec<U> { } // rhs | |
75 | // impl<T2> Foo<T2> for Vec<i32> { } // lhs | |
76 | // Generates: | |
77 | // not { compatible { exists<T1, U> { exists<T2> { Vec<U> = Vec<i32>, T1 = T2 } } } } | |
78 | // | |
79 | // Impls: | |
80 | // impl<T> Foo for Vec<T> where T: Bar { } | |
81 | // impl<U> Foo for Vec<U> where U: Baz { } | |
82 | // Generates: | |
83 | // not { compatible { exists<T> { exists<U> { Vec<T> = Vec<U>, T: Bar, U: Baz } } } } | |
84 | // | |
f035d41b | 85 | #[instrument(level = "debug", skip(self))] |
f9f354fc | 86 | fn disjoint(&self, lhs: &ImplDatum<I>, rhs: &ImplDatum<I>) -> bool { |
f9f354fc XL |
87 | let interner = self.db.interner(); |
88 | ||
89 | let (lhs_binders, lhs_bound) = lhs.binders.as_ref().into(); | |
90 | let (rhs_binders, rhs_bound) = rhs.binders.as_ref().into(); | |
91 | ||
92 | // Upshift the rhs variables in params to account for the joined binders | |
93 | let lhs_params = lhs_bound | |
94 | .trait_ref | |
95 | .substitution | |
3dfed10e | 96 | .as_slice(interner) |
f9f354fc XL |
97 | .iter() |
98 | .cloned(); | |
99 | let rhs_params = rhs_bound | |
100 | .trait_ref | |
101 | .substitution | |
3dfed10e | 102 | .as_slice(interner) |
f9f354fc | 103 | .iter() |
5869c6ff | 104 | .map(|param| param.clone().shifted_in(interner)); |
f9f354fc XL |
105 | |
106 | // Create an equality goal for every input type the trait, attempting | |
107 | // to unify the inputs to both impls with one another | |
108 | let params_goals = lhs_params | |
109 | .zip(rhs_params) | |
110 | .map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner)); | |
111 | ||
112 | // Upshift the rhs variables in where clauses | |
113 | let lhs_where_clauses = lhs_bound.where_clauses.iter().cloned(); | |
114 | let rhs_where_clauses = rhs_bound | |
115 | .where_clauses | |
116 | .iter() | |
5869c6ff | 117 | .map(|wc| wc.clone().shifted_in(interner)); |
f9f354fc XL |
118 | |
119 | // Create a goal for each clause in both where clauses | |
120 | let wc_goals = lhs_where_clauses | |
121 | .chain(rhs_where_clauses) | |
122 | .map(|wc| wc.cast(interner)); | |
123 | ||
124 | // Join all the goals we've created together with And, then quantify them | |
125 | // over the joined binders. This is our query. | |
126 | let goal = Box::new(Goal::all(interner, params_goals.chain(wc_goals))) | |
127 | .quantify(interner, QuantifierKind::Exists, lhs_binders) | |
128 | .quantify(interner, QuantifierKind::Exists, rhs_binders) | |
129 | .compatible(interner) | |
130 | .negate(interner); | |
131 | ||
132 | let canonical_goal = &goal.into_closed_goal(interner); | |
3dfed10e XL |
133 | let mut fresh_solver = (self.solver_builder)(); |
134 | let solution = fresh_solver.solve(self.db, canonical_goal); | |
f9f354fc XL |
135 | let result = match solution { |
136 | // Goal was proven with a unique solution, so no impl was found that causes these two | |
137 | // to overlap | |
138 | Some(Solution::Unique(_)) => true, | |
139 | // Goal was ambiguous, so there *may* be overlap | |
140 | Some(Solution::Ambig(_)) | | |
141 | // Goal cannot be proven, so there is some impl that causes overlap | |
142 | None => false, | |
143 | }; | |
144 | debug!("overlaps: result = {:?}", result); | |
145 | result | |
146 | } | |
147 | ||
148 | // Creates a goal which, if provable, means "more special" impl specializes the "less special" one. | |
149 | // | |
150 | // # General rule | |
151 | // | |
152 | // Given the more special impl: | |
153 | // | |
154 | // ```ignore | |
155 | // impl<P0..Pn> SomeTrait<T1..Tm> for T0 where WC_more | |
156 | // ``` | |
157 | // | |
158 | // and less special impl | |
159 | // | |
160 | // ```ignore | |
161 | // impl<Q0..Qo> SomeTrait<U1..Um> for U0 where WC_less | |
162 | // ``` | |
163 | // | |
164 | // create the goal: | |
165 | // | |
166 | // ```ignore | |
167 | // forall<P0..Pn> { | |
168 | // if (WC_more) {} | |
169 | // exists<Q0..Qo> { | |
170 | // T0 = U0, ..., Tm = Um, | |
171 | // WC_less | |
172 | // } | |
173 | // } | |
174 | // } | |
175 | // ``` | |
176 | // | |
177 | // # Example | |
178 | // | |
179 | // Given: | |
180 | // | |
181 | // * more: `impl<T: Clone> Foo for Vec<T>` | |
182 | // * less: `impl<U: Clone> Foo for U` | |
183 | // | |
184 | // Resulting goal: | |
185 | // | |
186 | // ```ignore | |
187 | // forall<T> { | |
188 | // if (T: Clone) { | |
189 | // exists<U> { | |
190 | // Vec<T> = U, U: Clone | |
191 | // } | |
192 | // } | |
193 | // } | |
194 | // ``` | |
f035d41b | 195 | #[instrument(level = "debug", skip(self))] |
f9f354fc XL |
196 | fn specializes(&self, less_special_id: ImplId<I>, more_special_id: ImplId<I>) -> bool { |
197 | let more_special = &self.db.impl_datum(more_special_id); | |
198 | let less_special = &self.db.impl_datum(less_special_id); | |
f035d41b | 199 | debug_span!("specializes", ?less_special, ?more_special); |
f9f354fc XL |
200 | |
201 | let interner = self.db.interner(); | |
202 | ||
203 | let gb = &mut GoalBuilder::new(self.db); | |
204 | ||
205 | // forall<P0..Pn> { ... } | |
206 | let goal = gb.forall( | |
207 | &more_special.binders, | |
208 | less_special_id, | |
209 | |gb, _, more_special_impl, less_special_id| { | |
210 | // if (WC_more) { ... } | |
211 | gb.implies(more_special_impl.where_clauses.iter().cloned(), |gb| { | |
212 | let less_special = &gb.db().impl_datum(less_special_id); | |
213 | ||
214 | // exists<Q0..Qn> { ... } | |
215 | gb.exists( | |
216 | &less_special.binders, | |
5869c6ff | 217 | more_special_impl.trait_ref.clone(), |
f9f354fc XL |
218 | |gb, _, less_special_impl, more_special_trait_ref| { |
219 | let interner = gb.interner(); | |
220 | ||
221 | // T0 = U0, ..., Tm = Um | |
222 | let params_goals = more_special_trait_ref | |
223 | .substitution | |
3dfed10e | 224 | .as_slice(interner) |
f9f354fc XL |
225 | .iter() |
226 | .cloned() | |
227 | .zip( | |
228 | less_special_impl | |
229 | .trait_ref | |
230 | .substitution | |
3dfed10e | 231 | .as_slice(interner) |
f9f354fc XL |
232 | .iter() |
233 | .cloned(), | |
234 | ) | |
235 | .map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner)); | |
236 | ||
237 | // <less_special_wc_goals> = where clauses from the less special impl | |
238 | let less_special_wc_goals = less_special_impl | |
239 | .where_clauses | |
240 | .iter() | |
241 | .cloned() | |
242 | .casted(interner); | |
243 | ||
244 | // <equality_goals> && WC_less | |
245 | gb.all(params_goals.chain(less_special_wc_goals)) | |
246 | }, | |
247 | ) | |
248 | }) | |
249 | }, | |
250 | ); | |
251 | ||
252 | let canonical_goal = &goal.into_closed_goal(interner); | |
3dfed10e | 253 | let mut fresh_solver = (self.solver_builder)(); |
1b1a35ee | 254 | let result = fresh_solver.has_unique_solution(self.db, canonical_goal); |
f9f354fc XL |
255 | |
256 | debug!("specializes: result = {:?}", result); | |
257 | ||
258 | result | |
259 | } | |
260 | } |