]>
Commit | Line | Data |
---|---|---|
1b1a35ee | 1 | use crate::normalize_deep::DeepNormalizer; |
5869c6ff | 2 | use crate::slg::ResolventOps; |
1b1a35ee | 3 | use crate::{ExClause, Literal, TimeStamp}; |
5869c6ff | 4 | use chalk_ir::cast::Caster; |
f035d41b XL |
5 | use chalk_ir::fold::shift::Shift; |
6 | use chalk_ir::fold::Fold; | |
7 | use chalk_ir::interner::{HasInterner, Interner}; | |
8 | use chalk_ir::zip::{Zip, Zipper}; | |
9 | use chalk_ir::*; | |
1b1a35ee | 10 | use chalk_solve::infer::InferenceTable; |
f035d41b XL |
11 | use tracing::{debug, instrument}; |
12 | ||
f035d41b XL |
13 | /////////////////////////////////////////////////////////////////////////// |
14 | // SLG RESOLVENTS | |
15 | // | |
16 | // The "SLG Resolvent" is used to combine a *goal* G with some | |
17 | // clause or answer *C*. It unifies the goal's selected literal | |
18 | // with the clause and then inserts the clause's conditions into | |
19 | // the goal's list of things to prove, basically. Although this is | |
20 | // one operation in EWFS, we have specialized variants for merging | |
21 | // a program clause and an answer (though they share some code in | |
22 | // common). | |
23 | // | |
24 | // Terminology note: The NFTD and RR papers use the term | |
25 | // "resolvent" to mean both the factor and the resolvent, but EWFS | |
26 | // distinguishes the two. We follow EWFS here since -- in the code | |
27 | // -- we tend to know whether there are delayed literals or not, | |
28 | // and hence to know which code path we actually want. | |
29 | // | |
30 | // From EWFS: | |
31 | // | |
32 | // Let G be an X-clause A :- D | L1,...Ln, where N > 0, and Li be selected atom. | |
33 | // | |
34 | // Let C be an X-clause with no delayed literals. Let | |
35 | // | |
36 | // C' = A' :- L'1...L'm | |
37 | // | |
38 | // be a variant of C such that G and C' have no variables in | |
39 | // common. | |
40 | // | |
41 | // Let Li and A' be unified with MGU S. | |
42 | // | |
43 | // Then: | |
44 | // | |
45 | // S(A :- D | L1...Li-1, L1'...L'm, Li+1...Ln) | |
46 | // | |
47 | // is the SLG resolvent of G with C. | |
48 | ||
5869c6ff | 49 | impl<I: Interner> ResolventOps<I> for InferenceTable<I> { |
f035d41b XL |
50 | /// Applies the SLG resolvent algorithm to incorporate a program |
51 | /// clause into the main X-clause, producing a new X-clause that | |
52 | /// must be solved. | |
53 | /// | |
54 | /// # Parameters | |
55 | /// | |
56 | /// - `goal` is the goal G that we are trying to solve | |
57 | /// - `clause` is the program clause that may be useful to that end | |
58 | #[instrument(level = "debug", skip(self, interner, environment, subst))] | |
59 | fn resolvent_clause( | |
60 | &mut self, | |
5869c6ff | 61 | db: &dyn UnificationDatabase<I>, |
f035d41b XL |
62 | interner: &I, |
63 | environment: &Environment<I>, | |
64 | goal: &DomainGoal<I>, | |
65 | subst: &Substitution<I>, | |
66 | clause: &ProgramClause<I>, | |
67 | ) -> Fallible<ExClause<I>> { | |
68 | // Relating the above description to our situation: | |
69 | // | |
70 | // - `goal` G, except with binders for any existential variables. | |
71 | // - Also, we always select the first literal in `ex_clause.literals`, so `i` is 0. | |
72 | // - `clause` is C, except with binders for any existential variables. | |
73 | ||
74 | // C' in the description above is `consequence :- conditions`. | |
75 | // | |
76 | // Note that G and C' have no variables in common. | |
77 | let ProgramClauseImplication { | |
78 | consequence, | |
79 | conditions, | |
1b1a35ee | 80 | constraints, |
f035d41b XL |
81 | priority: _, |
82 | } = { | |
83 | let ProgramClauseData(implication) = clause.data(interner); | |
84 | ||
5869c6ff | 85 | self.instantiate_binders_existentially(interner, implication.clone()) |
f035d41b | 86 | }; |
1b1a35ee | 87 | debug!(?consequence, ?conditions, ?constraints); |
f035d41b XL |
88 | |
89 | // Unify the selected literal Li with C'. | |
5869c6ff XL |
90 | let unification_result = self.relate( |
91 | interner, | |
92 | db, | |
93 | environment, | |
94 | Variance::Invariant, | |
95 | goal, | |
96 | &consequence, | |
97 | )?; | |
f035d41b XL |
98 | |
99 | // Final X-clause that we will return. | |
100 | let mut ex_clause = ExClause { | |
101 | subst: subst.clone(), | |
102 | ambiguous: false, | |
103 | constraints: vec![], | |
104 | subgoals: vec![], | |
105 | delayed_subgoals: vec![], | |
106 | answer_time: TimeStamp::default(), | |
107 | floundered_subgoals: vec![], | |
108 | }; | |
109 | ||
110 | // Add the subgoals/region-constraints that unification gave us. | |
5869c6ff XL |
111 | ex_clause.subgoals.extend( |
112 | unification_result | |
113 | .goals | |
114 | .into_iter() | |
115 | .casted(interner) | |
116 | .map(Literal::Positive), | |
117 | ); | |
f035d41b | 118 | |
1b1a35ee XL |
119 | ex_clause |
120 | .constraints | |
121 | .extend(constraints.as_slice(interner).to_owned()); | |
122 | ||
f035d41b XL |
123 | // Add the `conditions` from the program clause into the result too. |
124 | ex_clause | |
125 | .subgoals | |
126 | .extend(conditions.iter(interner).map(|c| match c.data(interner) { | |
127 | GoalData::Not(c1) => { | |
128 | Literal::Negative(InEnvironment::new(environment, Goal::clone(c1))) | |
129 | } | |
130 | _ => Literal::Positive(InEnvironment::new(environment, Goal::clone(c))), | |
131 | })); | |
132 | ||
133 | Ok(ex_clause) | |
134 | } | |
135 | ||
136 | /////////////////////////////////////////////////////////////////////////// | |
137 | // apply_answer_subst | |
138 | // | |
139 | // Apply answer subst has the job of "plugging in" the answer to a | |
140 | // query into the pending ex-clause. To see how it works, it's worth stepping | |
141 | // up one level. Imagine that first we are trying to prove a goal A: | |
142 | // | |
143 | // A :- T: Foo<Vec<?U>>, ?U: Bar | |
144 | // | |
145 | // this spawns a subgoal `T: Foo<Vec<?0>>`, and it's this subgoal that | |
146 | // has now produced an answer `?0 = u32`. When the goal A spawned the | |
147 | // subgoal, it will also have registered a `PendingExClause` with its | |
148 | // current state. At the point where *this* method has been invoked, | |
149 | // that pending ex-clause has been instantiated with fresh variables and setup, | |
150 | // so we have four bits of incoming information: | |
151 | // | |
152 | // - `ex_clause`, which is the remaining stuff to prove for the goal A. | |
153 | // Here, the inference variable `?U` has been instantiated with a fresh variable | |
154 | // `?X`. | |
155 | // - `A :- ?X: Bar` | |
156 | // - `selected_goal`, which is the thing we were trying to prove when we | |
157 | // spawned the subgoal. It shares inference variables with `ex_clause`. | |
158 | // - `T: Foo<Vec<?X>>` | |
159 | // - `answer_table_goal`, which is the subgoal in canonical form: | |
160 | // - `for<type> T: Foo<Vec<?0>>` | |
161 | // - `canonical_answer_subst`, which is an answer to `answer_table_goal`. | |
162 | // - `[?0 = u32]` | |
163 | // | |
164 | // In this case, this function will (a) unify `u32` and `?X` and then | |
165 | // (b) return `ex_clause` (extended possibly with new region constraints | |
166 | // and subgoals). | |
167 | // | |
168 | // One way to do this would be to (a) substitute | |
169 | // `canonical_answer_subst` into `answer_table_goal` (yielding `T: | |
170 | // Foo<Vec<u32>>`) and then (b) instantiate the result with fresh | |
171 | // variables (no effect in this instance) and then (c) unify that with | |
172 | // `selected_goal` (yielding, indirectly, that `?X = u32`). But that | |
173 | // is not what we do: it's inefficient, to start, but it also causes | |
174 | // problems because unification of projections can make new | |
175 | // sub-goals. That is, even if the answers don't involve any | |
176 | // projections, the table goals might, and this can create an infinite | |
177 | // loop (see also #74). | |
178 | // | |
179 | // What we do instead is to (a) instantiate the substitution, which | |
180 | // may have free variables in it (in this case, it would not, and the | |
181 | // instantiation would have no effect) and then (b) zip | |
182 | // `answer_table_goal` and `selected_goal` without having done any | |
183 | // substitution. After all, these ought to be basically the same, | |
184 | // since `answer_table_goal` was created by canonicalizing (and | |
185 | // possibly truncating, but we'll get to that later) | |
186 | // `selected_goal`. Then, whenever we reach a "free variable" in | |
187 | // `answer_table_goal`, say `?0`, we go to the instantiated answer | |
188 | // substitution and lookup the result (in this case, `u32`). We take | |
189 | // that result and unify it with whatever we find in `selected_goal` | |
190 | // (in this case, `?X`). | |
191 | // | |
192 | // Let's cover then some corner cases. First off, what is this | |
193 | // business of instantiating the answer? Well, the answer may not be a | |
194 | // simple type like `u32`, it could be a "family" of types, like | |
195 | // `for<type> Vec<?0>` -- i.e., `Vec<X>: Bar` for *any* `X`. In that | |
196 | // case, the instantiation would produce a substitution `[?0 := | |
197 | // Vec<?Y>]` (note that the key is not affected, just the value). So | |
198 | // when we do the unification, instead of unifying `?X = u32`, we | |
199 | // would unify `?X = Vec<?Y>`. | |
200 | // | |
201 | // Next, truncation. One key thing is that the `answer_table_goal` may | |
202 | // not be *exactly* the same as the `selected_goal` -- we will | |
203 | // truncate it if it gets too deep. so, in our example, it may be that | |
204 | // instead of `answer_table_goal` being `for<type> T: Foo<Vec<?0>>`, | |
205 | // it could have been truncated to `for<type> T: Foo<?0>` (which is a | |
206 | // more general goal). In that case, let's say that the answer is | |
207 | // still `[?0 = u32]`, meaning that `T: Foo<u32>` is true (which isn't | |
208 | // actually interesting to our original goal). When we do the zip | |
209 | // then, we will encounter `?0` in the `answer_table_goal` and pair | |
210 | // that with `Vec<?X>` from the pending goal. We will attempt to unify | |
211 | // `Vec<?X>` with `u32` (from the substitution), which will fail. That | |
212 | // failure will get propagated back up. | |
213 | ||
214 | #[instrument(level = "debug", skip(self, interner))] | |
215 | fn apply_answer_subst( | |
216 | &mut self, | |
217 | interner: &I, | |
5869c6ff | 218 | unification_database: &dyn UnificationDatabase<I>, |
f035d41b XL |
219 | ex_clause: &mut ExClause<I>, |
220 | selected_goal: &InEnvironment<Goal<I>>, | |
221 | answer_table_goal: &Canonical<InEnvironment<Goal<I>>>, | |
5869c6ff | 222 | canonical_answer_subst: Canonical<AnswerSubst<I>>, |
f035d41b | 223 | ) -> Fallible<()> { |
5869c6ff | 224 | debug!(selected_goal = ?DeepNormalizer::normalize_deep(self, interner, selected_goal.clone())); |
f035d41b XL |
225 | |
226 | // C' is now `answer`. No variables in common with G. | |
227 | let AnswerSubst { | |
228 | subst: answer_subst, | |
229 | ||
230 | // Assuming unification succeeds, we incorporate the | |
231 | // region constraints from the answer into the result; | |
232 | // we'll need them if this answer (which is not yet known | |
233 | // to be true) winds up being true, and otherwise (if the | |
234 | // answer is false or unknown) it doesn't matter. | |
235 | constraints: answer_constraints, | |
236 | ||
237 | delayed_subgoals, | |
5869c6ff | 238 | } = self.instantiate_canonical(interner, canonical_answer_subst); |
f035d41b XL |
239 | |
240 | AnswerSubstitutor::substitute( | |
241 | interner, | |
5869c6ff XL |
242 | unification_database, |
243 | self, | |
f035d41b XL |
244 | &selected_goal.environment, |
245 | &answer_subst, | |
246 | ex_clause, | |
247 | &answer_table_goal.value, | |
248 | selected_goal, | |
249 | )?; | |
1b1a35ee XL |
250 | ex_clause |
251 | .constraints | |
252 | .extend(answer_constraints.as_slice(interner).to_vec()); | |
f035d41b XL |
253 | // at that point we should only have goals that stemmed |
254 | // from non trivial self cycles | |
255 | ex_clause.delayed_subgoals.extend(delayed_subgoals); | |
256 | Ok(()) | |
257 | } | |
258 | } | |
259 | ||
260 | struct AnswerSubstitutor<'t, I: Interner> { | |
261 | table: &'t mut InferenceTable<I>, | |
262 | environment: &'t Environment<I>, | |
263 | answer_subst: &'t Substitution<I>, | |
264 | ||
265 | /// Tracks the debrujn index of the first binder that is outside | |
266 | /// the term we are traversing. This starts as `DebruijnIndex::INNERMOST`, | |
267 | /// since we have not yet traversed *any* binders, but when we visit | |
268 | /// the inside of a binder, it would be incremented. | |
269 | /// | |
270 | /// Example: If we are visiting `(for<type> A, B, C, for<type> for<type> D)`, | |
271 | /// then this would be: | |
272 | /// | |
273 | /// * `1`, when visiting `A`, | |
274 | /// * `0`, when visiting `B` and `C`, | |
275 | /// * `2`, when visiting `D`. | |
276 | outer_binder: DebruijnIndex, | |
277 | ||
278 | ex_clause: &'t mut ExClause<I>, | |
279 | interner: &'t I, | |
5869c6ff | 280 | unification_database: &'t dyn UnificationDatabase<I>, |
f035d41b XL |
281 | } |
282 | ||
283 | impl<I: Interner> AnswerSubstitutor<'_, I> { | |
284 | fn substitute<T: Zip<I>>( | |
285 | interner: &I, | |
5869c6ff | 286 | unification_database: &dyn UnificationDatabase<I>, |
f035d41b XL |
287 | table: &mut InferenceTable<I>, |
288 | environment: &Environment<I>, | |
289 | answer_subst: &Substitution<I>, | |
290 | ex_clause: &mut ExClause<I>, | |
291 | answer: &T, | |
292 | pending: &T, | |
293 | ) -> Fallible<()> { | |
294 | let mut this = AnswerSubstitutor { | |
295 | interner, | |
5869c6ff | 296 | unification_database, |
f035d41b XL |
297 | table, |
298 | environment, | |
299 | answer_subst, | |
300 | ex_clause, | |
301 | outer_binder: DebruijnIndex::INNERMOST, | |
302 | }; | |
5869c6ff | 303 | Zip::zip_with(&mut this, Variance::Invariant, answer, pending)?; |
f035d41b XL |
304 | Ok(()) |
305 | } | |
306 | ||
307 | fn unify_free_answer_var( | |
308 | &mut self, | |
309 | interner: &I, | |
5869c6ff XL |
310 | db: &dyn UnificationDatabase<I>, |
311 | variance: Variance, | |
f035d41b XL |
312 | answer_var: BoundVar, |
313 | pending: GenericArgData<I>, | |
314 | ) -> Fallible<bool> { | |
315 | let answer_index = match answer_var.index_if_bound_at(self.outer_binder) { | |
316 | Some(index) => index, | |
317 | ||
318 | // This variable is bound in the answer, not free, so it | |
319 | // doesn't represent a reference into the answer substitution. | |
320 | None => return Ok(false), | |
321 | }; | |
322 | ||
323 | let answer_param = self.answer_subst.at(interner, answer_index); | |
324 | ||
325 | let pending_shifted = pending | |
326 | .shifted_out_to(interner, self.outer_binder) | |
5869c6ff | 327 | .expect("truncate extracted a pending value that references internal binder"); |
f035d41b | 328 | |
5869c6ff | 329 | let result = self.table.relate( |
f035d41b | 330 | interner, |
5869c6ff XL |
331 | db, |
332 | &self.environment, | |
333 | variance, | |
334 | answer_param, | |
335 | &GenericArg::new(interner, pending_shifted), | |
336 | )?; | |
337 | ||
338 | self.ex_clause.subgoals.extend( | |
339 | result | |
340 | .goals | |
341 | .into_iter() | |
342 | .casted(interner) | |
343 | .map(Literal::Positive), | |
f035d41b XL |
344 | ); |
345 | ||
346 | Ok(true) | |
347 | } | |
348 | ||
349 | /// When we encounter a variable in the answer goal, we first try | |
350 | /// `unify_free_answer_var`. Assuming that this fails, the | |
351 | /// variable must be a bound variable in the answer goal -- in | |
352 | /// that case, there should be a corresponding bound variable in | |
353 | /// the pending goal. This bit of code just checks that latter | |
354 | /// case. | |
355 | fn assert_matching_vars( | |
356 | &mut self, | |
357 | answer_var: BoundVar, | |
358 | pending_var: BoundVar, | |
359 | ) -> Fallible<()> { | |
360 | let BoundVar { | |
361 | debruijn: answer_depth, | |
362 | index: answer_index, | |
363 | } = answer_var; | |
364 | let BoundVar { | |
365 | debruijn: pending_depth, | |
366 | index: pending_index, | |
367 | } = pending_var; | |
368 | ||
369 | // Both bound variables are bound within the term we are matching | |
370 | assert!(answer_depth.within(self.outer_binder)); | |
371 | ||
372 | // They are bound at the same (relative) depth | |
373 | assert_eq!(answer_depth, pending_depth); | |
374 | ||
375 | // They are bound at the same index within the binder | |
376 | assert_eq!(answer_index, pending_index,); | |
377 | ||
378 | Ok(()) | |
379 | } | |
380 | } | |
381 | ||
382 | impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> { | |
5869c6ff | 383 | fn zip_tys(&mut self, variance: Variance, answer: &Ty<I>, pending: &Ty<I>) -> Fallible<()> { |
f035d41b XL |
384 | let interner = self.interner; |
385 | ||
386 | if let Some(pending) = self.table.normalize_ty_shallow(interner, pending) { | |
5869c6ff | 387 | return Zip::zip_with(self, variance, answer, &pending); |
f035d41b XL |
388 | } |
389 | ||
390 | // If the answer has a variable here, then this is one of the | |
391 | // "inputs" to the subgoal table. We need to extract the | |
392 | // resulting answer that the subgoal found and unify it with | |
393 | // the value from our "pending subgoal". | |
29967ef6 | 394 | if let TyKind::BoundVar(answer_depth) = answer.kind(interner) { |
f035d41b XL |
395 | if self.unify_free_answer_var( |
396 | interner, | |
5869c6ff XL |
397 | self.unification_database, |
398 | variance, | |
f035d41b XL |
399 | *answer_depth, |
400 | GenericArgData::Ty(pending.clone()), | |
401 | )? { | |
402 | return Ok(()); | |
403 | } | |
404 | } | |
405 | ||
406 | // Otherwise, the answer and the selected subgoal ought to be a perfect match for | |
407 | // one another. | |
29967ef6 XL |
408 | match (answer.kind(interner), pending.kind(interner)) { |
409 | (TyKind::BoundVar(answer_depth), TyKind::BoundVar(pending_depth)) => { | |
f035d41b XL |
410 | self.assert_matching_vars(*answer_depth, *pending_depth) |
411 | } | |
412 | ||
5869c6ff XL |
413 | (TyKind::Dyn(answer), TyKind::Dyn(pending)) => { |
414 | Zip::zip_with(self, variance, answer, pending) | |
415 | } | |
f035d41b | 416 | |
5869c6ff XL |
417 | (TyKind::Alias(answer), TyKind::Alias(pending)) => { |
418 | Zip::zip_with(self, variance, answer, pending) | |
419 | } | |
f035d41b | 420 | |
29967ef6 | 421 | (TyKind::Placeholder(answer), TyKind::Placeholder(pending)) => { |
5869c6ff | 422 | Zip::zip_with(self, variance, answer, pending) |
f035d41b XL |
423 | } |
424 | ||
5869c6ff XL |
425 | (TyKind::Function(answer), TyKind::Function(pending)) => Zip::zip_with( |
426 | self, | |
427 | variance, | |
428 | &answer.clone().into_binders(interner), | |
429 | &pending.clone().into_binders(interner), | |
430 | ), | |
f035d41b | 431 | |
29967ef6 | 432 | (TyKind::InferenceVar(_, _), _) | (_, TyKind::InferenceVar(_, _)) => panic!( |
f035d41b XL |
433 | "unexpected inference var in answer `{:?}` or pending goal `{:?}`", |
434 | answer, pending, | |
435 | ), | |
436 | ||
29967ef6 | 437 | (TyKind::Adt(id_a, substitution_a), TyKind::Adt(id_b, substitution_b)) => { |
5869c6ff XL |
438 | if id_a != id_b { |
439 | return Err(NoSolution); | |
440 | } | |
441 | self.zip_substs( | |
442 | variance, | |
443 | Some(self.unification_database().adt_variance(*id_a)), | |
444 | substitution_a.as_slice(interner), | |
445 | substitution_b.as_slice(interner), | |
446 | ) | |
29967ef6 XL |
447 | } |
448 | ( | |
5869c6ff XL |
449 | TyKind::AssociatedType(id_a, substitution_a), |
450 | TyKind::AssociatedType(id_b, substitution_b), | |
29967ef6 | 451 | ) => { |
5869c6ff XL |
452 | if id_a != id_b { |
453 | return Err(NoSolution); | |
454 | } | |
455 | self.zip_substs( | |
456 | variance, | |
457 | None, | |
458 | substitution_a.as_slice(interner), | |
459 | substitution_b.as_slice(interner), | |
460 | ) | |
29967ef6 XL |
461 | } |
462 | (TyKind::Scalar(scalar_a), TyKind::Scalar(scalar_b)) => { | |
5869c6ff | 463 | Zip::zip_with(self, variance, scalar_a, scalar_b) |
29967ef6 XL |
464 | } |
465 | (TyKind::Str, TyKind::Str) => Ok(()), | |
5869c6ff XL |
466 | (TyKind::Tuple(arity_a, substitution_a), TyKind::Tuple(arity_b, substitution_b)) => { |
467 | if arity_a != arity_b { | |
468 | return Err(NoSolution); | |
469 | } | |
470 | self.zip_substs( | |
471 | variance, | |
472 | None, | |
473 | substitution_a.as_slice(interner), | |
474 | substitution_b.as_slice(interner), | |
475 | ) | |
29967ef6 XL |
476 | } |
477 | ( | |
5869c6ff XL |
478 | TyKind::OpaqueType(id_a, substitution_a), |
479 | TyKind::OpaqueType(id_b, substitution_b), | |
29967ef6 | 480 | ) => { |
5869c6ff XL |
481 | if id_a != id_b { |
482 | return Err(NoSolution); | |
483 | } | |
484 | self.zip_substs( | |
485 | variance, | |
486 | None, | |
487 | substitution_a.as_slice(interner), | |
488 | substitution_b.as_slice(interner), | |
489 | ) | |
29967ef6 | 490 | } |
5869c6ff XL |
491 | (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => Zip::zip_with(self, variance, ty_a, ty_b), |
492 | (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => { | |
493 | if id_a != id_b { | |
494 | return Err(NoSolution); | |
495 | } | |
496 | self.zip_substs( | |
497 | variance, | |
498 | Some(self.unification_database().fn_def_variance(*id_a)), | |
499 | substitution_a.as_slice(interner), | |
500 | substitution_b.as_slice(interner), | |
501 | ) | |
29967ef6 XL |
502 | } |
503 | ( | |
504 | TyKind::Ref(mutability_a, lifetime_a, ty_a), | |
505 | TyKind::Ref(mutability_b, lifetime_b, ty_b), | |
506 | ) => { | |
5869c6ff XL |
507 | if mutability_a != mutability_b { |
508 | return Err(NoSolution); | |
509 | } | |
510 | // The lifetime is `Contravariant` | |
511 | Zip::zip_with( | |
512 | self, | |
513 | variance.xform(Variance::Contravariant), | |
514 | lifetime_a, | |
515 | lifetime_b, | |
516 | )?; | |
517 | // The type is `Covariant` when not mut, `Invariant` otherwise | |
518 | let output_variance = match mutability_a { | |
519 | Mutability::Not => Variance::Covariant, | |
520 | Mutability::Mut => Variance::Invariant, | |
521 | }; | |
522 | Zip::zip_with(self, variance.xform(output_variance), ty_a, ty_b) | |
29967ef6 XL |
523 | } |
524 | (TyKind::Raw(mutability_a, ty_a), TyKind::Raw(mutability_b, ty_b)) => { | |
5869c6ff XL |
525 | if mutability_a != mutability_b { |
526 | return Err(NoSolution); | |
527 | } | |
528 | let ty_variance = match mutability_a { | |
529 | Mutability::Not => Variance::Covariant, | |
530 | Mutability::Mut => Variance::Invariant, | |
531 | }; | |
532 | Zip::zip_with(self, variance.xform(ty_variance), ty_a, ty_b) | |
29967ef6 XL |
533 | } |
534 | (TyKind::Never, TyKind::Never) => Ok(()), | |
535 | (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => { | |
5869c6ff XL |
536 | Zip::zip_with(self, variance, ty_a, ty_b)?; |
537 | Zip::zip_with(self, variance, const_a, const_b) | |
29967ef6 XL |
538 | } |
539 | (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => { | |
5869c6ff XL |
540 | if id_a != id_b { |
541 | return Err(NoSolution); | |
542 | } | |
543 | self.zip_substs( | |
544 | variance, | |
545 | None, | |
546 | substitution_a.as_slice(interner), | |
547 | substitution_b.as_slice(interner), | |
548 | ) | |
29967ef6 XL |
549 | } |
550 | (TyKind::Generator(id_a, substitution_a), TyKind::Generator(id_b, substitution_b)) => { | |
5869c6ff XL |
551 | if id_a != id_b { |
552 | return Err(NoSolution); | |
553 | } | |
554 | self.zip_substs( | |
555 | variance, | |
556 | None, | |
557 | substitution_a.as_slice(interner), | |
558 | substitution_b.as_slice(interner), | |
559 | ) | |
29967ef6 XL |
560 | } |
561 | ( | |
562 | TyKind::GeneratorWitness(id_a, substitution_a), | |
563 | TyKind::GeneratorWitness(id_b, substitution_b), | |
564 | ) => { | |
5869c6ff XL |
565 | if id_a != id_b { |
566 | return Err(NoSolution); | |
567 | } | |
568 | self.zip_substs( | |
569 | variance, | |
570 | None, | |
571 | substitution_a.as_slice(interner), | |
572 | substitution_b.as_slice(interner), | |
573 | ) | |
574 | } | |
575 | (TyKind::Foreign(id_a), TyKind::Foreign(id_b)) => { | |
576 | Zip::zip_with(self, variance, id_a, id_b) | |
29967ef6 | 577 | } |
29967ef6 XL |
578 | (TyKind::Error, TyKind::Error) => Ok(()), |
579 | ||
580 | (_, _) => panic!( | |
f035d41b XL |
581 | "structural mismatch between answer `{:?}` and pending goal `{:?}`", |
582 | answer, pending, | |
583 | ), | |
584 | } | |
585 | } | |
586 | ||
5869c6ff XL |
587 | fn zip_lifetimes( |
588 | &mut self, | |
589 | variance: Variance, | |
590 | answer: &Lifetime<I>, | |
591 | pending: &Lifetime<I>, | |
592 | ) -> Fallible<()> { | |
f035d41b XL |
593 | let interner = self.interner; |
594 | if let Some(pending) = self.table.normalize_lifetime_shallow(interner, pending) { | |
5869c6ff | 595 | return Zip::zip_with(self, variance, answer, &pending); |
f035d41b XL |
596 | } |
597 | ||
598 | if let LifetimeData::BoundVar(answer_depth) = answer.data(interner) { | |
599 | if self.unify_free_answer_var( | |
600 | interner, | |
5869c6ff XL |
601 | self.unification_database, |
602 | variance, | |
f035d41b XL |
603 | *answer_depth, |
604 | GenericArgData::Lifetime(pending.clone()), | |
605 | )? { | |
606 | return Ok(()); | |
607 | } | |
608 | } | |
609 | ||
610 | match (answer.data(interner), pending.data(interner)) { | |
611 | (LifetimeData::BoundVar(answer_depth), LifetimeData::BoundVar(pending_depth)) => { | |
612 | self.assert_matching_vars(*answer_depth, *pending_depth) | |
613 | } | |
614 | ||
29967ef6 | 615 | (LifetimeData::Static, LifetimeData::Static) |
5869c6ff XL |
616 | | (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_)) |
617 | | (LifetimeData::Erased, LifetimeData::Erased) | |
618 | | (LifetimeData::Empty(_), LifetimeData::Empty(_)) => { | |
f035d41b XL |
619 | assert_eq!(answer, pending); |
620 | Ok(()) | |
621 | } | |
622 | ||
623 | (LifetimeData::InferenceVar(_), _) | (_, LifetimeData::InferenceVar(_)) => panic!( | |
624 | "unexpected inference var in answer `{:?}` or pending goal `{:?}`", | |
625 | answer, pending, | |
626 | ), | |
627 | ||
29967ef6 XL |
628 | (LifetimeData::Static, _) |
629 | | (LifetimeData::BoundVar(_), _) | |
5869c6ff XL |
630 | | (LifetimeData::Placeholder(_), _) |
631 | | (LifetimeData::Erased, _) | |
632 | | (LifetimeData::Empty(_), _) => panic!( | |
f035d41b XL |
633 | "structural mismatch between answer `{:?}` and pending goal `{:?}`", |
634 | answer, pending, | |
635 | ), | |
636 | ||
5869c6ff | 637 | (LifetimeData::Phantom(void, _), _) => match *void {}, |
f035d41b XL |
638 | } |
639 | } | |
640 | ||
5869c6ff XL |
641 | fn zip_consts( |
642 | &mut self, | |
643 | variance: Variance, | |
644 | answer: &Const<I>, | |
645 | pending: &Const<I>, | |
646 | ) -> Fallible<()> { | |
f035d41b XL |
647 | let interner = self.interner; |
648 | if let Some(pending) = self.table.normalize_const_shallow(interner, pending) { | |
5869c6ff | 649 | return Zip::zip_with(self, variance, answer, &pending); |
f035d41b XL |
650 | } |
651 | ||
652 | let ConstData { | |
653 | ty: answer_ty, | |
654 | value: answer_value, | |
655 | } = answer.data(interner); | |
656 | let ConstData { | |
657 | ty: pending_ty, | |
658 | value: pending_value, | |
659 | } = pending.data(interner); | |
660 | ||
5869c6ff | 661 | self.zip_tys(variance, answer_ty, pending_ty)?; |
f035d41b XL |
662 | |
663 | if let ConstValue::BoundVar(answer_depth) = answer_value { | |
664 | if self.unify_free_answer_var( | |
665 | interner, | |
5869c6ff XL |
666 | self.unification_database, |
667 | variance, | |
f035d41b XL |
668 | *answer_depth, |
669 | GenericArgData::Const(pending.clone()), | |
670 | )? { | |
671 | return Ok(()); | |
672 | } | |
673 | } | |
674 | ||
675 | match (answer_value, pending_value) { | |
676 | (ConstValue::BoundVar(answer_depth), ConstValue::BoundVar(pending_depth)) => { | |
677 | self.assert_matching_vars(*answer_depth, *pending_depth) | |
678 | } | |
679 | ||
680 | (ConstValue::Placeholder(_), ConstValue::Placeholder(_)) => { | |
681 | assert_eq!(answer, pending); | |
682 | Ok(()) | |
683 | } | |
684 | ||
685 | (ConstValue::Concrete(c1), ConstValue::Concrete(c2)) => { | |
686 | assert!(c1.const_eq(answer_ty, c2, interner)); | |
687 | Ok(()) | |
688 | } | |
689 | ||
690 | (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => panic!( | |
691 | "unexpected inference var in answer `{:?}` or pending goal `{:?}`", | |
692 | answer, pending, | |
693 | ), | |
694 | ||
695 | (ConstValue::BoundVar(_), _) | |
696 | | (ConstValue::Placeholder(_), _) | |
697 | | (ConstValue::Concrete(_), _) => panic!( | |
698 | "structural mismatch between answer `{:?}` and pending goal `{:?}`", | |
699 | answer, pending, | |
700 | ), | |
701 | } | |
702 | } | |
703 | ||
5869c6ff XL |
704 | fn zip_binders<T>( |
705 | &mut self, | |
706 | variance: Variance, | |
707 | answer: &Binders<T>, | |
708 | pending: &Binders<T>, | |
709 | ) -> Fallible<()> | |
f035d41b XL |
710 | where |
711 | T: HasInterner<Interner = I> + Zip<I> + Fold<I, Result = T>, | |
712 | { | |
713 | self.outer_binder.shift_in(); | |
5869c6ff XL |
714 | Zip::zip_with( |
715 | self, | |
716 | variance, | |
717 | answer.skip_binders(), | |
718 | pending.skip_binders(), | |
719 | )?; | |
f035d41b XL |
720 | self.outer_binder.shift_out(); |
721 | Ok(()) | |
722 | } | |
723 | ||
724 | fn interner(&self) -> &'i I { | |
725 | self.interner | |
726 | } | |
5869c6ff XL |
727 | |
728 | fn unification_database(&self) -> &dyn UnificationDatabase<I> { | |
729 | self.unification_database | |
730 | } | |
f035d41b | 731 | } |