add Sized well-known impl and wf check

chalk-integration/src/db.rs

@@ -21,6 +21,7 @@ use chalk_rust_ir::AssociatedTyDatum;
 use chalk_rust_ir::AssociatedTyValue;
 use chalk_rust_ir::AssociatedTyValueId;
 use chalk_rust_ir::ImplDatum;
+use chalk_rust_ir::LangItem;
 use chalk_rust_ir::StructDatum;
 use chalk_rust_ir::TraitDatum;
 use chalk_solve::RustIrDatabase;
@@ -137,6 +138,10 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
             .impl_provided_for(auto_trait_id, struct_id)
     }
 
+    fn require_lang_item(&self, lang_item: LangItem) -> TraitId<ChalkIr> {
+        self.program_ir().unwrap().require_lang_item(lang_item)
+    }
+
     fn interner(&self) -> &ChalkIr {
         &ChalkIr
     }

chalk-integration/src/lowering.rs

@@ -3,7 +3,7 @@ use chalk_ir::interner::ChalkIr;
 use chalk_ir::{self, AssocTypeId, BoundVar, DebruijnIndex, ImplId, StructId, TraitId};
 use chalk_parse::ast::*;
 use chalk_rust_ir as rust_ir;
-use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, ToParameter};
+use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, LangItem, ToParameter};
 use lalrpop_intern::intern;
 use std::collections::BTreeMap;
 use std::sync::Arc;
