Skip to content

Commit b6f8adb

Browse files
committed
Make dyn Trait implement its super traits as well
This implements the impl rules from #203, as far as I understood them. It doesn't do the well-formedness or object safety rules.
1 parent 1c20731 commit b6f8adb

File tree

8 files changed

+419
-109
lines changed

8 files changed

+419
-109
lines changed

chalk-integration/src/lowering.rs

+1-2
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,12 @@ use chalk_ir::cast::{Cast, Caster};
22
use chalk_ir::interner::{ChalkIr, HasInterner};
33
use chalk_ir::{
44
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds,
5-
QuantifiedWhereClauses, StructId, Substitution, TraitId,
5+
QuantifiedWhereClauses, StructId, Substitution, ToParameter, TraitId,
66
};
77
use chalk_parse::ast::*;
88
use chalk_rust_ir as rust_ir;
99
use chalk_rust_ir::{
1010
Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyDatum, OpaqueTyDatumBound,
11-
ToParameter,
1211
};
1312
use lalrpop_intern::intern;
1413
use std::collections::BTreeMap;

chalk-ir/src/lib.rs

+94
Original file line numberDiff line numberDiff line change
@@ -1250,6 +1250,11 @@ impl<T: HasInterner> Binders<T> {
12501250
Self { binders, value }
12511251
}
12521252

1253+
pub fn empty(interner: &T::Interner, value: T) -> Self {
1254+
let binders = ParameterKinds::new(interner);
1255+
Self { binders, value }
1256+
}
1257+
12531258
/// Skips the binder and returns the "bound" value. This is a
12541259
/// risky thing to do because it's easy to get confused about
12551260
/// De Bruijn indices and the like. `skip_binder` is only valid
@@ -1287,6 +1292,18 @@ impl<T: HasInterner> Binders<T> {
12871292
}
12881293
}
12891294

1295+
pub fn filter_map<U, OP>(self, op: OP) -> Option<Binders<U>>
1296+
where
1297+
OP: FnOnce(T) -> Option<U>,
1298+
U: HasInterner<Interner = T::Interner>,
1299+
{
1300+
let value = op(self.value)?;
1301+
Some(Binders {
1302+
binders: self.binders,
1303+
value,
1304+
})
1305+
}
1306+
12901307
pub fn map_ref<'a, U, OP>(&'a self, op: OP) -> Binders<U>
12911308
where
12921309
OP: FnOnce(&'a T) -> U,
@@ -1295,6 +1312,19 @@ impl<T: HasInterner> Binders<T> {
12951312
self.as_ref().map(op)
12961313
}
12971314

1315+
/// Creates a `Substitution` containing bound vars such that applying this
1316+
/// substitution will not change the value, i.e. `^0.0, ^0.1, ^0.2` and so
1317+
/// on.
1318+
pub fn identity_substitution(&self, interner: &T::Interner) -> Substitution<T::Interner> {
1319+
Substitution::from(
1320+
interner,
1321+
self.binders
1322+
.iter(interner)
1323+
.enumerate()
1324+
.map(|(i, pk)| (pk, i).to_parameter(interner)),
1325+
)
1326+
}
1327+
12981328
/// Creates a fresh binders that contains a single type
12991329
/// variable. The result of the closure will be embedded in this
13001330
/// binder. Note that you should be careful with what you return
@@ -1317,6 +1347,36 @@ impl<T: HasInterner> Binders<T> {
13171347
}
13181348
}
13191349

1350+
impl<T, I> Binders<Binders<T>>
1351+
where
1352+
T: Fold<I, I> + HasInterner<Interner = I>,
1353+
T::Result: HasInterner<Interner = I>,
1354+
I: Interner,
1355+
{
1356+
/// This turns two levels of binders (`for<A> for<B>`) into one level (`for<A, B>`).
1357+
pub fn fuse_binders(self, interner: &T::Interner) -> Binders<T::Result> {
1358+
let num_binders = self.len(interner);
1359+
// generate a substitution to shift the indexes of the inner binder:
1360+
let subst = Substitution::from(
1361+
interner,
1362+
self.value
1363+
.binders
1364+
.iter(interner)
1365+
.enumerate()
1366+
.map(|(i, pk)| (pk, i + num_binders).to_parameter(interner)),
1367+
);
1368+
let value = self.value.substitute(interner, &subst);
1369+
let binders = ParameterKinds::from(
1370+
interner,
1371+
self.binders
1372+
.iter(interner)
1373+
.chain(self.value.binders.iter(interner))
1374+
.cloned(),
1375+
);
1376+
Binders { binders, value }
1377+
}
1378+
}
1379+
13201380
impl<T: HasInterner> From<Binders<T>> for (ParameterKinds<T::Interner>, T) {
13211381
fn from(binders: Binders<T>) -> Self {
13221382
(binders.binders, binders.value)
@@ -2073,6 +2133,40 @@ where
20732133
}
20742134
}
20752135

