Skip to content

Commit 35a0647

Browse files
committed
Handle bound vars in builtin trait impls
The builtin impls have the same problem that the dyn trait impl did, which is that they reuse the trait ref as given. The problem with that is that the recursive solver calls `program_clauses` with trait refs that contain bound vars from the original goal. So the builtin impls returned clauses with free bound vars, which is a problem. The solution is the same as for the dyn trait impls: Use the `Generalize` folder to collect those free bound vars and basically put a `forall` around them. To give an example: Looking for ``` Implemented((^0.0, ^0.1): Sized) ``` previously returned something like ``` if (Implemented(^0.1: Sized)) { Implemented((^0.0, ^0.1): Sized) } ``` as a clause; now it returns ``` forall<type, type> if (Implemented(^0.1: Sized)) { Implemented((^0.0, ^0.1): Sized) } ``` (The SLG solver instantiates goals before asking for program clauses, so it has inference variables instead of bound vars in those places.)
1 parent 499d492 commit 35a0647

File tree

5 files changed

+123
-23
lines changed

5 files changed

+123
-23
lines changed

chalk-solve/src/clauses.rs

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -225,13 +225,7 @@ fn program_clauses_that_could_match<I: Interner>(
225225
}
226226

227227
if let Some(well_known) = trait_datum.well_known {
228-
builtin_traits::add_builtin_program_clauses(
229-
db,
230-
builder,
231-
well_known,
232-
trait_ref,
233-
self_ty.data(interner),
234-
);
228+
builtin_traits::add_builtin_program_clauses(db, builder, well_known, trait_ref);
235229
}
236230
}
237231
DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => match &alias_eq.alias {

chalk-solve/src/clauses/builtin_traits.rs

Lines changed: 28 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
use super::builder::ClauseBuilder;
1+
use super::{builder::ClauseBuilder, generalize};
22
use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
3-
use chalk_ir::{Substitution, Ty, TyData};
3+
use chalk_ir::{Substitution, Ty};
44

55
mod clone;
66
mod copy;
@@ -13,22 +13,35 @@ pub fn add_builtin_program_clauses<I: Interner>(
1313
builder: &mut ClauseBuilder<'_, I>,
1414
well_known: WellKnownTrait,
1515
trait_ref: &TraitRef<I>,
16-
ty: &TyData<I>,
1716
) {
18-
if let Some(force_impl) = db.force_impl_for(well_known, ty) {
19-
if force_impl {
20-
builder.push_fact(trait_ref.clone());
17+
// If `trait_ref` contains bound vars, we want to universally quantify them.
18+
// `Generalize` collects them for us.
19+
let generalized = generalize::Generalize::apply(db.interner(), trait_ref);
20+
21+
builder.push_binders(&generalized, |builder, trait_ref| {
22+
let self_ty = trait_ref.self_type_parameter(db.interner());
23+
let ty = self_ty.data(db.interner());
24+
if let Some(force_impl) = db.force_impl_for(well_known, ty) {
25+
if force_impl {
26+
builder.push_fact(trait_ref.clone());
27+
}
28+
return;
2129
}
22-
return;
23-
}
2430

25-
match well_known {
26-
WellKnownTrait::SizedTrait => sized::add_sized_program_clauses(db, builder, trait_ref, ty),
27-
WellKnownTrait::CopyTrait => copy::add_copy_program_clauses(db, builder, trait_ref, ty),
28-
WellKnownTrait::CloneTrait => clone::add_clone_program_clauses(db, builder, trait_ref, ty),
29-
// Drop impls are provided explicitly
30-
WellKnownTrait::DropTrait => (),
31-
}
31+
match well_known {
32+
WellKnownTrait::SizedTrait => {
33+
sized::add_sized_program_clauses(db, builder, &trait_ref, ty)
34+
}
35+
WellKnownTrait::CopyTrait => {
36+
copy::add_copy_program_clauses(db, builder, &trait_ref, ty)
37+
}
38+
WellKnownTrait::CloneTrait => {
39+
clone::add_clone_program_clauses(db, builder, &trait_ref, ty)
40+
}
41+
// Drop impls are provided explicitly
42+
WellKnownTrait::DropTrait => (),
43+
}
44+
});
3245
}
3346

3447
/// Given a trait ref `T0: Trait` and a list of types `U0..Un`, pushes a clause of the form

chalk-solve/src/clauses/generalize.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ impl<'i, I: Interner> Folder<'i, I> for Generalize<'i, I> {
6767
let binder_vec = &mut self.binders;
6868
let new_index = self.mapping.entry(bound_var).or_insert_with(|| {
6969
let i = binder_vec.len();
70-
binder_vec.push(VariableKind::Ty);
70+
binder_vec.push(VariableKind::Lifetime);
7171
i
7272
});
7373
let new_var = BoundVar::new(outer_binder, *new_index);

tests/test/misc.rs

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -515,3 +515,43 @@ fn non_enumerable_traits_reorder() {
515515
}
516516
}
517517
}
518+
519+
#[test]
520+
fn builtin_impl_enumeration() {
521+
test! {
522+
program {
523+
#[lang(copy)]
524+
trait Copy { }
525+
526+
#[lang(sized)]
527+
trait Sized { }
528+
529+
#[lang(clone)]
530+
trait Clone { }
531+
532+
impl Copy for u8 {}
533+
impl Clone for u8 {}
534+
}
535+
536+
goal {
537+
exists<T> { T: Copy }
538+
} yields {
539+
// FIXME: wrong, e.g. &u8 is also Copy
540+
"Unique; substitution [?0 := Uint(U8)]"
541+
}
542+
543+
goal {
544+
exists<T> { T: Clone }
545+
} yields {
546+
// FIXME: wrong, e.g. &u8 is also Clone
547+
"Unique; substitution [?0 := Uint(U8)]"
548+
}
549+
550+
goal {
551+
exists<T> { T: Sized }
552+
} yields {
553+
// FIXME: wrong, most of the built-in types are Sized
554+
"No possible solution"
555+
}
556+
}
557+
}

