summaryrefslogtreecommitdiffstats
path: root/vendor/chalk-engine/src/slg
diff options
context:
space:
mode:
Diffstat (limited to 'vendor/chalk-engine/src/slg')
-rw-r--r--vendor/chalk-engine/src/slg/aggregate.rs642
-rw-r--r--vendor/chalk-engine/src/slg/resolvent.rs731
2 files changed, 1373 insertions, 0 deletions
diff --git a/vendor/chalk-engine/src/slg/aggregate.rs b/vendor/chalk-engine/src/slg/aggregate.rs
new file mode 100644
index 000000000..cce4e14dd
--- /dev/null
+++ b/vendor/chalk-engine/src/slg/aggregate.rs
@@ -0,0 +1,642 @@
+use crate::context::{self, AnswerResult};
+use crate::slg::SlgContextOps;
+use crate::slg::SubstitutionExt;
+use crate::CompleteAnswer;
+use chalk_ir::cast::Cast;
+use chalk_ir::interner::Interner;
+use chalk_ir::*;
+use chalk_solve::ext::*;
+use chalk_solve::infer::InferenceTable;
+use chalk_solve::solve::{Guidance, Solution};
+
+use std::fmt::Debug;
+
+/// Methods for combining solutions to yield an aggregate solution.
+pub trait AggregateOps<I: Interner> {
+ fn make_solution(
+ &self,
+ root_goal: &UCanonical<InEnvironment<Goal<I>>>,
+ answers: impl context::AnswerStream<I>,
+ should_continue: impl std::ops::Fn() -> bool,
+ ) -> Option<Solution<I>>;
+}
+
+/// Draws as many answers as it needs from `answers` (but
+/// no more!) in order to come up with a solution.
+impl<I: Interner> AggregateOps<I> for SlgContextOps<'_, I> {
+ fn make_solution(
+ &self,
+ root_goal: &UCanonical<InEnvironment<Goal<I>>>,
+ mut answers: impl context::AnswerStream<I>,
+ should_continue: impl std::ops::Fn() -> bool,
+ ) -> Option<Solution<I>> {
+ let interner = self.program.interner();
+ let CompleteAnswer { subst, ambiguous } = match answers.next_answer(&should_continue) {
+ AnswerResult::NoMoreSolutions => {
+ // No answers at all
+ return None;
+ }
+ AnswerResult::Answer(answer) => answer,
+ AnswerResult::Floundered => CompleteAnswer {
+ subst: self.identity_constrained_subst(root_goal),
+ ambiguous: true,
+ },
+ AnswerResult::QuantumExceeded => {
+ return Some(Solution::Ambig(Guidance::Unknown));
+ }
+ };
+
+ // Exactly 1 unconditional answer?
+ let next_answer = answers.peek_answer(&should_continue);
+ if next_answer.is_quantum_exceeded() {
+ if subst.value.subst.is_identity_subst(interner) {
+ return Some(Solution::Ambig(Guidance::Unknown));
+ } else {
+ return Some(Solution::Ambig(Guidance::Suggested(
+ subst.map(interner, |cs| cs.subst),
+ )));
+ }
+ }
+ if next_answer.is_no_more_solutions() && !ambiguous {
+ return Some(Solution::Unique(subst));
+ }
+
+ // Otherwise, we either have >1 answer, or else we have
+ // ambiguity. Either way, we are only going to be giving back
+ // **guidance**, and with guidance, the caller doesn't get
+ // back any region constraints. So drop them from our `subst`
+ // variable.
+ //
+ // FIXME-- there is actually a 3rd possibility. We could have
+ // >1 answer where all the answers have the same substitution,
+ // but different region constraints. We should collapse those
+ // cases into an `OR` region constraint at some point, but I
+ // leave that for future work. This is basically
+ // rust-lang/rust#21974.
+ let mut subst = subst.map(interner, |cs| cs.subst);
+
+ // Extract answers and merge them into `subst`. Stop once we have
+ // a trivial subst (or run out of answers).
+ let mut num_answers = 1;
+ let guidance = loop {
+ if subst.value.is_empty(interner) || is_trivial(interner, &subst) {
+ break Guidance::Unknown;
+ }
+
+ if !answers
+ .any_future_answer(|ref mut new_subst| new_subst.may_invalidate(interner, &subst))
+ {
+ break Guidance::Definite(subst);
+ }
+
+ if let Some(expected_answers) = self.expected_answers {
+ if num_answers >= expected_answers {
+ panic!("Too many answers for solution.");
+ }
+ }
+
+ let new_subst = match answers.next_answer(&should_continue) {
+ AnswerResult::Answer(answer1) => answer1.subst,
+ AnswerResult::Floundered => {
+ // FIXME: this doesn't trigger for any current tests
+ self.identity_constrained_subst(root_goal)
+ }
+ AnswerResult::NoMoreSolutions => {
+ break Guidance::Definite(subst);
+ }
+ AnswerResult::QuantumExceeded => {
+ break Guidance::Suggested(subst);
+ }
+ };
+ subst = merge_into_guidance(interner, &root_goal.canonical, subst, &new_subst);
+ num_answers += 1;
+ };
+
+ if let Some(expected_answers) = self.expected_answers {
+ assert_eq!(
+ expected_answers, num_answers,
+ "Not enough answers for solution."
+ );
+ }
+ Some(Solution::Ambig(guidance))
+ }
+}
+
+/// Given a current substitution used as guidance for `root_goal`, and
+/// a new possible answer to `root_goal`, returns a new set of
+/// guidance that encompasses both of them. This is often more general
+/// than the old guidance. For example, if we had a guidance of `?0 =
+/// u32` and the new answer is `?0 = i32`, then the guidance would
+/// become `?0 = ?X` (where `?X` is some fresh variable).
+fn merge_into_guidance<I: Interner>(
+ interner: I,
+ root_goal: &Canonical<InEnvironment<Goal<I>>>,
+ guidance: Canonical<Substitution<I>>,
+ answer: &Canonical<ConstrainedSubst<I>>,
+) -> Canonical<Substitution<I>> {
+ let mut infer = InferenceTable::new();
+ let Canonical {
+ value: ConstrainedSubst {
+ subst: subst1,
+ constraints: _,
+ },
+ binders: _,
+ } = answer;
+
+ // Collect the types that the two substitutions have in
+ // common.
+ let aggr_generic_args: Vec<_> = guidance
+ .value
+ .iter(interner)
+ .zip(subst1.iter(interner))
+ .enumerate()
+ .map(|(index, (p1, p2))| {
+ // We have two values for some variable X that
+ // appears in the root goal. Find out the universe
+ // of X.
+ let universe = *root_goal.binders.as_slice(interner)[index].skip_kind();
+
+ match p1.data(interner) {
+ GenericArgData::Ty(_) => (),
+ GenericArgData::Lifetime(_) => {
+ // Ignore the lifetimes from the substitution: we're just
+ // creating guidance here anyway.
+ return infer
+ .new_variable(universe)
+ .to_lifetime(interner)
+ .cast(interner);
+ }
+ GenericArgData::Const(_) => (),
+ };
+
+ // Combine the two types into a new type.
+ let mut aggr = AntiUnifier {
+ infer: &mut infer,
+ universe,
+ interner,
+ };
+ aggr.aggregate_generic_args(p1, p2)
+ })
+ .collect();
+
+ let aggr_subst = Substitution::from_iter(interner, aggr_generic_args);
+
+ infer.canonicalize(interner, aggr_subst).quantified
+}
+
+fn is_trivial<I: Interner>(interner: I, subst: &Canonical<Substitution<I>>) -> bool {
+ // A subst is trivial if..
+ subst
+ .value
+ .iter(interner)
+ .enumerate()
+ .all(|(index, parameter)| {
+ let is_trivial = |b: Option<BoundVar>| match b {
+ None => false,
+ Some(bound_var) => {
+ if let Some(index1) = bound_var.index_if_innermost() {
+ index == index1
+ } else {
+ false
+ }
+ }
+ };
+
+ match parameter.data(interner) {
+ // All types and consts are mapped to distinct variables. Since this
+ // has been canonicalized, those will also be the first N
+ // variables.
+ GenericArgData::Ty(t) => is_trivial(t.bound_var(interner)),
+ GenericArgData::Const(t) => is_trivial(t.bound_var(interner)),
+
+ // And no lifetime mappings. (This is too strict, but we never
+ // product substs with lifetimes.)
+ GenericArgData::Lifetime(_) => false,
+ }
+ })
+}
+
+/// [Anti-unification] is the act of taking two things that do not
+/// unify and finding a minimal generalization of them. So for
+/// example `Vec<u32>` anti-unified with `Vec<i32>` might be
+/// `Vec<?X>`. This is a **very simplistic** anti-unifier.
+///
+/// NOTE: The values here are canonicalized, but output is not, this means
+/// that any escaping bound variables that we see have to be replaced with
+/// inference variables.
+///
+/// [Anti-unification]: https://en.wikipedia.org/wiki/Anti-unification_(computer_science)
+struct AntiUnifier<'infer, I: Interner> {
+ infer: &'infer mut InferenceTable<I>,
+ universe: UniverseIndex,
+ interner: I,
+}
+
+impl<I: Interner> AntiUnifier<'_, I> {
+ fn aggregate_tys(&mut self, ty0: &Ty<I>, ty1: &Ty<I>) -> Ty<I> {
+ let interner = self.interner;
+ match (ty0.kind(interner), ty1.kind(interner)) {
+ // If we see bound things on either side, just drop in a
+ // fresh variable. This means we will sometimes
+ // overgeneralize. So for example if we have two
+ // solutions that are both `(X, X)`, we just produce `(Y,
+ // Z)` in all cases.
+ (TyKind::InferenceVar(_, _), TyKind::InferenceVar(_, _)) => self.new_ty_variable(),
+
+ // Ugh. Aggregating two types like `for<'a> fn(&'a u32,
+ // &'a u32)` and `for<'a, 'b> fn(&'a u32, &'b u32)` seems
+ // kinda hard. Don't try to be smart for now, just plop a
+ // variable in there and be done with it.
+ // This also ensures that any bound variables we do see
+ // were bound by `Canonical`.
+ (TyKind::BoundVar(_), TyKind::BoundVar(_))
+ | (TyKind::Function(_), TyKind::Function(_))
+ | (TyKind::Dyn(_), TyKind::Dyn(_)) => self.new_ty_variable(),
+
+ (
+ TyKind::Alias(AliasTy::Projection(proj1)),
+ TyKind::Alias(AliasTy::Projection(proj2)),
+ ) => self.aggregate_projection_tys(proj1, proj2),
+
+ (
+ TyKind::Alias(AliasTy::Opaque(opaque_ty1)),
+ TyKind::Alias(AliasTy::Opaque(opaque_ty2)),
+ ) => self.aggregate_opaque_ty_tys(opaque_ty1, opaque_ty2),
+
+ (TyKind::Placeholder(placeholder1), TyKind::Placeholder(placeholder2)) => {
+ self.aggregate_placeholder_tys(placeholder1, placeholder2)
+ }
+
+ (TyKind::Adt(id_a, substitution_a), TyKind::Adt(id_b, substitution_b)) => self
+ .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
+ .map(|(&name, substitution)| TyKind::Adt(name, substitution).intern(interner))
+ .unwrap_or_else(|| self.new_ty_variable()),
+ (
+ TyKind::AssociatedType(id_a, substitution_a),
+ TyKind::AssociatedType(id_b, substitution_b),
+ ) => self
+ .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
+ .map(|(&name, substitution)| {
+ TyKind::AssociatedType(name, substitution).intern(interner)
+ })
+ .unwrap_or_else(|| self.new_ty_variable()),
+ (TyKind::Scalar(scalar_a), TyKind::Scalar(scalar_b)) => {
+ if scalar_a == scalar_b {
+ TyKind::Scalar(*scalar_a).intern(interner)
+ } else {
+ self.new_ty_variable()
+ }
+ }
+ (TyKind::Str, TyKind::Str) => TyKind::Str.intern(interner),
+ (TyKind::Tuple(arity_a, substitution_a), TyKind::Tuple(arity_b, substitution_b)) => {
+ self.aggregate_name_and_substs(arity_a, substitution_a, arity_b, substitution_b)
+ .map(|(&name, substitution)| TyKind::Tuple(name, substitution).intern(interner))
+ .unwrap_or_else(|| self.new_ty_variable())
+ }
+ (
+ TyKind::OpaqueType(id_a, substitution_a),
+ TyKind::OpaqueType(id_b, substitution_b),
+ ) => self
+ .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
+ .map(|(&name, substitution)| {
+ TyKind::OpaqueType(name, substitution).intern(interner)
+ })
+ .unwrap_or_else(|| self.new_ty_variable()),
+ (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => {
+ TyKind::Slice(self.aggregate_tys(ty_a, ty_b)).intern(interner)
+ }
+ (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => self
+ .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
+ .map(|(&name, substitution)| TyKind::FnDef(name, substitution).intern(interner))
+ .unwrap_or_else(|| self.new_ty_variable()),
+ (TyKind::Ref(id_a, lifetime_a, ty_a), TyKind::Ref(id_b, lifetime_b, ty_b)) => {
+ if id_a == id_b {
+ TyKind::Ref(
+ *id_a,
+ self.aggregate_lifetimes(lifetime_a, lifetime_b),
+ self.aggregate_tys(ty_a, ty_b),
+ )
+ .intern(interner)
+ } else {
+ self.new_ty_variable()
+ }
+ }
+ (TyKind::Raw(id_a, ty_a), TyKind::Raw(id_b, ty_b)) => {
+ if id_a == id_b {
+ TyKind::Raw(*id_a, self.aggregate_tys(ty_a, ty_b)).intern(interner)
+ } else {
+ self.new_ty_variable()
+ }
+ }
+ (TyKind::Never, TyKind::Never) => TyKind::Never.intern(interner),
+ (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => TyKind::Array(
+ self.aggregate_tys(ty_a, ty_b),
+ self.aggregate_consts(const_a, const_b),
+ )
+ .intern(interner),
+ (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => self
+ .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
+ .map(|(&name, substitution)| TyKind::Closure(name, substitution).intern(interner))
+ .unwrap_or_else(|| self.new_ty_variable()),
+ (TyKind::Generator(id_a, substitution_a), TyKind::Generator(id_b, substitution_b)) => {
+ self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
+ .map(|(&name, substitution)| {
+ TyKind::Generator(name, substitution).intern(interner)
+ })
+ .unwrap_or_else(|| self.new_ty_variable())
+ }
+ (
+ TyKind::GeneratorWitness(id_a, substitution_a),
+ TyKind::GeneratorWitness(id_b, substitution_b),
+ ) => self
+ .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
+ .map(|(&name, substitution)| {
+ TyKind::GeneratorWitness(name, substitution).intern(interner)
+ })
+ .unwrap_or_else(|| self.new_ty_variable()),
+ (TyKind::Foreign(id_a), TyKind::Foreign(id_b)) => {
+ if id_a == id_b {
+ TyKind::Foreign(*id_a).intern(interner)
+ } else {
+ self.new_ty_variable()
+ }
+ }
+ (TyKind::Error, TyKind::Error) => TyKind::Error.intern(interner),
+
+ (_, _) => self.new_ty_variable(),
+ }
+ }
+
+ fn aggregate_placeholder_tys(
+ &mut self,
+ index1: &PlaceholderIndex,
+ index2: &PlaceholderIndex,
+ ) -> Ty<I> {
+ let interner = self.interner;
+ if index1 != index2 {
+ self.new_ty_variable()
+ } else {
+ TyKind::Placeholder(*index1).intern(interner)
+ }
+ }
+
+ fn aggregate_projection_tys(
+ &mut self,
+ proj1: &ProjectionTy<I>,
+ proj2: &ProjectionTy<I>,
+ ) -> Ty<I> {
+ let interner = self.interner;
+ let ProjectionTy {
+ associated_ty_id: name1,
+ substitution: substitution1,
+ } = proj1;
+ let ProjectionTy {
+ associated_ty_id: name2,
+ substitution: substitution2,
+ } = proj2;
+
+ self.aggregate_name_and_substs(name1, substitution1, name2, substitution2)
+ .map(|(&associated_ty_id, substitution)| {
+ TyKind::Alias(AliasTy::Projection(ProjectionTy {
+ associated_ty_id,
+ substitution,
+ }))
+ .intern(interner)
+ })
+ .unwrap_or_else(|| self.new_ty_variable())
+ }
+
+ fn aggregate_opaque_ty_tys(
+ &mut self,
+ opaque_ty1: &OpaqueTy<I>,
+ opaque_ty2: &OpaqueTy<I>,
+ ) -> Ty<I> {
+ let OpaqueTy {
+ opaque_ty_id: name1,
+ substitution: substitution1,
+ } = opaque_ty1;
+ let OpaqueTy {
+ opaque_ty_id: name2,
+ substitution: substitution2,
+ } = opaque_ty2;
+
+ self.aggregate_name_and_substs(name1, substitution1, name2, substitution2)
+ .map(|(&opaque_ty_id, substitution)| {
+ TyKind::Alias(AliasTy::Opaque(OpaqueTy {
+ opaque_ty_id,
+ substitution,
+ }))
+ .intern(self.interner)
+ })
+ .unwrap_or_else(|| self.new_ty_variable())
+ }
+
+ fn aggregate_name_and_substs<N>(
+ &mut self,
+ name1: N,
+ substitution1: &Substitution<I>,
+ name2: N,
+ substitution2: &Substitution<I>,
+ ) -> Option<(N, Substitution<I>)>
+ where
+ N: Copy + Eq + Debug,
+ {
+ let interner = self.interner;
+ if name1 != name2 {
+ return None;
+ }
+
+ let name = name1;
+
+ assert_eq!(
+ substitution1.len(interner),
+ substitution2.len(interner),
+ "does {:?} take {} substitution or {}? can't both be right",
+ name,
+ substitution1.len(interner),
+ substitution2.len(interner)
+ );
+
+ let substitution = Substitution::from_iter(
+ interner,
+ substitution1
+ .iter(interner)
+ .zip(substitution2.iter(interner))
+ .map(|(p1, p2)| self.aggregate_generic_args(p1, p2)),
+ );
+
+ Some((name, substitution))
+ }
+
+ fn aggregate_generic_args(&mut self, p1: &GenericArg<I>, p2: &GenericArg<I>) -> GenericArg<I> {
+ let interner = self.interner;
+ match (p1.data(interner), p2.data(interner)) {
+ (GenericArgData::Ty(ty1), GenericArgData::Ty(ty2)) => {
+ self.aggregate_tys(ty1, ty2).cast(interner)
+ }
+ (GenericArgData::Lifetime(l1), GenericArgData::Lifetime(l2)) => {
+ self.aggregate_lifetimes(l1, l2).cast(interner)
+ }
+ (GenericArgData::Const(c1), GenericArgData::Const(c2)) => {
+ self.aggregate_consts(c1, c2).cast(interner)
+ }
+ (GenericArgData::Ty(_), _)
+ | (GenericArgData::Lifetime(_), _)
+ | (GenericArgData::Const(_), _) => {
+ panic!("mismatched parameter kinds: p1={:?} p2={:?}", p1, p2)
+ }
+ }
+ }
+
+ fn aggregate_lifetimes(&mut self, l1: &Lifetime<I>, l2: &Lifetime<I>) -> Lifetime<I> {
+ let interner = self.interner;
+ match (l1.data(interner), l2.data(interner)) {
+ (LifetimeData::Phantom(void, ..), _) | (_, LifetimeData::Phantom(void, ..)) => {
+ match *void {}
+ }
+ (LifetimeData::BoundVar(..), _) | (_, LifetimeData::BoundVar(..)) => {
+ self.new_lifetime_variable()
+ }
+ _ => {
+ if l1 == l2 {
+ l1.clone()
+ } else {
+ self.new_lifetime_variable()
+ }
+ }
+ }
+ }
+
+ fn aggregate_consts(&mut self, c1: &Const<I>, c2: &Const<I>) -> Const<I> {
+ let interner = self.interner;
+
+ // It would be nice to check that c1 and c2 have the same type, even though
+ // on this stage of solving they should already have the same type.
+
+ let ConstData {
+ ty: c1_ty,
+ value: c1_value,
+ } = c1.data(interner);
+ let ConstData {
+ ty: _c2_ty,
+ value: c2_value,
+ } = c2.data(interner);
+
+ let ty = c1_ty.clone();
+
+ match (c1_value, c2_value) {
+ (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => {
+ self.new_const_variable(ty)
+ }
+
+ (ConstValue::BoundVar(_), _) | (_, ConstValue::BoundVar(_)) => {
+ self.new_const_variable(ty)
+ }
+
+ (ConstValue::Placeholder(_), ConstValue::Placeholder(_)) => {
+ if c1 == c2 {
+ c1.clone()
+ } else {
+ self.new_const_variable(ty)
+ }
+ }
+ (ConstValue::Concrete(e1), ConstValue::Concrete(e2)) => {
+ if e1.const_eq(&ty, e2, interner) {
+ c1.clone()
+ } else {
+ self.new_const_variable(ty)
+ }
+ }
+
+ (ConstValue::Placeholder(_), _) | (_, ConstValue::Placeholder(_)) => {
+ self.new_const_variable(ty)
+ }
+ }
+ }
+
+ fn new_ty_variable(&mut self) -> Ty<I> {
+ let interner = self.interner;
+ self.infer.new_variable(self.universe).to_ty(interner)
+ }
+
+ fn new_lifetime_variable(&mut self) -> Lifetime<I> {
+ let interner = self.interner;
+ self.infer.new_variable(self.universe).to_lifetime(interner)
+ }
+
+ fn new_const_variable(&mut self, ty: Ty<I>) -> Const<I> {
+ let interner = self.interner;
+ self.infer
+ .new_variable(self.universe)
+ .to_const(interner, ty)
+ }
+}
+
+#[cfg(test)]
+mod test {
+ use crate::slg::aggregate::AntiUnifier;
+ use chalk_integration::{arg, ty};
+ use chalk_ir::UniverseIndex;
+ use chalk_solve::infer::InferenceTable;
+
+ /// Test the equivalent of `Vec<i32>` vs `Vec<u32>`
+ #[test]
+ fn vec_i32_vs_vec_u32() {
+ use chalk_integration::interner::ChalkIr;
+ let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
+ let mut anti_unifier = AntiUnifier {
+ infer: &mut infer,
+ universe: UniverseIndex::root(),
+ interner: ChalkIr,
+ };
+
+ let ty = anti_unifier.aggregate_tys(
+ &ty!(apply (item 0) (apply (item 1))),
+ &ty!(apply (item 0) (apply (item 2))),
+ );
+ assert_eq!(ty!(apply (item 0) (infer 0)), ty);
+ }
+
+ /// Test the equivalent of `Vec<i32>` vs `Vec<i32>`
+ #[test]
+ fn vec_i32_vs_vec_i32() {
+ use chalk_integration::interner::ChalkIr;
+ let interner = ChalkIr;
+ let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
+ let mut anti_unifier = AntiUnifier {
+ interner,
+ infer: &mut infer,
+ universe: UniverseIndex::root(),
+ };
+
+ let ty = anti_unifier.aggregate_tys(
+ &ty!(apply (item 0) (apply (item 1))),
+ &ty!(apply (item 0) (apply (item 1))),
+ );
+ assert_eq!(ty!(apply (item 0) (apply (item 1))), ty);
+ }
+
+ /// Test the equivalent of `Vec<X>` vs `Vec<Y>`
+ #[test]
+ fn vec_x_vs_vec_y() {
+ use chalk_integration::interner::ChalkIr;
+ let interner = ChalkIr;
+ let mut infer: InferenceTable<ChalkIr> = InferenceTable::new();
+ let mut anti_unifier = AntiUnifier {
+ interner,
+ infer: &mut infer,
+ universe: UniverseIndex::root(),
+ };
+
+ // Note that the `var 0` and `var 1` in these types would be
+ // referring to canonicalized free variables, not variables in
+ // `infer`.
+ let ty = anti_unifier.aggregate_tys(
+ &ty!(apply (item 0) (infer 0)),
+ &ty!(apply (item 0) (infer 1)),
+ );
+
+ // But this `var 0` is from `infer.
+ assert_eq!(ty!(apply (item 0) (infer 0)), ty);
+ }
+}
diff --git a/vendor/chalk-engine/src/slg/resolvent.rs b/vendor/chalk-engine/src/slg/resolvent.rs
new file mode 100644
index 000000000..c6d0f8d5c
--- /dev/null
+++ b/vendor/chalk-engine/src/slg/resolvent.rs
@@ -0,0 +1,731 @@
+use crate::normalize_deep::DeepNormalizer;
+use crate::slg::ResolventOps;
+use crate::{ExClause, Literal, TimeStamp};
+use chalk_ir::cast::Caster;
+use chalk_ir::fold::shift::Shift;
+use chalk_ir::fold::Fold;
+use chalk_ir::interner::{HasInterner, Interner};
+use chalk_ir::zip::{Zip, Zipper};
+use chalk_ir::*;
+use chalk_solve::infer::InferenceTable;
+use tracing::{debug, instrument};
+
+///////////////////////////////////////////////////////////////////////////
+// SLG RESOLVENTS
+//
+// The "SLG Resolvent" is used to combine a *goal* G with some
+// clause or answer *C*. It unifies the goal's selected literal
+// with the clause and then inserts the clause's conditions into
+// the goal's list of things to prove, basically. Although this is
+// one operation in EWFS, we have specialized variants for merging
+// a program clause and an answer (though they share some code in
+// common).
+//
+// Terminology note: The NFTD and RR papers use the term
+// "resolvent" to mean both the factor and the resolvent, but EWFS
+// distinguishes the two. We follow EWFS here since -- in the code
+// -- we tend to know whether there are delayed literals or not,
+// and hence to know which code path we actually want.
+//
+// From EWFS:
+//
+// Let G be an X-clause A :- D | L1,...Ln, where N > 0, and Li be selected atom.
+//
+// Let C be an X-clause with no delayed literals. Let
+//
+// C' = A' :- L'1...L'm
+//
+// be a variant of C such that G and C' have no variables in
+// common.
+//
+// Let Li and A' be unified with MGU S.
+//
+// Then:
+//
+// S(A :- D | L1...Li-1, L1'...L'm, Li+1...Ln)
+//
+// is the SLG resolvent of G with C.
+
+impl<I: Interner> ResolventOps<I> for InferenceTable<I> {
+ /// Applies the SLG resolvent algorithm to incorporate a program
+ /// clause into the main X-clause, producing a new X-clause that
+ /// must be solved.
+ ///
+ /// # Parameters
+ ///
+ /// - `goal` is the goal G that we are trying to solve
+ /// - `clause` is the program clause that may be useful to that end
+ #[instrument(level = "debug", skip(self, interner, environment, subst))]
+ fn resolvent_clause(
+ &mut self,
+ db: &dyn UnificationDatabase<I>,
+ interner: I,
+ environment: &Environment<I>,
+ goal: &DomainGoal<I>,
+ subst: &Substitution<I>,
+ clause: &ProgramClause<I>,
+ ) -> Fallible<ExClause<I>> {
+ // Relating the above description to our situation:
+ //
+ // - `goal` G, except with binders for any existential variables.
+ // - Also, we always select the first literal in `ex_clause.literals`, so `i` is 0.
+ // - `clause` is C, except with binders for any existential variables.
+
+ // C' in the description above is `consequence :- conditions`.
+ //
+ // Note that G and C' have no variables in common.
+ let ProgramClauseImplication {
+ consequence,
+ conditions,
+ constraints,
+ priority: _,
+ } = {
+ let ProgramClauseData(implication) = clause.data(interner);
+
+ self.instantiate_binders_existentially(interner, implication.clone())
+ };
+ debug!(?consequence, ?conditions, ?constraints);
+
+ // Unify the selected literal Li with C'.
+ let unification_result = self.relate(
+ interner,
+ db,
+ environment,
+ Variance::Invariant,
+ goal,
+ &consequence,
+ )?;
+
+ // Final X-clause that we will return.
+ let mut ex_clause = ExClause {
+ subst: subst.clone(),
+ ambiguous: false,
+ constraints: vec![],
+ subgoals: vec![],
+ delayed_subgoals: vec![],
+ answer_time: TimeStamp::default(),
+ floundered_subgoals: vec![],
+ };
+
+ // Add the subgoals/region-constraints that unification gave us.
+ ex_clause.subgoals.extend(
+ unification_result
+ .goals
+ .into_iter()
+ .casted(interner)
+ .map(Literal::Positive),
+ );
+
+ ex_clause
+ .constraints
+ .extend(constraints.as_slice(interner).to_owned());
+
+ // Add the `conditions` from the program clause into the result too.
+ ex_clause
+ .subgoals
+ .extend(conditions.iter(interner).map(|c| match c.data(interner) {
+ GoalData::Not(c1) => {
+ Literal::Negative(InEnvironment::new(environment, Goal::clone(c1)))
+ }
+ _ => Literal::Positive(InEnvironment::new(environment, Goal::clone(c))),
+ }));
+
+ Ok(ex_clause)
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+ // apply_answer_subst
+ //
+ // Apply answer subst has the job of "plugging in" the answer to a
+ // query into the pending ex-clause. To see how it works, it's worth stepping
+ // up one level. Imagine that first we are trying to prove a goal A:
+ //
+ // A :- T: Foo<Vec<?U>>, ?U: Bar
+ //
+ // this spawns a subgoal `T: Foo<Vec<?0>>`, and it's this subgoal that
+ // has now produced an answer `?0 = u32`. When the goal A spawned the
+ // subgoal, it will also have registered a `PendingExClause` with its
+ // current state. At the point where *this* method has been invoked,
+ // that pending ex-clause has been instantiated with fresh variables and setup,
+ // so we have four bits of incoming information:
+ //
+ // - `ex_clause`, which is the remaining stuff to prove for the goal A.
+ // Here, the inference variable `?U` has been instantiated with a fresh variable
+ // `?X`.
+ // - `A :- ?X: Bar`
+ // - `selected_goal`, which is the thing we were trying to prove when we
+ // spawned the subgoal. It shares inference variables with `ex_clause`.
+ // - `T: Foo<Vec<?X>>`
+ // - `answer_table_goal`, which is the subgoal in canonical form:
+ // - `for<type> T: Foo<Vec<?0>>`
+ // - `canonical_answer_subst`, which is an answer to `answer_table_goal`.
+ // - `[?0 = u32]`
+ //
+ // In this case, this function will (a) unify `u32` and `?X` and then
+ // (b) return `ex_clause` (extended possibly with new region constraints
+ // and subgoals).
+ //
+ // One way to do this would be to (a) substitute
+ // `canonical_answer_subst` into `answer_table_goal` (yielding `T:
+ // Foo<Vec<u32>>`) and then (b) instantiate the result with fresh
+ // variables (no effect in this instance) and then (c) unify that with
+ // `selected_goal` (yielding, indirectly, that `?X = u32`). But that
+ // is not what we do: it's inefficient, to start, but it also causes
+ // problems because unification of projections can make new
+ // sub-goals. That is, even if the answers don't involve any
+ // projections, the table goals might, and this can create an infinite
+ // loop (see also #74).
+ //
+ // What we do instead is to (a) instantiate the substitution, which
+ // may have free variables in it (in this case, it would not, and the
+ // instantiation would have no effect) and then (b) zip
+ // `answer_table_goal` and `selected_goal` without having done any
+ // substitution. After all, these ought to be basically the same,
+ // since `answer_table_goal` was created by canonicalizing (and
+ // possibly truncating, but we'll get to that later)
+ // `selected_goal`. Then, whenever we reach a "free variable" in
+ // `answer_table_goal`, say `?0`, we go to the instantiated answer
+ // substitution and lookup the result (in this case, `u32`). We take
+ // that result and unify it with whatever we find in `selected_goal`
+ // (in this case, `?X`).
+ //
+ // Let's cover then some corner cases. First off, what is this
+ // business of instantiating the answer? Well, the answer may not be a
+ // simple type like `u32`, it could be a "family" of types, like
+ // `for<type> Vec<?0>` -- i.e., `Vec<X>: Bar` for *any* `X`. In that
+ // case, the instantiation would produce a substitution `[?0 :=
+ // Vec<?Y>]` (note that the key is not affected, just the value). So
+ // when we do the unification, instead of unifying `?X = u32`, we
+ // would unify `?X = Vec<?Y>`.
+ //
+ // Next, truncation. One key thing is that the `answer_table_goal` may
+ // not be *exactly* the same as the `selected_goal` -- we will
+ // truncate it if it gets too deep. so, in our example, it may be that
+ // instead of `answer_table_goal` being `for<type> T: Foo<Vec<?0>>`,
+ // it could have been truncated to `for<type> T: Foo<?0>` (which is a
+ // more general goal). In that case, let's say that the answer is
+ // still `[?0 = u32]`, meaning that `T: Foo<u32>` is true (which isn't
+ // actually interesting to our original goal). When we do the zip
+ // then, we will encounter `?0` in the `answer_table_goal` and pair
+ // that with `Vec<?X>` from the pending goal. We will attempt to unify
+ // `Vec<?X>` with `u32` (from the substitution), which will fail. That
+ // failure will get propagated back up.
+
+ #[instrument(level = "debug", skip(self, interner))]
+ fn apply_answer_subst(
+ &mut self,
+ interner: I,
+ unification_database: &dyn UnificationDatabase<I>,
+ ex_clause: &mut ExClause<I>,
+ selected_goal: &InEnvironment<Goal<I>>,
+ answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
+ canonical_answer_subst: Canonical<AnswerSubst<I>>,
+ ) -> Fallible<()> {
+ debug!(selected_goal = ?DeepNormalizer::normalize_deep(self, interner, selected_goal.clone()));
+
+ // C' is now `answer`. No variables in common with G.
+ let AnswerSubst {
+ subst: answer_subst,
+
+ // Assuming unification succeeds, we incorporate the
+ // region constraints from the answer into the result;
+ // we'll need them if this answer (which is not yet known
+ // to be true) winds up being true, and otherwise (if the
+ // answer is false or unknown) it doesn't matter.
+ constraints: answer_constraints,
+
+ delayed_subgoals,
+ } = self.instantiate_canonical(interner, canonical_answer_subst);
+
+ AnswerSubstitutor::substitute(
+ interner,
+ unification_database,
+ self,
+ &selected_goal.environment,
+ &answer_subst,
+ ex_clause,
+ &answer_table_goal.value,
+ selected_goal,
+ )?;
+ ex_clause
+ .constraints
+ .extend(answer_constraints.as_slice(interner).to_vec());
+ // at that point we should only have goals that stemmed
+ // from non trivial self cycles
+ ex_clause.delayed_subgoals.extend(delayed_subgoals);
+ Ok(())
+ }
+}
+
+struct AnswerSubstitutor<'t, I: Interner> {
+ table: &'t mut InferenceTable<I>,
+ environment: &'t Environment<I>,
+ answer_subst: &'t Substitution<I>,
+
+ /// Tracks the debrujn index of the first binder that is outside
+ /// the term we are traversing. This starts as `DebruijnIndex::INNERMOST`,
+ /// since we have not yet traversed *any* binders, but when we visit
+ /// the inside of a binder, it would be incremented.
+ ///
+ /// Example: If we are visiting `(for<type> A, B, C, for<type> for<type> D)`,
+ /// then this would be:
+ ///
+ /// * `1`, when visiting `A`,
+ /// * `0`, when visiting `B` and `C`,
+ /// * `2`, when visiting `D`.
+ outer_binder: DebruijnIndex,
+
+ ex_clause: &'t mut ExClause<I>,
+ interner: I,
+ unification_database: &'t dyn UnificationDatabase<I>,
+}
+
+impl<I: Interner> AnswerSubstitutor<'_, I> {
+ fn substitute<T: Zip<I>>(
+ interner: I,
+ unification_database: &dyn UnificationDatabase<I>,
+ table: &mut InferenceTable<I>,
+ environment: &Environment<I>,
+ answer_subst: &Substitution<I>,
+ ex_clause: &mut ExClause<I>,
+ answer: &T,
+ pending: &T,
+ ) -> Fallible<()> {
+ let mut this = AnswerSubstitutor {
+ interner,
+ unification_database,
+ table,
+ environment,
+ answer_subst,
+ ex_clause,
+ outer_binder: DebruijnIndex::INNERMOST,
+ };
+ Zip::zip_with(&mut this, Variance::Invariant, answer, pending)?;
+ Ok(())
+ }
+
+ fn unify_free_answer_var(
+ &mut self,
+ interner: I,
+ db: &dyn UnificationDatabase<I>,
+ variance: Variance,
+ answer_var: BoundVar,
+ pending: GenericArgData<I>,
+ ) -> Fallible<bool> {
+ let answer_index = match answer_var.index_if_bound_at(self.outer_binder) {
+ Some(index) => index,
+
+ // This variable is bound in the answer, not free, so it
+ // doesn't represent a reference into the answer substitution.
+ None => return Ok(false),
+ };
+
+ let answer_param = self.answer_subst.at(interner, answer_index);
+
+ let pending_shifted = pending
+ .shifted_out_to(interner, self.outer_binder)
+ .expect("truncate extracted a pending value that references internal binder");
+
+ let result = self.table.relate(
+ interner,
+ db,
+ self.environment,
+ variance,
+ answer_param,
+ &GenericArg::new(interner, pending_shifted),
+ )?;
+
+ self.ex_clause.subgoals.extend(
+ result
+ .goals
+ .into_iter()
+ .casted(interner)
+ .map(Literal::Positive),
+ );
+
+ Ok(true)
+ }
+
+ /// When we encounter a variable in the answer goal, we first try
+ /// `unify_free_answer_var`. Assuming that this fails, the
+ /// variable must be a bound variable in the answer goal -- in
+ /// that case, there should be a corresponding bound variable in
+ /// the pending goal. This bit of code just checks that latter
+ /// case.
+ fn assert_matching_vars(
+ &mut self,
+ answer_var: BoundVar,
+ pending_var: BoundVar,
+ ) -> Fallible<()> {
+ let BoundVar {
+ debruijn: answer_depth,
+ index: answer_index,
+ } = answer_var;
+ let BoundVar {
+ debruijn: pending_depth,
+ index: pending_index,
+ } = pending_var;
+
+ // Both bound variables are bound within the term we are matching
+ assert!(answer_depth.within(self.outer_binder));
+
+ // They are bound at the same (relative) depth
+ assert_eq!(answer_depth, pending_depth);
+
+ // They are bound at the same index within the binder
+ assert_eq!(answer_index, pending_index,);
+
+ Ok(())
+ }
+}
+
+impl<'i, I: Interner> Zipper<I> for AnswerSubstitutor<'i, I> {
+ fn zip_tys(&mut self, variance: Variance, answer: &Ty<I>, pending: &Ty<I>) -> Fallible<()> {
+ let interner = self.interner;
+
+ if let Some(pending) = self.table.normalize_ty_shallow(interner, pending) {
+ return Zip::zip_with(self, variance, answer, &pending);
+ }
+
+ // If the answer has a variable here, then this is one of the
+ // "inputs" to the subgoal table. We need to extract the
+ // resulting answer that the subgoal found and unify it with
+ // the value from our "pending subgoal".
+ if let TyKind::BoundVar(answer_depth) = answer.kind(interner) {
+ if self.unify_free_answer_var(
+ interner,
+ self.unification_database,
+ variance,
+ *answer_depth,
+ GenericArgData::Ty(pending.clone()),
+ )? {
+ return Ok(());
+ }
+ }
+
+ // Otherwise, the answer and the selected subgoal ought to be a perfect match for
+ // one another.
+ match (answer.kind(interner), pending.kind(interner)) {
+ (TyKind::BoundVar(answer_depth), TyKind::BoundVar(pending_depth)) => {
+ self.assert_matching_vars(*answer_depth, *pending_depth)
+ }
+
+ (TyKind::Dyn(answer), TyKind::Dyn(pending)) => {
+ Zip::zip_with(self, variance, answer, pending)
+ }
+
+ (TyKind::Alias(answer), TyKind::Alias(pending)) => {
+ Zip::zip_with(self, variance, answer, pending)
+ }
+
+ (TyKind::Placeholder(answer), TyKind::Placeholder(pending)) => {
+ Zip::zip_with(self, variance, answer, pending)
+ }
+
+ (TyKind::Function(answer), TyKind::Function(pending)) => Zip::zip_with(
+ self,
+ variance,
+ &answer.clone().into_binders(interner),
+ &pending.clone().into_binders(interner),
+ ),
+
+ (TyKind::InferenceVar(_, _), _) | (_, TyKind::InferenceVar(_, _)) => panic!(
+ "unexpected inference var in answer `{:?}` or pending goal `{:?}`",
+ answer, pending,
+ ),
+
+ (TyKind::Adt(id_a, substitution_a), TyKind::Adt(id_b, substitution_b)) => {
+ if id_a != id_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ Some(self.unification_database().adt_variance(*id_a)),
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (
+ TyKind::AssociatedType(id_a, substitution_a),
+ TyKind::AssociatedType(id_b, substitution_b),
+ ) => {
+ if id_a != id_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ None,
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (TyKind::Scalar(scalar_a), TyKind::Scalar(scalar_b)) => {
+ Zip::zip_with(self, variance, scalar_a, scalar_b)
+ }
+ (TyKind::Str, TyKind::Str) => Ok(()),
+ (TyKind::Tuple(arity_a, substitution_a), TyKind::Tuple(arity_b, substitution_b)) => {
+ if arity_a != arity_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ None,
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (
+ TyKind::OpaqueType(id_a, substitution_a),
+ TyKind::OpaqueType(id_b, substitution_b),
+ ) => {
+ if id_a != id_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ None,
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (TyKind::Slice(ty_a), TyKind::Slice(ty_b)) => Zip::zip_with(self, variance, ty_a, ty_b),
+ (TyKind::FnDef(id_a, substitution_a), TyKind::FnDef(id_b, substitution_b)) => {
+ if id_a != id_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ Some(self.unification_database().fn_def_variance(*id_a)),
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (
+ TyKind::Ref(mutability_a, lifetime_a, ty_a),
+ TyKind::Ref(mutability_b, lifetime_b, ty_b),
+ ) => {
+ if mutability_a != mutability_b {
+ return Err(NoSolution);
+ }
+ // The lifetime is `Contravariant`
+ Zip::zip_with(
+ self,
+ variance.xform(Variance::Contravariant),
+ lifetime_a,
+ lifetime_b,
+ )?;
+ // The type is `Covariant` when not mut, `Invariant` otherwise
+ let output_variance = match mutability_a {
+ Mutability::Not => Variance::Covariant,
+ Mutability::Mut => Variance::Invariant,
+ };
+ Zip::zip_with(self, variance.xform(output_variance), ty_a, ty_b)
+ }
+ (TyKind::Raw(mutability_a, ty_a), TyKind::Raw(mutability_b, ty_b)) => {
+ if mutability_a != mutability_b {
+ return Err(NoSolution);
+ }
+ let ty_variance = match mutability_a {
+ Mutability::Not => Variance::Covariant,
+ Mutability::Mut => Variance::Invariant,
+ };
+ Zip::zip_with(self, variance.xform(ty_variance), ty_a, ty_b)
+ }
+ (TyKind::Never, TyKind::Never) => Ok(()),
+ (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {
+ Zip::zip_with(self, variance, ty_a, ty_b)?;
+ Zip::zip_with(self, variance, const_a, const_b)
+ }
+ (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => {
+ if id_a != id_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ None,
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (TyKind::Generator(id_a, substitution_a), TyKind::Generator(id_b, substitution_b)) => {
+ if id_a != id_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ None,
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (
+ TyKind::GeneratorWitness(id_a, substitution_a),
+ TyKind::GeneratorWitness(id_b, substitution_b),
+ ) => {
+ if id_a != id_b {
+ return Err(NoSolution);
+ }
+ self.zip_substs(
+ variance,
+ None,
+ substitution_a.as_slice(interner),
+ substitution_b.as_slice(interner),
+ )
+ }
+ (TyKind::Foreign(id_a), TyKind::Foreign(id_b)) => {
+ Zip::zip_with(self, variance, id_a, id_b)
+ }
+ (TyKind::Error, TyKind::Error) => Ok(()),
+
+ (_, _) => panic!(
+ "structural mismatch between answer `{:?}` and pending goal `{:?}`",
+ answer, pending,
+ ),
+ }
+ }
+
+ fn zip_lifetimes(
+ &mut self,
+ variance: Variance,
+ answer: &Lifetime<I>,
+ pending: &Lifetime<I>,
+ ) -> Fallible<()> {
+ let interner = self.interner;
+ if let Some(pending) = self.table.normalize_lifetime_shallow(interner, pending) {
+ return Zip::zip_with(self, variance, answer, &pending);
+ }
+
+ if let LifetimeData::BoundVar(answer_depth) = answer.data(interner) {
+ if self.unify_free_answer_var(
+ interner,
+ self.unification_database,
+ variance,
+ *answer_depth,
+ GenericArgData::Lifetime(pending.clone()),
+ )? {
+ return Ok(());
+ }
+ }
+
+ match (answer.data(interner), pending.data(interner)) {
+ (LifetimeData::BoundVar(answer_depth), LifetimeData::BoundVar(pending_depth)) => {
+ self.assert_matching_vars(*answer_depth, *pending_depth)
+ }
+
+ (LifetimeData::Static, LifetimeData::Static)
+ | (LifetimeData::Placeholder(_), LifetimeData::Placeholder(_))
+ | (LifetimeData::Erased, LifetimeData::Erased)
+ | (LifetimeData::Empty(_), LifetimeData::Empty(_)) => {
+ assert_eq!(answer, pending);
+ Ok(())
+ }
+
+ (LifetimeData::InferenceVar(_), _) | (_, LifetimeData::InferenceVar(_)) => panic!(
+ "unexpected inference var in answer `{:?}` or pending goal `{:?}`",
+ answer, pending,
+ ),
+
+ (LifetimeData::Static, _)
+ | (LifetimeData::BoundVar(_), _)
+ | (LifetimeData::Placeholder(_), _)
+ | (LifetimeData::Erased, _)
+ | (LifetimeData::Empty(_), _) => panic!(
+ "structural mismatch between answer `{:?}` and pending goal `{:?}`",
+ answer, pending,
+ ),
+
+ (LifetimeData::Phantom(void, _), _) => match *void {},
+ }
+ }
+
+ fn zip_consts(
+ &mut self,
+ variance: Variance,
+ answer: &Const<I>,
+ pending: &Const<I>,
+ ) -> Fallible<()> {
+ let interner = self.interner;
+ if let Some(pending) = self.table.normalize_const_shallow(interner, pending) {
+ return Zip::zip_with(self, variance, answer, &pending);
+ }
+
+ let ConstData {
+ ty: answer_ty,
+ value: answer_value,
+ } = answer.data(interner);
+ let ConstData {
+ ty: pending_ty,
+ value: pending_value,
+ } = pending.data(interner);
+
+ self.zip_tys(variance, answer_ty, pending_ty)?;
+
+ if let ConstValue::BoundVar(answer_depth) = answer_value {
+ if self.unify_free_answer_var(
+ interner,
+ self.unification_database,
+ variance,
+ *answer_depth,
+ GenericArgData::Const(pending.clone()),
+ )? {
+ return Ok(());
+ }
+ }
+
+ match (answer_value, pending_value) {
+ (ConstValue::BoundVar(answer_depth), ConstValue::BoundVar(pending_depth)) => {
+ self.assert_matching_vars(*answer_depth, *pending_depth)
+ }
+
+ (ConstValue::Placeholder(_), ConstValue::Placeholder(_)) => {
+ assert_eq!(answer, pending);
+ Ok(())
+ }
+
+ (ConstValue::Concrete(c1), ConstValue::Concrete(c2)) => {
+ assert!(c1.const_eq(answer_ty, c2, interner));
+ Ok(())
+ }
+
+ (ConstValue::InferenceVar(_), _) | (_, ConstValue::InferenceVar(_)) => panic!(
+ "unexpected inference var in answer `{:?}` or pending goal `{:?}`",
+ answer, pending,
+ ),
+
+ (ConstValue::BoundVar(_), _)
+ | (ConstValue::Placeholder(_), _)
+ | (ConstValue::Concrete(_), _) => panic!(
+ "structural mismatch between answer `{:?}` and pending goal `{:?}`",
+ answer, pending,
+ ),
+ }
+ }
+
+ fn zip_binders<T>(
+ &mut self,
+ variance: Variance,
+ answer: &Binders<T>,
+ pending: &Binders<T>,
+ ) -> Fallible<()>
+ where
+ T: HasInterner<Interner = I> + Zip<I> + Fold<I, Result = T>,
+ {
+ self.outer_binder.shift_in();
+ Zip::zip_with(
+ self,
+ variance,
+ answer.skip_binders(),
+ pending.skip_binders(),
+ )?;
+ self.outer_binder.shift_out();
+ Ok(())
+ }
+
+ fn interner(&self) -> I {
+ self.interner
+ }
+
+ fn unification_database(&self) -> &dyn UnificationDatabase<I> {
+ self.unification_database
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-27 08:30:06 +0000