Skip to content

Commit 7a90a0a

Browse files
committed
Make DispatchFromDyn a well-known trait
Signed-off-by: Nick Cameron <nrc@ncameron.org>
1 parent 82cf22a commit 7a90a0a

File tree

7 files changed

+146
-2
lines changed

7 files changed

+146
-2
lines changed

chalk-integration/src/lowering.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1138,6 +1138,7 @@ impl Lower for WellKnownTrait {
11381138
WellKnownTrait::CoerceUnsized => rust_ir::WellKnownTrait::CoerceUnsized,
11391139
WellKnownTrait::DiscriminantKind => rust_ir::WellKnownTrait::DiscriminantKind,
11401140
WellKnownTrait::Generator => rust_ir::WellKnownTrait::Generator,
1141+
WellKnownTrait::DispatchFromDyn => rust_ir::WellKnownTrait::DispatchFromDyn,
11411142
}
11421143
}
11431144
}

chalk-parse/src/ast.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -159,6 +159,7 @@ pub enum WellKnownTrait {
159159
CoerceUnsized,
160160
DiscriminantKind,
161161
Generator,
162+
DispatchFromDyn,
162163
}
163164

164165
#[derive(Clone, PartialEq, Eq, Debug)]

chalk-parse/src/parser.lalrpop

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@ WellKnownTrait: WellKnownTrait = {
6767
"#" "[" "lang" "(" "coerce_unsized" ")" "]" => WellKnownTrait::CoerceUnsized,
6868
"#" "[" "lang" "(" "discriminant_kind" ")" "]" => WellKnownTrait::DiscriminantKind,
6969
"#" "[" "lang" "(" "generator" ")" "]" => WellKnownTrait::Generator,
70+
"#" "[" "lang" "(" "dispatch_from_dyn" ")" "]" => WellKnownTrait::DispatchFromDyn,
7071
};
7172

7273
AdtReprAttr: AdtReprAttr = {

chalk-solve/src/clauses/builtin_traits.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,6 @@ 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 => (),
3331
// Built-in traits are non-enumerable.
3432
_ if self_ty.is_general_var(db.interner(), binders) => return Err(Floundered),
3533
WellKnownTrait::Sized => {
@@ -52,6 +50,11 @@ pub fn add_builtin_program_clauses<I: Interner>(
5250
WellKnownTrait::Generator => {
5351
generator::add_generator_program_clauses(db, builder, self_ty)?;
5452
}
53+
// There are no builtin impls provided for the following traits:
54+
WellKnownTrait::Unpin
55+
| WellKnownTrait::Drop
56+
| WellKnownTrait::CoerceUnsized
57+
| WellKnownTrait::DispatchFromDyn => (),
5558
}
5659
Ok(())
5760
})

chalk-solve/src/display/items.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,7 @@ impl<I: Interner> RenderAsRust<I> for TraitDatum<I> {
204204
WellKnownTrait::CoerceUnsized => "coerce_unsized",
205205
WellKnownTrait::DiscriminantKind => "discriminant_kind",
206206
WellKnownTrait::Generator => "generator",
207+
WellKnownTrait::DispatchFromDyn => "dispatch_from_dyn",
207208
};
208209
writeln!(f, "#[lang({})]", name)?;
209210
}

chalk-solve/src/rust_ir.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -259,6 +259,7 @@ pub enum WellKnownTrait {
259259
CoerceUnsized,
260260
DiscriminantKind,
261261
Generator,
262+
DispatchFromDyn,
262263
}
263264

264265
chalk_ir::const_visit!(WellKnownTrait);

