1 files changed, 174 insertions, 0 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/infer/invert.rs b/vendor/chalk-solve-0.87.0/src/infer/invert.rs
new file mode 100644
index 000000000..e5bc3590c
--- /dev/null
+++ b/vendor/chalk-solve-0.87.0/src/infer/invert.rs
@@ -0,0 +1,174 @@
+use chalk_derive::FallibleTypeFolder;
+use chalk_ir::fold::shift::Shift;
+use chalk_ir::fold::{TypeFoldable, TypeFolder};
+use chalk_ir::interner::HasInterner;
+use chalk_ir::interner::Interner;
+use chalk_ir::*;
+use rustc_hash::FxHashMap;
+
+use super::canonicalize::Canonicalized;
+use super::{EnaVariable, InferenceTable};
+
+impl<I: Interner> InferenceTable<I> {
+    /// Converts `value` into a "negation" value -- meaning one that,
+    /// if we can find any answer to it, then the negation fails. For
+    /// goals that do not contain any free variables, then this is a
+    /// no-op operation.
+    ///
+    /// If `value` contains any existential variables that have not
+    /// yet been assigned a value, then this function will return
+    /// `None`, indicating that we cannot prove negation for this goal
+    /// yet.  This follows the approach in Clark's original
+    /// [negation-as-failure paper][1], where negative goals are only
+    /// permitted if they contain no free (existential) variables.
+    ///
+    /// [1]: https://www.doc.ic.ac.uk/~klc/NegAsFailure.pdf
+    ///
+    /// Restricting free existential variables is done because the
+    /// semantics of such queries is not what you expect: it basically
+    /// treats the existential as a universal. For example, consider:
+    ///
+    /// ```rust,ignore
+    /// struct Vec<T> {}
+    /// struct i32 {}
+    /// struct u32 {}
+    /// trait Foo {}
+    /// impl Foo for Vec<u32> {}
+    /// ```
+    ///
+    /// If we ask `exists<T> { not { Vec<T>: Foo } }`, what should happen?
+    /// If we allow negative queries to be definitively answered even when
+    /// they contain free variables, we will get a definitive *no* to the
+    /// entire goal! From a logical perspective, that's just wrong: there
+    /// does exists a `T` such that `not { Vec<T>: Foo }`, namely `i32`. The
+    /// problem is that the proof search procedure is actually trying to
+    /// prove something stronger, that there is *no* such `T`.
+    ///
+    /// An additional complication arises around free universal
+    /// variables.  Consider a query like `not { !0 = !1 }`, where
+    /// `!0` and `!1` are placeholders for universally quantified
+    /// types (i.e., `TyKind::Placeholder`). If we just tried to
+    /// prove `!0 = !1`, we would get false, because those types
+    /// cannot be unified -- this would then allow us to conclude that
+    /// `not { !0 = !1 }`, i.e., `forall<X, Y> { not { X = Y } }`, but
+    /// this is clearly not true -- what if X were to be equal to Y?
+    ///
+    /// Interestingly, the semantics of existential variables turns
+    /// out to be exactly what we want here. So, in addition to
+    /// forbidding existential variables in the original query, the
+    /// `negated` query also converts all universals *into*
+    /// existentials. Hence `negated` applies to `!0 = !1` would yield
+    /// `exists<X,Y> { X = Y }` (note that a canonical, i.e. closed,
+    /// result is returned). Naturally this has a solution, and hence
+    /// `not { !0 = !1 }` fails, as we expect.
+    ///
+    /// (One could imagine converting free existentials into
+    /// universals, rather than forbidding them altogether. This would
+    /// be conceivable, but overly strict. For example, the goal
+    /// `exists<T> { not { ?T: Clone }, ?T = Vec<i32> }` would come
+    /// back as false, when clearly this is true. This is because we
+    /// would wind up proving that `?T: Clone` can *never* be
+    /// satisfied (which is false), when we only really care about
+    /// `?T: Clone` in the case where `?T = Vec<i32>`. The current
+    /// version would delay processing the negative goal (i.e., return
+    /// `None`) until the second unification has occurred.)
+    pub fn invert<T>(&mut self, interner: I, value: T) -> Option<T>
+    where
+        T: TypeFoldable<I> + HasInterner<Interner = I>,
+    {
+        let Canonicalized {
+            free_vars,
+            quantified,
+            ..
+        } = self.canonicalize(interner, value);
+
+        // If the original contains free existential variables, give up.
+        if !free_vars.is_empty() {
+            return None;
+        }
+
+        // If this contains free universal variables, replace them with existentials.
+        assert!(quantified.binders.is_empty(interner));
+        let inverted = quantified
+            .value
+            .try_fold_with(&mut Inverter::new(interner, self), DebruijnIndex::INNERMOST)
+            .unwrap();
+        Some(inverted)
+    }
+
+    /// As `negated_instantiated`, but canonicalizes before
+    /// returning. Just a convenience function.
+    pub fn invert_then_canonicalize<T>(&mut self, interner: I, value: T) -> Option<Canonical<T>>
+    where
+        T: TypeFoldable<I> + HasInterner<Interner = I>,
+    {
+        let snapshot = self.snapshot();
+        let result = self.invert(interner, value);
+        let result = result.map(|r| self.canonicalize(interner, r).quantified);
+        self.rollback_to(snapshot);
+        result
+    }
+}
+
+#[derive(FallibleTypeFolder)]
+struct Inverter<'q, I: Interner> {
+    table: &'q mut InferenceTable<I>,
+    inverted_ty: FxHashMap<PlaceholderIndex, EnaVariable<I>>,
+    inverted_lifetime: FxHashMap<PlaceholderIndex, EnaVariable<I>>,
+    interner: I,
+}
+
+impl<'q, I: Interner> Inverter<'q, I> {
+    fn new(interner: I, table: &'q mut InferenceTable<I>) -> Self {
+        Inverter {
+            table,
+            inverted_ty: FxHashMap::default(),
+            inverted_lifetime: FxHashMap::default(),
+            interner,
+        }
+    }
+}
+
+impl<'i, I: Interner> TypeFolder<I> for Inverter<'i, I> {
+    fn as_dyn(&mut self) -> &mut dyn TypeFolder<I> {
+        self
+    }
+
+    fn fold_free_placeholder_ty(
+        &mut self,
+        universe: PlaceholderIndex,
+        _outer_binder: DebruijnIndex,
+    ) -> Ty<I> {
+        let table = &mut self.table;
+        self.inverted_ty
+            .entry(universe)
+            .or_insert_with(|| table.new_variable(universe.ui))
+            .to_ty(TypeFolder::interner(self))
+            .shifted_in(TypeFolder::interner(self))
+    }
+
+    fn fold_free_placeholder_lifetime(
+        &mut self,
+        universe: PlaceholderIndex,
+        _outer_binder: DebruijnIndex,
+    ) -> Lifetime<I> {
+        let table = &mut self.table;
+        self.inverted_lifetime
+            .entry(universe)
+            .or_insert_with(|| table.new_variable(universe.ui))
+            .to_lifetime(TypeFolder::interner(self))
+            .shifted_in(TypeFolder::interner(self))
+    }
+
+    fn forbid_free_vars(&self) -> bool {
+        true
+    }
+
+    fn forbid_inference_vars(&self) -> bool {
+        true
+    }
+
+    fn interner(&self) -> I {
+        self.interner
+    }
+}