Merge pull request #374 from Areredify/sized

nikomatsakis · web-flow · commit 73a74be3bc1d · 2020-04-07T17:18:54.000-04:00
add Sized well-known impl and wf check
diff --git a/chalk-integration/src/db.rs b/chalk-integration/src/db.rs
@@ -23,6 +23,7 @@ use chalk_rust_ir::AssociatedTyValueId;
 use chalk_rust_ir::ImplDatum;
 use chalk_rust_ir::StructDatum;
 use chalk_rust_ir::TraitDatum;
+use chalk_rust_ir::WellKnownTrait;
 use chalk_solve::RustIrDatabase;
 use chalk_solve::Solution;
 use chalk_solve::SolverChoice;
@@ -137,6 +138,12 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
             .impl_provided_for(auto_trait_id, struct_id)
     }
 
+    fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> TraitId<ChalkIr> {
+        self.program_ir()
+            .unwrap()
+            .well_known_trait_id(well_known_trait)
+    }
+
     fn interner(&self) -> &ChalkIr {
         &ChalkIr
     }
diff --git a/chalk-integration/src/error.rs b/chalk-integration/src/error.rs
@@ -1,6 +1,5 @@
 use chalk_ir::interner::ChalkIr;
 use chalk_parse::ast::{Identifier, Kind};
-use chalk_rust_ir::LangItem;
 use chalk_solve::coherence::CoherenceError;
 use chalk_solve::wf::WfError;
 
@@ -57,7 +56,6 @@ impl std::error::Error for ChalkError {}
 pub enum RustIrError {
     InvalidTypeName(Identifier),
     InvalidLifetimeName(Identifier),
-    DuplicateLangItem(LangItem),
     NotTrait(Identifier),
     NotStruct(Identifier),
     DuplicateOrShadowedParameters,
@@ -100,7 +98,6 @@ impl std::fmt::Display for RustIrError {
         match self {
             RustIrError::InvalidTypeName(name) => write!(f, "invalid type name `{}`", name),
             RustIrError::InvalidLifetimeName(name) => write!(f, "invalid lifetime name `{}`", name),
-            RustIrError::DuplicateLangItem(item) => write!(f, "duplicate lang item `{:?}`", item),
             RustIrError::NotTrait(name) => write!(
                 f,
                 "expected a trait, found `{}`, which is not a trait",
diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
@@ -249,6 +249,7 @@ impl LowerProgram for Program {
 
         let mut struct_data = BTreeMap::new();
         let mut trait_data = BTreeMap::new();
+        let mut well_known_traits = BTreeMap::new();
         let mut impl_data = BTreeMap::new();
         let mut associated_ty_data = BTreeMap::new();
         let mut associated_ty_values = BTreeMap::new();
@@ -270,10 +271,13 @@ 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 {
+                        well_known_traits.insert(well_known, trait_id);
+                    }
+
+                    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)];
@@ -370,6 +374,7 @@ impl LowerProgram for Program {
             trait_kinds,
             struct_data,
             trait_data,
+            well_known_traits,
             impl_data,
             associated_ty_values,
             associated_ty_data,
diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs
@@ -10,7 +10,7 @@ use chalk_ir::{
 };
 use chalk_rust_ir::{
     AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
-    TraitDatum,
+    TraitDatum, WellKnownTrait,
 };
 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 well_known_traits: BTreeMap<WellKnownTrait, TraitId<ChalkIr>>,
+
     /// For each associated ty declaration `type Foo` found in a trait:
     pub associated_ty_data: BTreeMap<AssocTypeId<ChalkIr>, Arc<AssociatedTyDatum<ChalkIr>>>,
 
@@ -318,6 +321,13 @@ impl RustIrDatabase<ChalkIr> for Program {
         })
     }
 
+    fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> TraitId<ChalkIr> {
+        *self
+            .well_known_traits
+            .get(&well_known_trait)
+            .unwrap_or_else(|| panic!("No lang item found for {:?}", well_known_trait))
+    }
+
     fn interner(&self) -> &ChalkIr {
         &ChalkIr
     }
diff --git a/chalk-integration/src/query.rs b/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)?;
         }
