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 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260
use crate::coherence::{CoherenceError, CoherenceSolver};
use crate::debug_span;
use crate::ext::*;
use crate::rust_ir::*;
use crate::{goal_builder::GoalBuilder, Solution};
use chalk_ir::cast::*;
use chalk_ir::fold::shift::Shift;
use chalk_ir::interner::Interner;
use chalk_ir::*;
use itertools::Itertools;
use tracing::{debug, instrument};
impl<I: Interner> CoherenceSolver<'_, I> {
pub(super) fn visit_specializations_of_trait(
&self,
mut record_specialization: impl FnMut(ImplId<I>, ImplId<I>),
) -> Result<(), CoherenceError<I>> {
// Ignore impls for marker traits as they are allowed to overlap.
let trait_datum = self.db.trait_datum(self.trait_id);
if trait_datum.flags.marker {
return Ok(());
}
// Iterate over every pair of impls for the same trait.
let impls = self.db.local_impls_to_coherence_check(self.trait_id);
for (l_id, r_id) in impls.into_iter().tuple_combinations() {
let lhs = &self.db.impl_datum(l_id);
let rhs = &self.db.impl_datum(r_id);
// Two negative impls never overlap.
if !lhs.is_positive() && !rhs.is_positive() {
continue;
}
// Check if the impls overlap, then if they do, check if one specializes
// the other. Note that specialization can only run one way - if both
// specialization checks return *either* true or false, that's an error.
if !self.disjoint(lhs, rhs) {
match (self.specializes(l_id, r_id), self.specializes(r_id, l_id)) {
(true, false) => record_specialization(l_id, r_id),
(false, true) => record_specialization(r_id, l_id),
(_, _) => {
return Err(CoherenceError::OverlappingImpls(self.trait_id));
}
}
}
}
Ok(())
}
// Test if the set of types that these two impls apply to overlap. If the test succeeds, these
// two impls are disjoint.
//
// We combine the binders of the two impls & treat them as existential quantifiers. Then we
// attempt to unify the input types to the trait provided by each impl, as well as prove that
// the where clauses from both impls all hold. At the end, we apply the `compatible` modality
// and negate the query. Negating the query means that we are asking chalk to prove that no
// such overlapping impl exists. By applying `compatible { G }`, chalk attempts to prove that
// "there exists a compatible world where G is provable." When we negate compatible, it turns
// into the statement "for all compatible worlds, G is not provable." This is exactly what we
// want since we want to ensure that there is no overlap in *all* compatible worlds, not just
// that there is no overlap in *some* compatible world.
//
// Examples:
//
// Impls:
// impl<T> Foo for T { } // rhs
// impl Foo for i32 { } // lhs
// Generates:
// not { compatible { exists<T> { exists<> { T = i32 } } } }
//
// Impls:
// impl<T1, U> Foo<T1> for Vec<U> { } // rhs
// impl<T2> Foo<T2> for Vec<i32> { } // lhs
// Generates:
// not { compatible { exists<T1, U> { exists<T2> { Vec<U> = Vec<i32>, T1 = T2 } } } }
//
// Impls:
// impl<T> Foo for Vec<T> where T: Bar { }
// impl<U> Foo for Vec<U> where U: Baz { }
// Generates:
// not { compatible { exists<T> { exists<U> { Vec<T> = Vec<U>, T: Bar, U: Baz } } } }
//
#[instrument(level = "debug", skip(self))]
fn disjoint(&self, lhs: &ImplDatum<I>, rhs: &ImplDatum<I>) -> bool {
let interner = self.db.interner();
let (lhs_binders, lhs_bound) = lhs.binders.as_ref().into();
let (rhs_binders, rhs_bound) = rhs.binders.as_ref().into();
// Upshift the rhs variables in params to account for the joined binders
let lhs_params = lhs_bound
.trait_ref
.substitution
.as_slice(interner)
.iter()
.cloned();
let rhs_params = rhs_bound
.trait_ref
.substitution
.as_slice(interner)
.iter()
.map(|param| param.clone().shifted_in(interner));
// Create an equality goal for every input type the trait, attempting
// to unify the inputs to both impls with one another
let params_goals = lhs_params
.zip(rhs_params)
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
// Upshift the rhs variables in where clauses
let lhs_where_clauses = lhs_bound.where_clauses.iter().cloned();
let rhs_where_clauses = rhs_bound
.where_clauses
.iter()
.map(|wc| wc.clone().shifted_in(interner));
// Create a goal for each clause in both where clauses
let wc_goals = lhs_where_clauses
.chain(rhs_where_clauses)
.map(|wc| wc.cast(interner));
// Join all the goals we've created together with And, then quantify them
// over the joined binders. This is our query.
let goal = Box::new(Goal::all(interner, params_goals.chain(wc_goals)))
.quantify(interner, QuantifierKind::Exists, lhs_binders)
.quantify(interner, QuantifierKind::Exists, rhs_binders)
.compatible(interner)
.negate(interner);
let canonical_goal = &goal.into_closed_goal(interner);
let mut fresh_solver = (self.solver_builder)();
let solution = fresh_solver.solve(self.db, canonical_goal);
let result = match solution {
// Goal was proven with a unique solution, so no impl was found that causes these two
// to overlap
Some(Solution::Unique(_)) => true,
// Goal was ambiguous, so there *may* be overlap
Some(Solution::Ambig(_)) |
// Goal cannot be proven, so there is some impl that causes overlap
None => false,
};
debug!("overlaps: result = {:?}", result);
result
}
// Creates a goal which, if provable, means "more special" impl specializes the "less special" one.
//
// # General rule
//
// Given the more special impl:
//
// ```ignore
// impl<P0..Pn> SomeTrait<T1..Tm> for T0 where WC_more
// ```
//
// and less special impl
//
// ```ignore
// impl<Q0..Qo> SomeTrait<U1..Um> for U0 where WC_less
// ```
//
// create the goal:
//
// ```ignore
// forall<P0..Pn> {
// if (WC_more) {}
// exists<Q0..Qo> {
// T0 = U0, ..., Tm = Um,
// WC_less
// }
// }
// }
// ```
//
// # Example
//
// Given:
//
// * more: `impl<T: Clone> Foo for Vec<T>`
// * less: `impl<U: Clone> Foo for U`
//
// Resulting goal:
//
// ```ignore
// forall<T> {
// if (T: Clone) {
// exists<U> {
// Vec<T> = U, U: Clone
// }
// }
// }
// ```
#[instrument(level = "debug", skip(self))]
fn specializes(&self, less_special_id: ImplId<I>, more_special_id: ImplId<I>) -> bool {
let more_special = &self.db.impl_datum(more_special_id);
let less_special = &self.db.impl_datum(less_special_id);
debug_span!("specializes", ?less_special, ?more_special);
let interner = self.db.interner();
let gb = &mut GoalBuilder::new(self.db);
// forall<P0..Pn> { ... }
let goal = gb.forall(
&more_special.binders,
less_special_id,
|gb, _, more_special_impl, less_special_id| {
// if (WC_more) { ... }
gb.implies(more_special_impl.where_clauses.iter().cloned(), |gb| {
let less_special = &gb.db().impl_datum(less_special_id);
// exists<Q0..Qn> { ... }
gb.exists(
&less_special.binders,
more_special_impl.trait_ref.clone(),
|gb, _, less_special_impl, more_special_trait_ref| {
let interner = gb.interner();
// T0 = U0, ..., Tm = Um
let params_goals = more_special_trait_ref
.substitution
.as_slice(interner)
.iter()
.cloned()
.zip(
less_special_impl
.trait_ref
.substitution
.as_slice(interner)
.iter()
.cloned(),
)
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));
// <less_special_wc_goals> = where clauses from the less special impl
let less_special_wc_goals = less_special_impl
.where_clauses
.iter()
.cloned()
.casted(interner);
// <equality_goals> && WC_less
gb.all(params_goals.chain(less_special_wc_goals))
},
)
})
},
);
let canonical_goal = &goal.into_closed_goal(interner);
let mut fresh_solver = (self.solver_builder)();
let result = fresh_solver.has_unique_solution(self.db, canonical_goal);
debug!("specializes: result = {:?}", result);
result
}
}