Skip to content

Commit

Permalink
Merge pull request #529 from Areredify/ucanonicalization_fix
Browse files Browse the repository at this point in the history 
Ucanonicalization fix
  • Loading branch information
@nikomatsakis
nikomatsakis authored Jun 16, 2020
2 parents 75048f9 + 5fc7fb3 commit 28fcc72
Show file tree
Hide file tree
Showing 3 changed files with 101 additions and 71 deletions.
5 changes: 5 additions & 0 deletions chalk-solve/src/infer/canonicalize.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,11 @@ impl<'q, I: Interner> Canonicalizer<'q, I> {
}

fn add(&mut self, free_var: ParameterEnaVariable<I>) -> usize {
self.max_universe = max(
self.max_universe,
self.table.universe_of_unbound_var(*free_var.skip_kind()),
);

self.free_vars
.iter()
.position(|v| v.skip_kind() == free_var.skip_kind())
Expand Down
141 changes: 70 additions & 71 deletions chalk-solve/src/infer/ucanonicalize.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,11 @@ impl<I: Interner> InferenceTable<I> {

// First, find all the universes that appear in `value`.
let mut universes = UniverseMap::new();

for universe in value0.binders.iter(interner) {
universes.add(*universe.skip_kind());
}

value0.value.visit_with(
&mut UCollector {
universes: &mut universes,
Expand All @@ -45,7 +50,7 @@ impl<I: Interner> InferenceTable<I> {
value0
.binders
.iter(interner)
.map(|pk| pk.map_ref(|&ui| universes.map_universe_to_canonical(ui))),
.map(|pk| pk.map_ref(|&ui| universes.map_universe_to_canonical(ui).unwrap())),
);

UCanonicalized {
Expand All @@ -72,11 +77,16 @@ pub(crate) struct UCanonicalized<T: HasInterner> {

pub(crate) trait UniverseMapExt {
fn add(&mut self, universe: UniverseIndex);
fn map_universe_to_canonical(&self, universe: UniverseIndex) -> UniverseIndex;
fn map_universe_to_canonical(&self, universe: UniverseIndex) -> Option<UniverseIndex>;
fn map_universe_from_canonical(&self, universe: UniverseIndex) -> UniverseIndex;
fn map_from_canonical<T, I>(&self, interner: &I, value: &T) -> T::Result
fn map_from_canonical<T, I>(
&self,
interner: &I,
canonical_value: &Canonical<T>,
) -> Canonical<T::Result>
where
T: Fold<I>,
T: Fold<I> + HasInterner<Interner = I>,
T::Result: HasInterner<Interner = I>,
I: Interner;
}
impl UniverseMapExt for UniverseMap {
Expand All @@ -91,66 +101,13 @@ impl UniverseMapExt for UniverseMap {
/// looking for the index I of U in `self.universes`. We will
/// return the universe with "counter" I. This effectively
/// "compresses" the range of universes to things from
/// `0..self.universes.len()`.
///
/// There is one subtle point, though: if we don't find U in the
/// vector, what should we return? This can only occur when we are
/// mapping the universes for existentially quantified variables
/// appearing in the original value. For example, if we have an initial
/// query like
///
/// ```notrust
/// !U1: Foo<?X, !U3>
/// ```
///
/// where `?X` is an existential variable in universe U2, and
/// `!U1` (resp. `!U3`) is a placeholder variable in universe U1
/// (resp. U3), then this will be canonicalized to
///
/// ```notrust
/// exists<U2> { !U1: Foo<?0, !U3>
/// ```
///
/// We will then collect the universe vector `[Root, 1, 3]`.
/// Hence we would remap the inner part to `!U1': Foo<?0, !U2'>`
/// (I am using the convention of writing U1' and U2' to indicate
/// the target universes that we are mapping to, which are
/// logically distinct). But what universe should we use for the
/// `exists` binder? `U2` is not in the set of universes we
/// collected initially. The answer is that we will remap U2 to
/// U1' in the final result, giving:
///
/// ```notrust
/// exists<U1'> { !U1': Foo<?0, !U2'>
/// ```
///
/// More generally, we pick the highest numbered universe we did
/// find that is still lower then the universe U we are
/// mapping. Effectively we "remapped" from U2 (in the original
/// multiverse) to U1; this is a sound approximation, because all
/// names from U1 are visible to U2 (but not vice
/// versa). Moreover, since there are no placeholders from U2 in
/// the original query, there is no way we would have equated `?0`
/// with such a name.
fn map_universe_to_canonical(&self, universe: UniverseIndex) -> UniverseIndex {
match self.universes.binary_search(&universe) {
Ok(index) => UniverseIndex { counter: index },

// `index` is the location in the vector where universe
// *would have* gone. So, in our example from the comment
// above, if we were looking up `U2` we would get back 2,
// since it would go between U1 (with index 1) and U3
// (with index 2). Therefore, we want to subtract one to
// get the biggest universe that is still lower than
// `universe`.
//
// Note that `index` can never be 0: that is always the
// root universe, we always add that to the vector.
Err(index) => {
assert!(index > 0);
UniverseIndex { counter: index - 1 }
}
}
/// `0..self.universes.len()`. If the universe is not present in the map,
/// we return `None`.
fn map_universe_to_canonical(&self, universe: UniverseIndex) -> Option<UniverseIndex> {
self.universes
.binary_search(&universe)
.ok()
.map(|index| UniverseIndex { counter: index })
}

/// Given a "canonical universe" -- one found in the
Expand Down Expand Up @@ -201,22 +158,39 @@ impl UniverseMapExt for UniverseMap {
/// of universes, since that determines visibility, and (b) that
/// the universe we produce does not correspond to any of the
/// other original universes.
fn map_from_canonical<T, I>(&self, interner: &I, value: &T) -> T::Result
fn map_from_canonical<T, I>(
&self,
interner: &I,
canonical_value: &Canonical<T>,
) -> Canonical<T::Result>
where
T: Fold<I>,
T: Fold<I> + HasInterner<Interner = I>,
T::Result: HasInterner<Interner = I>,
I: Interner,
{
debug!("map_from_canonical(value={:?})", value);
debug!("map_from_canonical(value={:?})", canonical_value);
debug!("map_from_canonical: universes = {:?}", self.universes);
value

let binders = canonical_value
.binders
.iter(interner)
.map(|cvk| cvk.map_ref(|&universe| self.map_universe_from_canonical(universe)));

let value = canonical_value
.value
.fold_with(
&mut UMapFromCanonical {
interner,
universes: self,
},
DebruijnIndex::INNERMOST,
)
.unwrap()
.unwrap();

Canonical {
binders: CanonicalVarKinds::from(interner, binders),
value,
}
}
}

Expand Down Expand Up @@ -272,7 +246,10 @@ where
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Ty<I>> {
let ui = self.universes.map_universe_to_canonical(universe0.ui);
let ui = self
.universes
.map_universe_to_canonical(universe0.ui)
.expect("Expected UCollector to encounter this universe");
Ok(PlaceholderIndex {
ui,
idx: universe0.idx,
Expand All @@ -285,14 +262,36 @@ where
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Lifetime<I>> {
let universe = self.universes.map_universe_to_canonical(universe0.ui);
let universe = self
.universes
.map_universe_to_canonical(universe0.ui)
.expect("Expected UCollector to encounter this universe");

Ok(PlaceholderIndex {
ui: universe,
idx: universe0.idx,
}
.to_lifetime(self.interner()))
}

fn fold_free_placeholder_const(
&mut self,
ty: &Ty<I>,
universe0: PlaceholderIndex,
_outer_binder: DebruijnIndex,
) -> Fallible<Const<I>> {
let universe = self
.universes
.map_universe_to_canonical(universe0.ui)
.expect("Expected UCollector to encounter this universe");

Ok(PlaceholderIndex {
ui: universe,
idx: universe0.idx,
}
.to_const(self.interner(), ty.clone()))
}

fn interner(&self) -> &'i I {
self.interner
}
Expand Down
26 changes: 26 additions & 0 deletions tests/test/misc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -672,3 +672,29 @@ fn not_really_ambig() {
}
}
}

#[test]
fn canonicalization_regression() {
test! {
program {
trait ForAny<X> {}
trait ForSame<X> {}

impl<X, Y> ForAny<X> for Y {}
impl<X> ForSame<X> for X {}
}

goal {
forall<A> {
forall<B> {
exists<E> {
A: ForAny<E>,
B: ForSame<E>
}
}
}
} yields {
"Unique; substitution [?0 := !2_0], lifetime constraints []"
}
}
}

0 comments on commit 28fcc72

Please sign in to comment.