use std::{fmt, iter};
use crate::{
ext::*, goal_builder::GoalBuilder, rust_ir::*, solve::Solver, split::Split, RustIrDatabase,
};
use chalk_ir::{
cast::*,
fold::shift::Shift,
interner::Interner,
visit::{Visit, VisitResult, Visitor},
*,
};
use tracing::debug;
#[derive(Debug)]
pub enum WfError<I: Interner> {
IllFormedTypeDecl(chalk_ir::AdtId<I>),
IllFormedOpaqueTypeDecl(chalk_ir::OpaqueTyId<I>),
IllFormedTraitImpl(chalk_ir::TraitId<I>),
}
impl<I: Interner> fmt::Display for WfError<I> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
WfError::IllFormedTypeDecl(id) => write!(
f,
"type declaration `{:?}` does not meet well-formedness requirements",
id
),
WfError::IllFormedOpaqueTypeDecl(id) => write!(
f,
"opaque type declaration `{:?}` does not meet well-formedness requirements",
id
),
WfError::IllFormedTraitImpl(id) => write!(
f,
"trait impl for `{:?}` does not meet well-formedness requirements",
id
),
}
}
}
impl<I: Interner> std::error::Error for WfError<I> {}
pub struct WfSolver<'a, I: Interner> {
db: &'a dyn RustIrDatabase<I>,
solver_builder: &'a dyn Fn() -> Box<dyn Solver<I>>,
}
struct InputTypeCollector<'i, I: Interner> {
types: Vec<Ty<I>>,
interner: &'i I,
}
impl<'i, I: Interner> InputTypeCollector<'i, I> {
fn new(interner: &'i I) -> Self {
Self {
types: Vec::new(),
interner,
}
}
fn types_in(interner: &'i I, value: impl Visit<I>) -> Vec<Ty<I>> {
let mut collector = Self::new(interner);
value.visit_with(&mut collector, DebruijnIndex::INNERMOST);
collector.types
}
}
impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> {
type Result = ();
fn as_dyn(&mut self) -> &mut dyn Visitor<'i, I, Result = Self::Result> {
self
}
fn interner(&self) -> &'i I {
self.interner
}
fn visit_where_clause(&mut self, where_clause: &WhereClause<I>, outer_binder: DebruijnIndex) {
match where_clause {
WhereClause::AliasEq(alias_eq) => alias_eq
.alias
.clone()
.intern(self.interner)
.visit_with(self, outer_binder),
WhereClause::Implemented(trait_ref) => {
trait_ref.visit_with(self, outer_binder);
}
WhereClause::TypeOutlives(TypeOutlives { ty, .. }) => ty.visit_with(self, outer_binder),
WhereClause::LifetimeOutlives(..) => {}
}
}
fn visit_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) {
let interner = self.interner();
let mut push_ty = || {
self.types
.push(ty.shifted_out_to(interner, outer_binder).unwrap())
};
match ty.kind(interner) {
TyKind::Adt(id, substitution) => {
push_ty();
id.visit_with(self, outer_binder);
substitution.visit_with(self, outer_binder);
}
TyKind::AssociatedType(assoc_ty, substitution) => {
push_ty();
assoc_ty.visit_with(self, outer_binder);
substitution.visit_with(self, outer_binder);
}
TyKind::Scalar(scalar) => {
push_ty();
scalar.visit_with(self, outer_binder);
}
TyKind::Str => {
push_ty();
}
TyKind::Tuple(arity, substitution) => {
push_ty();
arity.visit_with(self, outer_binder);
substitution.visit_with(self, outer_binder);
}
TyKind::OpaqueType(opaque_ty, substitution) => {
push_ty();
opaque_ty.visit_with(self, outer_binder);
substitution.visit_with(self, outer_binder);
}
TyKind::Slice(substitution) => {
push_ty();
substitution.visit_with(self, outer_binder);
}
TyKind::FnDef(fn_def, substitution) => {
push_ty();
fn_def.visit_with(self, outer_binder);
substitution.visit_with(self, outer_binder);
}
TyKind::Ref(mutability, lifetime, ty) => {
push_ty();
mutability.visit_with(self, outer_binder);
lifetime.visit_with(self, outer_binder);
ty.visit_with(self, outer_binder);
}
TyKind::Raw(mutability, substitution) => {
push_ty();
mutability.visit_with(self, outer_binder);
substitution.visit_with(self, outer_binder);
}
TyKind::Never => {
push_ty();
}
TyKind::Array(ty, const_) => {
push_ty();
ty.visit_with(self, outer_binder)
.combine(const_.visit_with(self, outer_binder))
}
TyKind::Closure(_id, substitution) => {
push_ty();
substitution.visit_with(self, outer_binder);
}
TyKind::Generator(_generator, substitution) => {
push_ty();
substitution.visit_with(self, outer_binder);
}
TyKind::GeneratorWitness(_witness, substitution) => {
push_ty();
substitution.visit_with(self, outer_binder);
}
TyKind::Foreign(_foreign_ty) => {
push_ty();
}
TyKind::Error => {
push_ty();
}
TyKind::Dyn(clauses) => {
push_ty();
clauses.visit_with(self, outer_binder);
}
TyKind::Alias(AliasTy::Projection(proj)) => {
push_ty();
proj.visit_with(self, outer_binder);
}
TyKind::Alias(AliasTy::Opaque(opaque_ty)) => {
push_ty();
opaque_ty.visit_with(self, outer_binder);
}
TyKind::Placeholder(_) => {
push_ty();
}
TyKind::BoundVar(..) => (),
TyKind::Function(..) => (),
TyKind::InferenceVar(..) => {
panic!("unexpected inference variable in wf rules: {:?}", ty)
}
}
}
}
impl<'a, I> WfSolver<'a, I>
where
I: Interner,
{
pub fn new(
db: &'a dyn RustIrDatabase<I>,
solver_builder: &'a dyn Fn() -> Box<dyn Solver<I>>,
) -> Self {
Self { db, solver_builder }
}
pub fn verify_adt_decl(&self, adt_id: AdtId<I>) -> Result<(), WfError<I>> {
let interner = self.db.interner();
let adt_datum = self.db.adt_datum(adt_id);
let is_enum = adt_datum.kind == AdtKind::Enum;
let mut gb = GoalBuilder::new(self.db);
let adt_data = adt_datum
.binders
.map_ref(|b| (&b.variants, &b.where_clauses));
let wg_goal = gb.forall(
&adt_data,
is_enum,
|gb, _, (variants, where_clauses), is_enum| {
let interner = gb.interner();
gb.implies(
where_clauses
.iter()
.cloned()
.map(|wc| wc.into_from_env_goal(interner)),
|gb| {
let sub_goals: Vec<_> = variants
.iter()
.flat_map(|variant| {
let fields = &variant.fields;
let sized_constraint_goal =
WfWellKnownConstraints::struct_sized_constraint(
gb.db(),
fields,
is_enum,
);
let types = InputTypeCollector::types_in(
gb.interner(),
(&fields, &where_clauses),
);
types
.into_iter()
.map(|ty| ty.well_formed().cast(interner))
.chain(sized_constraint_goal.into_iter())
})
.collect();
gb.all(sub_goals)
},
)
},
);
let wg_goal = wg_goal.into_closed_goal(interner);
let mut fresh_solver = (self.solver_builder)();
let is_legal = fresh_solver.has_unique_solution(self.db, &wg_goal);
if !is_legal {
Err(WfError::IllFormedTypeDecl(adt_id))
} else {
Ok(())
}
}
pub fn verify_trait_impl(&self, impl_id: ImplId<I>) -> Result<(), WfError<I>> {
let interner = self.db.interner();
let impl_datum = self.db.impl_datum(impl_id);
let trait_id = impl_datum.trait_id();
let impl_goal = Goal::all(
interner,
impl_header_wf_goal(self.db, impl_id).into_iter().chain(
impl_datum
.associated_ty_value_ids
.iter()
.filter_map(|&id| compute_assoc_ty_goal(self.db, id)),
),
);
if let Some(well_known) = self.db.trait_datum(trait_id).well_known {
self.verify_well_known_impl(impl_id, well_known)?
}
debug!("WF trait goal: {:?}", impl_goal);
let mut fresh_solver = (self.solver_builder)();
let is_legal =
fresh_solver.has_unique_solution(self.db, &impl_goal.into_closed_goal(interner));
if is_legal {
Ok(())
} else {
Err(WfError::IllFormedTraitImpl(trait_id))
}
}
pub fn verify_opaque_ty_decl(&self, opaque_ty_id: OpaqueTyId<I>) -> Result<(), WfError<I>> {
let interner = self.db.interner();
let mut gb = GoalBuilder::new(self.db);
let datum = self.db.opaque_ty_data(opaque_ty_id);
let bound = &datum.bound;
let goal = gb.forall(&bound, opaque_ty_id, |gb, _, bound, opaque_ty_id| {
let interner = gb.interner();
let subst = Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id));
let bounds = bound.bounds.substitute(interner, &subst);
let where_clauses = bound.where_clauses.substitute(interner, &subst);
let clauses = where_clauses
.iter()
.cloned()
.map(|wc| wc.into_from_env_goal(interner));
gb.implies(clauses, |gb| {
let interner = gb.interner();
gb.all(
bounds
.iter()
.cloned()
.map(|b| b.into_well_formed_goal(interner)),
)
})
});
debug!("WF opaque type goal: {:#?}", goal);
let mut new_solver = (self.solver_builder)();
let is_legal = new_solver.has_unique_solution(self.db, &goal.into_closed_goal(interner));
if is_legal {
Ok(())
} else {
Err(WfError::IllFormedOpaqueTypeDecl(opaque_ty_id))
}
}
pub fn verify_well_known_impl(
&self,
impl_id: ImplId<I>,
well_known: WellKnownTrait,
) -> Result<(), WfError<I>> {
let mut solver = (self.solver_builder)();
let impl_datum = self.db.impl_datum(impl_id);
let is_legal = match well_known {
WellKnownTrait::Copy => {
WfWellKnownConstraints::copy_impl_constraint(&mut *solver, self.db, &impl_datum)
}
WellKnownTrait::Drop => {
WfWellKnownConstraints::drop_impl_constraint(&mut *solver, self.db, &impl_datum)
}
WellKnownTrait::CoerceUnsized => {
WfWellKnownConstraints::coerce_unsized_impl_constraint(
&mut *solver,
self.db,
&impl_datum,
)
}
WellKnownTrait::Clone | WellKnownTrait::Unpin => true,
WellKnownTrait::Fn
| WellKnownTrait::FnOnce
| WellKnownTrait::FnMut
| WellKnownTrait::Unsize
| WellKnownTrait::Sized => false,
};
if is_legal {
Ok(())
} else {
Err(WfError::IllFormedTraitImpl(impl_datum.trait_id()))
}
}
}
fn impl_header_wf_goal<I: Interner>(
db: &dyn RustIrDatabase<I>,
impl_id: ImplId<I>,
) -> Option<Goal<I>> {
let impl_datum = db.impl_datum(impl_id);
if !impl_datum.is_positive() {
return None;
}
let impl_fields = impl_datum
.binders
.map_ref(|v| (&v.trait_ref, &v.where_clauses));
let mut gb = GoalBuilder::new(db);
let well_formed_goal = gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| {
let interner = gb.interner();
gb.implies(
impl_wf_environment(interner, &where_clauses, &trait_ref),
|gb| {
let types = InputTypeCollector::types_in(gb.interner(), &where_clauses);
debug!(input_types=?types);
let goals = types
.into_iter()
.map(|ty| ty.well_formed().cast(interner))
.chain(Some((*trait_ref).clone().well_formed().cast(interner)));
gb.all::<_, Goal<I>>(goals)
},
)
});
Some(well_formed_goal)
}
fn impl_wf_environment<'i, I: Interner>(
interner: &'i I,
where_clauses: &'i [QuantifiedWhereClause<I>],
trait_ref: &'i TraitRef<I>,
) -> impl Iterator<Item = ProgramClause<I>> + 'i {
let wc = where_clauses
.iter()
.cloned()
.map(move |qwc| qwc.into_from_env_goal(interner).cast(interner));
let types = InputTypeCollector::types_in(interner, trait_ref);
let types_wf = types
.into_iter()
.map(move |ty| ty.into_from_env_goal(interner).cast(interner));
wc.chain(types_wf)
}
fn compute_assoc_ty_goal<I: Interner>(
db: &dyn RustIrDatabase<I>,
assoc_ty_id: AssociatedTyValueId<I>,
) -> Option<Goal<I>> {
let mut gb = GoalBuilder::new(db);
let assoc_ty = &db.associated_ty_value(assoc_ty_id);
Some(gb.forall(
&assoc_ty.value.map_ref(|v| &v.ty),
assoc_ty_id,
|gb, assoc_ty_substitution, value_ty, assoc_ty_id| {
let interner = gb.interner();
let db = gb.db();
let assoc_ty = &db.associated_ty_value(assoc_ty_id);
let (impl_parameters, projection) = db
.impl_parameters_and_projection_from_associated_ty_value(
&assoc_ty_substitution.as_slice(interner),
assoc_ty,
);
let impl_id = assoc_ty.impl_id;
let impl_datum = &db.impl_datum(impl_id);
let ImplDatumBound {
trait_ref: impl_trait_ref,
where_clauses: impl_where_clauses,
} = impl_datum.binders.substitute(interner, impl_parameters);
let impl_wf_clauses =
impl_wf_environment(interner, &impl_where_clauses, &impl_trait_ref);
gb.implies(impl_wf_clauses, |gb| {
let assoc_ty_datum = db.associated_ty_data(projection.associated_ty_id);
let AssociatedTyDatumBound {
bounds: defn_bounds,
where_clauses: defn_where_clauses,
} = assoc_ty_datum
.binders
.substitute(interner, &projection.substitution);
gb.implies(
defn_where_clauses
.iter()
.cloned()
.map(|qwc| qwc.into_from_env_goal(interner)),
|gb| {
let types = InputTypeCollector::types_in(gb.interner(), value_ty);
let wf_goals = types
.into_iter()
.map(|ty| ty.well_formed())
.casted(interner);
let bound_goals = defn_bounds
.iter()
.cloned()
.flat_map(|qb| qb.into_where_clauses(interner, (*value_ty).clone()))
.map(|qwc| qwc.into_well_formed_goal(interner))
.casted(interner);
gb.all::<_, Goal<I>>(wf_goals.chain(bound_goals))
},
)
})
},
))
}
struct WfWellKnownConstraints;
impl WfWellKnownConstraints {
pub fn struct_sized_constraint<I: Interner>(
db: &dyn RustIrDatabase<I>,
fields: &[Ty<I>],
size_all: bool,
) -> Option<Goal<I>> {
let excluded = if size_all { 0 } else { 1 };
if fields.len() <= excluded {
return None;
}
let interner = db.interner();
let sized_trait = db.well_known_trait_id(WellKnownTrait::Sized)?;
Some(Goal::all(
interner,
fields[..fields.len() - excluded].iter().map(|ty| {
TraitRef {
trait_id: sized_trait,
substitution: Substitution::from1(interner, ty.clone()),
}
.cast(interner)
}),
))
}
fn copy_impl_constraint<I: Interner>(
solver: &mut dyn Solver<I>,
db: &dyn RustIrDatabase<I>,
impl_datum: &ImplDatum<I>,
) -> bool {
let interner = db.interner();
let mut gb = GoalBuilder::new(db);
let impl_fields = impl_datum
.binders
.map_ref(|v| (&v.trait_ref, &v.where_clauses));
match impl_datum
.binders
.skip_binders()
.trait_ref
.self_type_parameter(interner)
.kind(interner)
{
TyKind::Scalar(_)
| TyKind::Raw(_, _)
| TyKind::Ref(Mutability::Not, _, _)
| TyKind::Never => return true,
TyKind::Adt(_, _) => (),
_ => return false,
};
let well_formed_goal =
gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| {
let interner = gb.interner();
let ty = trait_ref.self_type_parameter(interner);
let (adt_id, substitution) = match ty.kind(interner) {
TyKind::Adt(adt_id, substitution) => (*adt_id, substitution),
_ => unreachable!(),
};
gb.implies(
impl_wf_environment(interner, &where_clauses, &trait_ref),
|gb| -> Goal<I> {
let db = gb.db();
let neg_drop_goal =
db.well_known_trait_id(WellKnownTrait::Drop)
.map(|drop_trait_id| {
TraitRef {
trait_id: drop_trait_id,
substitution: Substitution::from1(interner, ty.clone()),
}
.cast::<Goal<I>>(interner)
.negate(interner)
});
let adt_datum = db.adt_datum(adt_id);
let goals = adt_datum
.binders
.map_ref(|b| &b.variants)
.substitute(interner, substitution)
.into_iter()
.flat_map(|v| {
v.fields.into_iter().map(|f| {
TraitRef {
trait_id: trait_ref.trait_id,
substitution: Substitution::from1(interner, f),
}
.cast(interner)
})
})
.chain(neg_drop_goal.into_iter());
gb.all(goals)
},
)
});
solver.has_unique_solution(db, &well_formed_goal.into_closed_goal(interner))
}
fn drop_impl_constraint<I: Interner>(
solver: &mut dyn Solver<I>,
db: &dyn RustIrDatabase<I>,
impl_datum: &ImplDatum<I>,
) -> bool {
let interner = db.interner();
let adt_id = match impl_datum.self_type_adt_id(interner) {
Some(id) => id,
None => return false,
};
let mut gb = GoalBuilder::new(db);
let adt_datum = db.adt_datum(adt_id);
let impl_fields = impl_datum
.binders
.map_ref(|v| (&v.trait_ref, &v.where_clauses));
let implied_by_adt_def_goal =
gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| {
let interner = gb.interner();
gb.implies(
iter::once(
FromEnv::Ty(trait_ref.self_type_parameter(interner))
.cast::<DomainGoal<I>>(interner),
),
|gb| {
gb.all(
where_clauses
.iter()
.map(|wc| wc.clone().into_well_formed_goal(interner)),
)
},
)
});
let impl_self_ty = impl_datum
.binders
.map_ref(|b| b.trait_ref.self_type_parameter(interner));
let eq_goal = gb.forall(
&adt_datum.binders,
(adt_id, impl_self_ty),
|gb, substitution, _, (adt_id, impl_self_ty)| {
let interner = gb.interner();
let def_adt = TyKind::Adt(adt_id, substitution).intern(interner);
gb.exists(&impl_self_ty, def_adt, |gb, _, impl_adt, def_adt| {
let interner = gb.interner();
GoalData::EqGoal(EqGoal {
a: GenericArgData::Ty(def_adt).intern(interner),
b: GenericArgData::Ty(impl_adt.clone()).intern(interner),
})
.intern(interner)
})
},
);
let well_formed_goal = gb.all([implied_by_adt_def_goal, eq_goal].iter());
solver.has_unique_solution(db, &well_formed_goal.into_closed_goal(interner))
}
fn coerce_unsized_impl_constraint<I: Interner>(
solver: &mut dyn Solver<I>,
db: &dyn RustIrDatabase<I>,
impl_datum: &ImplDatum<I>,
) -> bool {
let interner = db.interner();
let mut gb = GoalBuilder::new(db);
let (binders, impl_datum) = impl_datum.binders.as_ref().into();
let trait_ref: &TraitRef<I> = &impl_datum.trait_ref;
let source = trait_ref.self_type_parameter(interner);
let target = trait_ref
.substitution
.at(interner, 1)
.assert_ty_ref(interner)
.clone();
let mut place_in_environment = |goal| -> Goal<I> {
gb.forall(
&Binders::new(
binders.clone(),
(goal, trait_ref, &impl_datum.where_clauses),
),
(),
|gb, _, (goal, trait_ref, where_clauses), ()| {
let interner = gb.interner();
gb.implies(
impl_wf_environment(interner, &where_clauses, &trait_ref),
|_| goal,
)
},
)
};
match (source.kind(interner), target.kind(interner)) {
(TyKind::Ref(s_m, _, source), TyKind::Ref(t_m, _, target))
| (TyKind::Ref(s_m, _, source), TyKind::Raw(t_m, target))
| (TyKind::Raw(s_m, source), TyKind::Raw(t_m, target)) => {
if (*s_m, *t_m) == (Mutability::Not, Mutability::Mut) {
return false;
}
let unsize_trait_id =
if let Some(id) = db.well_known_trait_id(WellKnownTrait::Unsize) {
id
} else {
return false;
};
let unsize_goal: Goal<I> = TraitRef {
trait_id: unsize_trait_id,
substitution: Substitution::from_iter(
interner,
[source.clone(), target.clone()].iter().cloned(),
),
}
.cast(interner);
let unsize_goal = place_in_environment(unsize_goal);
solver.has_unique_solution(db, &unsize_goal.into_closed_goal(interner))
}
(TyKind::Adt(source_id, subst_a), TyKind::Adt(target_id, subst_b)) => {
let adt_datum = db.adt_datum(*source_id);
if source_id != target_id || adt_datum.kind != AdtKind::Struct {
return false;
}
let fields = adt_datum
.binders
.map_ref(|bound| &bound.variants.last().unwrap().fields);
let (source_fields, target_fields) = (
fields.substitute(interner, subst_a),
fields.substitute(interner, subst_b),
);
let uneq_field_ids: Vec<usize> = (0..source_fields.len())
.filter(|&i| {
if let Some(adt_id) = source_fields[i].adt_id(interner) {
if db.adt_datum(adt_id).flags.phantom_data {
return false;
}
}
let eq_goal: Goal<I> = EqGoal {
a: source_fields[i].clone().cast(interner),
b: target_fields[i].clone().cast(interner),
}
.cast(interner);
let eq_goal = place_in_environment(eq_goal);
!solver.has_unique_solution(db, &eq_goal.into_closed_goal(interner))
})
.collect();
if uneq_field_ids.len() != 1 {
return false;
}
let field_id = uneq_field_ids[0];
let coerce_unsized_goal: Goal<I> = TraitRef {
trait_id: trait_ref.trait_id,
substitution: Substitution::from_iter(
interner,
[
source_fields[field_id].clone(),
target_fields[field_id].clone(),
]
.iter()
.cloned(),
),
}
.cast(interner);
let coerce_unsized_goal = place_in_environment(coerce_unsized_goal);
solver.has_unique_solution(db, &coerce_unsized_goal.into_closed_goal(interner))
}
_ => false,
}
}
}