diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index f1e64ce2c34..c8a5290e2ba 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -35,6 +35,7 @@ pub struct TraitDefn { pub parameter_kinds: Vec, pub where_clauses: Vec, pub assoc_ty_defns: Vec, + pub auto: bool, } pub struct AssocTyDefn { @@ -93,7 +94,7 @@ impl Kinded for Parameter { pub struct Impl { pub parameter_kinds: Vec, - pub trait_ref: TraitRef, + pub trait_ref: PolarizedTraitRef, pub where_clauses: Vec, pub assoc_ty_values: Vec, } @@ -139,6 +140,21 @@ pub struct TraitRef { pub args: Vec, } +pub enum PolarizedTraitRef { + Positive(TraitRef), + Negative(TraitRef), +} + +impl PolarizedTraitRef { + pub fn from_bool(polarity: bool, trait_ref: TraitRef) -> PolarizedTraitRef { + if polarity { + PolarizedTraitRef::Positive(trait_ref) + } else { + PolarizedTraitRef::Negative(trait_ref) + } + } +} + #[derive(Copy, Clone, Debug)] pub struct Identifier { pub str: InternedString, diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 7c99ffe4287..77887334415 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -47,12 +47,17 @@ StructDefn: StructDefn = { } }; +AutoKeyword: () = "#" "[" "auto" "]"; + TraitDefn: TraitDefn = { - "trait" > "{" "}" => TraitDefn { + "trait" > "{" + "}" => + TraitDefn { name: n, parameter_kinds: p, where_clauses: w, assoc_ty_defns: a, + auto: auto.is_some(), } }; @@ -64,14 +69,17 @@ AssocTyDefn: AssocTyDefn = { }; Impl: Impl = { - "impl" > > "for" "{" - "}" => + "impl" > > "for" "{" + "}" => { let mut args = vec![Parameter::Ty(s)]; args.extend(a); Impl { parameter_kinds: p, - trait_ref: TraitRef { trait_name: t, args: args }, + trait_ref: PolarizedTraitRef::from_bool(mark.is_none(), TraitRef { + trait_name: t, + args: args, + }), where_clauses: w, assoc_ty_values: assoc, } diff --git a/src/coherence/solve.rs b/src/coherence/solve.rs index b358779dc73..e349ae31f41 100644 --- a/src/coherence/solve.rs +++ b/src/coherence/solve.rs @@ -17,12 +17,12 @@ impl Program { // Create a vector of references to impl datums, sorted by trait ref let impl_data = self.impl_data.iter().sorted_by(|&(_, lhs), &(_, rhs)| { - lhs.binders.value.trait_ref.trait_id.cmp(&rhs.binders.value.trait_ref.trait_id) + lhs.binders.value.trait_ref.trait_ref().trait_id.cmp(&rhs.binders.value.trait_ref.trait_ref().trait_id) }); // Group impls by trait. let impl_groupings = impl_data.into_iter().group_by(|&(_, impl_datum)| { - impl_datum.binders.value.trait_ref.trait_id + impl_datum.binders.value.trait_ref.trait_ref().trait_id }); @@ -31,6 +31,11 @@ impl Program { let impls: Vec<(&ItemId, &ImplDatum)> = impls.collect(); for ((&l_id, lhs), (&r_id, rhs)) in impls.into_iter().tuple_combinations() { + // Two negative impls never overlap. + if !lhs.binders.value.trait_ref.is_positive() && !rhs.binders.value.trait_ref.is_positive() { + continue; + } + // Check if the impls overlap, then if they do, check if one specializes // the other. Note that specialization can only run one way - if both // specialization checks return *either* true or false, that's an error. @@ -133,6 +138,11 @@ impl Solver { // } // } fn specializes(&mut self, less_special: &ImplDatum, more_special: &ImplDatum) -> bool { + // Negative impls cannot specialize. + if !less_special.binders.value.trait_ref.is_positive() || !more_special.binders.value.trait_ref.is_positive() { + return false; + } + let more_len = more_special.binders.len(); // Create parameter equality goals. @@ -160,5 +170,5 @@ impl Solver { } fn params(impl_datum: &ImplDatum) -> &[Parameter] { - &impl_datum.binders.value.trait_ref.parameters + &impl_datum.binders.value.trait_ref.trait_ref().parameters } diff --git a/src/fold/mod.rs b/src/fold/mod.rs index f37d083eae5..b952acc789f 100644 --- a/src/fold/mod.rs +++ b/src/fold/mod.rs @@ -195,6 +195,7 @@ macro_rules! enum_fold { } } +enum_fold!(PolarizedTraitRef[] { Positive(a), Negative(a) }); enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold); enum_fold!(DomainGoal[] { Implemented(a), Normalize(a), WellFormed(a) }); enum_fold!(WellFormed[] { Ty(a), TraitRef(a) }); diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 15580e1eeac..b4281b951e9 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -2,7 +2,7 @@ use cast::Cast; use chalk_parse::ast; use lalrpop_intern::InternedString; use solve::infer::{TyInferenceVariable, LifetimeInferenceVariable}; -use std::collections::{HashMap, BTreeMap}; +use std::collections::{HashSet, HashMap, BTreeMap}; use std::sync::Arc; pub type Identifier = InternedString; @@ -24,8 +24,11 @@ pub struct Program { /// For each trait: pub trait_data: HashMap, - /// For each trait: + /// For each associated ty: pub associated_ty_data: HashMap, + + /// For each default impl (automatically generated for auto traits): + pub default_impl_data: Vec, } impl Program { @@ -85,7 +88,8 @@ impl Environment { where I: IntoIterator { let mut env = self.clone(); - env.clauses.extend(clauses); + let env_clauses: HashSet<_> = env.clauses.into_iter().chain(clauses).collect(); + env.clauses = env_clauses.into_iter().collect(); Arc::new(env) } @@ -182,12 +186,23 @@ pub struct ImplDatum { #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct ImplDatumBound { - pub trait_ref: TraitRef, + pub trait_ref: PolarizedTraitRef, pub where_clauses: Vec, pub associated_ty_values: Vec, pub specialization_priority: usize, } +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct DefaultImplDatum { + pub binders: Binders, +} + +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub struct DefaultImplDatumBound { + pub trait_ref: TraitRef, + pub accessible_tys: Vec, +} + #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct StructDatum { pub binders: Binders, @@ -209,6 +224,7 @@ pub struct TraitDatum { pub struct TraitDatumBound { pub trait_ref: TraitRef, pub where_clauses: Vec, + pub auto: bool, } #[derive(Clone, Debug, PartialEq, Eq, Hash)] @@ -343,6 +359,28 @@ pub struct TraitRef { pub parameters: Vec, } +#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)] +pub enum PolarizedTraitRef { + Positive(TraitRef), + Negative(TraitRef), +} + +impl PolarizedTraitRef { + pub fn is_positive(&self) -> bool { + match *self { + PolarizedTraitRef::Positive(_) => true, + PolarizedTraitRef::Negative(_) => false, + } + } + + pub fn trait_ref(&self) -> &TraitRef { + match *self { + PolarizedTraitRef::Positive(ref tr) | + PolarizedTraitRef::Negative(ref tr) => tr + } + } +} + /// A "domain goal" is a goal that is directly about Rust, rather than a pure /// logical statement. As much as possible, the Chalk solver should avoid /// decomposing this enum, and instead treat its values opaquely. @@ -374,9 +412,8 @@ impl DomainGoal { pub fn expanded(self, program: &Program) -> impl Iterator { let mut expanded = vec![]; match self { - DomainGoal::Implemented(ref trait_ref) => { - expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast()); - } + DomainGoal::Implemented(ref trait_ref) => + expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast()), DomainGoal::Normalize(Normalize { ref projection, .. }) => { let (associated_ty_data, trait_params, _) = program.split_projection(&projection); let trait_ref = TraitRef { @@ -500,6 +537,31 @@ pub enum FullyReducedGoal { DomainGoal(Canonical>), } +impl FullyReducedGoal { + pub fn into_binders(self) -> Vec> { + match self { + FullyReducedGoal::EqGoal(Canonical { binders, .. }) | + FullyReducedGoal::DomainGoal(Canonical { binders, ..}) => binders, + } + } + + /// A goal has coinductive semantics if it is of the form `T: AutoTrait`. + pub fn is_coinductive(&self, program: &ProgramEnvironment) -> bool { + if let FullyReducedGoal::DomainGoal(Canonical { + value: InEnvironment { + goal: DomainGoal::Implemented(ref tr), + .. + }, + .. + }) = *self { + let trait_datum = &program.trait_data[&tr.trait_id]; + return trait_datum.binders.value.auto; + } + + false + } +} + impl Canonical { pub fn map(self, op: OP) -> Canonical where OP: FnOnce(T) -> U diff --git a/src/lower/default.rs b/src/lower/default.rs new file mode 100644 index 00000000000..227064257c6 --- /dev/null +++ b/src/lower/default.rs @@ -0,0 +1,80 @@ +use ir::*; +use solve::infer::InferenceTable; +use cast::Cast; + +impl Program { + pub(super) fn add_default_impls(&mut self) { + // For each auto trait `MyAutoTrait` and for each struct/type `MyStruct` + for auto_trait in self.trait_data.values().filter(|t| t.binders.value.auto) { + for struct_datum in self.struct_data.values() { + + // `MyStruct: MyAutoTrait` + let trait_ref = TraitRef { + trait_id: auto_trait.binders.value.trait_ref.trait_id, + parameters: vec![ + ParameterKind::Ty(Ty::Apply(struct_datum.binders.value.self_ty.clone())) + ] + }; + + // If a positive or negative impl is already provided for a type family + // which includes `MyStruct`, we do not generate a default impl. + if self.impl_provided_for(trait_ref.clone(), struct_datum) { + continue; + } + + self.default_impl_data.push(DefaultImplDatum { + binders: Binders { + binders: struct_datum.binders.binders.clone(), + value: DefaultImplDatumBound { + trait_ref, + accessible_tys: struct_datum.binders.value.fields.clone(), + } + } + }); + } + } + } + + fn impl_provided_for(&self, trait_ref: TraitRef, struct_datum: &StructDatum) -> bool { + let goal: DomainGoal = trait_ref.cast(); + + let env = Environment::new(); + let mut infer = InferenceTable::new(); + + let goal = infer.instantiate_in(env.universe, struct_datum.binders.binders.clone(), &goal); + + for impl_datum in self.impl_data.values() { + // We retrieve the trait ref given by the positive impl (even if the actual impl is negative) + let impl_goal: DomainGoal = impl_datum.binders.value.trait_ref.trait_ref().clone().cast(); + + let impl_goal = infer.instantiate_in(env.universe, impl_datum.binders.binders.clone(), &impl_goal); + + // We check whether the impl `MyStruct: (!)MyAutoTrait` unifies with an existing impl. + // Examples: + // + // ``` + // struct MyStruct; + // impl Send for T where T: Foo { } + // ``` + // `MyStruct: Send` unifies with `T: Send` so no default impl is generated for `MyStruct`. + // + // ``` + // struct MyStruct; + // impl Send for Vec where T: Foo { } + // ``` + // `Vec: Send` unifies with `Vec: Send` so no default impl is generated for `Vec`. + // But a default impl is generated for `MyStruct`. + // + // ``` + // struct MyStruct; + // impl !Send for T where T: Foo { } + // ``` + // `MyStruct: !Send` unifies with `T: !Send` so no default impl is generated for `MyStruct`. + if infer.unify(&Environment::new(), &goal, &impl_goal).is_ok() { + return true; + } + } + + false + } +} diff --git a/src/lower/mod.rs b/src/lower/mod.rs index 0aab85e1158..5049d705668 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -8,6 +8,7 @@ use errors::*; use ir; mod test; +mod default; type TypeIds = HashMap; type TypeKinds = HashMap; @@ -117,6 +118,9 @@ impl LowerProgram for Program { let mut associated_ty_infos = HashMap::new(); for (item, &item_id) in self.items.iter().zip(&item_ids) { if let Item::TraitDefn(ref d) = *item { + if d.auto && !d.assoc_ty_defns.is_empty() { + bail!("auto trait cannot define associated types"); + } for defn in &d.assoc_ty_defns { let addl_parameter_kinds = defn.all_parameters(); let info = AssociatedTyInfo { id: next_item_id(), addl_parameter_kinds }; @@ -177,7 +181,16 @@ impl LowerProgram for Program { } } - let mut program = ir::Program { type_ids, type_kinds, struct_data, trait_data, impl_data, associated_ty_data, }; + let mut program = ir::Program { + type_ids, + type_kinds, + struct_data, + trait_data, + impl_data, + associated_ty_data, + default_impl_data: Vec::new(), + }; + program.add_default_impls(); program.record_specialization_priorities()?; Ok(program) } @@ -435,8 +448,7 @@ trait LowerStructDefn { } impl LowerStructDefn for StructDefn { - fn lower_struct(&self, item_id: ir::ItemId, env: &Env) -> Result - { + fn lower_struct(&self, item_id: ir::ItemId, env: &Env) -> Result { let binders = env.in_binders(self.all_parameters(), |env| { let self_ty = ir::ApplicationTy { name: ir::TypeName::ItemId(item_id), @@ -502,6 +514,19 @@ impl LowerTraitRef for TraitRef { } } +trait LowerPolarizedTraitRef { + fn lower(&self, env: &Env) -> Result; +} + +impl LowerPolarizedTraitRef for PolarizedTraitRef { + fn lower(&self, env: &Env) -> Result { + Ok(match *self { + PolarizedTraitRef::Positive(ref tr) => ir::PolarizedTraitRef::Positive(tr.lower(env)?), + PolarizedTraitRef::Negative(ref tr) => ir::PolarizedTraitRef::Negative(tr.lower(env)?), + }) + } +} + trait LowerProjectionTy { fn lower(&self, env: &Env) -> Result; } @@ -634,7 +659,12 @@ impl LowerImpl for Impl { fn lower_impl(&self, empty_env: &Env) -> Result { let binders = empty_env.in_binders(self.all_parameters(), |env| { let trait_ref = self.trait_ref.lower(env)?; - let trait_id = trait_ref.trait_id; + + if !trait_ref.is_positive() && !self.assoc_ty_values.is_empty() { + bail!("negative impls cannot define associated values"); + } + + let trait_id = trait_ref.trait_ref().trait_id; let where_clauses = self.lower_where_clauses(&env)?; let associated_ty_values = try!(self.assoc_ty_values.iter() .map(|v| v.lower(trait_id, env)) @@ -679,9 +709,20 @@ impl LowerTrait for TraitDefn { trait_id: trait_id, parameters: self.parameter_refs() }; + + if self.auto { + if trait_ref.parameters.len() > 1 { + bail!("auto trait cannot have parameters"); + } + if !self.where_clauses.is_empty() { + bail!("auto trait cannot have where clauses"); + } + } + Ok(ir::TraitDatumBound { trait_ref: trait_ref, where_clauses: self.lower_where_clauses(env)?, + auto: self.auto, }) })?; @@ -785,12 +826,17 @@ impl ir::Program { program_clauses.extend(self.struct_data.values().flat_map(|d| d.to_program_clauses(self))); program_clauses.extend(self.trait_data.values().flat_map(|d| d.to_program_clauses(self))); program_clauses.extend(self.associated_ty_data.values().flat_map(|d| d.to_program_clauses(self))); + program_clauses.extend(self.default_impl_data.iter().map(|d| d.to_program_clause())); for datum in self.impl_data.values() { - program_clauses.push(datum.to_program_clause(self)); - program_clauses.extend(datum.binders.value.associated_ty_values.iter().flat_map(|atv| { - atv.to_program_clauses(datum) - })); + // If we encounter a negative impl, do not generate any rule. Negative impls + // are currently just there to deactivate default impls for auto traits. + if datum.binders.value.trait_ref.is_positive() { + program_clauses.push(datum.to_program_clause(self)); + program_clauses.extend(datum.binders.value.associated_ty_values.iter().flat_map(|atv| { + atv.to_program_clauses(datum) + })); + } } let trait_data = self.trait_data.clone(); @@ -810,7 +856,7 @@ impl ir::ImplDatum { ir::ProgramClause { implication: self.binders.map_ref(|bound| { ir::ProgramClauseImplication { - consequence: bound.trait_ref.clone().cast(), + consequence: bound.trait_ref.trait_ref().clone().cast(), conditions: bound.where_clauses .iter() .cloned() @@ -824,6 +870,52 @@ impl ir::ImplDatum { } } +impl ir::DefaultImplDatum { + /// For each accessible type `T` in a struct which needs a default implementation for the auto + /// trait `Foo` (accessible types are the struct fields types), we add a bound `T: Foo` (which + /// is then expanded with `WF(T: Foo)`). For example, given: + /// + /// ```notrust + /// #[auto] trait Send { } + /// + /// struct MyList { + /// data: T, + /// next: Box>>, + /// } + /// + /// ``` + /// + /// generate: + /// + /// ```notrust + /// forall { + /// (MyList: Send) :- + /// (T: Send), WF(T: Send), + /// (Box>>: Send), WF(Box>>: Send) + /// } + /// ``` + fn to_program_clause(&self) -> ir::ProgramClause { + ir::ProgramClause { + implication: self.binders.map_ref(|bound| { + ir::ProgramClauseImplication { + consequence: bound.trait_ref.clone().cast(), + conditions: { + let wc = bound.accessible_tys.iter().cloned().map(|ty| { + ir::TraitRef { + trait_id: bound.trait_ref.trait_id, + parameters: vec![ir::ParameterKind::Ty(ty)], + } + }); + + wc.casted().collect() + }, + } + }), + fallback_clause: false, + } + } +} + impl ir::AssociatedTyValue { /// Given: /// @@ -856,7 +948,7 @@ impl ir::AssociatedTyValue { // // 1. require that the trait is implemented // 2. any where-clauses from the `type` declaration in the impl - let impl_trait_ref = impl_datum.binders.value.trait_ref.up_shift(self.value.len()); + let impl_trait_ref = impl_datum.binders.value.trait_ref.trait_ref().up_shift(self.value.len()); let conditions: Vec = Some(impl_trait_ref.clone().cast()) .into_iter() @@ -989,11 +1081,13 @@ impl ir::TraitDatum { .cloned() .flat_map(|wc| wc.expanded(program)) .collect::>(); + + let wf = ir::WellFormed::TraitRef(self.binders.value.trait_ref.clone()); - let wf = ir::ProgramClause { + let clauses = ir::ProgramClause { implication: self.binders.map_ref(|bound| { ir::ProgramClauseImplication { - consequence: ir::WellFormed::TraitRef(bound.trait_ref.clone()).cast(), + consequence: wf.clone().cast(), conditions: { let tys = bound.trait_ref.parameters @@ -1010,14 +1104,13 @@ impl ir::TraitDatum { fallback_clause: false, }; - let mut clauses = vec![wf]; - + let mut clauses = vec![clauses]; for wc in where_clauses { clauses.push(ir::ProgramClause { - implication: self.binders.map_ref(|bound| { + implication: self.binders.map_ref(|_| { ir::ProgramClauseImplication { consequence: wc, - conditions: vec![ir::WellFormed::TraitRef(bound.trait_ref.clone()).cast()] + conditions: vec![wf.clone().cast()] } }), fallback_clause: false, diff --git a/src/lower/test.rs b/src/lower/test.rs index 2b40824758a..e0147280de5 100755 --- a/src/lower/test.rs +++ b/src/lower/test.rs @@ -63,6 +63,79 @@ fn not_trait() { } } +#[test] +fn auto_trait() { + lowering_error! { + program { + #[auto] trait Foo { } + } + error_msg { + "auto trait cannot have parameters" + } + } + + lowering_error! { + program { + trait Bar { } + #[auto] trait Foo where Self: Bar { } + } + error_msg { + "auto trait cannot have where clauses" + } + } + + lowering_error! { + program { + #[auto] trait Foo { + type Item; + } + } + error_msg { + "auto trait cannot define associated types" + } + } + + lowering_success! { + program { + #[auto] trait Send { } + } + } +} + +#[test] +fn negative_impl() { + lowering_error! { + program { + trait Foo { + type Item; + } + + struct i32 { } + + impl !Foo for i32 { + type Item = i32; + } + } + error_msg { + "negative impls cannot define associated values" + } + } + + lowering_success! { + program { + trait Foo { } + + trait Iterator { + type Item; + } + + struct i32 { } + + impl !Foo for T where T: Iterator { } + } + } +} + #[test] fn invalid_name() { lowering_error! { @@ -133,7 +206,9 @@ fn atc_accounting() { println!("{}", impl_text); assert_eq!(&impl_text[..], r#"ImplDatum { binders: for ImplDatumBound { - trait_ref: Vec as Iterable, + trait_ref: Positive( + Vec as Iterable + ), where_clauses: [], associated_ty_values: [ AssociatedTyValue { @@ -389,3 +464,38 @@ fn overlapping_assoc_types() { } } } + +#[test] +fn overlapping_negative_positive_impls() { + lowering_error! { + program { + trait Send { } + struct i32 { } + + impl Send for i32 { } + impl !Send for i32 { } + } error_msg { + "overlapping impls of trait \"Send\"" + } + } +} + +#[test] +fn overlapping_negative_impls() { + lowering_success! { + program { + trait Send { } + trait Foo { } + trait Bar { } + + struct Vec { } + struct i32 { } + + impl Foo for i32 { } + impl Bar for i32 { } + + impl !Send for Vec where T: Foo { } + impl !Send for Vec where T: Bar { } + } + } +} diff --git a/src/solve/fulfill.rs b/src/solve/fulfill.rs index 9e1335af4f7..d8e2d1e42ab 100644 --- a/src/solve/fulfill.rs +++ b/src/solve/fulfill.rs @@ -98,11 +98,7 @@ impl<'s> Fulfill<'s> { self.infer.instantiate(universes, arg) } - /// Instantiates `arg` with fresh existential variables in the - /// given universe; the kinds of the variables are implied by - /// `binders`. This is used to apply a universally quantified - /// clause like `forall X, 'Y. P => Q`. Here the `binders` - /// argument is referring to `X, 'Y`. + /// Wraps `InferenceTable::instantiate_in` pub fn instantiate_in(&mut self, universe: UniverseIndex, binders: U, @@ -110,7 +106,7 @@ impl<'s> Fulfill<'s> { where T: Fold, U: IntoIterator> { - self.instantiate(binders.into_iter().map(|pk| pk.map(|_| universe)), arg) + self.infer.instantiate_in(universe, binders, arg) } /// Unifies `a` and `b` in the given environment. @@ -262,16 +258,19 @@ impl<'s> Fulfill<'s> { for (i, var) in free_vars.into_iter().enumerate() { match var { ParameterKind::Ty(ty) => { - let new_ty = subst.tys.get(&TyInferenceVariable::from_depth(i)) - .expect("apply_solution failed to locate type variable in substitution"); - self.unify(empty_env, &ty.to_ty(), &new_ty) - .expect("apply_solution failed to substitute"); + // Should always be `Some(..)` unless we applied coinductive semantics + // somewhere and hence returned an empty substitution. + if let Some(new_ty) = subst.tys.get(&TyInferenceVariable::from_depth(i)) { + self.unify(empty_env, &ty.to_ty(), &new_ty) + .expect("apply_solution failed to substitute"); + } } ParameterKind::Lifetime(lt) => { - let new_lt = subst.lifetimes.get(&LifetimeInferenceVariable::from_depth(i)) - .expect("apply_solution failed to find lifetime variable in substitution"); - self.unify(empty_env, <.to_lifetime(), &new_lt) - .expect("apply_solution failed to substitute"); + // Same as above. + if let Some(new_lt) = subst.lifetimes.get(&LifetimeInferenceVariable::from_depth(i)) { + self.unify(empty_env, <.to_lifetime(), &new_lt) + .expect("apply_solution failed to substitute"); + } } } } diff --git a/src/solve/infer/instantiate.rs b/src/solve/infer/instantiate.rs index 5d420de95ac..d724dbd56e7 100644 --- a/src/solve/infer/instantiate.rs +++ b/src/solve/infer/instantiate.rs @@ -18,6 +18,21 @@ impl InferenceTable { let mut instantiator = Instantiator { vars }; arg.fold_with(&mut instantiator, 0).expect("") } + + /// Instantiates `arg` with fresh existential variables in the + /// given universe; the kinds of the variables are implied by + /// `binders`. This is used to apply a universally quantified + /// clause like `forall X, 'Y. P => Q`. Here the `binders` + /// argument is referring to `X, 'Y`. + pub fn instantiate_in(&mut self, + universe: UniverseIndex, + binders: U, + arg: &T) -> T::Result + where T: Fold, + U: IntoIterator> + { + self.instantiate(binders.into_iter().map(|pk| pk.map(|_| universe)), arg) + } } struct Instantiator { diff --git a/src/solve/solver.rs b/src/solve/solver.rs index d836f7ae7dc..c5789112120 100644 --- a/src/solve/solver.rs +++ b/src/solve/solver.rs @@ -129,10 +129,31 @@ impl Solver { panic!("overflow depth reached"); } - // If the goal is already on the stack, we found a cycle and indicate it by setting - // `slot.cycle = true`. If there is no cached answer, we can't make any more progress - // and return `Err`. If there is one, use this answer. - if let Some(slot) = self.stack.iter_mut().find(|s| { s.goal == goal }) { + // The goal was already on the stack: we found a cycle. + if let Some(index) = self.stack.iter().position(|s| { s.goal == goal }) { + + // If we are facing a goal of the form `?0: AutoTrait`, we apply coinductive semantics: + // if all the components of the cycle also have coinductive semantics, we accept + // the cycle `(?0: AutoTrait) :- ... :- (?0: AutoTrait)` as an infinite proof for + // `?0: AutoTrait` and we do not perform any substitution. + if self.stack.iter() + .skip(index) + .map(|s| &s.goal) + .chain(Some(&goal)) + .all(|g| g.is_coinductive(&*self.program)) + { + let value = ConstrainedSubst { + subst: Substitution::empty(), + constraints: vec![], + }; + debug!("applying coinductive semantics"); + return Ok(Solution::Unique(Canonical { value, binders: goal.into_binders() })); + } + + // Else we indicate that we found a cycle by setting `slot.cycle = true`. + // If there is no cached answer, we can't make any more progress and return `Err`. + // If there is one, use this answer. + let slot = &mut self.stack[index]; slot.cycle = true; debug!("cycle detected: previous solution {:?}", slot.answer); return slot.answer.clone().ok_or("cycle".into()); @@ -283,7 +304,7 @@ impl Solver { let subst = Substitution::from_binders(&binders); let (goal, (clause, subst)) = fulfill.instantiate(binders.iter().cloned(), &(goal, (clause, subst))); - let ProgramClauseImplication { consequence, conditions} = + let ProgramClauseImplication { consequence, conditions } = fulfill.instantiate_in(goal.environment.universe, clause.binders, &clause.value); fulfill.unify(&goal.environment, &goal.goal, &consequence)?; diff --git a/src/solve/test.rs b/src/solve/test.rs index b5d792da02d..19132b001db 100644 --- a/src/solve/test.rs +++ b/src/solve/test.rs @@ -1423,3 +1423,176 @@ fn inapplicable_assumption_does_not_shadow() { } } } + +#[test] +fn auto_trait_without_impls() { + test! { + program { + #[auto] trait Send { } + + struct i32 { } + + struct Useless { } + + struct Data { + data: T + } + } + + goal { + i32: Send + } yields { + "Unique" + } + + // No fields so `Useless` is `Send`. + goal { + forall { + Useless: Send + } + } yields { + "Unique" + } + + goal { + forall { + if (T: Send) { + Data: Send + } + } + } yields { + "Unique" + } + } +} + +#[test] +fn auto_trait_with_impls() { + test! { + program { + #[auto] trait Send { } + + struct i32 { } + struct f32 { } + struct Vec { } + + impl Send for Vec where T: Send { } + impl !Send for i32 { } + } + + goal { + i32: Send + } yields { + "No possible solution" + } + + goal { + f32: Send + } yields { + "Unique" + } + + goal { + Vec: Send + } yields { + "No possible solution" + } + + goal { + Vec: Send + } yields { + "Unique" + } + + goal { + forall { + Vec: Send + } + } yields { + "CannotProve" + } + } +} + +#[test] +fn coinductive_semantics() { + test! { + program { + #[auto] trait Send { } + + struct i32 { } + + struct Ptr { } + impl Send for Ptr where T: Send { } + + struct List { + data: T, + next: Ptr> + } + } + + goal { + forall { + List: Send + } + } yields { + "CannotProve" + } + + // `WellFormed(T)` because of the hand-written impl for `Ptr`. + goal { + forall { + if (WellFormed(T), T: Send) { + List: Send + } + } + } yields { + "Unique" + } + + goal { + List: Send + } yields { + "Unique" + } + + goal { + exists { + T: Send + } + } yields { + "Ambiguous" + } + } +} + +#[test] +fn mixed_semantics() { + test! { + program { + #[auto] trait Send { } + trait Foo { } + + impl Send for T where T: Foo { } + impl Foo for T where T: Send { } + } + + // We have a cycle `(T: Send) :- (T: Foo) :- (T: Send)` with a non-coinductive + // inner component `T: Foo` so we reject it. + goal { + exists { + T: Send + } + } yields { + "No possible solution" + } + + goal { + exists { + T: Foo + } + } yields { + "No possible solution" + } + } +} diff --git a/src/zip.rs b/src/zip.rs index d5b5cebcb88..070706e6abc 100644 --- a/src/zip.rs +++ b/src/zip.rs @@ -155,6 +155,7 @@ macro_rules! enum_zip { } } +enum_zip!(PolarizedTraitRef { Positive, Negative }); enum_zip!(DomainGoal { Implemented, Normalize, WellFormed }); enum_zip!(LeafGoal { DomainGoal, EqGoal }); enum_zip!(WellFormed { Ty, TraitRef });