Skip to content

Require where clauses from the impl on Normalize goal #237

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 3, 2019
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 13 additions & 7 deletions chalk-solve/src/clauses/program_clauses.rs
Original file line number Diff line number Diff line change
@@ -52,7 +52,7 @@ impl ToProgramClauses for AssociatedTyValue {
///
/// Then for the following impl:
/// ```notrust
/// impl<T> Iterable for Vec<T> {
/// impl<T> Iterable for Vec<T> where T: Clone {
/// type IntoIter<'a> = Iter<'a, T>;
/// }
/// ```
@@ -63,7 +63,7 @@ impl ToProgramClauses for AssociatedTyValue {
/// -- Rule Normalize-From-Impl
/// forall<'a, T> {
/// Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :-
/// Implemented(Vec<T>: Iterable), // (1)
/// Implemented(T: Clone), // (1)
/// Implemented(Iter<'a, T>: 'a). // (2)
/// }
/// ```
@@ -109,18 +109,24 @@ impl ToProgramClauses for AssociatedTyValue {
// Assemble the full list of conditions for projection to be valid.
// This comes in two parts, marked as (1) and (2) in doc above:
//
// 1. require that the trait is implemented
// 1. require that the where clauses from the impl apply
// 2. any where-clauses from the `type` declaration in the trait: the
// parameters must be substituted with those of the impl
let where_clauses = associated_ty
let assoc_ty_where_clauses = associated_ty
.where_clauses
.iter()
.map(|wc| Subst::apply(&all_parameters, wc))
.casted();

let conditions: Vec<Goal> = where_clauses
.chain(Some(impl_trait_ref.clone().cast()))
.collect();
let impl_where_clauses = impl_datum
.binders
.value
.where_clauses
.iter()
.map(|wc| wc.shifted_in(self.value.len()))
.casted();

let conditions: Vec<Goal> = assoc_ty_where_clauses.chain(impl_where_clauses).collect();

// Bound parameters + `Self` type of the trait-ref
let parameters: Vec<_> = {
56 changes: 56 additions & 0 deletions src/test.rs
Original file line number Diff line number Diff line change
@@ -549,6 +549,62 @@ fn normalize_basic() {
}
}

#[test]
fn normalize_into_iterator() {
test! {
program {
trait IntoIterator { type Item; }
trait Iterator { type Item; }
struct Vec<T> { }
struct u32 { }
impl<T> IntoIterator for Vec<T> {
type Item = T;
}
impl<T> IntoIterator for T where T: Iterator {
type Item = <T as Iterator>::Item;
}
}

goal {
forall<T> {
exists<U> {
Normalize(<Vec<T> as IntoIterator>::Item -> U)
}
}
} yields {
"Unique"
}
}
}

#[ignore] // currently failing
#[test]
fn projection_equality() {
test! {
program {
trait Trait1 {
type Type;
}
trait Trait2<T> { }
impl<T, U> Trait2<T> for U where U: Trait1<Type = T> {}

struct u32 {}
struct S {}
impl Trait1 for S {
type Type = u32;
}
}

goal {
exists<U> {
S: Trait2<U>
}
} yields {
"Unique"
}
}
}

#[test]
fn normalize_gat1() {
test! {