diff --git a/chalk-rust-ir/src/lib.rs b/chalk-rust-ir/src/lib.rs
@@ -15,9 +15,6 @@ use chalk_ir::{
 };
 use std::iter;
 
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
-pub enum LangItem {}
-
 /// Identifier for an "associated type value" found in some impl.
 #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct AssociatedTyValueId<I: Interner>(pub I::DefId);
@@ -78,7 +75,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>>,
@@ -134,7 +131,7 @@ pub struct TraitDatum<I: Interner> {
 
 /// A list of the traits that are "well known" to chalk, which means that
 /// the chalk-solve crate has special, hard-coded impls for them.
-#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
+#[derive(Copy, Clone, Debug, PartialEq, Eq, Ord, PartialOrd, Hash)]
 pub enum WellKnownTrait {
     SizedTrait,
     CopyTrait,
diff --git a/chalk-solve/src/clauses/builtin_traits.rs b/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 */ }
     }
diff --git a/chalk-solve/src/clauses/builtin_traits/sized.rs b/chalk-solve/src/clauses/builtin_traits/sized.rs
@@ -0,0 +1,45 @@
+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);
+
+    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));
+}
diff --git a/chalk-solve/src/lib.rs b/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 well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> TraitId<I>;
+
     fn interner(&self) -> &I;
 }
 
diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs
@@ -196,6 +196,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
@@ -209,7 +212,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()),
+                    )
                 },
             )
         });
@@ -230,7 +239,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,
@@ -256,8 +272,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))
         }
     }
 }
@@ -470,3 +485,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.well_known_trait_id(WellKnownTrait::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)
+        }),
+    ))
+}
diff --git a/tests/test/auto_traits.rs b/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>>
             }
diff --git a/tests/test/wf_lowering.rs b/tests/test/wf_lowering.rs
@@ -636,3 +636,77 @@ fn assoc_type_recursive_bound() {
         }
     }
 }
+
+#[test]
+fn struct_sized_constraints() {
+    lowering_error! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+
+            struct S<T> {
+                t1: T,
+                t2: T
+            }
+        } error_msg {
+            "type declaration `S` does not meet well-formedness requirements"
+        }
+    }
+
+    lowering_success! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+
+            struct Foo { }
+
+            struct S<T> {
+                t1: Foo,
+                t2: T
+            }
+        }
+    }
+
+    lowering_success! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+
+            struct S<T> where T: Sized {
+                t1: T,
+                t2: T
+            }
+        }
+    }
+
+    lowering_success! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+
+            struct Foo {}
+
+            struct G<T> {
+                foo: S<S<Foo>>,
+                s: S<S<S<T>>>
+            }
+
+            struct S<T> {
+                t1: T
+            }
+        }
+    }
+
+    lowering_error! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+
+            struct Foo {}
+
+            impl Sized for Foo {}
+        } error_msg {
+            "trait impl for `Sized` does not meet well-formedness requirements"
+        }
+    }
+}

Original file line number	Diff line number	Diff line change
`@@ -100,7 +100,6 @@ fn checked_program(db: &impl LoweringDatabase) -> Result<Arc<Program>, ChalkErro`
`100`	`100`
`101`	`101`	`let () = tls::set_current_program(&program, \|\| -> Result<(), ChalkError> {`
`102`	`102`	`let solver = wf::WfSolver::new(db, db.solver_choice());`
`103`		`-`
`104`	`103`	`for &id in program.struct_data.keys() {`
`105`	`104`	`solver.verify_struct_decl(id)?;`
`106`	`105`	`}`
Original file line number	Diff line number	Diff line change
`@@ -76,6 +76,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {`
`76`	`76`	`false`
`77`	`77`	`}`
`78`	`78`
	`79`	`+ /// Returns id of a trait lang item, if found`
	`80`	`+ fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> TraitId<I>;`
	`81`	`+`
`79`	`82`	`fn interner(&self) -> &I;`
`80`	`83`	`}`
`81`	`84`