Skip to content

Commit 7cd2682

Browse files
borsbors
committed
Auto merge of #728 - matthewjasper:wf-clauses, r=jackh726
More clause fixes - Makes all traits with built-in implementations effectively non-enumerable - Handle clause generation for trait objects with escaping canonical vars - Check more things for some of the clauses for `WellFormed` - Make const generics have type `usize` in chalk-integration
2 parents 514a60a + f8ba227 commit 7cd2682

File tree

14 files changed

+304
-65
lines changed

14 files changed

+304
-65
lines changed

‎chalk-integration/src/lowering.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -107,8 +107,8 @@ lower_param_map!(
107107
))
108108
);
109109

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

114114
impl Lower for VariableKind {
@@ -128,7 +128,7 @@ impl Lower for VariableKind {
128128
n,
129129
),
130130
VariableKind::Lifetime(n) => (chalk_ir::VariableKind::Lifetime, n),
131-
VariableKind::Const(ref n) => (chalk_ir::VariableKind::Const(get_type_of_u32()), n),
131+
VariableKind::Const(ref n) => (chalk_ir::VariableKind::Const(get_type_of_usize()), n),
132132
};
133133

134134
chalk_ir::WithKind::new(kind, n.str.clone())
@@ -830,7 +830,7 @@ impl LowerWithEnv for Const {
830830
.map(|c| c.clone())
831831
}
832832
Const::Value(value) => Ok(chalk_ir::ConstData {
833-
ty: get_type_of_u32(),
833+
ty: get_type_of_usize(),
834834
value: chalk_ir::ConstValue::Concrete(chalk_ir::ConcreteConst { interned: *value }),
835835
}
836836
.intern(interner)),

‎chalk-solve/src/clauses.rs

Lines changed: 149 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ use chalk_ir::interner::Interner;
1111
use chalk_ir::*;
1212
use rustc_hash::FxHashSet;
1313
use std::iter;
14+
use std::marker::PhantomData;
1415
use tracing::{debug, instrument};
1516

