Handle scalars and tuples for the builtin Sized trait

Author: marmeladema

chalk-solve/src/clauses/builtin_traits.rs

@@ -1,6 +1,6 @@
 use super::builder::ClauseBuilder;
 use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
-use chalk_ir::TyData;
+use chalk_ir::{Substitution, Ty, TyData};
 
 mod clone;
 mod copy;
@@ -30,3 +30,27 @@ pub fn add_builtin_program_clauses<I: Interner>(
         WellKnownTrait::DropTrait => (),
     }
 }
+
+/// Given a trait ref `T0: Trait` and a list of types `U0..Un`, pushes a clause of the form
+/// `Implemented(T0: Trait) :- Implemented(U0: Trait) .. Implemented(Un: Trait)`
+pub fn needs_impl_for_tys<I: Interner>(
+    db: &dyn RustIrDatabase<I>,
+    builder: &mut ClauseBuilder<'_, I>,
+    trait_ref: &TraitRef<I>,
+    tys: impl Iterator<Item = Ty<I>>,
+) {
+    // The trait must take one parameter (a type)
+    debug_assert_eq!(
+        db.trait_datum(trait_ref.trait_id)
+            .binders
+            .len(db.interner()),
+        1,
+    );
+    builder.push_clause(
+        trait_ref.clone(),
+        tys.map(|ty| TraitRef {
+            trait_id: trait_ref.trait_id,
+            substitution: Substitution::from1(db.interner(), ty),
+        }),
+    );
+}

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

@@ -1,27 +1,17 @@
 use std::iter;
 
+use crate::clauses::builtin_traits::needs_impl_for_tys;
 use crate::clauses::ClauseBuilder;
 use crate::{Interner, RustIrDatabase, TraitRef};
-use chalk_ir::{ApplicationTy, Substitution, TyData, TypeName};
+use chalk_ir::{ApplicationTy, StructId, Substitution, TyData, TypeName};
 
-pub fn add_sized_program_clauses<I: Interner>(
+fn push_struct_sized_conditions<I: Interner>(
     db: &dyn RustIrDatabase<I>,
     builder: &mut ClauseBuilder<'_, I>,
     trait_ref: &TraitRef<I>,
-    ty: &TyData<I>,
+    struct_id: StructId<I>,
+    substitution: &Substitution<I>,
 ) {
-    let interner = db.interner();
-
-    let (struct_id, substitution) = match ty {
-        TyData::Apply(ApplicationTy {
-            name: TypeName::Struct(struct_id),
-            substitution,
-        }) => (*struct_id, substitution),
-        // TODO(areredify)
-        // when #368 lands, extend this to handle everything accordingly
-        _ => return,
-    };
-
     let struct_datum = db.struct_datum(struct_id);
 
     // Structs with no fields are always Sized
@@ -30,16 +20,65 @@ pub fn add_sized_program_clauses<I: Interner>(
         return;
     }
 
+    let interner = db.interner();
+
     // To check if a struct type S<..> is Sized, we only have to look at its last field.
     // This is because the WF checks for structs require that all the other fields must be Sized.
     let last_field_ty = struct_datum
         .binders
         .map_ref(|b| b.fields.last().unwrap())
         .substitute(interner, substitution);
 
-    let last_field_sized_goal = TraitRef {
-        trait_id: trait_ref.trait_id,
-        substitution: Substitution::from1(interner, last_field_ty),
-    };
-    builder.push_clause(trait_ref.clone(), iter::once(last_field_sized_goal));
+    needs_impl_for_tys(db, builder, trait_ref, iter::once(last_field_ty));
+}
+
+fn push_tuple_sized_conditions<I: Interner>(
+    db: &dyn RustIrDatabase<I>,
+    builder: &mut ClauseBuilder<'_, I>,
+    trait_ref: &TraitRef<I>,
+    arity: usize,
+    substitution: &Substitution<I>,
+) {
+    // Empty tuples are always Sized
+    if arity == 0 {
+        builder.push_fact(trait_ref.clone());
+        return;
+    }
+
+    let interner = db.interner();
+
+    // To check if a tuple is Sized, we only have to look at its last element.
+    // This is because the WF checks for tuples require that all the other elements must be Sized.
+    let last_elem_ty = substitution
+        .iter(interner)
+        .last()
+        .unwrap()
+        .ty(interner)
+        .unwrap()
+        .clone();
+
+    needs_impl_for_tys(db, builder, trait_ref, iter::once(last_elem_ty));
+}
+
+pub fn add_sized_program_clauses<I: Interner>(
+    db: &dyn RustIrDatabase<I>,
+    builder: &mut ClauseBuilder<'_, I>,
+    trait_ref: &TraitRef<I>,
+    ty: &TyData<I>,
+) {
+    match ty {
+        TyData::Apply(ApplicationTy { name, substitution }) => match name {
+            TypeName::Struct(struct_id) => {
+                push_struct_sized_conditions(db, builder, trait_ref, *struct_id, substitution)
+            }
+            TypeName::Scalar(_) => builder.push_fact(trait_ref.clone()),
+            TypeName::Tuple(arity) => {
+                push_tuple_sized_conditions(db, builder, trait_ref, *arity, substitution)
+            }
+            _ => return,
+        },
+        // TODO(areredify)
+        // when #368 lands, extend this to handle everything accordingly
+        _ => return,
+    }
 }

tests/test/scalars.rs

@@ -136,3 +136,29 @@ fn scalars_are_well_formed() {
         goal { WellFormed(char) } yields { "Unique" }
     }
 }
+
+#[test]
+fn scalars_are_sized() {
+    test! {
+        program {
+            #[lang(sized)] trait Sized { }
+        }
+
+        goal { i8: Sized } yields { "Unique" }
+        goal { i16: Sized } yields { "Unique" }
+        goal { i32: Sized } yields { "Unique" }
+        goal { i64: Sized } yields { "Unique" }
+        goal { i128: Sized } yields { "Unique" }
+        goal { isize: Sized } yields { "Unique" }
+        goal { u8: Sized } yields { "Unique" }
+        goal { u16: Sized } yields { "Unique" }
+        goal { u32: Sized } yields { "Unique" }
+        goal { u64: Sized } yields { "Unique" }
+        goal { u128: Sized } yields { "Unique" }
+        goal { usize: Sized } yields { "Unique" }
+        goal { f32: Sized } yields { "Unique" }
+        goal { f64: Sized } yields { "Unique" }
+        goal { bool: Sized } yields { "Unique" }
+        goal { char: Sized } yields { "Unique" }
+    }
+}

tests/test/tuples.rs

@@ -34,3 +34,53 @@ fn tuple_trait_impl() {
         }
     }
 }
+
+#[test]
+fn tuples_are_sized() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+
+            trait Foo {}
+        }
+
+        goal {
+            (dyn Foo,): Sized
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            (u8, dyn Foo): Sized
+        } yields {
+            "No possible solution"
+        }
+
+        // It should not be well-formed because for tuples, only
+        // the last element is allowed not to be Sized.
+        goal {
+            (dyn Foo, u8): Sized
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            (): Sized
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            (u8,): Sized
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            (u8, u8): Sized
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}