Skip to content

Commit 10013b1

Browse files
nikomatsakisnikomatsakis
committed
use gb for wf conditions on associated type values
1 parent acad3a4 commit 10013b1

File tree

1 file changed

+84
-103
lines changed

1 file changed

+84
-103
lines changed

‎chalk-solve/src/wf.rs

Lines changed: 84 additions & 103 deletions
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,7 @@ where
243243
let goal = gb.forall(
244244
&impl_fields,
245245
&impl_datum.associated_ty_value_ids,
246-
|gb, _, (trait_ref, where_clauses), associated_ty_value_ids| {
246+
|gb, impl_substitution, (trait_ref, where_clauses), associated_ty_value_ids| {
247247
let interner = gb.interner();
248248

249249
// if (WC) { ... }
@@ -275,9 +275,10 @@ where
275275
|gb| {
276276
let db = gb.db();
277277

278-
let assoc_ty_goals = associated_ty_value_ids
279-
.iter()
280-
.filter_map(|&id| Self::compute_assoc_ty_goal(db, id));
278+
let assoc_ty_goals =
279+
associated_ty_value_ids.iter().filter_map(|&id| {
280+
Self::compute_assoc_ty_goal(db, &impl_substitution, id)
281+
});
281282

282283
// We retrieve all the input types of the where clauses appearing on the trait impl,
283284
// e.g. in:
@@ -355,110 +356,90 @@ where
355356
/// ```
356357
fn compute_assoc_ty_goal(
357358
db: &dyn RustIrDatabase<I>,
359+
impl_substitution: &Substitution<I>,
358360
assoc_ty_id: AssociatedTyValueId<I>,
359361
) -> Option<Goal<I>> {
360-
let interner = db.interner();
362+
let mut gb = GoalBuilder::new(db);
361363
let assoc_ty = &db.associated_ty_value(assoc_ty_id);
362364

363-
// Split the binders on the assoc. ty value into those
364-
// from the *impl* (in our example, `T`) and those from
365-
// the associated type (in our example, `'a`).
366-
let (impl_binders, value_binders) =
367-
db.split_associated_ty_value_parameters(&assoc_ty.value.binders, assoc_ty);
368-
369-
// In our final goal, the binders from the impl will be
370-
// something like `^1.N` -- i.e., a debruijn index of 1 --
371-
// and the binders from the associted type value will be `^0.N`.
372-
let all_parameters: Vec<_> = {
373-
let value_parameters = value_binders
374-
.iter()
375-
.zip(0..)
376-
.map(|p| p.to_parameter(interner));
377-
let impl_debruin = DebruijnIndex::INNERMOST.shifted_in();
378-
let impl_parameters = impl_binders
379-
.iter()
380-
.zip(0..)
381-
.map(|p| p.to_parameter_at_depth(interner, impl_debruin));
382-
value_parameters.chain(impl_parameters).collect()
383-
};
384-
385-
// Get the projection for this associated type:
386-
//
387-
// * `projection`: `<Box<!T> as Foo>::Item<'!a>`
388-
let (_, projection) =
389-
db.impl_parameters_and_projection_from_associated_ty_value(&all_parameters, assoc_ty);
390-
391-
// Get the ty that the impl is using -- `Box<&'!a !T>`, in our example
392-
let AssociatedTyValueBound { ty: value_ty } =
393-
assoc_ty.value.substitute(interner, &all_parameters);
394-
395-
let mut input_types = Vec::new();
396-
value_ty.fold(interner, &mut input_types);
397-
398-
// We require that `WellFormed(T)` for each type that appears in the value
399-
let wf_goals = input_types
400-
.into_iter()
401-
.map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)))
402-
.casted(interner);
403-
404-
// Get the bounds and where clauses from the trait
405-
// declaration, substituted appropriately.
406-
//
407-
// From our example:
408-
//
409-
// * bounds
410-
// * original in trait, `Clone`
411-
// * after substituting impl parameters, `Clone`
412-
// * note that the self-type is not yet supplied for bounds,
413-
// we will do that later
414-
// * where clauses
415-
// * original in trait, `Self: 'a`
416-
// * after substituting impl parameters, `Box<!T>: '!a`
417-
let assoc_ty_datum = db.associated_ty_data(projection.associated_ty_id);
418-
let AssociatedTyDatumBound {
419-
bounds: defn_bounds,
420-
where_clauses: defn_where_clauses,
421-
} = assoc_ty_datum
422-
.binders
423-
.substitute(interner, &projection.substitution);
424-
425-
// Check that the `value_ty` meets the bounds from the trait.
426-
// Here we take the substituted bounds (`defn_bounds`) and we
427-
// supply the self-type `value_ty` to yield the final result.
428-
//
429-
// In our example, the bound was `Clone`, so the combined
430-
// result is `Box<!T>: Clone`. This is then converted to a
431-
// well-formed goal like `WellFormed(Box<!T>: Clone)`.
432-
let bound_goals = defn_bounds
433-
.iter()
434-
.cloned()
435-
.flat_map(|qb| qb.into_where_clauses(interner, value_ty.clone()))
436-
.map(|qwc| qwc.into_well_formed_goal(interner))
437-
.casted(interner);
438-
439-
// Concatenate the WF goals of inner types + the requirements from trait
440-
let goals = wf_goals.chain(bound_goals);
441-
let goal = Goal::all(interner, goals);
442-
if goal.is_trivially_true(interner) {
443-
return None;
444-
}
445-
446-
// Add where clauses from the associated ty definition. We must
447-
// substitute parameters here, like we did with the bounds above.
448-
let hypotheses = defn_where_clauses
449-
.iter()
450-
.cloned()
451-
.map(|qwc| qwc.into_from_env_goal(interner))
452-
.casted(interner)
453-
.collect();
454-
455-
let goal = GoalData::Implies(hypotheses, goal).intern(interner);
365+
// Create `forall<'a> { .. }`
366+
Some(gb.partially_forall(
367+
&assoc_ty.value.map_ref(|v| &v.ty),
368+
impl_substitution,
369+
assoc_ty_id,
370+
|gb, assoc_ty_substitution, value_ty, assoc_ty_id| {
371+
let interner = gb.interner();
372+
let db = gb.db();
373+
374+
// Hmm, because `Arc<AssociatedTyValue>` does not implement `Fold`, we can't pass this value through,
375+
// just the id, so we have to fetch `assoc_ty` from the database again.
376+
// Implementing `Fold` for `AssociatedTyValue` doesn't *quite* seem right though, as that
377+
// would result in a deep clone, and the value is inert. We could do some more refatoring
378+
// (move the `Arc` behind a newtype, for example) to fix this, but for now doesn't
379+
// seem worth it.
380+
let assoc_ty = &db.associated_ty_value(assoc_ty_id);
381+
382+
let (_, projection) = db.impl_parameters_and_projection_from_associated_ty_value(
383+
&assoc_ty_substitution.parameters(interner),
384+
assoc_ty,
385+
);
386+
387+
// Get the bounds and where clauses from the trait
388+
// declaration, substituted appropriately.
389+
//
390+
// From our example:
391+
//
392+
// * bounds
393+
// * original in trait, `Clone`
394+
// * after substituting impl parameters, `Clone`
395+
// * note that the self-type is not yet supplied for bounds,
396+
// we will do that later
397+
// * where clauses
398+
// * original in trait, `Self: 'a`
399+
// * after substituting impl parameters, `Box<!T>: '!a`
400+
let assoc_ty_datum = db.associated_ty_data(projection.associated_ty_id);
401+
let AssociatedTyDatumBound {
402+
bounds: defn_bounds,
403+
where_clauses: defn_where_clauses,
404+
} = assoc_ty_datum
405+
.binders
406+
.substitute(interner, &projection.substitution);
407+
408+
// Create `if (/* where clauses on associated type value */) { .. }`
409+
gb.implies(
410+
defn_where_clauses
411+
.iter()
412+
.cloned()
413+
.map(|qwc| qwc.into_from_env_goal(interner)),
414+
|gb| {
415+
let mut input_types = Vec::new();
416+
value_ty.fold(interner, &mut input_types);
456417

457-
debug!("compute_assoc_ty_goal: goal={:?}", goal);
418+
// We require that `WellFormed(T)` for each type that appears in the value
419+
let wf_goals = input_types
420+
.into_iter()
421+
.map(|ty| DomainGoal::WellFormed(WellFormed::Ty(ty)))
422+
.casted(interner);
458423

459-
// Create a composed goal that is universally quantified over
460-
// the parameters from the associated type value (e.g.,
461-
// `forall<'a> { .. }` in our example).
462-
Some(goal.quantify(interner, QuantifierKind::ForAll, value_binders.to_vec()))
424+
// Check that the `value_ty` meets the bounds from the trait.
425+
// Here we take the substituted bounds (`defn_bounds`) and we
426+
// supply the self-type `value_ty` to yield the final result.
427+
//
428+
// In our example, the bound was `Clone`, so the combined
429+
// result is `Box<!T>: Clone`. This is then converted to a
430+
// well-formed goal like `WellFormed(Box<!T>: Clone)`.
431+
let bound_goals = defn_bounds
432+
.iter()
433+
.cloned()
434+
.flat_map(|qb| qb.into_where_clauses(interner, value_ty.clone()))
435+
.map(|qwc| qwc.into_well_formed_goal(interner))
436+
.casted(interner);
437+
438+
// Concatenate the WF goals of inner types + the requirements from trait
439+
gb.all::<_, Goal<I>>(wf_goals.chain(bound_goals))
440+
},
441+
)
442+
},
443+
))
463444
}
464445
}

0 commit comments

Comments
 (0)