1617
pub mod builder;
@@ -583,7 +584,7 @@ pub fn program_clauses_that_could_match<I: Interner>(
583584
| DomainGoal::IsUpstream(ty)
584585
| DomainGoal::DownstreamType(ty)
585586
| DomainGoal::IsFullyVisible(ty)
586-
| DomainGoal::IsLocal(ty) => match_ty(builder, environment, ty)?,
587+
| DomainGoal::IsLocal(ty) => match_ty(builder, environment, &ty)?,
587588
DomainGoal::FromEnv(_) => (), // Computed in the environment
588589
DomainGoal::Normalize(Normalize { alias, ty: _ }) => match alias {
589590
AliasTy::Projection(proj) => {
@@ -885,43 +886,150 @@ fn match_ty<I: Interner>(
885886
.db
886887
.fn_def_datum(*fn_def_id)
887888
.to_program_clauses(builder, environment),
888-
TyKind::Str | TyKind::Never | TyKind::Scalar(_) | TyKind::Foreign(_) => {
889+
TyKind::Str
890+
| TyKind::Never
891+
| TyKind::Scalar(_)
892+
| TyKind::Foreign(_)
893+
| TyKind::Tuple(0, _) => {
889894
// These have no substitutions, so they are trivially WF
890895
builder.push_fact(WellFormed::Ty(ty.clone()));
891896
}
892897
TyKind::Raw(mutbl, _) => {
898+
// forall<T> WF(*const T) :- WF(T);
893899
builder.push_bound_ty(|builder, ty| {
894-
builder.push_fact(WellFormed::Ty(
895-
TyKind::Raw(*mutbl, ty).intern(builder.interner()),
896-
));
900+
builder.push_clause(
901+
WellFormed::Ty(TyKind::Raw(*mutbl, ty.clone()).intern(builder.interner())),
902+
Some(WellFormed::Ty(ty)),
903+
);
897904
});
898905
}
899906
TyKind::Ref(mutbl, _, _) => {
907+
// forall<'a, T> WF(&'a T) :- WF(T), T: 'a
900908
builder.push_bound_ty(|builder, ty| {
901909
builder.push_bound_lifetime(|builder, lifetime| {
902-
builder.push_fact(WellFormed::Ty(
903-
TyKind::Ref(*mutbl, lifetime, ty).intern(builder.interner()),
904-
));
910+
let ref_ty = TyKind::Ref(*mutbl, lifetime.clone(), ty.clone())
911+
.intern(builder.interner());
912+
builder.push_clause(
913+
WellFormed::Ty(ref_ty),
914+
[
915+
DomainGoal::WellFormed(WellFormed::Ty(ty.clone())),
916+
DomainGoal::Holds(WhereClause::TypeOutlives(TypeOutlives {
917+
ty,
918+
lifetime,
919+
})),
920+
],
921+
);
905922
})
906923
});
907924
}
908925
TyKind::Slice(_) => {
926+
// forall<T> WF([T]) :- T: Sized, WF(T)
909927
builder.push_bound_ty(|builder, ty| {
910-
builder.push_fact(WellFormed::Ty(TyKind::Slice(ty).intern(builder.interner())));
928+
let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
929+
builder.push_clause(
930+
WellFormed::Ty(TyKind::Slice(ty.clone()).intern(builder.interner())),
931+
sized
932+
.map(|id| {
933+
DomainGoal::Holds(WhereClause::Implemented(TraitRef {
934+
trait_id: id,
935+
substitution: Substitution::from1(interner, ty.clone()),
936+
}))
937+
})
938+
.into_iter()
939+
.chain(Some(DomainGoal::WellFormed(WellFormed::Ty(ty)))),
940+
);
911941
});
912942
}
913-
TyKind::Tuple(_, _)
914-
| TyKind::Array(_, _)
915-
| TyKind::Closure(_, _)
916-
| TyKind::Generator(_, _)
917-
| TyKind::GeneratorWitness(_, _) => {
943+
TyKind::Array(..) => {
944+
// forall<T. const N: usize> WF([T, N]) :- T: Sized
945+
let interner = builder.interner();
946+
let binders = Binders::new(
947+
VariableKinds::from_iter(
948+
interner,
949+
[
950+
VariableKind::Ty(TyVariableKind::General),
951+
VariableKind::Const(
952+
TyKind::Scalar(Scalar::Uint(UintTy::Usize)).intern(interner),
953+
),
954+
],
955+
),
956+
PhantomData::<I>,
957+
);
958+
builder.push_binders(binders, |builder, PhantomData| {
959+
let placeholders_in_scope = builder.placeholders_in_scope();
960+
let placeholder_count = placeholders_in_scope.len();
961+
let ty = placeholders_in_scope[placeholder_count - 2]
962+
.assert_ty_ref(interner)
963+
.clone();
964+
let size = placeholders_in_scope[placeholder_count - 1]
965+
.assert_const_ref(interner)
966+
.clone();
967+
968+
let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
969+
let array_ty = TyKind::Array(ty.clone(), size).intern(interner);
970+
builder.push_clause(
971+
WellFormed::Ty(array_ty),
972+
sized
973+
.map(|id| {
974+
DomainGoal::Holds(WhereClause::Implemented(TraitRef {
975+
trait_id: id,
976+
substitution: Substitution::from1(interner, ty.clone()),
977+
}))
978+
})
979+
.into_iter()
980+
.chain(Some(DomainGoal::WellFormed(WellFormed::Ty(ty)))),
981+
);
982+
});
983+
}
984+
TyKind::Tuple(len, _) => {
985+
// WF((T0, ..., Tn, U)) :- T0: Sized, ..., Tn: Sized, WF(T0), ..., WF(Tn), WF(U)
986+
let interner = builder.interner();
987+
let binders = Binders::new(
988+
VariableKinds::from_iter(
989+
interner,
990+
iter::repeat_with(|| VariableKind::Ty(TyVariableKind::General)).take(*len),
991+
),
992+
PhantomData::<I>,
993+
);
994+
builder.push_binders(binders, |builder, PhantomData| {
995+
let placeholders_in_scope = builder.placeholders_in_scope();
996+
997+
let substs = Substitution::from_iter(
998+
builder.interner(),
999+
&placeholders_in_scope[placeholders_in_scope.len() - len..],
1000+
);
1001+
1002+
let tuple_ty = TyKind::Tuple(*len, substs.clone()).intern(interner);
1003+
let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
1004+
builder.push_clause(
1005+
WellFormed::Ty(tuple_ty),
1006+
substs.as_slice(interner)[..*len - 1]
1007+
.iter()
1008+
.filter_map(|s| {
1009+
let ty_var = s.assert_ty_ref(interner).clone();
1010+
sized.map(|id| {
1011+
DomainGoal::Holds(WhereClause::Implemented(TraitRef {
1012+
trait_id: id,
1013+
substitution: Substitution::from1(interner, ty_var),
1014+
}))
1015+
})
1016+
})
1017+
.chain(substs.iter(interner).map(|subst| {
1018+
DomainGoal::WellFormed(WellFormed::Ty(
1019+
subst.assert_ty_ref(interner).clone(),
1020+
))
1021+
})),
1022+
);
1023+
});
1024+
}
1025+
TyKind::Closure(_, _) | TyKind::Generator(_, _) | TyKind::GeneratorWitness(_, _) => {
9181026
let ty = generalize::Generalize::apply(builder.db.interner(), ty.clone());
9191027
builder.push_binders(ty, |builder, ty| {
9201028
builder.push_fact(WellFormed::Ty(ty.clone()));
9211029
});
9221030
}
9231031
TyKind::Placeholder(_) => {
924-
builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone())));
1032+
builder.push_fact(WellFormed::Ty(ty.clone()));
9251033
}
9261034
TyKind::Alias(AliasTy::Projection(proj)) => builder
9271035
.db
@@ -945,30 +1053,35 @@ fn match_ty<I: Interner>(
9451053
// - Bounds on the associated types
9461054
// - Checking that all associated types are specified, including
9471055
// those on supertraits.
948-
// - For trait objects with GATs, check that the bounds are fully
949-
// general (`dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
1056+
// - For trait objects with GATs, if we allow them in the future,
1057+
// check that the bounds are fully general (
1058+
// `dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
9501059
// `dyn StreamingIterator<Item<'static> = &'static ()>` is not).
951-
let bounds = dyn_ty
952-
.bounds
953-
.clone()
954-
.substitute(interner, &[ty.clone().cast::<GenericArg<I>>(interner)]);
955-
956-
let mut wf_goals = Vec::new();
957-
958-
wf_goals.extend(bounds.iter(interner).flat_map(|bound| {
959-
bound.map_ref(|bound| -> Vec<_> {
960-
match bound {
961-
WhereClause::Implemented(trait_ref) => {
962-
vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
1060+
let generalized_ty =
1061+
generalize::Generalize::apply(builder.db.interner(), dyn_ty.clone());
1062+
builder.push_binders(generalized_ty, |builder, dyn_ty| {
1063+
let bounds = dyn_ty
1064+
.bounds
1065+
.clone()
1066+
.substitute(interner, &[ty.clone().cast::<GenericArg<I>>(interner)]);
1067+
1068+
let mut wf_goals = Vec::new();
1069+
1070+
wf_goals.extend(bounds.iter(interner).flat_map(|bound| {
1071+
bound.map_ref(|bound| -> Vec<_> {
1072+
match bound {
1073+
WhereClause::Implemented(trait_ref) => {
1074+
vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
1075+
}
1076+
WhereClause::AliasEq(_)
1077+
| WhereClause::LifetimeOutlives(_)
1078+
| WhereClause::TypeOutlives(_) => vec![],
9631079
}
964-
WhereClause::AliasEq(_)
965-
| WhereClause::LifetimeOutlives(_)
966-
| WhereClause::TypeOutlives(_) => vec![],
967-
}
968-
})
969-
}));
1080+
})
1081+
}));
9701082

971-
builder.push_clause(WellFormed::Ty(ty.clone()), wf_goals);
1083+
builder.push_clause(WellFormed::Ty(ty.clone()), wf_goals);
1084+
});
9721085
}
9731086
})
9741087
}

‎chalk-solve/src/clauses/builtin_traits.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,10 @@ pub fn add_builtin_program_clauses<I: Interner>(
2828
let ty = self_ty.kind(db.interner()).clone();
2929

3030
match well_known {
31+
// There are no builtin impls provided for the following traits:
32+
WellKnownTrait::Unpin | WellKnownTrait::Drop | WellKnownTrait::CoerceUnsized => (),
33+
// Built-in traits are non-enumerable.
34+
_ if self_ty.is_general_var(db.interner(), binders) => return Err(Floundered),
3135
WellKnownTrait::Sized => {
3236
sized::add_sized_program_clauses(db, builder, trait_ref, ty, binders)?;
3337
}
@@ -48,8 +52,6 @@ pub fn add_builtin_program_clauses<I: Interner>(
4852
WellKnownTrait::Generator => {
4953
generator::add_generator_program_clauses(db, builder, self_ty)?;
5054
}
51-
// There are no builtin impls provided for the following traits:
52-
WellKnownTrait::Unpin | WellKnownTrait::Drop | WellKnownTrait::CoerceUnsized => (),
5355
}
5456
Ok(())
5557
})

‎chalk-solve/src/clauses/builtin_traits/fn_family.rs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -156,8 +156,6 @@ pub fn add_fn_trait_program_clauses<I: Interner>(
156156
});
157157
Ok(())
158158
}
159-
// Function traits are non-enumerable
160-
TyKind::InferenceVar(..) | TyKind::BoundVar(_) | TyKind::Alias(..) => Err(Floundered),
161159
_ => Ok(()),
162160
}
163161
}

