Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More clause fixes #728

Merged
merged 3 commits into from
Nov 28, 2021
Merged

More clause fixes #728

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d636c06
Use usize for const generics in chalk-integration
matthewjasper Nov 13, 2020
d66bfe9
Force builtin traits to be non-enumerable
matthewjasper Nov 13, 2020
f8ba227
Check more requirements in WF clauses
matthewjasper Nov 13, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions chalk-integration/src/lowering.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,8 +107,8 @@ lower_param_map!(
))
);

fn get_type_of_u32() -> chalk_ir::Ty<ChalkIr> {
chalk_ir::TyKind::Scalar(chalk_ir::Scalar::Uint(chalk_ir::UintTy::U32)).intern(&ChalkIr)
fn get_type_of_usize() -> chalk_ir::Ty<ChalkIr> {
chalk_ir::TyKind::Scalar(chalk_ir::Scalar::Uint(chalk_ir::UintTy::Usize)).intern(&ChalkIr)
}

impl Lower for VariableKind {
Expand All @@ -128,7 +128,7 @@ impl Lower for VariableKind {
n,
),
VariableKind::Lifetime(n) => (chalk_ir::VariableKind::Lifetime, n),
VariableKind::Const(ref n) => (chalk_ir::VariableKind::Const(get_type_of_u32()), n),
VariableKind::Const(ref n) => (chalk_ir::VariableKind::Const(get_type_of_usize()), n),
};

chalk_ir::WithKind::new(kind, n.str.clone())
Expand Down Expand Up @@ -830,7 +830,7 @@ impl LowerWithEnv for Const {
.map(|c| c.clone())
}
Const::Value(value) => Ok(chalk_ir::ConstData {
ty: get_type_of_u32(),
ty: get_type_of_usize(),
value: chalk_ir::ConstValue::Concrete(chalk_ir::ConcreteConst { interned: *value }),
}
.intern(interner)),
Expand Down
185 changes: 149 additions & 36 deletions chalk-solve/src/clauses.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ use chalk_ir::interner::Interner;
use chalk_ir::*;
use rustc_hash::FxHashSet;
use std::iter;
use std::marker::PhantomData;
use tracing::{debug, instrument};

pub mod builder;
Expand Down Expand Up @@ -583,7 +584,7 @@ pub fn program_clauses_that_could_match<I: Interner>(
| DomainGoal::IsUpstream(ty)
| DomainGoal::DownstreamType(ty)
| DomainGoal::IsFullyVisible(ty)
| DomainGoal::IsLocal(ty) => match_ty(builder, environment, ty)?,
| DomainGoal::IsLocal(ty) => match_ty(builder, environment, &ty)?,
DomainGoal::FromEnv(_) => (), // Computed in the environment
DomainGoal::Normalize(Normalize { alias, ty: _ }) => match alias {
AliasTy::Projection(proj) => {
Expand Down Expand Up @@ -885,43 +886,150 @@ fn match_ty<I: Interner>(
.db
.fn_def_datum(*fn_def_id)
.to_program_clauses(builder, environment),
TyKind::Str | TyKind::Never | TyKind::Scalar(_) | TyKind::Foreign(_) => {
TyKind::Str
| TyKind::Never
| TyKind::Scalar(_)
| TyKind::Foreign(_)
| TyKind::Tuple(0, _) => {
// These have no substitutions, so they are trivially WF
builder.push_fact(WellFormed::Ty(ty.clone()));
}
TyKind::Raw(mutbl, _) => {
// forall<T> WF(*const T) :- WF(T);
builder.push_bound_ty(|builder, ty| {
builder.push_fact(WellFormed::Ty(
TyKind::Raw(*mutbl, ty).intern(builder.interner()),
));
builder.push_clause(
WellFormed::Ty(TyKind::Raw(*mutbl, ty.clone()).intern(builder.interner())),
Some(WellFormed::Ty(ty)),
);
});
}
TyKind::Ref(mutbl, _, _) => {
// forall<'a, T> WF(&'a T) :- WF(T), T: 'a
builder.push_bound_ty(|builder, ty| {
builder.push_bound_lifetime(|builder, lifetime| {
builder.push_fact(WellFormed::Ty(
TyKind::Ref(*mutbl, lifetime, ty).intern(builder.interner()),
));
let ref_ty = TyKind::Ref(*mutbl, lifetime.clone(), ty.clone())
.intern(builder.interner());
builder.push_clause(
WellFormed::Ty(ref_ty),
[
DomainGoal::WellFormed(WellFormed::Ty(ty.clone())),
DomainGoal::Holds(WhereClause::TypeOutlives(TypeOutlives {
ty,
lifetime,
})),
],
);
})
});
}
TyKind::Slice(_) => {
// forall<T> WF([T]) :- T: Sized, WF(T)
builder.push_bound_ty(|builder, ty| {
builder.push_fact(WellFormed::Ty(TyKind::Slice(ty).intern(builder.interner())));
let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
builder.push_clause(
WellFormed::Ty(TyKind::Slice(ty.clone()).intern(builder.interner())),
sized
.map(|id| {
DomainGoal::Holds(WhereClause::Implemented(TraitRef {
trait_id: id,
substitution: Substitution::from1(interner, ty.clone()),
}))
})
.into_iter()
.chain(Some(DomainGoal::WellFormed(WellFormed::Ty(ty)))),
);
});
}
TyKind::Tuple(_, _)
| TyKind::Array(_, _)
| TyKind::Closure(_, _)
| TyKind::Generator(_, _)
| TyKind::GeneratorWitness(_, _) => {
TyKind::Array(..) => {
// forall<T. const N: usize> WF([T, N]) :- T: Sized
let interner = builder.interner();
let binders = Binders::new(
VariableKinds::from_iter(
interner,
[
VariableKind::Ty(TyVariableKind::General),
VariableKind::Const(
TyKind::Scalar(Scalar::Uint(UintTy::Usize)).intern(interner),
),
],
),
PhantomData::<I>,
);
builder.push_binders(binders, |builder, PhantomData| {
let placeholders_in_scope = builder.placeholders_in_scope();
let placeholder_count = placeholders_in_scope.len();
let ty = placeholders_in_scope[placeholder_count - 2]
.assert_ty_ref(interner)
.clone();
let size = placeholders_in_scope[placeholder_count - 1]
.assert_const_ref(interner)
.clone();

let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
let array_ty = TyKind::Array(ty.clone(), size).intern(interner);
builder.push_clause(
WellFormed::Ty(array_ty),
sized
.map(|id| {
DomainGoal::Holds(WhereClause::Implemented(TraitRef {
trait_id: id,
substitution: Substitution::from1(interner, ty.clone()),
}))
})
.into_iter()
.chain(Some(DomainGoal::WellFormed(WellFormed::Ty(ty)))),
);
});
}
TyKind::Tuple(len, _) => {
// WF((T0, ..., Tn, U)) :- T0: Sized, ..., Tn: Sized, WF(T0), ..., WF(Tn), WF(U)
let interner = builder.interner();
let binders = Binders::new(
VariableKinds::from_iter(
interner,
iter::repeat_with(|| VariableKind::Ty(TyVariableKind::General)).take(*len),
),
PhantomData::<I>,
);
builder.push_binders(binders, |builder, PhantomData| {
let placeholders_in_scope = builder.placeholders_in_scope();

let substs = Substitution::from_iter(
builder.interner(),
&placeholders_in_scope[placeholders_in_scope.len() - len..],
);

let tuple_ty = TyKind::Tuple(*len, substs.clone()).intern(interner);
let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
builder.push_clause(
WellFormed::Ty(tuple_ty),
substs.as_slice(interner)[..*len - 1]
.iter()
.filter_map(|s| {
let ty_var = s.assert_ty_ref(interner).clone();
sized.map(|id| {
DomainGoal::Holds(WhereClause::Implemented(TraitRef {
trait_id: id,
substitution: Substitution::from1(interner, ty_var),
}))
})
})
.chain(substs.iter(interner).map(|subst| {
DomainGoal::WellFormed(WellFormed::Ty(
subst.assert_ty_ref(interner).clone(),
))
})),
);
});
}
TyKind::Closure(_, _) | TyKind::Generator(_, _) | TyKind::GeneratorWitness(_, _) => {
let ty = generalize::Generalize::apply(builder.db.interner(), ty.clone());
builder.push_binders(ty, |builder, ty| {
builder.push_fact(WellFormed::Ty(ty.clone()));
});
}
TyKind::Placeholder(_) => {
builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone())));
builder.push_fact(WellFormed::Ty(ty.clone()));
}
TyKind::Alias(AliasTy::Projection(proj)) => builder
.db
Expand All @@ -945,30 +1053,35 @@ fn match_ty<I: Interner>(
// - Bounds on the associated types
// - Checking that all associated types are specified, including
// those on supertraits.
// - For trait objects with GATs, check that the bounds are fully
// general (`dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
// - For trait objects with GATs, if we allow them in the future,
// check that the bounds are fully general (
// `dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
// `dyn StreamingIterator<Item<'static> = &'static ()>` is not).
let bounds = dyn_ty
.bounds
.clone()
.substitute(interner, &[ty.clone().cast::<GenericArg<I>>(interner)]);

let mut wf_goals = Vec::new();

wf_goals.extend(bounds.iter(interner).flat_map(|bound| {
bound.map_ref(|bound| -> Vec<_> {
match bound {
WhereClause::Implemented(trait_ref) => {
vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
let generalized_ty =
generalize::Generalize::apply(builder.db.interner(), dyn_ty.clone());
builder.push_binders(generalized_ty, |builder, dyn_ty| {
let bounds = dyn_ty
.bounds
.clone()
.substitute(interner, &[ty.clone().cast::<GenericArg<I>>(interner)]);

let mut wf_goals = Vec::new();

wf_goals.extend(bounds.iter(interner).flat_map(|bound| {
bound.map_ref(|bound| -> Vec<_> {
match bound {
WhereClause::Implemented(trait_ref) => {
vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
}
WhereClause::AliasEq(_)
| WhereClause::LifetimeOutlives(_)
| WhereClause::TypeOutlives(_) => vec![],
}
WhereClause::AliasEq(_)
| WhereClause::LifetimeOutlives(_)
| WhereClause::TypeOutlives(_) => vec![],
}
})
}));
})
}));

builder.push_clause(WellFormed::Ty(ty.clone()), wf_goals);
builder.push_clause(WellFormed::Ty(ty.clone()), wf_goals);
});
}
})
}
Expand Down
6 changes: 4 additions & 2 deletions chalk-solve/src/clauses/builtin_traits.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,10 @@ pub fn add_builtin_program_clauses<I: Interner>(
let ty = self_ty.kind(db.interner()).clone();

match well_known {
// There are no builtin impls provided for the following traits:
WellKnownTrait::Unpin | WellKnownTrait::Drop | WellKnownTrait::CoerceUnsized => (),
// Built-in traits are non-enumerable.
_ if self_ty.is_general_var(db.interner(), binders) => return Err(Floundered),
WellKnownTrait::Sized => {
sized::add_sized_program_clauses(db, builder, trait_ref, ty, binders)?;
}
Expand All @@ -48,8 +52,6 @@ pub fn add_builtin_program_clauses<I: Interner>(
WellKnownTrait::Generator => {
generator::add_generator_program_clauses(db, builder, self_ty)?;
}
// There are no builtin impls provided for the following traits:
WellKnownTrait::Unpin | WellKnownTrait::Drop | WellKnownTrait::CoerceUnsized => (),
}
Ok(())
})
Expand Down
2 changes: 0 additions & 2 deletions chalk-solve/src/clauses/builtin_traits/fn_family.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,8 +156,6 @@ pub fn add_fn_trait_program_clauses<I: Interner>(
});
Ok(())
}
// Function traits are non-enumerable
TyKind::InferenceVar(..) | TyKind::BoundVar(_) | TyKind::Alias(..) => Err(Floundered),
_ => Ok(()),
}
}
3 changes: 1 addition & 2 deletions tests/lowering/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -806,8 +806,7 @@ fn algebraic_data_types() {
type Owned: Borrow<Self>;
}