2136+
pub trait ToParameter {
2137+
/// Utility for converting a list of all the binders into scope
2138+
/// into references to those binders. Simply pair the binders with
2139+
/// the indices, and invoke `to_parameter()` on the `(binder,
2140+
/// index)` pair. The result will be a reference to a bound
2141+
/// variable of appropriate kind at the corresponding index.
2142+
fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
2143+
self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST)
2144+
}
2145+
2146+
fn to_parameter_at_depth<I: Interner>(
2147+
&self,
2148+
interner: &I,
2149+
debruijn: DebruijnIndex,
2150+
) -> Parameter<I>;
2151+
}
2152+
2153+
impl<'a> ToParameter for (&'a ParameterKind<()>, usize) {
2154+
fn to_parameter_at_depth<I: Interner>(
2155+
&self,
2156+
interner: &I,
2157+
debruijn: DebruijnIndex,
2158+
) -> Parameter<I> {
2159+
let &(binder, index) = self;
2160+
let bound_var = BoundVar::new(debruijn, index);
2161+
match *binder {
2162+
ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var)
2163+
.intern(interner)
2164+
.cast(interner),
2165+
ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner),
2166+
}
2167+
}
2168+
}
2169+
20762170
impl<'i, I: Interner> Folder<'i, I> for &SubstFolder<'i, I> {
20772171
fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
20782172
self

chalk-rust-ir/src/lib.rs

+7-37
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,9 @@ use chalk_ir::cast::Cast;
99
use chalk_ir::fold::shift::Shift;
1010
use chalk_ir::interner::{Interner, TargetInterner};
1111
use chalk_ir::{
12-
AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData,
13-
OpaqueTyId, Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId,
14-
Substitution, TraitId, TraitRef, Ty, TyData, TypeName, WhereClause,
12+
AliasEq, AliasTy, AssocTypeId, Binders, DebruijnIndex, ImplId, OpaqueTyId, Parameter,
13+
ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, ToParameter,
14+
TraitId, TraitRef, Ty, TyData, TypeName, WhereClause,
1515
};
1616
use std::iter;
1717

@@ -167,6 +167,10 @@ impl<I: Interner> TraitDatum<I> {
167167
pub fn is_coinductive_trait(&self) -> bool {
168168
self.flags.coinductive
169169
}
170+
171+
pub fn where_clauses(&self) -> Binders<&Vec<QuantifiedWhereClause<I>>> {
172+
self.binders.as_ref().map(|td| &td.where_clauses)
173+
}
170174
}
171175

172176
#[derive(Clone, Debug, PartialEq, Eq, Hash, HasInterner)]
@@ -331,40 +335,6 @@ impl<T> Anonymize for [ParameterKind<T>] {
331335
}
332336
}
333337

334-
pub trait ToParameter {
335-
/// Utility for converting a list of all the binders into scope
336-
/// into references to those binders. Simply pair the binders with
337-
/// the indices, and invoke `to_parameter()` on the `(binder,
338-
/// index)` pair. The result will be a reference to a bound
339-
/// variable of appropriate kind at the corresponding index.
340-
fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
341-
self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST)
342-
}
343-
344-
fn to_parameter_at_depth<I: Interner>(
345-
&self,
346-
interner: &I,
347-
debruijn: DebruijnIndex,
348-
) -> Parameter<I>;
349-
}
350-
351-
impl<'a> ToParameter for (&'a ParameterKind<()>, usize) {
352-
fn to_parameter_at_depth<I: Interner>(
353-
&self,
354-
interner: &I,
355-
debruijn: DebruijnIndex,
356-
) -> Parameter<I> {
357-
let &(binder, index) = self;
358-
let bound_var = BoundVar::new(debruijn, index);
359-
match *binder {
360-
ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var)
361-
.intern(interner)
362-
.cast(interner),
363-
ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner),
364-
}
365-
}
366-
}
367-
368338
/// Represents an associated type declaration found inside of a trait:
369339
///
370340
/// ```notrust

