Skip to content

Commit

Permalink
Generate clauses for placeholder associated types
Browse files Browse the repository at this point in the history
  • Loading branch information
@lowr
lowr committed Apr 30, 2023
1 parent df8aa32 commit 4699940
Show file tree
Hide file tree
Showing 3 changed files with 102 additions and 10 deletions.
9 changes: 9 additions & 0 deletions chalk-solve/src/clauses.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -440,6 +440,11 @@ pub fn program_clauses_that_could_match<I: Interner>(
.to_program_clauses(builder, environment);
}

TyKind::AssociatedType(assoc_ty_id, _) => {
db.associated_ty_data(*assoc_ty_id)
.to_program_clauses(builder, environment);
}

TyKind::Dyn(_) => {
// If the self type is a `dyn trait` type, generate program-clauses
// that indicates that it implements its own traits.
Expand Down Expand Up @@ -524,6 +529,10 @@ pub fn program_clauses_that_could_match<I: Interner>(
db.opaque_ty_data(*opaque_ty_id)
.to_program_clauses(builder, environment);
}
TyKind::AssociatedType(assoc_ty_id, _) => {
db.associated_ty_data(*assoc_ty_id)
.to_program_clauses(builder, environment);
}
// If the self type is a `dyn trait` type, generate program-clauses
// for any associated type bindings it contains.
// FIXME: see the fixme for the analogous code for Implemented goals.
Expand Down
56 changes: 46 additions & 10 deletions chalk-solve/src/clauses/program_clauses.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -768,6 +768,24 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
/// `AliasEq` to fallback *or* normalize it. So instead we
/// handle this kind of reasoning through the `FromEnv` predicate.
///
/// Another set of clauses we generate for each associated type is about placeholder associated
/// types (i.e. `TyKind::AssociatedType`). Given
///
/// ```notrust
/// trait Foo {
/// type Assoc<'a, T>: Bar<U = Ty> where WC;
/// }
/// ```
///
/// we generate
///
/// ```notrust
/// forall<Self, 'a, T> {
/// Implemented((Foo::Assoc<'a, T>)<Self>: Bar) :- WC.
/// AliasEq(<<(Foo::Assoc<'a, T>)<Self>> as Bar>::U = Ty) :- WC.
/// }
/// ```
///
/// We also generate rules specific to WF requirements and implied bounds:
///
/// ```notrust
Expand Down Expand Up @@ -818,11 +836,11 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {

// Construct an application from the projection. So if we have `<T as Iterator>::Item`,
// we would produce `(Iterator::Item)<T>`.
let ty = TyKind::AssociatedType(self.id, substitution).intern(interner);
let placeholder_ty = TyKind::AssociatedType(self.id, substitution).intern(interner);

let projection_eq = AliasEq {
alias: AliasTy::Projection(projection.clone()),
ty: ty.clone(),
ty: placeholder_ty.clone(),
};

// Fallback rule. The solver uses this to move between the projection
Expand All @@ -839,7 +857,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
// WellFormed((Foo::Assoc)<Self>) :- WellFormed(Self: Foo), WellFormed(WC).
// }
builder.push_clause(
WellFormed::Ty(ty.clone()),
WellFormed::Ty(placeholder_ty.clone()),
iter::once(WellFormed::Trait(trait_ref.clone()).cast::<Goal<_>>(interner))
.chain(
where_clauses
Expand All @@ -856,7 +874,10 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
// forall<Self> {
// FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>).
// }
builder.push_clause(FromEnv::Trait(trait_ref.clone()), Some(ty.from_env()));
builder.push_clause(
FromEnv::Trait(trait_ref.clone()),
Some(placeholder_ty.from_env()),
);

// Reverse rule for where clauses.
//
Expand All @@ -869,18 +890,18 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
builder.push_binders(qwc.clone(), |builder, wc| {
builder.push_clause(
wc.into_from_env_goal(interner),
Some(FromEnv::Ty(ty.clone())),
Some(FromEnv::Ty(placeholder_ty.clone())),
);
});
}

// Reverse rule for implied bounds.
//
// forall<Self> {
// FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
// }
for quantified_bound in bounds {
builder.push_binders(quantified_bound, |builder, bound| {
// Reverse rule for implied bounds.
//
// forall<Self> {
// FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC
// }
for wc in bound.into_where_clauses(interner, projection_ty.clone()) {
builder.push_clause(
wc.into_from_env_goal(interner),
Expand All @@ -890,6 +911,21 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
.chain(where_clauses.iter().cloned().casted(interner)),
);
}

// Rules for the corresponding placeholder type.
//
// When `Foo::Assoc` has a bound `type Assoc: Trait<T = Ty>`, we generate:
//
// forall<Self> {
// Implemented((Foo::Assoc)<Self>: Trait) :- WC
// AliasEq(<(Foo::Assoc)<Self> as Trait>::T = Ty) :- WC
// }
for wc in bound.into_where_clauses(interner, placeholder_ty.clone()) {
builder.push_clause(
wc,
where_clauses.iter().cloned(),
);
}
});
}

Expand Down
47 changes: 47 additions & 0 deletions tests/test/projection.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1158,3 +1158,50 @@ fn projection_to_opaque() {
}
}
}

#[test]
fn clauses_for_placeholder_projection_types() {
test! {
program {
trait Iterator { type Item; }
trait IntoIterator {
type Item;
type IntoIter: Iterator<Item = <Self as IntoIterator>::Item>;
}

struct Vec<T> { }
impl<T> IntoIterator for Vec<T> {
type Item = T;
type IntoIter = Iter<T>;
}

struct Iter<T> { }
impl<T> Iterator for Iter<T> {
type Item = T;
}

opaque type Opaque<T>: IntoIterator<Item = T> = Vec<T>;
}

goal {
forall<T> {
<Opaque<T> as IntoIterator>::IntoIter: Iterator
}
} yields {
expect![[r#"Unique"#]]
}

goal {
forall<T> {
exists<U> {
<<Opaque<T> as IntoIterator>::IntoIter as Iterator>::Item = U
}
}
} yields[SolverChoice::slg_default()] {
// FIXME: chalk#234?
expect![[r#"Ambiguous; no inference guidance"#]]
} yields[SolverChoice::recursive_default()] {
expect![[r#"Unique; substitution [?0 := !1_0]"#]]
}
}
}

0 comments on commit 4699940

Please sign in to comment.