‎tests/lowering/mod.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -806,8 +806,7 @@ fn algebraic_data_types() {
806806
type Owned: Borrow<Self>;
807807
}
808808

809-
// FIXME(#435) should be `B: 'a + ToOwned`
810-
enum Cow<'a, B> where B: ToOwned {
809+
enum Cow<'a, B> where B: ToOwned, B: 'a {
811810
Borrowed(&'a B),
812811
Owned(<B as ToOwned>::Owned),
813812
}

‎tests/test/arrays.rs

Lines changed: 24 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -102,16 +102,37 @@ fn arrays_are_not_clone_if_element_not_clone() {
102102
}
103103

104104
#[test]
105-
fn arrays_are_well_formed() {
105+
fn arrays_are_well_formed_if_elem_sized() {
106106
test! {
107-
program { }
107+
program {
108+
#[lang(sized)]
109+
trait Sized { }
110+
}
108111

109112
goal {
110113
forall<const N, T> {
111-
WellFormed([T; N])
114+
if (T: Sized) {
115+
WellFormed([T; N])
116+
}
112117
}
113118
} yields {
114119
"Unique"
115120
}
121+
122+
goal {
123+
forall<const N, T> {
124+
WellFormed([T; N])
125+
}
126+
} yields {
127+
"No possible solution"
128+
}
129+
130+
goal {
131+
exists<const N, T> {
132+
WellFormed([T; N])
133+
}
134+
} yields {
135+
"Ambiguous; no inference guidance"
136+
}
116137
}
117138
}

‎tests/test/cycle.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,6 @@ fn infinite_recursion() {
226226
fn cycle_with_ambiguity() {
227227
test! {
228228
program {
229-
#[non_enumerable]
230229
#[lang(sized)]
231230
trait Sized { }
232231
trait From<T> {}

‎tests/test/existential_types.rs

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -417,3 +417,20 @@ fn dyn_associated_type_binding() {
417417
}
418418
}
419419
}
420+
421+
#[test]
422+
fn dyn_well_formed() {
423+
test! {
424+
program {
425+
trait MyTrait {}
426+
}
427+
428+
goal {
429+
exists<'s> {
430+
WellFormed(dyn MyTrait + 's)
431+
}
432+
} yields {
433+
"Unique"
434+
}
435+
}
436+
}

‎tests/test/misc.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -815,7 +815,7 @@ fn env_bound_vars() {
815815
}
816816
}
817817
} yields {
818-
"Unique"
818+
"Ambiguous; definite substitution for<?U0> { [?0 := '^0.0] }"
819819
}
820820
goal {
821821
exists<'a> {

0 commit comments

Comments
 (0)