// FIXME(#435) should be `B: 'a + ToOwned`
enum Cow<'a, B> where B: ToOwned {
enum Cow<'a, B> where B: ToOwned, B: 'a {
Borrowed(&'a B),
Owned(<B as ToOwned>::Owned),
}
Expand Down
27 changes: 24 additions & 3 deletions tests/test/arrays.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,16 +102,37 @@ fn arrays_are_not_clone_if_element_not_clone() {
}

#[test]
fn arrays_are_well_formed() {
fn arrays_are_well_formed_if_elem_sized() {
test! {
program { }
program {
#[lang(sized)]
trait Sized { }
}

goal {
forall<const N, T> {
WellFormed([T; N])
if (T: Sized) {
WellFormed([T; N])
}
}
} yields {
"Unique"
}

goal {
forall<const N, T> {
WellFormed([T; N])
}
} yields {
"No possible solution"
}

goal {
exists<const N, T> {
WellFormed([T; N])
}
} yields {
"Ambiguous; no inference guidance"
}
}
}
1 change: 0 additions & 1 deletion tests/test/cycle.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -226,7 +226,6 @@ fn infinite_recursion() {
fn cycle_with_ambiguity() {
test! {
program {
#[non_enumerable]
#[lang(sized)]
trait Sized { }
trait From<T> {}
Expand Down
17 changes: 17 additions & 0 deletions tests/test/existential_types.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -417,3 +417,20 @@ fn dyn_associated_type_binding() {
}
}
}

#[test]
fn dyn_well_formed() {
test! {
program {
trait MyTrait {}
}

goal {
exists<'s> {
WellFormed(dyn MyTrait + 's)
}
} yields {
"Unique"
}
}
}
2 changes: 1 addition & 1 deletion tests/test/misc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -815,7 +815,7 @@ fn env_bound_vars() {
}
}
} yields {
"Unique"
"Ambiguous; definite substitution for<?U0> { [?0 := '^0.0] }"
}
goal {
exists<'a> {
Expand Down
Loading