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 { + // ProjectionEq(>::AssocType = U) :- + // Normalize(>::AssocType -> 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(>::AssocType = U)` + let projection = ty::ProjectionPredicate { + projection_ty, + ty: tcx.mk_ty(ty_var), + }; + + // `Normalize(>::AssocType -> U)` + let hypothesis = tcx.mk_goal( + DomainGoal::Normalize(projection).into_goal() + ); + + // ProjectionEq(>::AssocType = U) :- + // Normalize(>::AssocType -> 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 { ProjectionEq(>::Assoc == ^3) :- Normalize(>::Assoc -> ^3). } = note: forall { FromEnv(Self: Foo) :- FromEnv(Unnormalized(>::Assoc)). } = note: forall { ProjectionEq(>::Assoc == Unnormalized(>::Assoc)). } = note: forall { WellFormed(Unnormalized(>::Assoc)) :- Implemented(Self: Foo). }