chalk-solve/src/clauses.rs

+13-68
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ use rustc_hash::FxHashSet;
1212

1313
pub mod builder;
1414
mod builtin_traits;
15+
mod dyn_ty;
1516
mod env_elaborator;
1617
mod generalize;
1718
pub mod program_clauses;
@@ -198,76 +199,20 @@ fn program_clauses_that_could_match<I: Interner>(
198199
}
199200
}
200201

201-
// If the self type `S` is a `dyn trait` type, we wish to generate program-clauses
202-
// that indicates that it implements its own traits. For example, a `dyn Write` type
203-
// implements `Write` and so on.
202+
// If the self type is a `dyn trait` type, generate program-clauses
203+
// that indicates that it implements its own traits.
204+
// FIXME: This is presently rather wasteful, in that we don't check that the
205+
// these program clauses we are generating are actually relevant to the goal
206+
// `goal` that we are actually *trying* to prove (though there is some later
207+
// code that will screen out irrelevant stuff).
204208
//
205-
// To see how this works, consider as an example the type `dyn Fn(&u8)`. This is
206-
// really shorthand for `dyn for<'a> Fn<(&'a u8), Output = ()>`, and we represent
207-
// that type as something like this:
208-
//
209-
// ```
210-
// dyn(exists<T> {
211-
// forall<'a> { Implemented(T: Fn<'a>) },
212-
// forall<'a> { AliasEq(<T as Fn<'a>>::Output, ()) },
213-
// })
214-
// ```
215-
//
216-
// so what we will do is to generate one program clause
217-
// for each of the conditions. Thus we get two program
218-
// clauses:
219-
//
220-
// ```
221-
// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
222-
// ```
223-
//
224-
// and
225-
//
226-
// ```
227-
// forall<'a> { AliasEq(<dyn Fn(&u8) as Fn<'a>>::Output, ()) },
228-
// ```
229-
//
230-
// FIXME. This is presently rather wasteful, in that we
231-
// don't check that the these program clauses we are
232-
// generating are actually relevant to the goal `goal`
233-
// that we are actually *trying* to prove (though there is
234-
// some later code that will screen out irrelevant
235-
// stuff).
236-
//
237-
// In other words, in our example, if we were trying to
238-
// prove `Implemented(dyn Fn(&u8): Clone)`, we would have
239-
// generated two clauses that are totally irrelevant to
240-
// that goal, because they let us prove other things but
241-
// not `Clone`.
209+
// In other words, if we were trying to prove `Implemented(dyn
210+
// Fn(&u8): Clone)`, we would still generate two clauses that are
211+
// totally irrelevant to that goal, because they let us prove other
212+
// things but not `Clone`.
242213
let self_ty = trait_ref.self_type_parameter(interner);
243-
if let TyData::Dyn(dyn_ty) = self_ty.data(interner) {
244-
// In this arm, `self_ty` is the `dyn Fn(&u8)`,
245-
// and `bounded_ty` is the `exists<T> { .. }`
246-
// clauses shown above.
247-
248-
// Turn free BoundVars in the type into new existentials. E.g.
249-
// we might get some `dyn Foo<?X>`, and we don't want to return
250-
// a clause with a free variable. We can instead return a
251-
// slightly more general clause by basically turning this into
252-
// `exists<A> dyn Foo<A>`.
253-
let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty);
254-
255-
builder.push_binders(&generalized_dyn_ty, |builder, dyn_ty| {
256-
for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) {
257-
// Replace the `T` from `exists<T> { .. }` with `self_ty`,
258-
// yielding clases like
259-
//
260-
// ```
261-
// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
262-
// ```
263-
let qwc =
264-
exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]);
265-
266-
builder.push_binders(&qwc, |builder, wc| {
267-
builder.push_fact(wc);
268-
});
269-
}
270-
});
214+
if let TyData::Dyn(_) = self_ty.data(interner) {
215+
dyn_ty::build_dyn_self_ty_clauses(db, builder, self_ty.clone())
271216
}
272217

273218
match self_ty.data(interner) {

chalk-solve/src/clauses/builder.rs

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ use crate::RustIrDatabase;
33
use chalk_ir::fold::Fold;
44
use chalk_ir::interner::{HasInterner, Interner};
55
use chalk_ir::*;
6-
use chalk_rust_ir::*;
76
use std::marker::PhantomData;
87

98
/// The "clause builder" is a useful tool for building up sets of

0 commit comments

Comments
 (0)