chalk-solve/src/wf.rs

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -420,6 +420,13 @@ where
420420
&impl_datum,
421421
)
422422
}
423+
WellKnownTrait::DispatchFromDyn => {
424+
WfWellKnownConstraints::dispatch_from_dyn_constraint(
425+
&mut *solver,
426+
self.db,
427+
&impl_datum,
428+
)
429+
}
423430
WellKnownTrait::Clone | WellKnownTrait::Unpin => true,
424431
// You can't add a manual implementation for the following traits:
425432
WellKnownTrait::Fn
@@ -1061,4 +1068,133 @@ impl WfWellKnownConstraints {
10611068
_ => false,
10621069
}
10631070
}
1071+
1072+
/// Verify constraints ofa DispatchForDyn impl.
1073+
///
1074+
/// Rules for DispatchForDyn impl to be considered well-formed:
1075+
///
1076+
/// * Self and the type parameter must both be references or raw pointers with the same mutabilty
1077+
/// * OR all the following hold:
1078+
/// - Self and the type parameter must be structs
1079+
/// - Self and the type parameter must have the same definitions
1080+
/// - Self must not be `#[repr(packed)]` or `#[repr(C)]`
1081+
/// - Self must have exactly one field which is not a 1-ZST, and that field must have a
1082+
/// different type in the type parameter (i.e., it is a field being coerced)
1083+
/// - `DispatchForDyn` is implemented for the type of the field being coerced.
1084+
fn dispatch_from_dyn_constraint<I: Interner>(
1085+
solver: &mut dyn Solver<I>,
1086+
db: &dyn RustIrDatabase<I>,
1087+
impl_datum: &ImplDatum<I>,
1088+
) -> bool {
1089+
let interner = db.interner();
1090+
let mut gb = GoalBuilder::new(db);
1091+
1092+
let (binders, impl_datum) = impl_datum.binders.as_ref().into();
1093+
1094+
let trait_ref: &TraitRef<I> = &impl_datum.trait_ref;
1095+
1096+
// DispatchForDyn specifies that Self (source) can be coerced to T (target; its single type parameter).
1097+
let source = trait_ref.self_type_parameter(interner);
1098+
let target = trait_ref
1099+
.substitution
1100+
.at(interner, 1)
1101+
.assert_ty_ref(interner)
1102+
.clone();
1103+
1104+
let mut place_in_environment = |goal| -> Goal<I> {
1105+
gb.forall(
1106+
&Binders::new(
1107+
binders.clone(),
1108+
(goal, trait_ref, &impl_datum.where_clauses),
1109+
),
1110+
(),
1111+
|gb, _, (goal, trait_ref, where_clauses), ()| {
1112+
let interner = gb.interner();
1113+
gb.implies(
1114+
impl_wf_environment(interner, &where_clauses, &trait_ref),
1115+
|_| goal,
1116+
)
1117+
},
1118+
)
1119+
};
1120+
1121+
match (source.kind(interner), target.kind(interner)) {
1122+
(TyKind::Ref(s_m, _, _), TyKind::Ref(t_m, _, _))
1123+
| (TyKind::Raw(s_m, _), TyKind::Raw(t_m, _))
1124+
if s_m != t_m =>
1125+
{
1126+
true
1127+
}
1128+
(TyKind::Adt(source_id, subst_a), TyKind::Adt(target_id, subst_b)) => {
1129+
let adt_datum = db.adt_datum(*source_id);
1130+
1131+
// Definitions are equal and are structs.
1132+
if source_id != target_id || adt_datum.kind != AdtKind::Struct {
1133+
return false;
1134+
}
1135+
1136+
// Not repr(C) or repr(packed).
1137+
let repr = db.adt_repr(*source_id);
1138+
if repr.c || repr.packed {
1139+
return false;
1140+
}
1141+
1142+
// Collect non 1-ZST fields; there must be exactly one.
1143+
let fields = adt_datum
1144+
.binders
1145+
.map_ref(|bound| &bound.variants.last().unwrap().fields)
1146+
.cloned();
1147+
1148+
let (source_fields, target_fields) = (
1149+
fields.clone().substitute(interner, subst_a),
1150+
fields.substitute(interner, subst_b),
1151+
);
1152+
1153+
let mut non_zst_fields: Vec<_> = source_fields
1154+
.iter()
1155+
.zip(target_fields.iter())
1156+
.filter(|(sf, tf)| {
1157+
// TODO ignore 1-ZST fields
1158+
true
1159+
})
1160+
.collect();
1161+
1162+
if non_zst_fields.len() != 1 {
1163+
return false;
1164+
}
1165+
1166+
// The field being coerced (the interesting field).
1167+
let (field_src, field_tgt) = non_zst_fields.pop().unwrap();
1168+
1169+
// The interesting field is different in the source and target types.
1170+
let eq_goal: Goal<I> = EqGoal {
1171+
a: field_src.clone().cast(interner),
1172+
b: field_tgt.clone().cast(interner),
1173+
}
1174+
.cast(interner);
1175+
let eq_goal = place_in_environment(eq_goal);
1176+
if solver.has_unique_solution(db, &eq_goal.into_closed_goal(interner)) {
1177+
return false;
1178+
}
1179+
1180+
// Type(field_src): DispatchForDyn<Type(field_tgt)>
1181+
let field_dispatch_goal: Goal<I> = TraitRef {
1182+
trait_id: trait_ref.trait_id,
1183+
substitution: Substitution::from_iter(
1184+
interner,
1185+
[field_src.clone(), field_tgt.clone()].iter().cloned(),
1186+
),
1187+
}
1188+
.cast(interner);
1189+
let field_dispatch_goal = place_in_environment(field_dispatch_goal);
1190+
if !solver.has_unique_solution(db, &field_dispatch_goal.into_closed_goal(interner))
1191+
{
1192+
return false;
1193+
}
1194+
1195+
true
1196+
}
1197+
_ => false,
1198+
}
1199+
}
10641200
}

0 commit comments

Comments
 (0)