tests/test/tuples.rs

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,13 +82,41 @@ fn tuples_are_sized() {
8282
} yields {
8383
"Unique; substitution [], lifetime constraints []"
8484
}
85+
86+
goal {
87+
exists<T> { (T, u8): Sized }
88+
} yields {
89+
"Unique; for<?U0> { substitution [?0 := ^0.0], lifetime constraints [] }"
90+
}
91+
92+
goal {
93+
forall<T> { (T, u8): Sized }
94+
} yields {
95+
"Unique; substitution [], lifetime constraints []"
96+
}
97+
98+
goal {
99+
forall<T> { (u8, T): Sized }
100+
} yields {
101+
"No possible solution"
102+
}
103+
104+
goal {
105+
forall<T> { if (T: Sized) { (u8, T): Sized } }
106+
} yields {
107+
"Unique; substitution [], lifetime constraints []"
108+
}
85109
}
86110
}
87111

88112
#[test]
89113
fn tuples_are_copy() {
90114
test! {
91115
program {
116+
// FIXME: If we don't declare Copy non-enumerable, `exists<T> { T:
117+
// Copy }` gives wrong results, because it doesn't consider the
118+
// built-in impls.
119+
#[non_enumerable]
92120
#[lang(copy)]
93121
trait Copy { }
94122

@@ -132,13 +160,26 @@ fn tuples_are_copy() {
132160
} yields {
133161
"Unique; substitution [], lifetime constraints []"
134162
}
163+
164+
goal {
165+
exists<T> { (T, u8): Copy }
166+
} yields {
167+
"Ambiguous"
168+
}
169+
170+
goal {
171+
forall<T> { if (T: Copy) { (T, u8): Copy } }
172+
} yields {
173+
"Unique; substitution [], lifetime constraints []"
174+
}
135175
}
136176
}
137177

138178
#[test]
139179
fn tuples_are_clone() {
140180
test! {
141181
program {
182+
#[non_enumerable] // see above
142183
#[lang(clone)]
143184
trait Clone { }
144185

@@ -182,5 +223,17 @@ fn tuples_are_clone() {
182223
} yields {
183224
"Unique; substitution [], lifetime constraints []"
184225
}
226+
227+
goal {
228+
exists<T> { (T, u8): Clone }
229+
} yields {
230+
"Ambiguous"
231+
}
232+
233+
goal {
234+
forall<T> { if (T: Clone) { (T, u8): Clone } }
235+
} yields {
236+
"Unique; substitution [], lifetime constraints []"
237+
}
185238
}
186239
}

0 commit comments

Comments
 (0)