1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 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
}
}