Skip to content

Commit 1635ed5

Browse files
committed
Auto merge of #780 - lowr:patch/supertrait-assoc-bounds, r=jackh726
Generate `Normalize` clauses for dyn and opaque types When a trait `Trait` has a transitive supertrait defined like `trait SuperTrait: AnotherTrait<Assoc = Ty>`, we've been generating `impl AnotherTrait` for `dyn Trait` and `opaque type T: Trait` but without accounting for the associated type bound. This patch adds `Normalize` clauses that correspond to such bounds. For example, given the following definition ```rust trait SuperTrait where WC { type Assoc where AssocWC; } trait Trait: SuperTrait<Assoc = Ty> {} ``` we generate the following clauses ```rust // for dyn Trait Implemented(dyn Trait: SuperTrait) :- WC Normalize(<dyn Trait as SuperTrait>::Assoc -> Ty) :- WC, AssocWC // this patch adds this // for placeholder !T for opaque type T: Trait Implemented(!T: SuperTrait) :- WC Normalize(<!T as SuperTrait>::Assoc -> Ty) :- WC, AssocWC // this patch adds this ``` I think this doesn't contradict #203 as "we may legitimately assume that all things talking directly about `?Self` are true", but I'm not really sure if this is the right direction. One caveat is that this patch exacerbates "wastefulness" as in [this comment](https://github.com/rust-lang/chalk/blob/1b32e5d9286ca48c50683177419b6f1512a49be5/chalk-solve/src/clauses.rs#L446-L449) as it adds the `Normalize` clauses even when we're trying to prove other kinds of goals. Fixes #777
2 parents df8aa32 + 1346728 commit 1635ed5

File tree

5 files changed

+194
-36
lines changed

5 files changed

+194
-36
lines changed

chalk-solve/src/clauses.rs

+16-1
Original file line numberDiff line numberDiff line change
@@ -624,7 +624,10 @@ pub fn program_clauses_that_could_match<I: Interner>(
624624

625625
if let Some(well_known) = trait_datum.well_known {
626626
builtin_traits::add_builtin_assoc_program_clauses(
627-
db, builder, well_known, self_ty,
627+
db,
628+
builder,
629+
well_known,
630+
self_ty.clone(),
628631
)?;
629632
}
630633

@@ -645,6 +648,18 @@ pub fn program_clauses_that_could_match<I: Interner>(
645648
proj.associated_ty_id,
646649
);
647650
}
651+
652+
// When `self_ty` is dyn type or opaque type, there may be associated type bounds
653+
// for which we generate `Normalize` clauses.
654+
match self_ty.kind(interner) {
655+
// FIXME: see the fixme for the analogous code for Implemented goals.
656+
TyKind::Dyn(_) => dyn_ty::build_dyn_self_ty_clauses(db, builder, self_ty),
657+
TyKind::OpaqueType(id, _) => {
658+
db.opaque_ty_data(*id)
659+
.to_program_clauses(builder, environment);
660+
}
661+
_ => {}
662+
}
648663
}
649664
AliasTy::Opaque(_) => (),
650665
},
+92-35
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,43 @@
1+
use itertools::{Either, Itertools};
12
use rustc_hash::FxHashSet;
23

34
use super::builder::ClauseBuilder;
4-
use crate::RustIrDatabase;
5+
use crate::{split::Split, RustIrDatabase};
56
use chalk_ir::{
6-
fold::shift::Shift, interner::Interner, Binders, BoundVar, DebruijnIndex, TraitId, TraitRef,
7-
WhereClause,
7+
fold::shift::Shift, interner::Interner, AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex,
8+
Normalize, ProjectionTy, TraitId, TraitRef, Ty, WhereClause,
89
};
910

