Skip to content

add Sized well-known impl and wf check #374

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Apr 7, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions chalk-integration/src/db.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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
}
Expand Down
3 changes: 0 additions & 3 deletions chalk-integration/src/error.rs
Original file line number Diff line number Diff line change
@@ -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;

Expand Down Expand Up @@ -57,7 +56,6 @@ impl std::error::Error for ChalkError {}
pub enum RustIrError {
InvalidTypeName(Identifier),
InvalidLifetimeName(Identifier),
DuplicateLangItem(LangItem),
NotTrait(Identifier),
NotStruct(Identifier),
DuplicateOrShadowedParameters,
Expand Down Expand Up @@ -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",
Expand Down
13 changes: 9 additions & 4 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -246,6 +246,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();
Expand All @@ -267,10 +268,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)];
Expand Down Expand Up @@ -367,6 +371,7 @@ impl LowerProgram for Program {
trait_kinds,
struct_data,
trait_data,
well_known_traits,
impl_data,
associated_ty_values,
associated_ty_data,
Expand Down
12 changes: 11 additions & 1 deletion chalk-integration/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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>>>,

Expand Down Expand Up @@ -309,6 +312,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
}
Expand Down
1 change: 0 additions & 1 deletion chalk-integration/src/query.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)?;
}
Expand Down
7 changes: 2 additions & 5 deletions chalk-rust-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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>>,
Expand Down Expand Up @@ -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,
Expand Down
4 changes: 3 additions & 1 deletion chalk-solve/src/clauses/builtin_traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>(
Expand All @@ -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 */ }
}
Expand Down
45 changes: 45 additions & 0 deletions chalk-solve/src/clauses/builtin_traits/sized.rs
Original file line number Diff line number Diff line change
@@ -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));
}
3 changes: 3 additions & 0 deletions chalk-solve/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
48 changes: 45 additions & 3 deletions chalk-solve/src/wf.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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()),
)
},
)
});
Expand All @@ -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,
Expand All @@ -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))
}
}
}
Expand Down Expand Up @@ -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.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)
}),
))
}
3 changes: 2 additions & 1 deletion tests/test/auto_traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>>
}
Expand Down
74 changes: 74 additions & 0 deletions tests/test/wf_lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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"
}
}
}