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
}
}