Fix binding levels in implied bounds rules

This commit is contained in:
scalexm 2018-11-24 20:17:42 +01:00
parent c0d7803950
commit ea4187a842

View File

@ -211,7 +211,6 @@ fn program_clauses_for_trait<'a, 'tcx>(
let where_clauses = &predicates let where_clauses = &predicates
.iter() .iter()
.map(|(wc, _)| wc.lower()) .map(|(wc, _)| wc.lower())
.map(|wc| wc.subst(tcx, bound_vars))
.collect::<Vec<_>>(); .collect::<Vec<_>>();
// Rule Implied-Bound-From-Trait // Rule Implied-Bound-From-Trait
@ -232,14 +231,13 @@ fn program_clauses_for_trait<'a, 'tcx>(
.map(|wc| { .map(|wc| {
// we move binders to the left // we move binders to the left
wc.map_bound(|goal| ProgramClause { wc.map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(), // FIXME: As where clauses can only bind lifetimes for now, and that named
// bound regions have a def-id, it is safe to just inject `bound_vars` and
// FIXME: As where clauses can only bind lifetimes for now, // `hypotheses` (which contain named vars bound at index `0`) into this
// and that named bound regions have a def-id, it is safe // binding level. This may change if we ever allow where clauses to bind
// to just inject `hypotheses` (which contains named vars bound at index `0`) // types (e.g. for GATs things), because bound types only use a `BoundVar`
// into this binding level. This may change if we ever allow where clauses
// to bind types (e.g., for GATs things), because bound types only use a `BoundVar`
// index (no def-id). // index (no def-id).
goal: goal.subst(tcx, bound_vars).into_from_env_goal(),
hypotheses, hypotheses,
category: ProgramClauseCategory::ImpliedBound, category: ProgramClauseCategory::ImpliedBound,
@ -346,7 +344,6 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
let where_clauses = tcx.predicates_of(def_id).predicates let where_clauses = tcx.predicates_of(def_id).predicates
.iter() .iter()
.map(|(wc, _)| wc.lower()) .map(|(wc, _)| wc.lower())
.map(|wc| wc.subst(tcx, bound_vars))
.collect::<Vec<_>>(); .collect::<Vec<_>>();
// `WellFormed(Ty<...>) :- WC1, ..., WCm` // `WellFormed(Ty<...>) :- WC1, ..., WCm`
@ -355,7 +352,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
hypotheses: tcx.mk_goals( hypotheses: tcx.mk_goals(
where_clauses where_clauses
.iter() .iter()
.cloned() .map(|wc| wc.subst(tcx, bound_vars))
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))), .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
), ),
category: ProgramClauseCategory::WellFormed, category: ProgramClauseCategory::WellFormed,
@ -383,11 +380,10 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
.map(|wc| { .map(|wc| {
// move the binders to the left // move the binders to the left
wc.map_bound(|goal| ProgramClause { wc.map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(), // FIXME: we inject `bound_vars` and `hypotheses` into this binding
// level, which may be incorrect in the future: see the FIXME in
// FIXME: we inject `hypotheses` into this binding level, // `program_clauses_for_trait`.
// which may be incorrect in the future: see the FIXME in goal: goal.subst(tcx, bound_vars).into_from_env_goal(),
// `program_clauses_for_trait`
hypotheses, hypotheses,
category: ProgramClauseCategory::ImpliedBound, category: ProgramClauseCategory::ImpliedBound,