From e853d6c5b6c4eb6f66569bc86c0655a74ef3897d Mon Sep 17 00:00:00 2001
From: csmoe <35686186+csmoe@users.noreply.github.com>
Date: Sun, 8 Jul 2018 22:28:24 +0800
Subject: [PATCH] Implement `ProjectionEq-Normalize`
---
src/librustc_traits/lowering/mod.rs | 44 ++++++++++++++++++++++++-
src/test/ui/chalkify/lower_trait.stderr | 1 +
2 files changed, 44 insertions(+), 1 deletion(-)
diff --git a/src/librustc_traits/lowering/mod.rs b/src/librustc_traits/lowering/mod.rs
index 471c0e7abbc..83b90cf1bf2 100644
--- a/src/librustc_traits/lowering/mod.rs
+++ b/src/librustc_traits/lowering/mod.rs
@@ -496,9 +496,51 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
};
let from_env_clause = Clause::ForAll(ty::Binder::bind(from_env_clause));
+ // Rule ProjectionEq-Normalize
+ //
+ // ProjectionEq can succeed by normalizing:
+ // ```
+ // forall<Self, P1..Pn, Pn+1..Pm, U> {
+ // ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :-
+ // Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
+ // }
+ // ```
+
+ let offset = tcx.generics_of(trait_id).params
+ .iter()
+ .map(|p| p.index)
+ .max()
+ .unwrap_or(0);
+ // Add a new type param after the existing ones (`U` in the comment above).
+ let ty_var = ty::Bound(
+ ty::BoundTy::new(ty::INNERMOST, ty::BoundVar::from_u32(offset + 1))
+ );
+
+ // `ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U)`
+ let projection = ty::ProjectionPredicate {
+ projection_ty,
+ ty: tcx.mk_ty(ty_var),
+ };
+
+ // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> U)`
+ let hypothesis = tcx.mk_goal(
+ DomainGoal::Normalize(projection).into_goal()
+ );
+
+ // ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :-
+ // Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
+ let normalize_clause = ProgramClause {
+ goal: DomainGoal::Holds(WhereClause::ProjectionEq(projection)),
+ hypotheses: tcx.mk_goals(iter::once(hypothesis)),
+ category: ProgramClauseCategory::Other,
+ };
+ let normalize_clause = Clause::ForAll(ty::Binder::bind(normalize_clause));
+
let clauses = iter::once(projection_eq_clause)
.chain(iter::once(wf_clause))
- .chain(iter::once(from_env_clause));
+ .chain(iter::once(from_env_clause))
+ .chain(iter::once(normalize_clause));
+
tcx.mk_clauses(clauses)
}
diff --git a/src/test/ui/chalkify/lower_trait.stderr b/src/test/ui/chalkify/lower_trait.stderr
index 6a3f7aa6376..c957a2ac7e7 100644
--- a/src/test/ui/chalkify/lower_trait.stderr
+++ b/src/test/ui/chalkify/lower_trait.stderr
@@ -15,6 +15,7 @@ error: program clause dump
LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
+ = note: forall<Self, S, T, ^3> { ProjectionEq(<Self as Foo<S, T>>::Assoc == ^3) :- Normalize(<Self as Foo<S, T>>::Assoc -> ^3). }
= note: forall<Self, S, T> { FromEnv(Self: Foo<S, T>) :- FromEnv(Unnormalized(<Self as Foo<S, T>>::Assoc)). }
= note: forall<Self, S, T> { ProjectionEq(<Self as Foo<S, T>>::Assoc == Unnormalized(<Self as Foo<S, T>>::Assoc)). }
= note: forall<Self, S, T> { WellFormed(Unnormalized(<Self as Foo<S, T>>::Assoc)) :- Implemented(Self: Foo<S, T>). }