]>
Commit | Line | Data |
---|---|---|
a2a8927a | 1 | use std::ops::ControlFlow; |
f9f354fc XL |
2 | use std::{fmt, iter}; |
3 | ||
1b1a35ee XL |
4 | use crate::{ |
5 | ext::*, goal_builder::GoalBuilder, rust_ir::*, solve::Solver, split::Split, RustIrDatabase, | |
6 | }; | |
7 | use chalk_ir::{ | |
8 | cast::*, | |
9 | fold::shift::Shift, | |
10 | interner::Interner, | |
a2a8927a | 11 | visit::{Visit, Visitor}, |
1b1a35ee XL |
12 | *, |
13 | }; | |
f035d41b | 14 | use tracing::debug; |
f9f354fc XL |
15 | |
16 | #[derive(Debug)] | |
17 | pub enum WfError<I: Interner> { | |
f035d41b | 18 | IllFormedTypeDecl(chalk_ir::AdtId<I>), |
1b1a35ee | 19 | IllFormedOpaqueTypeDecl(chalk_ir::OpaqueTyId<I>), |
f9f354fc XL |
20 | IllFormedTraitImpl(chalk_ir::TraitId<I>), |
21 | } | |
22 | ||
23 | impl<I: Interner> fmt::Display for WfError<I> { | |
24 | fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { | |
25 | match self { | |
26 | WfError::IllFormedTypeDecl(id) => write!( | |
27 | f, | |
28 | "type declaration `{:?}` does not meet well-formedness requirements", | |
29 | id | |
30 | ), | |
1b1a35ee XL |
31 | WfError::IllFormedOpaqueTypeDecl(id) => write!( |
32 | f, | |
33 | "opaque type declaration `{:?}` does not meet well-formedness requirements", | |
34 | id | |
35 | ), | |
f9f354fc XL |
36 | WfError::IllFormedTraitImpl(id) => write!( |
37 | f, | |
38 | "trait impl for `{:?}` does not meet well-formedness requirements", | |
39 | id | |
40 | ), | |
41 | } | |
42 | } | |
43 | } | |
44 | ||
45 | impl<I: Interner> std::error::Error for WfError<I> {} | |
46 | ||
3dfed10e XL |
47 | pub struct WfSolver<'a, I: Interner> { |
48 | db: &'a dyn RustIrDatabase<I>, | |
49 | solver_builder: &'a dyn Fn() -> Box<dyn Solver<I>>, | |
f9f354fc XL |
50 | } |
51 | ||
a2a8927a | 52 | struct InputTypeCollector<I: Interner> { |
f9f354fc | 53 | types: Vec<Ty<I>>, |
a2a8927a | 54 | interner: I, |
f9f354fc XL |
55 | } |
56 | ||
a2a8927a XL |
57 | impl<I: Interner> InputTypeCollector<I> { |
58 | fn new(interner: I) -> Self { | |
f9f354fc XL |
59 | Self { |
60 | types: Vec::new(), | |
61 | interner, | |
62 | } | |
63 | } | |
64 | ||
a2a8927a | 65 | fn types_in(interner: I, value: impl Visit<I>) -> Vec<Ty<I>> { |
f9f354fc XL |
66 | let mut collector = Self::new(interner); |
67 | value.visit_with(&mut collector, DebruijnIndex::INNERMOST); | |
68 | collector.types | |
69 | } | |
70 | } | |
71 | ||
a2a8927a | 72 | impl<I: Interner> Visitor<I> for InputTypeCollector<I> { |
5869c6ff | 73 | type BreakTy = (); |
a2a8927a | 74 | fn as_dyn(&mut self) -> &mut dyn Visitor<I, BreakTy = Self::BreakTy> { |
f9f354fc XL |
75 | self |
76 | } | |
77 | ||
a2a8927a | 78 | fn interner(&self) -> I { |
f9f354fc XL |
79 | self.interner |
80 | } | |
81 | ||
5869c6ff XL |
82 | fn visit_where_clause( |
83 | &mut self, | |
84 | where_clause: &WhereClause<I>, | |
85 | outer_binder: DebruijnIndex, | |
86 | ) -> ControlFlow<()> { | |
f9f354fc XL |
87 | match where_clause { |
88 | WhereClause::AliasEq(alias_eq) => alias_eq | |
89 | .alias | |
90 | .clone() | |
91 | .intern(self.interner) | |
92 | .visit_with(self, outer_binder), | |
5869c6ff | 93 | WhereClause::Implemented(trait_ref) => trait_ref.visit_with(self, outer_binder), |
3dfed10e | 94 | WhereClause::TypeOutlives(TypeOutlives { ty, .. }) => ty.visit_with(self, outer_binder), |
a2a8927a | 95 | WhereClause::LifetimeOutlives(..) => ControlFlow::Continue(()), |
f9f354fc XL |
96 | } |
97 | } | |
98 | ||
5869c6ff | 99 | fn visit_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> ControlFlow<()> { |
f9f354fc XL |
100 | let interner = self.interner(); |
101 | ||
102 | let mut push_ty = || { | |
103 | self.types | |
5869c6ff | 104 | .push(ty.clone().shifted_out_to(interner, outer_binder).unwrap()) |
f9f354fc | 105 | }; |
29967ef6 XL |
106 | match ty.kind(interner) { |
107 | TyKind::Adt(id, substitution) => { | |
108 | push_ty(); | |
109 | id.visit_with(self, outer_binder); | |
5869c6ff | 110 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
111 | } |
112 | TyKind::AssociatedType(assoc_ty, substitution) => { | |
113 | push_ty(); | |
114 | assoc_ty.visit_with(self, outer_binder); | |
5869c6ff | 115 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
116 | } |
117 | TyKind::Scalar(scalar) => { | |
118 | push_ty(); | |
5869c6ff | 119 | scalar.visit_with(self, outer_binder) |
29967ef6 XL |
120 | } |
121 | TyKind::Str => { | |
122 | push_ty(); | |
a2a8927a | 123 | ControlFlow::Continue(()) |
29967ef6 XL |
124 | } |
125 | TyKind::Tuple(arity, substitution) => { | |
126 | push_ty(); | |
127 | arity.visit_with(self, outer_binder); | |
5869c6ff | 128 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
129 | } |
130 | TyKind::OpaqueType(opaque_ty, substitution) => { | |
131 | push_ty(); | |
132 | opaque_ty.visit_with(self, outer_binder); | |
5869c6ff | 133 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
134 | } |
135 | TyKind::Slice(substitution) => { | |
136 | push_ty(); | |
5869c6ff | 137 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
138 | } |
139 | TyKind::FnDef(fn_def, substitution) => { | |
140 | push_ty(); | |
141 | fn_def.visit_with(self, outer_binder); | |
5869c6ff | 142 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
143 | } |
144 | TyKind::Ref(mutability, lifetime, ty) => { | |
145 | push_ty(); | |
146 | mutability.visit_with(self, outer_binder); | |
147 | lifetime.visit_with(self, outer_binder); | |
5869c6ff | 148 | ty.visit_with(self, outer_binder) |
29967ef6 XL |
149 | } |
150 | TyKind::Raw(mutability, substitution) => { | |
151 | push_ty(); | |
152 | mutability.visit_with(self, outer_binder); | |
5869c6ff | 153 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
154 | } |
155 | TyKind::Never => { | |
156 | push_ty(); | |
a2a8927a | 157 | ControlFlow::Continue(()) |
29967ef6 XL |
158 | } |
159 | TyKind::Array(ty, const_) => { | |
160 | push_ty(); | |
5869c6ff XL |
161 | ty.visit_with(self, outer_binder); |
162 | const_.visit_with(self, outer_binder) | |
29967ef6 XL |
163 | } |
164 | TyKind::Closure(_id, substitution) => { | |
165 | push_ty(); | |
5869c6ff | 166 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
167 | } |
168 | TyKind::Generator(_generator, substitution) => { | |
169 | push_ty(); | |
5869c6ff | 170 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
171 | } |
172 | TyKind::GeneratorWitness(_witness, substitution) => { | |
173 | push_ty(); | |
5869c6ff | 174 | substitution.visit_with(self, outer_binder) |
29967ef6 XL |
175 | } |
176 | TyKind::Foreign(_foreign_ty) => { | |
177 | push_ty(); | |
a2a8927a | 178 | ControlFlow::Continue(()) |
29967ef6 XL |
179 | } |
180 | TyKind::Error => { | |
f9f354fc | 181 | push_ty(); |
a2a8927a | 182 | ControlFlow::Continue(()) |
f9f354fc XL |
183 | } |
184 | ||
29967ef6 | 185 | TyKind::Dyn(clauses) => { |
f9f354fc | 186 | push_ty(); |
5869c6ff | 187 | clauses.visit_with(self, outer_binder) |
f9f354fc XL |
188 | } |
189 | ||
29967ef6 | 190 | TyKind::Alias(AliasTy::Projection(proj)) => { |
f9f354fc | 191 | push_ty(); |
5869c6ff | 192 | proj.visit_with(self, outer_binder) |
f9f354fc XL |
193 | } |
194 | ||
29967ef6 | 195 | TyKind::Alias(AliasTy::Opaque(opaque_ty)) => { |
f9f354fc | 196 | push_ty(); |
5869c6ff | 197 | opaque_ty.visit_with(self, outer_binder) |
f9f354fc XL |
198 | } |
199 | ||
29967ef6 | 200 | TyKind::Placeholder(_) => { |
f9f354fc | 201 | push_ty(); |
a2a8927a | 202 | ControlFlow::Continue(()) |
f9f354fc XL |
203 | } |
204 | ||
205 | // Type parameters do not carry any input types (so we can sort of assume they are | |
206 | // always WF). | |
a2a8927a | 207 | TyKind::BoundVar(..) => ControlFlow::Continue(()), |
f9f354fc XL |
208 | |
209 | // Higher-kinded types such as `for<'a> fn(&'a u32)` introduce their own implied | |
210 | // bounds, and these bounds will be enforced upon calling such a function. In some | |
211 | // sense, well-formedness requirements for the input types of an HKT will be enforced | |
212 | // lazily, so no need to include them here. | |
a2a8927a | 213 | TyKind::Function(..) => ControlFlow::Continue(()), |
f9f354fc | 214 | |
29967ef6 | 215 | TyKind::InferenceVar(..) => { |
f9f354fc XL |
216 | panic!("unexpected inference variable in wf rules: {:?}", ty) |
217 | } | |
218 | } | |
219 | } | |
220 | } | |
221 | ||
3dfed10e | 222 | impl<'a, I> WfSolver<'a, I> |
f9f354fc XL |
223 | where |
224 | I: Interner, | |
225 | { | |
226 | /// Constructs a new `WfSolver`. | |
3dfed10e XL |
227 | pub fn new( |
228 | db: &'a dyn RustIrDatabase<I>, | |
229 | solver_builder: &'a dyn Fn() -> Box<dyn Solver<I>>, | |
230 | ) -> Self { | |
231 | Self { db, solver_builder } | |
f9f354fc XL |
232 | } |
233 | ||
f035d41b | 234 | pub fn verify_adt_decl(&self, adt_id: AdtId<I>) -> Result<(), WfError<I>> { |
f9f354fc XL |
235 | let interner = self.db.interner(); |
236 | ||
237 | // Given a struct like | |
238 | // | |
239 | // ```rust | |
240 | // struct Foo<T> where T: Eq { | |
241 | // data: Vec<T> | |
242 | // } | |
243 | // ``` | |
3dfed10e XL |
244 | let adt_datum = self.db.adt_datum(adt_id); |
245 | let is_enum = adt_datum.kind == AdtKind::Enum; | |
f9f354fc XL |
246 | |
247 | let mut gb = GoalBuilder::new(self.db); | |
3dfed10e | 248 | let adt_data = adt_datum |
f9f354fc | 249 | .binders |
3dfed10e | 250 | .map_ref(|b| (&b.variants, &b.where_clauses)); |
f9f354fc XL |
251 | |
252 | // We make a goal like... | |
253 | // | |
254 | // forall<T> { ... } | |
3dfed10e XL |
255 | let wg_goal = gb.forall( |
256 | &adt_data, | |
257 | is_enum, | |
258 | |gb, _, (variants, where_clauses), is_enum| { | |
259 | let interner = gb.interner(); | |
f9f354fc | 260 | |
3dfed10e XL |
261 | // (FromEnv(T: Eq) => ...) |
262 | gb.implies( | |
263 | where_clauses | |
264 | .iter() | |
265 | .cloned() | |
266 | .map(|wc| wc.into_from_env_goal(interner)), | |
267 | |gb| { | |
268 | let sub_goals: Vec<_> = variants | |
269 | .iter() | |
270 | .flat_map(|variant| { | |
271 | let fields = &variant.fields; | |
272 | ||
273 | // When checking if Enum is well-formed, we require that all fields of | |
274 | // each variant are sized. For `structs`, we relax this requirement to | |
275 | // all but the last field. | |
276 | let sized_constraint_goal = | |
1b1a35ee | 277 | WfWellKnownConstraints::struct_sized_constraint( |
3dfed10e XL |
278 | gb.db(), |
279 | fields, | |
280 | is_enum, | |
281 | ); | |
282 | ||
283 | // WellFormed(Vec<T>), for each field type `Vec<T>` or type that appears in the where clauses | |
284 | let types = InputTypeCollector::types_in( | |
285 | gb.interner(), | |
286 | (&fields, &where_clauses), | |
287 | ); | |
288 | ||
289 | types | |
290 | .into_iter() | |
291 | .map(|ty| ty.well_formed().cast(interner)) | |
292 | .chain(sized_constraint_goal.into_iter()) | |
293 | }) | |
294 | .collect(); | |
295 | ||
296 | gb.all(sub_goals) | |
297 | }, | |
298 | ) | |
299 | }, | |
300 | ); | |
f9f354fc XL |
301 | |
302 | let wg_goal = wg_goal.into_closed_goal(interner); | |
3dfed10e | 303 | let mut fresh_solver = (self.solver_builder)(); |
1b1a35ee | 304 | let is_legal = fresh_solver.has_unique_solution(self.db, &wg_goal); |
f9f354fc XL |
305 | |
306 | if !is_legal { | |
f035d41b | 307 | Err(WfError::IllFormedTypeDecl(adt_id)) |
f9f354fc XL |
308 | } else { |
309 | Ok(()) | |
310 | } | |
311 | } | |
312 | ||
313 | pub fn verify_trait_impl(&self, impl_id: ImplId<I>) -> Result<(), WfError<I>> { | |
314 | let interner = self.db.interner(); | |
315 | ||
316 | let impl_datum = self.db.impl_datum(impl_id); | |
317 | let trait_id = impl_datum.trait_id(); | |
318 | ||
319 | let impl_goal = Goal::all( | |
320 | interner, | |
321 | impl_header_wf_goal(self.db, impl_id).into_iter().chain( | |
322 | impl_datum | |
323 | .associated_ty_value_ids | |
324 | .iter() | |
325 | .filter_map(|&id| compute_assoc_ty_goal(self.db, id)), | |
326 | ), | |
327 | ); | |
328 | ||
1b1a35ee XL |
329 | if let Some(well_known) = self.db.trait_datum(trait_id).well_known { |
330 | self.verify_well_known_impl(impl_id, well_known)? | |
331 | } | |
332 | ||
f9f354fc XL |
333 | debug!("WF trait goal: {:?}", impl_goal); |
334 | ||
3dfed10e | 335 | let mut fresh_solver = (self.solver_builder)(); |
1b1a35ee XL |
336 | let is_legal = |
337 | fresh_solver.has_unique_solution(self.db, &impl_goal.into_closed_goal(interner)); | |
f9f354fc XL |
338 | |
339 | if is_legal { | |
340 | Ok(()) | |
341 | } else { | |
342 | Err(WfError::IllFormedTraitImpl(trait_id)) | |
343 | } | |
344 | } | |
1b1a35ee XL |
345 | |
346 | pub fn verify_opaque_ty_decl(&self, opaque_ty_id: OpaqueTyId<I>) -> Result<(), WfError<I>> { | |
347 | // Given an opaque type like | |
348 | // ```notrust | |
349 | // opaque type Foo<T>: Clone where T: Bar = Baz; | |
350 | // ``` | |
351 | let interner = self.db.interner(); | |
352 | ||
353 | let mut gb = GoalBuilder::new(self.db); | |
354 | ||
355 | let datum = self.db.opaque_ty_data(opaque_ty_id); | |
356 | let bound = &datum.bound; | |
357 | ||
358 | // We make a goal like | |
359 | // | |
360 | // forall<T> | |
5e7ed085 | 361 | let goal = gb.forall(bound, opaque_ty_id, |gb, _, bound, opaque_ty_id| { |
1b1a35ee XL |
362 | let interner = gb.interner(); |
363 | ||
364 | let subst = Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id)); | |
365 | ||
5869c6ff XL |
366 | let bounds = bound.bounds.clone().substitute(interner, &subst); |
367 | let where_clauses = bound.where_clauses.clone().substitute(interner, &subst); | |
1b1a35ee XL |
368 | |
369 | let clauses = where_clauses | |
370 | .iter() | |
371 | .cloned() | |
372 | .map(|wc| wc.into_from_env_goal(interner)); | |
373 | ||
374 | // if (WellFormed(T: Bar)) | |
375 | gb.implies(clauses, |gb| { | |
376 | let interner = gb.interner(); | |
377 | ||
378 | // all(WellFormed(Baz: Clone)) | |
379 | gb.all( | |
380 | bounds | |
381 | .iter() | |
382 | .cloned() | |
383 | .map(|b| b.into_well_formed_goal(interner)), | |
384 | ) | |
385 | }) | |
386 | }); | |
387 | ||
388 | debug!("WF opaque type goal: {:#?}", goal); | |
389 | ||
390 | let mut new_solver = (self.solver_builder)(); | |
391 | let is_legal = new_solver.has_unique_solution(self.db, &goal.into_closed_goal(interner)); | |
392 | ||
393 | if is_legal { | |
394 | Ok(()) | |
395 | } else { | |
396 | Err(WfError::IllFormedOpaqueTypeDecl(opaque_ty_id)) | |
397 | } | |
398 | } | |
399 | ||
400 | /// Verify builtin rules for well-known traits | |
401 | pub fn verify_well_known_impl( | |
402 | &self, | |
403 | impl_id: ImplId<I>, | |
404 | well_known: WellKnownTrait, | |
405 | ) -> Result<(), WfError<I>> { | |
406 | let mut solver = (self.solver_builder)(); | |
407 | let impl_datum = self.db.impl_datum(impl_id); | |
408 | ||
409 | let is_legal = match well_known { | |
410 | WellKnownTrait::Copy => { | |
411 | WfWellKnownConstraints::copy_impl_constraint(&mut *solver, self.db, &impl_datum) | |
412 | } | |
413 | WellKnownTrait::Drop => { | |
414 | WfWellKnownConstraints::drop_impl_constraint(&mut *solver, self.db, &impl_datum) | |
415 | } | |
416 | WellKnownTrait::CoerceUnsized => { | |
417 | WfWellKnownConstraints::coerce_unsized_impl_constraint( | |
418 | &mut *solver, | |
419 | self.db, | |
420 | &impl_datum, | |
421 | ) | |
422 | } | |
5e7ed085 FG |
423 | WellKnownTrait::DispatchFromDyn => { |
424 | WfWellKnownConstraints::dispatch_from_dyn_constraint( | |
425 | &mut *solver, | |
426 | self.db, | |
427 | &impl_datum, | |
428 | ) | |
429 | } | |
1b1a35ee XL |
430 | WellKnownTrait::Clone | WellKnownTrait::Unpin => true, |
431 | // You can't add a manual implementation for the following traits: | |
432 | WellKnownTrait::Fn | |
433 | | WellKnownTrait::FnOnce | |
434 | | WellKnownTrait::FnMut | |
435 | | WellKnownTrait::Unsize | |
5869c6ff | 436 | | WellKnownTrait::Sized |
a2a8927a XL |
437 | | WellKnownTrait::DiscriminantKind |
438 | | WellKnownTrait::Generator => false, | |
1b1a35ee XL |
439 | }; |
440 | ||
441 | if is_legal { | |
442 | Ok(()) | |
443 | } else { | |
444 | Err(WfError::IllFormedTraitImpl(impl_datum.trait_id())) | |
445 | } | |
446 | } | |
f9f354fc XL |
447 | } |
448 | ||
449 | fn impl_header_wf_goal<I: Interner>( | |
450 | db: &dyn RustIrDatabase<I>, | |
451 | impl_id: ImplId<I>, | |
452 | ) -> Option<Goal<I>> { | |
453 | let impl_datum = db.impl_datum(impl_id); | |
454 | ||
455 | if !impl_datum.is_positive() { | |
456 | return None; | |
457 | } | |
458 | ||
459 | let impl_fields = impl_datum | |
460 | .binders | |
461 | .map_ref(|v| (&v.trait_ref, &v.where_clauses)); | |
462 | ||
463 | let mut gb = GoalBuilder::new(db); | |
464 | // forall<P0...Pn> {...} | |
465 | let well_formed_goal = gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| { | |
466 | let interner = gb.interner(); | |
467 | ||
f9f354fc XL |
468 | // if (WC && input types are well formed) { ... } |
469 | gb.implies( | |
5e7ed085 | 470 | impl_wf_environment(interner, where_clauses, trait_ref), |
f9f354fc XL |
471 | |gb| { |
472 | // We retrieve all the input types of the where clauses appearing on the trait impl, | |
473 | // e.g. in: | |
474 | // ``` | |
475 | // impl<T, K> Foo for (T, K) where T: Iterator<Item = (HashSet<K>, Vec<Box<T>>)> { ... } | |
476 | // ``` | |
477 | // we would retrieve `HashSet<K>`, `Box<T>`, `Vec<Box<T>>`, `(HashSet<K>, Vec<Box<T>>)`. | |
478 | // We will have to prove that these types are well-formed (e.g. an additional `K: Hash` | |
479 | // bound would be needed here). | |
480 | let types = InputTypeCollector::types_in(gb.interner(), &where_clauses); | |
481 | ||
482 | // Things to prove well-formed: input types of the where-clauses, projection types | |
483 | // appearing in the header, associated type values, and of course the trait ref. | |
3dfed10e | 484 | debug!(input_types=?types); |
f9f354fc XL |
485 | let goals = types |
486 | .into_iter() | |
487 | .map(|ty| ty.well_formed().cast(interner)) | |
1b1a35ee | 488 | .chain(Some((*trait_ref).clone().well_formed().cast(interner))); |
f9f354fc XL |
489 | |
490 | gb.all::<_, Goal<I>>(goals) | |
491 | }, | |
492 | ) | |
493 | }); | |
494 | ||
1b1a35ee | 495 | Some(well_formed_goal) |
f9f354fc XL |
496 | } |
497 | ||
498 | /// Creates the conditions that an impl (and its contents of an impl) | |
499 | /// can assume to be true when proving that it is well-formed. | |
500 | fn impl_wf_environment<'i, I: Interner>( | |
a2a8927a | 501 | interner: I, |
f9f354fc XL |
502 | where_clauses: &'i [QuantifiedWhereClause<I>], |
503 | trait_ref: &'i TraitRef<I>, | |
504 | ) -> impl Iterator<Item = ProgramClause<I>> + 'i { | |
505 | // if (WC) { ... } | |
506 | let wc = where_clauses | |
507 | .iter() | |
508 | .cloned() | |
509 | .map(move |qwc| qwc.into_from_env_goal(interner).cast(interner)); | |
510 | ||
511 | // We retrieve all the input types of the type on which we implement the trait: we will | |
512 | // *assume* that these types are well-formed, e.g. we will be able to derive that | |
513 | // `K: Hash` holds without writing any where clause. | |
514 | // | |
515 | // Example: | |
516 | // ``` | |
517 | // struct HashSet<K> where K: Hash { ... } | |
518 | // | |
519 | // impl<K> Foo for HashSet<K> { | |
520 | // // Inside here, we can rely on the fact that `K: Hash` holds | |
521 | // } | |
522 | // ``` | |
523 | let types = InputTypeCollector::types_in(interner, trait_ref); | |
524 | ||
525 | let types_wf = types | |
526 | .into_iter() | |
527 | .map(move |ty| ty.into_from_env_goal(interner).cast(interner)); | |
528 | ||
529 | wc.chain(types_wf) | |
530 | } | |
531 | ||
532 | /// Associated type values are special because they can be parametric (independently of | |
533 | /// the impl), so we issue a special goal which is quantified using the binders of the | |
534 | /// associated type value, for example in: | |
535 | /// | |
536 | /// ```ignore | |
537 | /// trait Foo { | |
538 | /// type Item<'a>: Clone where Self: 'a | |
539 | /// } | |
540 | /// | |
541 | /// impl<T> Foo for Box<T> { | |
542 | /// type Item<'a> = Box<&'a T>; | |
543 | /// } | |
544 | /// ``` | |
545 | /// | |
546 | /// we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`. | |
547 | /// | |
548 | /// Note that there is no binder for `T` in the above: the goal we | |
549 | /// generate is expected to be exected in the context of the | |
550 | /// larger WF goal for the impl, which already has such a | |
551 | /// binder. So the entire goal for the impl might be: | |
552 | /// | |
553 | /// ```ignore | |
554 | /// forall<T> { | |
555 | /// WellFormed(Box<T>) /* this comes from the impl, not this routine */, | |
556 | /// forall<'a> { WellFormed(Box<&'a T>) }, | |
557 | /// } | |
558 | /// ``` | |
559 | fn compute_assoc_ty_goal<I: Interner>( | |
560 | db: &dyn RustIrDatabase<I>, | |
561 | assoc_ty_id: AssociatedTyValueId<I>, | |
562 | ) -> Option<Goal<I>> { | |
563 | let mut gb = GoalBuilder::new(db); | |
564 | let assoc_ty = &db.associated_ty_value(assoc_ty_id); | |
565 | ||
566 | // Create `forall<T, 'a> { .. }` | |
567 | Some(gb.forall( | |
568 | &assoc_ty.value.map_ref(|v| &v.ty), | |
569 | assoc_ty_id, | |
570 | |gb, assoc_ty_substitution, value_ty, assoc_ty_id| { | |
571 | let interner = gb.interner(); | |
572 | let db = gb.db(); | |
573 | ||
574 | // Hmm, because `Arc<AssociatedTyValue>` does not implement `Fold`, we can't pass this value through, | |
575 | // just the id, so we have to fetch `assoc_ty` from the database again. | |
576 | // Implementing `Fold` for `AssociatedTyValue` doesn't *quite* seem right though, as that | |
577 | // would result in a deep clone, and the value is inert. We could do some more refatoring | |
578 | // (move the `Arc` behind a newtype, for example) to fix this, but for now doesn't | |
579 | // seem worth it. | |
580 | let assoc_ty = &db.associated_ty_value(assoc_ty_id); | |
581 | ||
582 | let (impl_parameters, projection) = db | |
583 | .impl_parameters_and_projection_from_associated_ty_value( | |
5e7ed085 | 584 | assoc_ty_substitution.as_slice(interner), |
f9f354fc XL |
585 | assoc_ty, |
586 | ); | |
587 | ||
588 | // If (/* impl WF environment */) { ... } | |
589 | let impl_id = assoc_ty.impl_id; | |
590 | let impl_datum = &db.impl_datum(impl_id); | |
591 | let ImplDatumBound { | |
592 | trait_ref: impl_trait_ref, | |
593 | where_clauses: impl_where_clauses, | |
5869c6ff XL |
594 | } = impl_datum |
595 | .binders | |
596 | .clone() | |
597 | .substitute(interner, impl_parameters); | |
f9f354fc XL |
598 | let impl_wf_clauses = |
599 | impl_wf_environment(interner, &impl_where_clauses, &impl_trait_ref); | |
600 | gb.implies(impl_wf_clauses, |gb| { | |
601 | // Get the bounds and where clauses from the trait | |
602 | // declaration, substituted appropriately. | |
603 | // | |
604 | // From our example: | |
605 | // | |
606 | // * bounds | |
607 | // * original in trait, `Clone` | |
608 | // * after substituting impl parameters, `Clone` | |
609 | // * note that the self-type is not yet supplied for bounds, | |
610 | // we will do that later | |
611 | // * where clauses | |
612 | // * original in trait, `Self: 'a` | |
613 | // * after substituting impl parameters, `Box<!T>: '!a` | |
614 | let assoc_ty_datum = db.associated_ty_data(projection.associated_ty_id); | |
615 | let AssociatedTyDatumBound { | |
616 | bounds: defn_bounds, | |
617 | where_clauses: defn_where_clauses, | |
618 | } = assoc_ty_datum | |
619 | .binders | |
5869c6ff | 620 | .clone() |
f9f354fc XL |
621 | .substitute(interner, &projection.substitution); |
622 | ||
623 | // Create `if (/* where clauses on associated type value */) { .. }` | |
624 | gb.implies( | |
625 | defn_where_clauses | |
626 | .iter() | |
627 | .cloned() | |
628 | .map(|qwc| qwc.into_from_env_goal(interner)), | |
629 | |gb| { | |
630 | let types = InputTypeCollector::types_in(gb.interner(), value_ty); | |
631 | ||
632 | // We require that `WellFormed(T)` for each type that appears in the value | |
633 | let wf_goals = types | |
634 | .into_iter() | |
635 | .map(|ty| ty.well_formed()) | |
636 | .casted(interner); | |
637 | ||
638 | // Check that the `value_ty` meets the bounds from the trait. | |
639 | // Here we take the substituted bounds (`defn_bounds`) and we | |
640 | // supply the self-type `value_ty` to yield the final result. | |
641 | // | |
642 | // In our example, the bound was `Clone`, so the combined | |
643 | // result is `Box<!T>: Clone`. This is then converted to a | |
644 | // well-formed goal like `WellFormed(Box<!T>: Clone)`. | |
645 | let bound_goals = defn_bounds | |
646 | .iter() | |
647 | .cloned() | |
648 | .flat_map(|qb| qb.into_where_clauses(interner, (*value_ty).clone())) | |
649 | .map(|qwc| qwc.into_well_formed_goal(interner)) | |
650 | .casted(interner); | |
651 | ||
652 | // Concatenate the WF goals of inner types + the requirements from trait | |
653 | gb.all::<_, Goal<I>>(wf_goals.chain(bound_goals)) | |
654 | }, | |
655 | ) | |
656 | }) | |
657 | }, | |
658 | )) | |
659 | } | |
660 | ||
661 | /// Defines methods to compute well-formedness goals for well-known | |
662 | /// traits (e.g. a goal for all fields of struct in a Copy impl to be Copy) | |
1b1a35ee | 663 | struct WfWellKnownConstraints; |
f9f354fc | 664 | |
1b1a35ee | 665 | impl WfWellKnownConstraints { |
f9f354fc XL |
666 | /// Computes a goal to prove Sized constraints on a struct definition. |
667 | /// Struct is considered well-formed (in terms of Sized) when it either | |
668 | /// has no fields or all of it's fields except the last are proven to be Sized. | |
669 | pub fn struct_sized_constraint<I: Interner>( | |
670 | db: &dyn RustIrDatabase<I>, | |
671 | fields: &[Ty<I>], | |
3dfed10e | 672 | size_all: bool, |
f9f354fc | 673 | ) -> Option<Goal<I>> { |
3dfed10e XL |
674 | let excluded = if size_all { 0 } else { 1 }; |
675 | ||
676 | if fields.len() <= excluded { | |
f9f354fc XL |
677 | return None; |
678 | } | |
679 | ||
680 | let interner = db.interner(); | |
681 | ||
f035d41b | 682 | let sized_trait = db.well_known_trait_id(WellKnownTrait::Sized)?; |
f9f354fc XL |
683 | |
684 | Some(Goal::all( | |
685 | interner, | |
3dfed10e | 686 | fields[..fields.len() - excluded].iter().map(|ty| { |
f9f354fc XL |
687 | TraitRef { |
688 | trait_id: sized_trait, | |
689 | substitution: Substitution::from1(interner, ty.clone()), | |
690 | } | |
691 | .cast(interner) | |
692 | }), | |
693 | )) | |
694 | } | |
695 | ||
1b1a35ee | 696 | /// Verify constraints on a Copy implementation. |
f9f354fc XL |
697 | /// Copy impl is considered well-formed for |
698 | /// a) certain builtin types (scalar values, shared ref, etc..) | |
3dfed10e | 699 | /// b) adts which |
f9f354fc XL |
700 | /// 1) have all Copy fields |
701 | /// 2) don't have a Drop impl | |
702 | fn copy_impl_constraint<I: Interner>( | |
1b1a35ee | 703 | solver: &mut dyn Solver<I>, |
f9f354fc | 704 | db: &dyn RustIrDatabase<I>, |
1b1a35ee XL |
705 | impl_datum: &ImplDatum<I>, |
706 | ) -> bool { | |
f9f354fc XL |
707 | let interner = db.interner(); |
708 | ||
1b1a35ee XL |
709 | let mut gb = GoalBuilder::new(db); |
710 | ||
711 | let impl_fields = impl_datum | |
712 | .binders | |
713 | .map_ref(|v| (&v.trait_ref, &v.where_clauses)); | |
f9f354fc | 714 | |
f035d41b XL |
715 | // Implementations for scalars, pointer types and never type are provided by libcore. |
716 | // User implementations on types other than ADTs are forbidden. | |
1b1a35ee XL |
717 | match impl_datum |
718 | .binders | |
719 | .skip_binders() | |
720 | .trait_ref | |
721 | .self_type_parameter(interner) | |
29967ef6 | 722 | .kind(interner) |
1b1a35ee | 723 | { |
29967ef6 XL |
724 | TyKind::Scalar(_) |
725 | | TyKind::Raw(_, _) | |
726 | | TyKind::Ref(Mutability::Not, _, _) | |
727 | | TyKind::Never => return true, | |
728 | ||
729 | TyKind::Adt(_, _) => (), | |
f035d41b | 730 | |
1b1a35ee | 731 | _ => return false, |
f9f354fc XL |
732 | }; |
733 | ||
1b1a35ee XL |
734 | // Well fomedness goal for ADTs |
735 | let well_formed_goal = | |
736 | gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| { | |
737 | let interner = gb.interner(); | |
f035d41b | 738 | |
1b1a35ee | 739 | let ty = trait_ref.self_type_parameter(interner); |
f035d41b | 740 | |
29967ef6 XL |
741 | let (adt_id, substitution) = match ty.kind(interner) { |
742 | TyKind::Adt(adt_id, substitution) => (*adt_id, substitution), | |
1b1a35ee XL |
743 | |
744 | _ => unreachable!(), | |
745 | }; | |
746 | ||
747 | // if (WC) { ... } | |
748 | gb.implies( | |
5e7ed085 | 749 | impl_wf_environment(interner, where_clauses, trait_ref), |
1b1a35ee XL |
750 | |gb| -> Goal<I> { |
751 | let db = gb.db(); | |
752 | ||
753 | // not { Implemented(ImplSelfTy: Drop) } | |
754 | let neg_drop_goal = | |
755 | db.well_known_trait_id(WellKnownTrait::Drop) | |
756 | .map(|drop_trait_id| { | |
757 | TraitRef { | |
758 | trait_id: drop_trait_id, | |
759 | substitution: Substitution::from1(interner, ty.clone()), | |
760 | } | |
761 | .cast::<Goal<I>>(interner) | |
762 | .negate(interner) | |
763 | }); | |
764 | ||
765 | let adt_datum = db.adt_datum(adt_id); | |
766 | ||
767 | let goals = adt_datum | |
768 | .binders | |
769 | .map_ref(|b| &b.variants) | |
5869c6ff | 770 | .cloned() |
1b1a35ee XL |
771 | .substitute(interner, substitution) |
772 | .into_iter() | |
773 | .flat_map(|v| { | |
774 | v.fields.into_iter().map(|f| { | |
775 | // Implemented(FieldTy: Copy) | |
776 | TraitRef { | |
777 | trait_id: trait_ref.trait_id, | |
778 | substitution: Substitution::from1(interner, f), | |
779 | } | |
780 | .cast(interner) | |
781 | }) | |
782 | }) | |
783 | .chain(neg_drop_goal.into_iter()); | |
784 | gb.all(goals) | |
785 | }, | |
786 | ) | |
787 | }); | |
f9f354fc | 788 | |
1b1a35ee | 789 | solver.has_unique_solution(db, &well_formed_goal.into_closed_goal(interner)) |
f9f354fc XL |
790 | } |
791 | ||
1b1a35ee | 792 | /// Verifies constraints on a Drop implementation |
f9f354fc XL |
793 | /// Drop implementation is considered well-formed if: |
794 | /// a) it's implemented on an ADT | |
795 | /// b) The generic parameters of the impl's type must all be parameters | |
796 | /// of the Drop impl itself (i.e., no specialization like | |
797 | /// `impl Drop for S<Foo> {...}` is allowed). | |
798 | /// c) Any bounds on the genereic parameters of the impl must be | |
799 | /// deductible from the bounds imposed by the struct definition | |
800 | /// (i.e. the implementation must be exactly as generic as the ADT definition). | |
801 | /// | |
802 | /// ```rust,ignore | |
803 | /// struct S<T1, T2> { } | |
804 | /// struct Foo<T> { } | |
805 | /// | |
806 | /// impl<U1: Copy, U2: Sized> Drop for S<U2, Foo<U1>> { } | |
807 | /// ``` | |
808 | /// | |
809 | /// generates the following: | |
810 | /// goal derived from c): | |
811 | /// | |
812 | /// ```notrust | |
813 | /// forall<U1, U2> { | |
814 | /// Implemented(U1: Copy), Implemented(U2: Sized) :- FromEnv(S<U2, Foo<U1>>) | |
815 | /// } | |
816 | /// ``` | |
817 | /// | |
818 | /// goal derived from b): | |
819 | /// ```notrust | |
820 | /// forall <T1, T2> { | |
821 | /// exists<U1, U2> { | |
822 | /// S<T1, T2> = S<U2, Foo<U1>> | |
823 | /// } | |
824 | /// } | |
825 | /// ``` | |
826 | fn drop_impl_constraint<I: Interner>( | |
1b1a35ee | 827 | solver: &mut dyn Solver<I>, |
f9f354fc XL |
828 | db: &dyn RustIrDatabase<I>, |
829 | impl_datum: &ImplDatum<I>, | |
1b1a35ee | 830 | ) -> bool { |
f9f354fc XL |
831 | let interner = db.interner(); |
832 | ||
f035d41b | 833 | let adt_id = match impl_datum.self_type_adt_id(interner) { |
f9f354fc XL |
834 | Some(id) => id, |
835 | // Drop can only be implemented on a nominal type | |
1b1a35ee | 836 | None => return false, |
f9f354fc XL |
837 | }; |
838 | ||
839 | let mut gb = GoalBuilder::new(db); | |
840 | ||
f035d41b | 841 | let adt_datum = db.adt_datum(adt_id); |
f9f354fc XL |
842 | |
843 | let impl_fields = impl_datum | |
844 | .binders | |
845 | .map_ref(|v| (&v.trait_ref, &v.where_clauses)); | |
846 | ||
847 | // forall<ImplP1...ImplPn> { .. } | |
f035d41b | 848 | let implied_by_adt_def_goal = |
f9f354fc XL |
849 | gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| { |
850 | let interner = gb.interner(); | |
851 | ||
852 | // FromEnv(ImplSelfType) => ... | |
853 | gb.implies( | |
854 | iter::once( | |
855 | FromEnv::Ty(trait_ref.self_type_parameter(interner)) | |
856 | .cast::<DomainGoal<I>>(interner), | |
857 | ), | |
858 | |gb| { | |
859 | // All(ImplWhereClauses) | |
860 | gb.all( | |
861 | where_clauses | |
862 | .iter() | |
863 | .map(|wc| wc.clone().into_well_formed_goal(interner)), | |
864 | ) | |
865 | }, | |
866 | ) | |
867 | }); | |
868 | ||
869 | let impl_self_ty = impl_datum | |
870 | .binders | |
871 | .map_ref(|b| b.trait_ref.self_type_parameter(interner)); | |
872 | ||
873 | // forall<StructP1..StructPN> {...} | |
874 | let eq_goal = gb.forall( | |
f035d41b | 875 | &adt_datum.binders, |
29967ef6 XL |
876 | (adt_id, impl_self_ty), |
877 | |gb, substitution, _, (adt_id, impl_self_ty)| { | |
f9f354fc XL |
878 | let interner = gb.interner(); |
879 | ||
29967ef6 | 880 | let def_adt = TyKind::Adt(adt_id, substitution).intern(interner); |
f9f354fc XL |
881 | |
882 | // exists<ImplP1...ImplPn> { .. } | |
f035d41b XL |
883 | gb.exists(&impl_self_ty, def_adt, |gb, _, impl_adt, def_adt| { |
884 | let interner = gb.interner(); | |
885 | ||
886 | // StructName<StructP1..StructPn> = ImplSelfType | |
887 | GoalData::EqGoal(EqGoal { | |
888 | a: GenericArgData::Ty(def_adt).intern(interner), | |
889 | b: GenericArgData::Ty(impl_adt.clone()).intern(interner), | |
890 | }) | |
891 | .intern(interner) | |
892 | }) | |
f9f354fc XL |
893 | }, |
894 | ); | |
895 | ||
1b1a35ee XL |
896 | let well_formed_goal = gb.all([implied_by_adt_def_goal, eq_goal].iter()); |
897 | ||
898 | solver.has_unique_solution(db, &well_formed_goal.into_closed_goal(interner)) | |
899 | } | |
900 | ||
901 | /// Verify constraints a CoerceUnsized impl. | |
902 | /// Rules for CoerceUnsized impl to be considered well-formed: | |
a2a8927a XL |
903 | /// 1) pointer conversions: `&[mut] T -> &[mut] U`, `&[mut] T -> *[mut] U`, |
904 | /// `*[mut] T -> *[mut] U` are considered valid if | |
905 | /// 1) `T: Unsize<U>` | |
1b1a35ee XL |
906 | /// 2) mutability is respected, i.e. immutable -> immutable, mutable -> immutable, |
907 | /// mutable -> mutable conversions are allowed, immutable -> mutable is not. | |
a2a8927a | 908 | /// 2) struct conversions of structures with the same definition, `S<P0...Pn>` -> `S<Q0...Qn>`. |
1b1a35ee XL |
909 | /// To check if this impl is legal, we would walk down the fields of `S` |
910 | /// and consider their types with both substitutes. We are looking to find | |
a2a8927a XL |
911 | /// exactly one (non-phantom) field that has changed its type (from `T` to `U`), and |
912 | /// expect `T` to be unsizeable to `U`, i.e. `T: CoerceUnsized<U>`. | |
5869c6ff | 913 | /// |
1b1a35ee XL |
914 | /// As an example, consider a struct |
915 | /// ```rust | |
916 | /// struct Foo<T, U> { | |
917 | /// extra: T, | |
918 | /// ptr: *mut U, | |
919 | /// } | |
920 | /// ``` | |
921 | /// | |
922 | /// We might have an impl that allows (e.g.) `Foo<T, [i32; 3]>` to be unsized | |
923 | /// to `Foo<T, [i32]>`. That impl would look like: | |
924 | /// ```rust,ignore | |
925 | /// impl<T, U: Unsize<V>, V> CoerceUnsized<Foo<T, V>> for Foo<T, U> {} | |
926 | /// ``` | |
927 | /// In this case: | |
5869c6ff | 928 | /// |
1b1a35ee XL |
929 | /// - `extra` has type `T` before and type `T` after |
930 | /// - `ptr` has type `*mut U` before and type `*mut V` after | |
5869c6ff | 931 | /// |
1b1a35ee XL |
932 | /// Since just one field changed, we would then check that `*mut U: CoerceUnsized<*mut V>` |
933 | /// is implemented. This will work out because `U: Unsize<V>`, and we have a libcore rule | |
934 | /// that `*mut U` can be coerced to `*mut V` if `U: Unsize<V>`. | |
935 | fn coerce_unsized_impl_constraint<I: Interner>( | |
936 | solver: &mut dyn Solver<I>, | |
937 | db: &dyn RustIrDatabase<I>, | |
938 | impl_datum: &ImplDatum<I>, | |
939 | ) -> bool { | |
940 | let interner = db.interner(); | |
941 | let mut gb = GoalBuilder::new(db); | |
942 | ||
943 | let (binders, impl_datum) = impl_datum.binders.as_ref().into(); | |
944 | ||
945 | let trait_ref: &TraitRef<I> = &impl_datum.trait_ref; | |
946 | ||
947 | let source = trait_ref.self_type_parameter(interner); | |
948 | let target = trait_ref | |
949 | .substitution | |
950 | .at(interner, 1) | |
951 | .assert_ty_ref(interner) | |
952 | .clone(); | |
953 | ||
954 | let mut place_in_environment = |goal| -> Goal<I> { | |
955 | gb.forall( | |
956 | &Binders::new( | |
957 | binders.clone(), | |
958 | (goal, trait_ref, &impl_datum.where_clauses), | |
959 | ), | |
960 | (), | |
961 | |gb, _, (goal, trait_ref, where_clauses), ()| { | |
962 | let interner = gb.interner(); | |
963 | gb.implies( | |
5e7ed085 | 964 | impl_wf_environment(interner, where_clauses, trait_ref), |
1b1a35ee XL |
965 | |_| goal, |
966 | ) | |
967 | }, | |
968 | ) | |
969 | }; | |
970 | ||
29967ef6 XL |
971 | match (source.kind(interner), target.kind(interner)) { |
972 | (TyKind::Ref(s_m, _, source), TyKind::Ref(t_m, _, target)) | |
973 | | (TyKind::Ref(s_m, _, source), TyKind::Raw(t_m, target)) | |
974 | | (TyKind::Raw(s_m, source), TyKind::Raw(t_m, target)) => { | |
975 | if (*s_m, *t_m) == (Mutability::Not, Mutability::Mut) { | |
976 | return false; | |
977 | } | |
1b1a35ee | 978 | |
29967ef6 XL |
979 | let unsize_trait_id = |
980 | if let Some(id) = db.well_known_trait_id(WellKnownTrait::Unsize) { | |
981 | id | |
982 | } else { | |
983 | return false; | |
984 | }; | |
985 | ||
986 | // Source: Unsize<Target> | |
987 | let unsize_goal: Goal<I> = TraitRef { | |
988 | trait_id: unsize_trait_id, | |
989 | substitution: Substitution::from_iter( | |
990 | interner, | |
991 | [source.clone(), target.clone()].iter().cloned(), | |
992 | ), | |
993 | } | |
994 | .cast(interner); | |
1b1a35ee | 995 | |
29967ef6 XL |
996 | // ImplEnv -> Source: Unsize<Target> |
997 | let unsize_goal = place_in_environment(unsize_goal); | |
1b1a35ee | 998 | |
29967ef6 XL |
999 | solver.has_unique_solution(db, &unsize_goal.into_closed_goal(interner)) |
1000 | } | |
1001 | (TyKind::Adt(source_id, subst_a), TyKind::Adt(target_id, subst_b)) => { | |
1002 | let adt_datum = db.adt_datum(*source_id); | |
1b1a35ee | 1003 | |
29967ef6 XL |
1004 | if source_id != target_id || adt_datum.kind != AdtKind::Struct { |
1005 | return false; | |
1006 | } | |
1b1a35ee | 1007 | |
29967ef6 XL |
1008 | let fields = adt_datum |
1009 | .binders | |
5869c6ff XL |
1010 | .map_ref(|bound| &bound.variants.last().unwrap().fields) |
1011 | .cloned(); | |
1b1a35ee | 1012 | |
29967ef6 | 1013 | let (source_fields, target_fields) = ( |
5869c6ff | 1014 | fields.clone().substitute(interner, subst_a), |
29967ef6 XL |
1015 | fields.substitute(interner, subst_b), |
1016 | ); | |
1b1a35ee | 1017 | |
29967ef6 XL |
1018 | // collect fields with unequal ids |
1019 | let uneq_field_ids: Vec<usize> = (0..source_fields.len()) | |
1020 | .filter(|&i| { | |
1021 | // ignore phantom data fields | |
1022 | if let Some(adt_id) = source_fields[i].adt_id(interner) { | |
1023 | if db.adt_datum(adt_id).flags.phantom_data { | |
1024 | return false; | |
1025 | } | |
1b1a35ee XL |
1026 | } |
1027 | ||
29967ef6 XL |
1028 | let eq_goal: Goal<I> = EqGoal { |
1029 | a: source_fields[i].clone().cast(interner), | |
1030 | b: target_fields[i].clone().cast(interner), | |
1b1a35ee XL |
1031 | } |
1032 | .cast(interner); | |
1033 | ||
29967ef6 XL |
1034 | // ImplEnv -> Source.fields[i] = Target.fields[i] |
1035 | let eq_goal = place_in_environment(eq_goal); | |
1b1a35ee | 1036 | |
29967ef6 XL |
1037 | // We are interested in !UNEQUAL! fields |
1038 | !solver.has_unique_solution(db, &eq_goal.into_closed_goal(interner)) | |
1039 | }) | |
1040 | .collect(); | |
1041 | ||
1042 | if uneq_field_ids.len() != 1 { | |
1043 | return false; | |
1044 | } | |
1045 | ||
1046 | let field_id = uneq_field_ids[0]; | |
1047 | ||
1048 | // Source.fields[i]: CoerceUnsized<TargetFields[i]> | |
1049 | let coerce_unsized_goal: Goal<I> = TraitRef { | |
1050 | trait_id: trait_ref.trait_id, | |
1051 | substitution: Substitution::from_iter( | |
1052 | interner, | |
1053 | [ | |
1054 | source_fields[field_id].clone(), | |
1055 | target_fields[field_id].clone(), | |
1056 | ] | |
1057 | .iter() | |
1058 | .cloned(), | |
1059 | ), | |
1b1a35ee | 1060 | } |
29967ef6 XL |
1061 | .cast(interner); |
1062 | ||
1063 | // ImplEnv -> Source.fields[i]: CoerceUnsized<TargetFields[i]> | |
1064 | let coerce_unsized_goal = place_in_environment(coerce_unsized_goal); | |
1065 | ||
1066 | solver.has_unique_solution(db, &coerce_unsized_goal.into_closed_goal(interner)) | |
1b1a35ee XL |
1067 | } |
1068 | _ => false, | |
1069 | } | |
f9f354fc | 1070 | } |
5e7ed085 FG |
1071 | |
1072 | /// Verify constraints of a DispatchFromDyn impl. | |
1073 | /// | |
1074 | /// Rules for DispatchFromDyn impl to be considered well-formed: | |
1075 | /// | |
1076 | /// * Self and the type parameter must both be references or raw pointers with the same mutabilty | |
1077 | /// * OR all the following hold: | |
1078 | /// - Self and the type parameter must be structs | |
1079 | /// - Self and the type parameter must have the same definitions | |
1080 | /// - Self must not be `#[repr(packed)]` or `#[repr(C)]` | |
1081 | /// - Self must have exactly one field which is not a 1-ZST (there may be any number of 1-ZST | |
1082 | /// fields), and that field must have a different type in the type parameter (i.e., it is | |
1083 | /// the field being coerced) | |
1084 | /// - `DispatchFromDyn` is implemented for the type of the field being coerced. | |
1085 | fn dispatch_from_dyn_constraint<I: Interner>( | |
1086 | solver: &mut dyn Solver<I>, | |
1087 | db: &dyn RustIrDatabase<I>, | |
1088 | impl_datum: &ImplDatum<I>, | |
1089 | ) -> bool { | |
1090 | let interner = db.interner(); | |
1091 | let mut gb = GoalBuilder::new(db); | |
1092 | ||
1093 | let (binders, impl_datum) = impl_datum.binders.as_ref().into(); | |
1094 | ||
1095 | let trait_ref: &TraitRef<I> = &impl_datum.trait_ref; | |
1096 | ||
1097 | // DispatchFromDyn specifies that Self (source) can be coerced to T (target; its single type parameter). | |
1098 | let source = trait_ref.self_type_parameter(interner); | |
1099 | let target = trait_ref | |
1100 | .substitution | |
1101 | .at(interner, 1) | |
1102 | .assert_ty_ref(interner) | |
1103 | .clone(); | |
1104 | ||
1105 | let mut place_in_environment = |goal| -> Goal<I> { | |
1106 | gb.forall( | |
1107 | &Binders::new( | |
1108 | binders.clone(), | |
1109 | (goal, trait_ref, &impl_datum.where_clauses), | |
1110 | ), | |
1111 | (), | |
1112 | |gb, _, (goal, trait_ref, where_clauses), ()| { | |
1113 | let interner = gb.interner(); | |
1114 | gb.implies( | |
1115 | impl_wf_environment(interner, &where_clauses, &trait_ref), | |
1116 | |_| goal, | |
1117 | ) | |
1118 | }, | |
1119 | ) | |
1120 | }; | |
1121 | ||
1122 | match (source.kind(interner), target.kind(interner)) { | |
1123 | (TyKind::Ref(s_m, _, _), TyKind::Ref(t_m, _, _)) | |
1124 | | (TyKind::Raw(s_m, _), TyKind::Raw(t_m, _)) | |
1125 | if s_m == t_m => | |
1126 | { | |
1127 | true | |
1128 | } | |
1129 | (TyKind::Adt(source_id, subst_a), TyKind::Adt(target_id, subst_b)) => { | |
1130 | let adt_datum = db.adt_datum(*source_id); | |
1131 | ||
1132 | // Definitions are equal and are structs. | |
1133 | if source_id != target_id || adt_datum.kind != AdtKind::Struct { | |
1134 | return false; | |
1135 | } | |
1136 | ||
1137 | // Not repr(C) or repr(packed). | |
1138 | let repr = db.adt_repr(*source_id); | |
1139 | if repr.c || repr.packed { | |
1140 | return false; | |
1141 | } | |
1142 | ||
1143 | // Collect non 1-ZST fields; there must be exactly one. | |
1144 | let fields = adt_datum | |
1145 | .binders | |
1146 | .map_ref(|bound| &bound.variants.last().unwrap().fields) | |
1147 | .cloned(); | |
1148 | ||
1149 | let (source_fields, target_fields) = ( | |
1150 | fields.clone().substitute(interner, subst_a), | |
1151 | fields.substitute(interner, subst_b), | |
1152 | ); | |
1153 | ||
1154 | let mut non_zst_fields: Vec<_> = source_fields | |
1155 | .iter() | |
1156 | .zip(target_fields.iter()) | |
1157 | .filter(|(sf, _)| match sf.adt_id(interner) { | |
1158 | Some(adt) => !db.adt_size_align(adt).one_zst(), | |
1159 | None => true, | |
1160 | }) | |
1161 | .collect(); | |
1162 | ||
1163 | if non_zst_fields.len() != 1 { | |
1164 | return false; | |
1165 | } | |
1166 | ||
1167 | // The field being coerced (the interesting field). | |
1168 | let (field_src, field_tgt) = non_zst_fields.pop().unwrap(); | |
1169 | ||
1170 | // The interesting field is different in the source and target types. | |
1171 | let eq_goal: Goal<I> = EqGoal { | |
1172 | a: field_src.clone().cast(interner), | |
1173 | b: field_tgt.clone().cast(interner), | |
1174 | } | |
1175 | .cast(interner); | |
1176 | let eq_goal = place_in_environment(eq_goal); | |
1177 | if solver.has_unique_solution(db, &eq_goal.into_closed_goal(interner)) { | |
1178 | return false; | |
1179 | } | |
1180 | ||
1181 | // Type(field_src): DispatchFromDyn<Type(field_tgt)> | |
1182 | let field_dispatch_goal: Goal<I> = TraitRef { | |
1183 | trait_id: trait_ref.trait_id, | |
1184 | substitution: Substitution::from_iter( | |
1185 | interner, | |
1186 | [field_src.clone(), field_tgt.clone()].iter().cloned(), | |
1187 | ), | |
1188 | } | |
1189 | .cast(interner); | |
1190 | let field_dispatch_goal = place_in_environment(field_dispatch_goal); | |
1191 | if !solver.has_unique_solution(db, &field_dispatch_goal.into_closed_goal(interner)) | |
1192 | { | |
1193 | return false; | |
1194 | } | |
1195 | ||
1196 | true | |
1197 | } | |
1198 | _ => false, | |
1199 | } | |
1200 | } | |
f9f354fc | 1201 | } |