@@ -246,6 +246,7 @@ impl LowerProgram for Program {
 
         let mut struct_data = BTreeMap::new();
         let mut trait_data = BTreeMap::new();
+        let mut trait_lang_items = BTreeMap::new();
         let mut impl_data = BTreeMap::new();
         let mut associated_ty_data = BTreeMap::new();
         let mut associated_ty_values = BTreeMap::new();
@@ -267,10 +268,24 @@ impl LowerProgram for Program {
                 }
                 Item::TraitDefn(ref trait_defn) => {
                     let trait_id = TraitId(raw_id);
-                    trait_data.insert(
-                        trait_id,
-                        Arc::new(trait_defn.lower_trait(trait_id, &empty_env)?),
-                    );
+                    let trait_datum = trait_defn.lower_trait(trait_id, &empty_env)?;
+
+                    if let Some(well_known) = trait_datum.well_known {
+                        if let Some(lang_item) = match well_known {
+                            rust_ir::WellKnownTrait::SizedTrait => Some(LangItem::SizedTrait),
+                            _ => None,
+                        } {
+                            use std::collections::btree_map::Entry;
+                            match trait_lang_items.entry(lang_item) {
+                                Entry::Vacant(vacant) => vacant.insert(trait_id),
+                                Entry::Occupied(_) => {
+                                    return Err(RustIrError::DuplicateLangItem(lang_item))
+                                }
+                            };
+                        }
+                    }
+
+                    trait_data.insert(trait_id, Arc::new(trait_datum));
 
                     for assoc_ty_defn in &trait_defn.assoc_ty_defns {
                         let lookup = &associated_ty_lookups[&(trait_id, assoc_ty_defn.name.str)];
@@ -367,6 +382,7 @@ impl LowerProgram for Program {
             trait_kinds,
             struct_data,
             trait_data,
+            trait_lang_items,
             impl_data,
             associated_ty_values,
             associated_ty_data,

chalk-integration/src/program.rs

@@ -9,8 +9,8 @@ use chalk_ir::{
     TraitId, Ty, TyData, TypeName,
 };
 use chalk_rust_ir::{
-    AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
-    TraitDatum,
+    AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, LangItem,
+    StructDatum, TraitDatum,
 };
 use chalk_solve::split::Split;
 use chalk_solve::RustIrDatabase;
@@ -45,6 +45,9 @@ pub struct Program {
     /// For each trait:
     pub trait_data: BTreeMap<TraitId<ChalkIr>, Arc<TraitDatum<ChalkIr>>>,
 
+    /// For each trait lang item
+    pub trait_lang_items: BTreeMap<LangItem, TraitId<ChalkIr>>,
+
     /// For each associated ty declaration `type Foo` found in a trait:
     pub associated_ty_data: BTreeMap<AssocTypeId<ChalkIr>, Arc<AssociatedTyDatum<ChalkIr>>>,
 
@@ -309,6 +312,13 @@ impl RustIrDatabase<ChalkIr> for Program {
         })
     }
 
+    fn require_lang_item(&self, lang_item: LangItem) -> TraitId<ChalkIr> {
+        *self
+            .trait_lang_items
+            .get(&lang_item)
+            .unwrap_or_else(|| panic!("No lang item found for {:?}", lang_item))
+    }
+
     fn interner(&self) -> &ChalkIr {
         &ChalkIr
     }

chalk-integration/src/query.rs

@@ -100,7 +100,6 @@ fn checked_program(db: &impl LoweringDatabase) -> Result<Arc<Program>, ChalkErro
 
     let () = tls::set_current_program(&program, || -> Result<(), ChalkError> {
         let solver = wf::WfSolver::new(db, db.solver_choice());
-
         for &id in program.struct_data.keys() {
             solver.verify_struct_decl(id)?;
         }

chalk-rust-ir/src/lib.rs

@@ -15,8 +15,10 @@ use chalk_ir::{
 };
 use std::iter;
 
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
-pub enum LangItem {}
+#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)]
+pub enum LangItem {
+    SizedTrait,
+}
 
 /// Identifier for an "associated type value" found in some impl.
 #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
@@ -78,7 +80,7 @@ impl<I: Interner> StructDatum<I> {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)]
 pub struct StructDatumBound<I: Interner> {
     pub fields: Vec<Ty<I>>,
     pub where_clauses: Vec<QuantifiedWhereClause<I>>,

chalk-solve/src/clauses/builtin_traits.rs

@@ -2,6 +2,8 @@ use super::builder::ClauseBuilder;
 use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
 use chalk_ir::TyData;
 
+mod sized;
+
 /// For well known traits we have special hard-coded impls, either as an
 /// optimization or to enforce special rules for correctness.
 pub fn add_builtin_program_clauses<I: Interner>(
@@ -16,7 +18,7 @@ pub fn add_builtin_program_clauses<I: Interner>(
     }
 
     match well_known {
-        WellKnownTrait::SizedTrait => { /* TODO */ }
+        WellKnownTrait::SizedTrait => sized::add_sized_program_clauses(db, builder, trait_ref, ty),
         WellKnownTrait::CopyTrait => { /* TODO */ }
         WellKnownTrait::CloneTrait => { /* TODO */ }
     }

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

@@ -0,0 +1,46 @@
+use std::iter;
+
+use crate::clauses::ClauseBuilder;
+use crate::{Interner, RustIrDatabase, TraitRef};
+use chalk_ir::{ApplicationTy, Substitution, TyData, TypeName};
+
+pub fn add_sized_program_clauses<I: Interner>(
+    db: &dyn RustIrDatabase<I>,
+    builder: &mut ClauseBuilder<'_, I>,
+    trait_ref: &TraitRef<I>,
+    ty: &TyData<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
+    if struct_datum.binders.map_ref(|b| b.fields.is_empty()).value {
+        builder.push_fact(trait_ref.clone());
+        return;
+    }
+
+    // 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)
+        .clone();
+
+    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));
+}

chalk-solve/src/lib.rs

@@ -76,6 +76,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {
         false
     }
 
+    /// Returns id of a trait lang item, if found
+    fn require_lang_item(&self, lang_item: LangItem) -> TraitId<I>;
+
     fn interner(&self) -> &I;
 }
 

chalk-solve/src/wf.rs

@@ -190,6 +190,9 @@ where
         let wg_goal = gb.forall(&struct_data, (), |gb, _, (fields, where_clauses), ()| {
             let interner = gb.interner();
 
+            // struct is well-formed in terms of Sized
+            let sized_constraint_goal = compute_struct_sized_constraint(gb.db(), fields);
+
             // (FromEnv(T: Eq) => ...)
             gb.implies(
                 where_clauses
@@ -203,7 +206,13 @@ where
                     fields.fold(gb.interner(), &mut input_types);
                     // ...in a where clause.
                     where_clauses.fold(gb.interner(), &mut input_types);
-                    gb.all(input_types.into_iter().map(|ty| ty.well_formed()))
+
+                    gb.all(
+                        input_types
+                            .into_iter()
+                            .map(|ty| ty.well_formed().cast(interner))
+                            .chain(sized_constraint_goal.into_iter()),
+                    )
                 },
             )
         });
@@ -224,7 +233,14 @@ where
 
     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();
+
+        // You can't manually implement Sized
+        if let Some(WellKnownTrait::SizedTrait) = self.db.trait_datum(trait_id).well_known {
+            return Err(WfError::IllFormedTraitImpl(trait_id));
+        }
 
         let impl_goal = Goal::all(
             interner,
@@ -250,8 +266,7 @@ where
         if is_legal {
             Ok(())
         } else {
-            let trait_ref = &impl_datum.binders.value.trait_ref;
-            Err(WfError::IllFormedTraitImpl(trait_ref.trait_id))
+            Err(WfError::IllFormedTraitImpl(trait_id))
         }
     }
 }
@@ -464,3 +479,30 @@ fn compute_assoc_ty_goal<I: Interner>(
         },
     ))
 }
+
+/// Computes a goal to prove Sized constraints on a struct definition.
+/// Struct is considered well-formed (in terms of Sized) when it either
+/// has no fields or all of it's fields except the last are proven to be Sized.  
+fn compute_struct_sized_constraint<I: Interner>(
+    db: &dyn RustIrDatabase<I>,
+    fields: &[Ty<I>],
+) -> Option<Goal<I>> {
+    if fields.len() <= 1 {
+        return None;
+    }
+
+    let interner = db.interner();
+
+    let sized_trait = db.require_lang_item(LangItem::SizedTrait);
+
+    Some(Goal::all(
+        interner,
+        fields[..fields.len() - 1].iter().map(|ty| {
+            TraitRef {
+                trait_id: sized_trait,
+                substitution: Substitution::from1(interner, ty.clone()),
+            }
+            .cast(interner)
+        }),
+    ))
+}

tests/test/auto_traits.rs

@@ -6,14 +6,15 @@ use super::*;
 fn auto_semantics() {
     test! {
         program {
+            #[lang(sized)] trait Sized { }
             #[auto] trait Send { }
 
             struct i32 { }
 
             struct Ptr<T> { }
             impl<T> Send for Ptr<T> where T: Send { }
 
-            struct List<T> {
+            struct List<T> where T: Sized {
                 data: T,
                 next: Ptr<List<T>>
             }