1
Fork 0

always emit AliasRelate goals when relating aliases

Add `StructurallyRelateAliases` to allow instantiating infer vars with rigid aliases.
Change `instantiate_query_response` to be infallible in the new solver. This requires canonicalization to not hide any information used by the query, so weaken
universe compression. It also modifies `term_is_fully_unconstrained` to allow
region inference variables in a higher universe.
This commit is contained in:
lcnr 2024-02-26 10:17:43 +01:00
parent eeeb9b4d31
commit 1b3164f5c9
21 changed files with 417 additions and 272 deletions

View file

@ -58,8 +58,6 @@ pub struct GoalEvaluation<'tcx> {
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
pub kind: GoalEvaluationKind<'tcx>,
pub evaluation: CanonicalGoalEvaluation<'tcx>,
/// The nested goals from instantiating the query response.
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
}
#[derive(Eq, PartialEq)]

View file

@ -48,20 +48,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
},
};
writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
if eval.returned_goals.len() > 0 {
writeln!(self.f, "NESTED GOALS ADDED TO CALLER: [")?;
self.nested(|this| {
for goal in eval.returned_goals.iter() {
writeln!(this.f, "ADDED GOAL: {goal:?},")?;
}
Ok(())
})?;
writeln!(self.f, "]")
} else {
Ok(())
}
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
}
pub(super) fn format_canonical_goal_evaluation(