10-
/// Generate `Implemented` clauses for `dyn Trait` and opaque types. We need to generate
11-
/// `Implemented` clauses for all super traits, and for each trait we require
12-
/// its where clauses. (See #203.)
11+
/// Generate `Implemented` and `Normalize` clauses for `dyn Trait` and opaque types.
12+
/// We need to generate those clauses for all super traits, and for each trait we
13+
/// require its where clauses. (See #203)
1314
pub(super) fn push_trait_super_clauses<I: Interner>(
1415
db: &dyn RustIrDatabase<I>,
1516
builder: &mut ClauseBuilder<'_, I>,
1617
trait_ref: TraitRef<I>,
1718
) {
1819
let interner = db.interner();
19-
// Given`trait SuperTrait: WC`, which is a super trait
20+
// Given `trait SuperTrait: WC`, which is a super trait
2021
// of `Trait` (including actually just being the same trait);
2122
// then we want to push
2223
// - for `dyn Trait`:
2324
// `Implemented(dyn Trait: SuperTrait) :- WC`.
2425
// - for placeholder `!T` of `opaque type T: Trait = HiddenTy`:
2526
// `Implemented(!T: SuperTrait) :- WC`
26-
27-
let super_trait_refs =
27+
//
28+
// When `SuperTrait` has `AliasEq` bounds like `trait SuperTrait: AnotherTrait<Assoc = Ty>`,
29+
// we also push
30+
// - for `dyn Trait`:
31+
// `Normalize(<dyn Trait as AnotherTrait>::Assoc -> Ty) :- AssocWC, WC`
32+
// - for placeholder `!T` of `opaque type T: Trait = HiddenTy`:
33+
// `Normalize(<!T as AnotherTrait>::Assoc -> Ty) :- AssocWC, WC`
34+
// where `WC` and `AssocWC` are the where clauses for `AnotherTrait` and `AnotherTrait::Assoc`
35+
// respectively.
36+
let (super_trait_refs, super_trait_proj) =
2837
super_traits(db, trait_ref.trait_id).substitute(interner, &trait_ref.substitution);
2938

3039
for q_super_trait_ref in super_trait_refs {
31-
builder.push_binders(q_super_trait_ref.clone(), |builder, super_trait_ref| {
40+
builder.push_binders(q_super_trait_ref, |builder, super_trait_ref| {
3241
let trait_datum = db.trait_datum(super_trait_ref.trait_id);
3342
let wc = trait_datum
3443
.where_clauses()
@@ -37,12 +46,40 @@ pub(super) fn push_trait_super_clauses<I: Interner>(
3746
builder.push_clause(super_trait_ref, wc);
3847
});
3948
}
49+
50+
for q_super_trait_proj in super_trait_proj {
51+
builder.push_binders(q_super_trait_proj, |builder, (proj, ty)| {
52+
let assoc_ty_datum = db.associated_ty_data(proj.associated_ty_id);
53+
let trait_datum = db.trait_datum(assoc_ty_datum.trait_id);
54+
let assoc_wc = assoc_ty_datum
55+
.binders
56+
.map_ref(|b| &b.where_clauses)
57+
.into_iter()
58+
.map(|wc| wc.cloned().substitute(interner, &proj.substitution));
59+
60+
let impl_params = db.trait_parameters_from_projection(&proj);
61+
let impl_wc = trait_datum
62+
.where_clauses()
63+
.into_iter()
64+
.map(|wc| wc.cloned().substitute(interner, impl_params));
65+
builder.push_clause(
66+
Normalize {
67+
alias: AliasTy::Projection(proj.clone()),
68+
ty,
69+
},
70+
impl_wc.chain(assoc_wc),
71+
);
72+
});
73+
}
4074
}
4175

42-
pub fn super_traits<I: Interner>(
76+
fn super_traits<I: Interner>(
4377
db: &dyn RustIrDatabase<I>,
4478
trait_id: TraitId<I>,
45-
) -> Binders<Vec<Binders<TraitRef<I>>>> {
79+
) -> Binders<(
80+
Vec<Binders<TraitRef<I>>>,
81+
Vec<Binders<(ProjectionTy<I>, Ty<I>)>>,
82+
)> {
4683
let interner = db.interner();
4784
let mut seen_traits = FxHashSet::default();
4885
let trait_datum = db.trait_datum(trait_id);
@@ -57,13 +94,21 @@ pub fn super_traits<I: Interner>(
5794
},
5895
);
5996
let mut trait_refs = Vec::new();
60-
go(db, trait_ref, &mut seen_traits, &mut trait_refs);
97+
let mut aliases = Vec::new();
98+
go(
99+
db,
100+
trait_ref,
101+
&mut seen_traits,
102+
&mut trait_refs,
103+
&mut aliases,
104+
);
61105

62106
fn go<I: Interner>(
63107
db: &dyn RustIrDatabase<I>,
64108
trait_ref: Binders<TraitRef<I>>,
65109
seen_traits: &mut FxHashSet<TraitId<I>>,
66110
trait_refs: &mut Vec<Binders<TraitRef<I>>>,
111+
aliases: &mut Vec<Binders<(ProjectionTy<I>, Ty<I>)>>,
67112
) {
68113
let interner = db.interner();
69114
let trait_id = trait_ref.skip_binders().trait_id;
@@ -73,32 +118,39 @@ pub fn super_traits<I: Interner>(
73118
}
74119
trait_refs.push(trait_ref.clone());
75120
let trait_datum = db.trait_datum(trait_id);
76-
let super_trait_refs = trait_datum
121+
let (super_trait_refs, super_trait_projs): (Vec<_>, Vec<_>) = trait_datum
77122
.binders
78123
.map_ref(|td| {
79124
td.where_clauses
80125
.iter()
81-
.filter_map(|qwc| {
82-
qwc.as_ref().filter_map(|wc| match wc {
83-
WhereClause::Implemented(tr) => {
84-
let self_ty = tr.self_type_parameter(db.interner());
126+
.filter(|qwc| {
127+
let trait_ref = match qwc.skip_binders() {
128+
WhereClause::Implemented(tr) => tr.clone(),
129+
WhereClause::AliasEq(AliasEq {
130+
alias: AliasTy::Projection(p),
131+
..
132+
}) => db.trait_ref_from_projection(p),
133+
_ => return false,
134+
};
135+
// We're looking for where clauses of the form
136+
// `Self: Trait` or `<Self as Trait>::Assoc`. `Self` is
137+
// ^1.0 because we're one binder in.
138+
trait_ref.self_type_parameter(interner).bound_var(interner)
139+
== Some(BoundVar::new(DebruijnIndex::ONE, 0))
140+
})
141+
.cloned()
142+
.partition_map(|qwc| {
143+
let (value, binders) = qwc.into_value_and_skipped_binders();
85144

86-
// We're looking for where clauses
87-
// of the form `Self: Trait`. That's
88-
// ^1.0 because we're one binder in.
89-
if self_ty.bound_var(db.interner())
90-
!= Some(BoundVar::new(DebruijnIndex::ONE, 0))
91-
{
92-
return None;
93-
}
94-
Some(tr.clone())
95-
}
96-
WhereClause::AliasEq(_) => None,
97-
WhereClause::LifetimeOutlives(..) => None,
98-
WhereClause::TypeOutlives(..) => None,
99-
})
145+
match value {
146+
WhereClause::Implemented(tr) => Either::Left(Binders::new(binders, tr)),
147+
WhereClause::AliasEq(AliasEq {
148+
alias: AliasTy::Projection(p),
149+
ty,
150+
}) => Either::Right(Binders::new(binders, (p, ty))),
151+
_ => unreachable!(),
152+
}
100153
})
101-
.collect::<Vec<_>>()
102154
})
103155
// we skip binders on the trait_ref here and add them to the binders
104156
// on the trait ref in the loop below. We could probably avoid this if
@@ -109,10 +161,15 @@ pub fn super_traits<I: Interner>(
109161
// binders of super_trait_ref.
110162
let actual_binders = Binders::new(trait_ref.binders.clone(), q_super_trait_ref);
111163
let q_super_trait_ref = actual_binders.fuse_binders(interner);
112-
go(db, q_super_trait_ref, seen_traits, trait_refs);
164+
go(db, q_super_trait_ref, seen_traits, trait_refs, aliases);
165+
}
166+
for q_super_trait_proj in super_trait_projs {
167+
let actual_binders = Binders::new(trait_ref.binders.clone(), q_super_trait_proj);
168+
let q_super_trait_proj = actual_binders.fuse_binders(interner);
169+
aliases.push(q_super_trait_proj);
113170
}
114171
seen_traits.remove(&trait_id);
115172
}
116173

117-
Binders::new(trait_datum.binders.binders.clone(), trait_refs)
174+
Binders::new(trait_datum.binders.binders.clone(), (trait_refs, aliases))
118175
}

tests/test/existential_types.rs

+25
Original file line numberDiff line numberDiff line change
@@ -406,6 +406,31 @@ fn dyn_associated_type_binding() {
406406
}
407407
}
408408

409+
#[test]
410+
fn dyn_assoc_in_super_trait_bounds() {
411+
test! {
412+
program {
413+
trait Base { type Output; }
414+
trait Trait where Self: Base<Output = usize> {}
415+
}
416+
417+
goal {
418+
forall<'s> {
419+
dyn Trait + 's: Trait
420+
}
421+
} yields {
422+
expect![[r#"Unique"#]]
423+
}
424+
425+
goal {
426+
forall<'s> {
427+
dyn Trait + 's: Base
428+
}
429+
} yields {
430+
expect![[r#"Unique"#]]
431+
}
432+
}
433+
}
409434
#[test]
410435
fn dyn_well_formed() {
411436
test! {

tests/test/opaque_types.rs

+30
Original file line numberDiff line numberDiff line change
@@ -283,3 +283,33 @@ fn opaque_super_trait() {
283283
}
284284
}
285285
}
286+
287+
#[test]
288+
fn opaque_assoc_in_super_trait_bounds() {
289+
test! {
290+
program {
291+
trait Foo {
292+
type A;
293+
}
294+
trait EmptyFoo where Self: Foo<A = ()> { }
295+
impl Foo for i32 {
296+
type A = ();
297+
}
298+
impl<T> EmptyFoo for T where T: Foo<A = ()> { }
299+
300+
opaque type T: EmptyFoo = i32;
301+
}
302+
303+
goal {
304+
T: EmptyFoo
305+
} yields {
306+
expect![[r#"Unique"#]]
307+
}
308+
309+
goal {
310+
T: Foo
311+
} yields {
312+
expect![[r#"Unique"#]]
313+
}
314+
}
315+
}

tests/test/projection.rs

+31
Original file line numberDiff line numberDiff line change
@@ -1158,3 +1158,34 @@ fn projection_to_opaque() {
11581158
}
11591159
}
11601160
}
1161+
1162+
#[test]
1163+
fn projection_from_super_trait_bounds() {
1164+
test! {
1165+
program {
1166+
trait Foo {
1167+
type A;
1168+
}
1169+
trait Bar where Self: Foo<A = ()> {}
1170+
impl Foo for i32 {
1171+
type A = ();
1172+
}
1173+
impl Bar for i32 {}
1174+
opaque type Opaque: Bar = i32;
1175+
}
1176+
1177+
goal {
1178+
forall<'a> {
1179+
<dyn Bar + 'a as Foo>::A = ()
1180+
}
1181+
} yields {
1182+
expect![[r#"Unique"#]]
1183+
}
1184+
1185+
goal {
1186+
<Opaque as Foo>::A = ()
1187+
} yields {
1188+
expect![[r#"Unique"#]]
1189+
}
1190+
}
1191+
}

0 commit comments

Comments
 (0)