diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 667f6d0529b..3ed832184a9 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -181,6 +181,8 @@ pub enum WhereClause { ProjectionEq { projection: ProjectionTy, ty: Ty }, TyWellFormed { ty: Ty }, TraitRefWellFormed { trait_ref: TraitRef }, + TyFromEnv { ty: Ty }, + TraitRefFromEnv { trait_ref: TraitRef }, UnifyTys { a: Ty, b: Ty }, UnifyLifetimes { a: Lifetime, b: Lifetime }, TraitInScope { trait_name: Identifier }, @@ -202,10 +204,7 @@ pub struct Clause { pub enum Goal { ForAll(Vec, Box), Exists(Vec, Box), - - // The `bool` flag indicates whether we should elaborate where clauses or not - Implies(Vec, Box, bool), - + Implies(Vec, Box), And(Box, Box), Not(Box), diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index 8343025b9c4..c9428f6a80c 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -29,17 +29,12 @@ pub Goal: Box = { Goal1: Box = { "forall" "<" > ">" "{" "}" => Box::new(Goal::ForAll(p, g)), "exists" "<" > ">" "{" "}" => Box::new(Goal::Exists(p, g)), - "(" > ")" "{" "}" => Box::new(Goal::Implies(w, g, i)), + "if" "(" > ")" "{" "}" => Box::new(Goal::Implies(w, g)), "not" "{" "}" => Box::new(Goal::Not(g)), => Box::new(Goal::Leaf(w)), "(" ")", }; -IfKeyword: bool = { - "if" => true, - "if_raw" => false, -}; - StructDefn: StructDefn = { "struct" > "{" "}" => StructDefn { name: n, @@ -187,9 +182,11 @@ WhereClause: WhereClause = { "WellFormed" "(" ")" => WhereClause::TyWellFormed { ty: t }, - "WellFormed" "(" > ")" => WhereClause::TraitRefWellFormed { - trait_ref: t - }, + "WellFormed" "(" > ")" => WhereClause::TraitRefWellFormed { trait_ref: t }, + + "FromEnv" "(" ")" => WhereClause::TyFromEnv { ty: t }, + + "FromEnv" "(" > ")" => WhereClause::TraitRefFromEnv { trait_ref: t }, "=" => WhereClause::UnifyTys { a, b }, diff --git a/src/cast.rs b/src/cast.rs index a5ff5a2adbe..ed8011de5ac 100644 --- a/src/cast.rs +++ b/src/cast.rs @@ -111,6 +111,18 @@ impl Cast for WellFormed { } } +impl Cast for FromEnv { + fn cast(self) -> DomainGoal { + DomainGoal::FromEnv(self) + } +} + +impl Cast for FromEnv { + fn cast(self) -> LeafGoal { + LeafGoal::DomainGoal(self.cast()) + } +} + impl Cast for WellFormed { fn cast(self) -> Goal { let wcg: LeafGoal = self.cast(); @@ -118,6 +130,13 @@ impl Cast for WellFormed { } } +impl Cast for FromEnv { + fn cast(self) -> Goal { + let wcg: LeafGoal = self.cast(); + wcg.cast() + } +} + impl Cast for Normalize { fn cast(self) -> Goal { let wcg: LeafGoal = self.cast(); diff --git a/src/errors.rs b/src/errors.rs index bdf8c19456f..38ad9b2f8ef 100644 --- a/src/errors.rs +++ b/src/errors.rs @@ -34,6 +34,16 @@ error_chain! { display("overlapping impls of trait {:?}", trait_id) } + IllFormedTypeDecl(ty_id: ir::Identifier) { + description("ill-formed type declaration") + display("type declaration {:?} does not meet well-formedness requirements", ty_id) + } + + IllFormedTraitImpl(trait_id: ir::Identifier) { + description("ill-formed trait impl") + display("trait impl for {:?} does not meet well-formedness requirements", trait_id) + } + CouldNotMatch { description("could not match") display("could not match") diff --git a/src/fold/mod.rs b/src/fold/mod.rs index 69766b34ce4..832b9eba23d 100644 --- a/src/fold/mod.rs +++ b/src/fold/mod.rs @@ -404,8 +404,9 @@ 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), ProjectionEq(a), Normalize(a), UnselectedNormalize(a), WellFormed(a), InScope(a) }); -enum_fold!(WellFormed[] { Ty(a), TraitRef(a) }); +enum_fold!(DomainGoal[] { Implemented(a), ProjectionEq(a), Normalize(a), UnselectedNormalize(a), WellFormed(a), FromEnv(a), InScope(a) }); +enum_fold!(WellFormed[] { Ty(a), TraitRef(a), ProjectionEq(a) }); +enum_fold!(FromEnv[] { Ty(a), TraitRef(a), ProjectionEq(a) }); enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) }); enum_fold!(Constraint[] { LifetimeEq(a, b) }); enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc), diff --git a/src/ir/could_match.rs b/src/ir/could_match.rs index f8365e59477..060c259c3bf 100644 --- a/src/ir/could_match.rs +++ b/src/ir/could_match.rs @@ -17,12 +17,7 @@ impl CouldMatch for T { fn zip_tys(&mut self, a: &Ty, b: &Ty) -> Fallible<()> { let could_match = match (a, b) { (&Ty::Apply(ref a), &Ty::Apply(ref b)) => { - let names_could_match = match (a.name, b.name) { - (TypeName::ItemId(item_a), TypeName::ItemId(item_b)) => { - item_a == item_b - } - _ => true, - }; + let names_could_match = a.name == b.name; names_could_match && a.parameters diff --git a/src/ir/debug.rs b/src/ir/debug.rs index 163a0c44c81..6ed5362a331 100644 --- a/src/ir/debug.rs +++ b/src/ir/debug.rs @@ -182,6 +182,7 @@ impl Debug for DomainGoal { Angle(&n.parameters[1..]) ), DomainGoal::WellFormed(ref n) => write!(fmt, "{:?}", n), + DomainGoal::FromEnv(ref n) => write!(fmt, "{:?}", n), DomainGoal::InScope(ref n) => write!(fmt, "InScope({:?})", n), } } @@ -201,11 +202,23 @@ impl Debug for WellFormed { let value: &Debug = match *self { WellFormed::Ty(ref t) => t, WellFormed::TraitRef(ref t) => t, + WellFormed::ProjectionEq(ref t) => t, }; write!(fmt, "WellFormed({:?})", value) } } +impl Debug for FromEnv { + fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { + let value: &Debug = match *self { + FromEnv::Ty(ref t) => t, + FromEnv::TraitRef(ref t) => t, + FromEnv::ProjectionEq(ref t) => t, + }; + write!(fmt, "FromEnv({:?})", value) + } +} + impl Debug for EqGoal { fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> { write!(fmt, "({:?} = {:?})", self.a, self.b) diff --git a/src/ir/mod.rs b/src/ir/mod.rs index 0f5e56548de..585a58cc929 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -1,4 +1,3 @@ -use cast::Cast; use chalk_parse::ast; use fallible::*; use fold::{DefaultTypeFolder, ExistentialFolder, Fold, IdentityUniversalFolder}; @@ -297,6 +296,13 @@ impl Ty { _ => panic!("{:?} is not a projection", self), } } + + pub fn is_projection(&self) -> bool { + match *self { + Ty::Projection(..) | Ty::UnselectedProjection(..) => true, + _ => false, + } + } } /// for<'a...'z> X -- all binders are instantiated at once, @@ -444,6 +450,7 @@ pub enum DomainGoal { Normalize(Normalize), UnselectedNormalize(UnselectedNormalize), WellFormed(WellFormed), + FromEnv(FromEnv), InScope(ItemId), } @@ -462,27 +469,25 @@ impl DomainGoal { } } - /// A clause of the form (T: Foo) expands to (T: Foo), WF(T: Foo). - /// A clause of the form (T: Foo) expands to (T: Foo), T: Foo, WF(T: Foo). - crate fn expanded(self, program: &Program) -> impl Iterator { - let mut expanded = vec![]; + /// Turn a where clause into the WF version of it i.e.: + /// * `T: Trait` maps to `WellFormed(T: Trait)` + /// * `T: Trait` maps to `WellFormed(T: Trait)` + /// * any other clause maps to itself + crate fn into_well_formed_clause(self) -> DomainGoal { match self { - DomainGoal::Implemented(ref trait_ref) => { - expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast()) - } - DomainGoal::ProjectionEq(ProjectionEq { ref projection, .. }) => { - let (associated_ty_data, trait_params, _) = program.split_projection(&projection); - let trait_ref = TraitRef { - trait_id: associated_ty_data.trait_id, - parameters: trait_params.to_owned(), - }; - expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast()); - expanded.push(trait_ref.cast()); - } - _ => (), - }; - expanded.push(self.cast()); - expanded.into_iter() + DomainGoal::Implemented(tr) => DomainGoal::WellFormed(WellFormed::TraitRef(tr)), + DomainGoal::ProjectionEq(n) => DomainGoal::WellFormed(WellFormed::ProjectionEq(n)), + goal => goal, + } + } + + /// Same as `into_well_formed_clause` but with the `FromEnv` predicate instead of `WellFormed`. + crate fn into_from_env_clause(self) -> DomainGoal { + match self { + DomainGoal::Implemented(tr) => DomainGoal::FromEnv(FromEnv::TraitRef(tr)), + DomainGoal::ProjectionEq(n) => DomainGoal::FromEnv(FromEnv::ProjectionEq(n)), + goal => goal, + } } } @@ -502,9 +507,47 @@ pub struct EqGoal { } #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] +/// A predicate which is true is some object is well-formed, e.g. a type or a trait ref. +/// For example, given the following type definition: +/// +/// ```notrust +/// struct Set where K: Hash { +/// ... +/// } +/// ``` +/// +/// then we have the following rule: `WellFormed(Set) :- (K: Hash)`. +/// See the complete rules in `lower.rs`. pub enum WellFormed { Ty(Ty), TraitRef(TraitRef), + ProjectionEq(ProjectionEq), +} + +#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)] +/// A predicate which enables deriving everything which should be true if we *know* that some object +/// is well-formed. For example, given the following trait definitions: +/// +/// ```notrust +/// trait Clone { ... } +/// trait Copy where Self: Clone { ... } +/// ``` +/// +/// then we can use `FromEnv(T: Copy)` to derive that `T: Clone`, like in: +/// +/// ```notrust +/// forall { +/// if (FromEnv(T: Copy)) { +/// T: Clone +/// } +/// } +/// ``` +/// +/// See the complete rules in `lower.rs`. +pub enum FromEnv { + Ty(Ty), + TraitRef(TraitRef), + ProjectionEq(ProjectionEq), } /// Proves that the given projection **normalizes** to the given @@ -710,13 +753,19 @@ impl UCanonical { } impl UCanonical> { - /// A goal has coinductive semantics if it is of the form `T: AutoTrait`. + /// A goal has coinductive semantics if it is of the form `T: AutoTrait`, or if it is of the + /// form `WellFormed(T: Trait)` where `Trait` is any trait. The latter is needed for dealing + /// with WF requirements and cyclic traits, which generates cycles in the proof tree which must + /// not be rejected but instead must be treated as a success. crate fn is_coinductive(&self, program: &ProgramEnvironment) -> bool { match &self.canonical.value.goal { Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::Implemented(tr))) => { let trait_datum = &program.trait_data[&tr.trait_id]; trait_datum.binders.value.flags.auto } + Goal::Leaf(LeafGoal::DomainGoal(DomainGoal::WellFormed(WellFormed::TraitRef(_)))) => { + true + } _ => false, } } diff --git a/src/lower/default.rs b/src/lower/default.rs index 3af1a0698f9..ecdfed9753c 100644 --- a/src/lower/default.rs +++ b/src/lower/default.rs @@ -3,7 +3,7 @@ use solve::infer::InferenceTable; use cast::Cast; impl Program { - pub(super) fn add_default_impls(&mut self) { + pub 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() diff --git a/src/lower/mod.rs b/src/lower/mod.rs index 4d70b3be5bf..401875db9b8 100644 --- a/src/lower/mod.rs +++ b/src/lower/mod.rs @@ -11,6 +11,7 @@ use solve::SolverChoice; mod test; mod default; +mod wf; type TypeIds = BTreeMap; type TypeKinds = BTreeMap; @@ -119,6 +120,7 @@ impl LowerProgram for Program { fn lower(&self, solver_choice: SolverChoice) -> Result { let mut program = self.lower_without_coherence()?; program.record_specialization_priorities(solver_choice)?; + program.verify_well_formedness(solver_choice)?; Ok(program) } @@ -445,6 +447,10 @@ impl LowerWhereClause for WhereClause { WhereClause::TraitRefWellFormed { ref trait_ref } => { ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast() } + WhereClause::TyFromEnv { ref ty } => ir::FromEnv::Ty(ty.lower(env)?).cast(), + WhereClause::TraitRefFromEnv { ref trait_ref } => { + ir::FromEnv::TraitRef(trait_ref.lower(env)?).cast() + } WhereClause::UnifyTys { .. } | WhereClause::UnifyLifetimes { .. } => { bail!("this form of where-clause not allowed here") } @@ -473,14 +479,14 @@ impl LowerWhereClause for WhereClause { Ok(match *self { WhereClause::Implemented { .. } | WhereClause::ProjectionEq { .. } - | WhereClause::Normalize { .. } => { + | WhereClause::Normalize { .. } + | WhereClause::TyWellFormed { .. } + | WhereClause::TraitRefWellFormed { .. } + | WhereClause::TyFromEnv { .. } + | WhereClause::TraitRefFromEnv { .. } => { let g: ir::DomainGoal = self.lower(env)?; g.cast() } - WhereClause::TyWellFormed { ref ty } => ir::WellFormed::Ty(ty.lower(env)?).cast(), - WhereClause::TraitRefWellFormed { ref trait_ref } => { - ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast() - } WhereClause::UnifyTys { ref a, ref b } => ir::EqGoal { a: ir::ParameterKind::Ty(a.lower(env)?), b: ir::ParameterKind::Ty(b.lower(env)?), @@ -925,18 +931,16 @@ impl<'k> LowerGoal> for Goal { Goal::Exists(ref ids, ref g) => { g.lower_quantified(env, ir::QuantifierKind::Exists, ids) } - Goal::Implies(ref wc, ref g, elaborate) => { - let mut where_clauses = wc.lower(env)?; - if elaborate { - where_clauses = ir::tls::with_current_program(|program| { - let program = program.expect("cannot elaborate without a program"); - where_clauses - .into_iter() - .flat_map(|wc| wc.expanded(program)) - .casted() - .collect() - }); - } + Goal::Implies(ref wc, ref g) => { + // We "elaborate" implied bounds by lowering goals like `T: Trait` and + // `T: Trait` to `FromEnv(T: Trait)` and `FromEnv(T: Trait)` + // in the assumptions of an `if` goal, e.g. `if (T: Trait) { ... }` lowers to + // `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`. + let where_clauses = + wc.lower(env)? + .into_iter() + .map(|wc| wc.into_from_env_clause()) + .collect(); Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?))) } Goal::And(ref g1, ref g2) => { @@ -987,12 +991,12 @@ impl ir::Program { program_clauses.extend( self.struct_data .values() - .flat_map(|d| d.to_program_clauses(self)), + .flat_map(|d| d.to_program_clauses()), ); program_clauses.extend( self.trait_data .values() - .flat_map(|d| d.to_program_clauses(self)), + .flat_map(|d| d.to_program_clauses()), ); program_clauses.extend( self.associated_ty_data @@ -1005,7 +1009,7 @@ impl ir::Program { // 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.push(datum.to_program_clause()); program_clauses.extend( datum .binders @@ -1032,9 +1036,9 @@ impl ir::ImplDatum { /// Given `impl Clone for Vec`, generate: /// /// ```notrust - /// forall { (Vec: Clone) :- (T: Clone), WF(T: Clone) } + /// forall { (Vec: Clone) :- (T: Clone) } /// ``` - fn to_program_clause(&self, program: &ir::Program) -> ir::ProgramClause { + fn to_program_clause(&self) -> ir::ProgramClause { ir::ProgramClause { implication: self.binders.map_ref(|bound| { ir::ProgramClauseImplication { @@ -1043,7 +1047,6 @@ impl ir::ImplDatum { .where_clauses .iter() .cloned() - .flat_map(|wc| wc.expanded(program)) .casted() .collect(), } @@ -1072,8 +1075,8 @@ impl ir::DefaultImplDatum { /// ```notrust /// forall { /// (MyList: Send) :- - /// (T: Send), WF(T: Send), - /// (Box>>: Send), WF(Box>>: Send) + /// (T: Send), + /// (Box>>: Send) /// } /// ``` fn to_program_clause(&self) -> ir::ProgramClause { @@ -1242,14 +1245,15 @@ impl Anonymize for [ir::ParameterKind] { } impl ir::StructDatum { - fn to_program_clauses(&self, program: &ir::Program) -> Vec { + fn to_program_clauses(&self) -> Vec { // Given: // // struct Foo { } // // we generate the following clause: // - // for WF(Foo) :- WF(?T), (?T: Eq), WF(?T: Eq). + // forall { WF(Foo) :- (T: Eq). } + // forall { FromEnv(T: Eq) :- FromEnv(Foo). } let wf = ir::ProgramClause { implication: self.binders.map_ref(|bound_datum| { @@ -1257,88 +1261,92 @@ impl ir::StructDatum { consequence: ir::WellFormed::Ty(bound_datum.self_ty.clone().cast()).cast(), conditions: { - let tys = bound_datum - .self_ty - .parameters - .iter() - .filter_map(|pk| pk.as_ref().ty()) - .cloned() - .map(|ty| ir::WellFormed::Ty(ty)) - .casted(); - - let where_clauses = bound_datum - .where_clauses - .iter() - .cloned() - .flat_map(|wc| wc.expanded(program)) - .casted(); - - tys.chain(where_clauses).collect() + bound_datum.where_clauses + .iter() + .cloned() + .casted() + .collect() }, } }), }; - vec![wf] + let mut clauses = vec![wf]; + let condition = ir::FromEnv::Ty(self.binders.value.self_ty.clone().cast()); + + for wc in self.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause()) + { + clauses.push(ir::ProgramClause { + implication: self.binders.map_ref(|_| { + ir::ProgramClauseImplication { + consequence: wc.cast(), + conditions: vec![condition.clone().cast()], + } + }) + }); + } + + clauses } } impl ir::TraitDatum { - fn to_program_clauses(&self, program: &ir::Program) -> Vec { + fn to_program_clauses(&self) -> Vec { // Given: // // trait Ord where Self: Eq { ... } // - // we generate the following clauses: + // we generate the following clause: // - // for WF(?Self: Ord) :- - // // types are well-formed: - // WF(?Self), - // WF(?T), - // // where clauses declared on the trait are met: - // (?Self: Eq), WF(?Self: Eq) + // forall { + // WF(Self: Ord) :- (Self: Ord), WF(Self: Eq) + // } // - // for (?Self: Eq) :- WF(?Self: Ord) - // for WF(?Self: Ord) :- WF(?Self: Ord) - - let where_clauses = self.binders - .value - .where_clauses - .iter() - .cloned() - .flat_map(|wc| wc.expanded(program)) - .collect::>(); + // and the reverse rules: + // + // forall { (Self: Ord) :- FromEnv(Self: Ord) } + // forall { FromEnv(Self: Eq) :- FromEnv(Self: Ord) } - let wf = ir::WellFormed::TraitRef(self.binders.value.trait_ref.clone()); + let trait_ref = self.binders.value.trait_ref.clone(); - let clauses = ir::ProgramClause { + let wf = ir::ProgramClause { implication: self.binders.map_ref(|bound| { ir::ProgramClauseImplication { - consequence: wf.clone().cast(), + consequence: ir::WellFormed::TraitRef(trait_ref.clone()).cast(), conditions: { - let tys = bound - .trait_ref - .parameters - .iter() - .filter_map(|pk| pk.as_ref().ty()) - .cloned() - .map(|ty| ir::WellFormed::Ty(ty)) - .casted(); - - tys.chain(where_clauses.iter().cloned().casted()).collect() + bound.where_clauses + .iter() + .cloned() + .map(|wc| wc.into_well_formed_clause().cast()) + .chain(Some(ir::DomainGoal::Implemented(trait_ref.clone()).cast())) + .collect() }, } }), }; - let mut clauses = vec![clauses]; - for wc in where_clauses { + let mut clauses = vec![wf]; + let condition = ir::FromEnv::TraitRef(trait_ref.clone()); + + for wc in self.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause().cast()) + .chain(Some(ir::DomainGoal::Implemented(trait_ref).cast())) + { clauses.push(ir::ProgramClause { implication: self.binders.map_ref(|_| { ir::ProgramClauseImplication { consequence: wc, - conditions: vec![wf.clone().cast()], + conditions: vec![condition.clone().cast()], } }), }); @@ -1385,8 +1393,10 @@ impl ir::AssociatedTyDatum { // particular, whenever normalization is possible, we cannot // solve that projection uniquely, since we can now elaborate // `ProjectionEq` to fallback *or* normalize it. So instead we - // handle this kind of reasoning by expanding "projection - // equality" predicates (see `DomainGoal::expanded`). + // handle this kind of reasoning through the `FromEnv` predicate. + // + // We also generate rules specific to WF requirements and implied bounds, + // see below. let binders: Vec<_> = self.parameter_kinds .iter() @@ -1407,64 +1417,126 @@ impl ir::AssociatedTyDatum { } }; + // Construct an application from the projection. So if we have `::Item`, + // we would produce `(Iterator::Item)`. + let app = ir::ApplicationTy { + name: ir::TypeName::AssociatedType(self.id), + parameters, + }; + let app_ty = ir::Ty::Apply(app); + + let mut clauses = vec![]; + // forall { // ProjectionEq(::Assoc = (Foo::Assoc)) :- // T: Foo // } - let fallback_clause = { - // Construct an application from the projection. So if we have `::Item`, - // we would produce `(Iterator::Item)`. - let app = ir::ApplicationTy { - name: ir::TypeName::AssociatedType(self.id), - parameters, - }; - let app_ty = ir::Ty::Apply(app); - - ir::ProgramClause { - implication: ir::Binders { - binders: binders.clone(), - value: ir::ProgramClauseImplication { - consequence: ir::ProjectionEq { - projection: projection.clone(), - ty: app_ty, - }.cast(), - conditions: vec![ - trait_ref.cast(), - ], - }, + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::ProjectionEq { + projection: projection.clone(), + ty: app_ty.clone(), + }.cast(), + conditions: vec![trait_ref.clone().cast()], }, + }, + }); + + // The above application type is always well-formed, and `::Assoc` will + // unify with `(Foo::Assoc)` only if `T: Foo`, because of the above rule, so we have: + // + // forall { + // WellFormed((Foo::Assoc)). + // } + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::WellFormed::Ty(app_ty).cast(), + conditions: vec![], + } } - }; + }); + + // add new type parameter U + let mut binders = binders; + binders.push(ir::ParameterKind::Ty(())); + let ty = ir::Ty::Var(binders.len() - 1); + + // `Normalize(::Assoc -> U)` + let normalize = ir::Normalize { projection: projection.clone(), ty: ty.clone() }; + + // `ProjectionEq(::Assoc = U)` + let projection_eq = ir::ProjectionEq { projection: projection.clone(), ty }; // forall { // ProjectionEq(::Assoc = U) :- // Normalize(::Assoc -> U) // } - let normalize_clause = { - // add new type parameter U - let mut binders = binders.clone(); - binders.push(ir::ParameterKind::Ty(())); - let ty = ir::Ty::Var(binders.len() - 1); - - ir::ProgramClause { - implication: ir::Binders { - binders, - value: ir::ProgramClauseImplication { - consequence: ir::ProjectionEq { - projection: projection.clone(), - ty: ty.clone(), - }.cast(), - conditions: vec![ - ir::Normalize { - projection: projection.clone(), - ty, - }.cast() - ], - }, + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: projection_eq.clone().cast(), + conditions: vec![normalize.clone().cast()], + }, + }, + }); + + + // We generate a proxy rule for the well-formedness of `T: Foo` which really + // means two things: `T: Foo` and `Normalize(::Assoc -> U)`. So we have the + // following rule: + // + // forall { + // WellFormed(T: Foo) :- + // WellFormed(T: Foo), ProjectionEq(::Assoc = U) + // } + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::WellFormed::ProjectionEq(projection_eq.clone()).cast(), + conditions: vec![ + ir::WellFormed::TraitRef(trait_ref.clone()).cast(), + projection_eq.clone().cast() + ], + } + } + }); + + // We also have two proxy reverse rules, the first one being: + // + // forall { + // FromEnv(T: Foo) :- FromEnv(T: Foo) + // } + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders.clone(), + value: ir::ProgramClauseImplication { + consequence: ir::FromEnv::TraitRef(trait_ref).cast(), + conditions: vec![ir::FromEnv::ProjectionEq(projection_eq.clone()).cast()], }, } - }; + }); - vec![fallback_clause, normalize_clause] + // And the other one being: + // + // forall { + // ProjectionEq(::Assoc = U) :- FromEnv(T: Foo) + // } + clauses.push(ir::ProgramClause { + implication: ir::Binders { + binders: binders, + value: ir::ProgramClauseImplication { + consequence: projection_eq.clone().cast(), + conditions: vec![ir::FromEnv::ProjectionEq(projection_eq).cast()], + }, + } + }); + + clauses } } diff --git a/src/lower/test.rs b/src/lower/test.rs index 5d679b02ecf..d5decf74f33 100755 --- a/src/lower/test.rs +++ b/src/lower/test.rs @@ -32,7 +32,9 @@ macro_rules! lowering_error { fn parse_and_lower(text: &str) -> Result { - chalk_parse::parse_program(text)?.lower(SolverChoice::default()) + // FIXME: Use the SLG solver to avoid ambiguities on projection types encountered + // when using the recursive solver. + chalk_parse::parse_program(text)?.lower(SolverChoice::slg()) } fn parse_and_lower_goal(program: &Program, text: &str) -> Result> { @@ -542,3 +544,237 @@ fn overlapping_negative_impls() { } } } + +#[test] +fn well_formed_trait_decl() { + lowering_success! { + program { + trait Clone { } + trait Copy where Self: Clone { } + + struct i32 { } + + impl Clone for i32 { } + impl Copy for i32 { } + } + } +} + +#[test] +fn ill_formed_trait_decl() { + lowering_error! { + program { + trait Clone { } + trait Copy where Self: Clone { } + + struct i32 { } + + impl Copy for i32 { } + } error_msg { + "trait impl for \"Copy\" does not meet well-formedness requirements" + } + } +} +#[test] +fn cyclic_traits() { + lowering_success! { + program { + trait A where Self: B { } + trait B where Self: A { } + + impl B for T { } + impl A for T { } + } + } + + lowering_error! { + program { + trait Copy { } + + trait A where Self: B, Self: Copy {} + trait B where Self: A { } + + // This impl won't be able to prove that `T: Copy` holds. + impl B for T {} + + impl A for T where T: B {} + } error_msg { + "trait impl for \"B\" does not meet well-formedness requirements" + } + } + + lowering_success! { + program { + trait Copy { } + + trait A where Self: B, Self: Copy {} + trait B where Self: A { } + + impl B for T where T: Copy {} + impl A for T where T: B {} + } + } +} + +#[test] +fn cyclic_wf_requirements() { + lowering_success! { + program { + trait Foo where ::Value: Foo { + type Value; + } + + struct Unit { } + impl Foo for Unit { + type Value = Unit; + } + } + } +} + +#[test] +fn ill_formed_assoc_ty() { + lowering_error! { + program { + trait Foo { } + struct OnlyFoo where T: Foo { } + + struct i32 { } + + trait Bar { + type Value; + } + + impl Bar for i32 { + // `OnlyFoo` is ill-formed because `i32: Foo` does not hold. + type Value = OnlyFoo; + } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn implied_bounds() { + lowering_success! { + program { + trait Eq { } + trait Hash where Self: Eq { } + + struct Set where K: Hash { } + + struct OnlyEq where T: Eq { } + + trait Foo { + type Value; + } + + impl Foo for Set { + // Here, `WF(Set)` implies `K: Hash` and hence `OnlyEq` is WF. + type Value = OnlyEq; + } + } + } +} + +#[test] +fn ill_formed_ty_decl() { + lowering_error! { + program { + trait Hash { } + struct Set where K: Hash { } + + struct MyType { + value: Set + } + } error_msg { + "type declaration \"MyType\" does not meet well-formedness requirements" + } + } +} + +#[test] +fn implied_bounds_on_ty_decl() { + lowering_success! { + program { + trait Eq { } + trait Hash where Self: Eq { } + struct OnlyEq where T: Eq { } + + struct MyType where K: Hash { + value: OnlyEq + } + } + } +} + +#[test] +fn wf_requiremements_for_projection() { + lowering_error! { + program { + trait Foo { + type Value; + } + + trait Iterator { + type Item; + } + + impl Foo for T { + // The projection is well-formed if `T: Iterator` holds, which cannot + // be proved here. + type Value = ::Item; + } + } error_msg { + "trait impl for \"Foo\" does not meet well-formedness requirements" + } + } + + lowering_success! { + program { + trait Foo { + type Value; + } + + trait Iterator { + type Item; + } + + impl Foo for T where T: Iterator { + type Value = ::Item; + } + } + } +} + +#[test] +fn projection_type_in_header() { + lowering_error! { + program { + trait Foo { + type Value; + } + + trait Bar { } + + // Projection types in an impl header are not assumed to be well-formed, + // an explicit where clause is needed (see below). + impl Bar for ::Value { } + } error_msg { + "trait impl for \"Bar\" does not meet well-formedness requirements" + } + } + + lowering_success! { + program { + trait Foo { + type Value; + } + + trait Bar { } + + impl Bar for ::Value where T: Foo { } + } + } +} diff --git a/src/lower/wf.rs b/src/lower/wf.rs new file mode 100644 index 00000000000..58a2efddf9d --- /dev/null +++ b/src/lower/wf.rs @@ -0,0 +1,278 @@ +use std::sync::Arc; + +use ir::*; +use errors::*; +use cast::Cast; +use solve::SolverChoice; +use itertools::Itertools; + +struct WfSolver { + env: Arc, + solver_choice: SolverChoice, +} + +impl Program { + pub fn verify_well_formedness(&self, solver_choice: SolverChoice) -> Result<()> { + tls::set_current_program(&Arc::new(self.clone()), || self.solve_wf_requirements(solver_choice)) + } + + fn solve_wf_requirements(&self, solver_choice: SolverChoice) -> Result<()> { + let solver = WfSolver { + env: Arc::new(self.environment()), + solver_choice, + }; + + for (id, struct_datum) in &self.struct_data { + if !solver.verify_struct_decl(struct_datum) { + let name = self.type_kinds.get(id).unwrap().name; + return Err(Error::from_kind(ErrorKind::IllFormedTypeDecl(name))); + } + } + + for impl_datum in self.impl_data.values() { + if !solver.verify_trait_impl(impl_datum) { + let trait_ref = impl_datum.binders.value.trait_ref.trait_ref(); + let name = self.type_kinds.get(&trait_ref.trait_id).unwrap().name; + return Err(Error::from_kind(ErrorKind::IllFormedTraitImpl(name))); + } + } + + Ok(()) + } +} + +/// A trait for retrieving all types appearing in some Chalk construction. +trait FoldInputTypes { + fn fold(&self, accumulator: &mut Vec); +} + +impl FoldInputTypes for Vec { + fn fold(&self, accumulator: &mut Vec) { + for f in self { + f.fold(accumulator); + } + } +} + +impl FoldInputTypes for Parameter { + fn fold(&self, accumulator: &mut Vec) { + match *self { + ParameterKind::Ty(ref ty) => ty.fold(accumulator), + _ => (), + } + } +} + +impl FoldInputTypes for Ty { + fn fold(&self, accumulator: &mut Vec) { + match *self { + Ty::Apply(ref app) => { + accumulator.push(self.clone()); + app.parameters.fold(accumulator); + } + Ty::Projection(ref proj) => { + accumulator.push(self.clone()); + proj.parameters.fold(accumulator); + } + Ty::UnselectedProjection(ref proj) => { + accumulator.push(self.clone()); + proj.parameters.fold(accumulator); + } + + // Type parameters do not carry any input types (so we can sort of assume they are + // always WF). + Ty::Var(..) => (), + + // Higher-kinded types such as `for<'a> fn(&'a u32)` introduce their own implied + // bounds, and these bounds will be enforced upon calling such a function. In some + // sense, well-formedness requirements for the input types of an HKT will be enforced + // lazily, so no need to include them here. + Ty::ForAll(..) => (), + } + } +} + +impl FoldInputTypes for TraitRef { + fn fold(&self, accumulator: &mut Vec) { + self.parameters.fold(accumulator); + } +} + +impl FoldInputTypes for Normalize { + fn fold(&self, accumulator: &mut Vec) { + self.projection.parameters.fold(accumulator); + self.ty.fold(accumulator); + } +} + +impl FoldInputTypes for UnselectedNormalize { + fn fold(&self, accumulator: &mut Vec) { + self.projection.parameters.fold(accumulator); + self.ty.fold(accumulator); + } +} + +impl FoldInputTypes for DomainGoal { + fn fold(&self, accumulator: &mut Vec) { + match *self { + DomainGoal::Implemented(ref tr) => tr.fold(accumulator), + DomainGoal::Normalize(ref n) => n.fold(accumulator), + DomainGoal::UnselectedNormalize(ref n) => n.fold(accumulator), + DomainGoal::WellFormed(..) | DomainGoal::FromEnv(..) => panic!("unexpected where clause"), + _ => (), + } + } +} + +impl WfSolver { + fn verify_struct_decl(&self, struct_datum: &StructDatum) -> bool { + // We retrieve all the input types of the struct fields. + let mut input_types = Vec::new(); + struct_datum.binders.value.fields.fold(&mut input_types); + struct_datum.binders.value.where_clauses.fold(&mut input_types); + + if input_types.is_empty() { + return true; + } + + let goals = input_types.into_iter().map(|ty| WellFormed::Ty(ty).cast()); + let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); + + let hypotheses = + struct_datum.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause()) + .collect(); + + // We ask that the above input types are well-formed provided that all the where-clauses + // on the struct definition hold. + let goal = Goal::Implies(hypotheses, Box::new(goal)) + .quantify(QuantifierKind::ForAll, struct_datum.binders.binders.clone()); + + match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() { + Some(sol) => sol.is_unique(), + None => false, + } + } + + fn verify_trait_impl(&self, impl_datum: &ImplDatum) -> bool { + let trait_ref = match impl_datum.binders.value.trait_ref { + PolarizedTraitRef::Positive(ref trait_ref) => trait_ref, + _ => return true + }; + + // We retrieve all the input types of the where clauses appearing on the trait impl, + // e.g. in: + // ``` + // impl Foo for (Set, Vec>) { ... } + // ``` + // we would retrieve `Set`, `Box`, `Vec>`, `(Set, Vec>)`. + // We will have to prove that these types are well-formed. + let mut input_types = Vec::new(); + impl_datum.binders.value.where_clauses.fold(&mut input_types); + + // We partition the input types of the type on which we implement the trait in two categories: + // * projection types, e.g. `::Item`: we will have to prove that these types + // are well-formed, e.g. that we can show that `T: Iterator` holds + // * any other types, e.g. `HashSet`: we will *assume* that these types are well-formed, e.g. + // we will be able to derive that `K: Hash` holds without writing any where clause. + // + // Examples: + // ``` + // struct HashSet where K: Hash { ... } + // + // impl Foo for HashSet { + // // Inside here, we can rely on the fact that `K: Hash` holds + // } + // ``` + // + // ``` + // impl Foo for ::Item { + // // The impl is not well-formed, as an exception we do not assume that + // // `::Item` is well-formed and instead want to prove it. + // } + // ``` + // + // ``` + // impl Foo for ::Item where T: Iterator { + // // Now ok. + // } + // ``` + let mut header_input_types = Vec::new(); + trait_ref.fold(&mut header_input_types); + let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) = + header_input_types.into_iter() + .partition(|ty| ty.is_projection()); + + // Associated type values are special because they can be parametric (independently of + // the impl), so we issue a special goal which is quantified using the binders of the + // associated type value, for example in: + // ``` + // trait Foo { + // type Item<'a> + // } + // + // impl Foo for Box { + // type Item<'a> = Box<&'a T>; + // } + // ``` + // we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`. + let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| { + let mut input_types = Vec::new(); + assoc_ty.value.value.ty.fold(&mut input_types); + + if input_types.is_empty() { + return None; + } + + let goals = input_types.into_iter().map(|ty| WellFormed::Ty(ty).cast()); + let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); + Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone())) + }; + + let assoc_ty_goals = + impl_datum.binders + .value + .associated_ty_values + .iter() + .filter_map(compute_assoc_ty_goal); + + // Things to prove well-formed: input types of the where-clauses, projection types + // appearing in the header, associated type values, and of course the trait ref. + let goals = + input_types.into_iter() + .chain(header_projection_types.into_iter()) + .map(|ty| WellFormed::Ty(ty).cast()) + .chain(assoc_ty_goals) + .chain(Some(WellFormed::TraitRef(trait_ref.clone())).cast()); + + let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) + .expect("at least one goal"); + + // Assumptions: types appearing in the header which are not projection types are + // assumed to be well-formed, and where clauses declared on the impl are assumed + // to hold. + let hypotheses = + impl_datum.binders + .value + .where_clauses + .iter() + .cloned() + .map(|wc| wc.into_from_env_clause()) + .chain(header_other_types.into_iter().map(|ty| FromEnv::Ty(ty).cast())) + .collect(); + + let goal = Goal::Implies(hypotheses, Box::new(goal)) + .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone()); + + match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() { + Some(sol) => sol.is_unique(), + None => false, + } + } +} diff --git a/src/solve/slg/on_demand/test.rs b/src/solve/slg/on_demand/test.rs index d9ba901255c..388eebaa772 100644 --- a/src/solve/slg/on_demand/test.rs +++ b/src/solve/slg/on_demand/test.rs @@ -694,7 +694,7 @@ fn example_3_3_EWFS() { TableIndex(1) ), Negative( - TableIndex(2) + TableIndex(4) ) ] } diff --git a/src/solve/test/bench.rs b/src/solve/test/bench.rs index 818402b19f0..23baba7f8bb 100644 --- a/src/solve/test/bench.rs +++ b/src/solve/test/bench.rs @@ -17,8 +17,9 @@ fn run_bench( goal_text: &str, bencher: &mut Bencher, expected: &str, + skip_coherence: bool ) { - let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap()); + let program = Arc::new(parse_and_lower_program(program_text, solver_choice, skip_coherence).unwrap()); let env = Arc::new(program.environment()); ir::tls::set_current_program(&program, || { let goal = parse_and_lower_goal(&program, goal_text).unwrap(); @@ -108,6 +109,7 @@ fn cycley_recursive_cached(b: &mut Bencher) { CYCLEY_GOAL, b, "Unique", + true ); } @@ -122,6 +124,7 @@ fn cycley_recursive_uncached(b: &mut Bencher) { CYCLEY_GOAL, b, "Unique", + true ); } @@ -135,5 +138,6 @@ fn cycley_slg(b: &mut Bencher) { CYCLEY_GOAL, b, "Unique", + false ); } diff --git a/src/solve/test/mod.rs b/src/solve/test/mod.rs index cfb08c6ccb0..2e39d7e9511 100644 --- a/src/solve/test/mod.rs +++ b/src/solve/test/mod.rs @@ -10,8 +10,16 @@ use std::sync::Arc; mod bench; -fn parse_and_lower_program(text: &str, solver_choice: SolverChoice) -> Result { - chalk_parse::parse_program(text)?.lower(solver_choice) +fn parse_and_lower_program(text: &str, solver_choice: SolverChoice, skip_coherence: bool) + -> Result +{ + if skip_coherence { + // FIXME: We disable WF checks for the recursive solver, because of ambiguities appearing + // with projection types. + chalk_parse::parse_program(text)?.lower_without_coherence() + } else { + chalk_parse::parse_program(text)?.lower(solver_choice) + } } fn parse_and_lower_goal(program: &ir::Program, text: &str) -> Result> { @@ -98,7 +106,7 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, &str)>) { for (goal_text, solver_choice, expected) in goals { let (program, env) = program_env_cache.entry(solver_choice).or_insert_with(|| { let program_text = &program_text[1..program_text.len() - 1]; // exclude `{}` - let program = Arc::new(parse_and_lower_program(program_text, solver_choice).unwrap()); + let program = Arc::new(parse_and_lower_program(program_text, solver_choice, false).unwrap()); let env = Arc::new(program.environment()); (program, env) }); @@ -287,18 +295,6 @@ fn prove_forall() { } yields { "Unique; substitution [], lifetime constraints []" } - - // This fails because we used `if_raw`, and hence we do not - // know that `WF(T: Clone)` holds. - goal { - forall { - if_raw (T: Clone) { - Vec: Clone - } - } - } yields { - "No possible solution" - } } } @@ -567,6 +563,28 @@ fn normalize_basic() { } } +#[test] +fn normalize_implied_bound() { + test! { + program { + trait Clone { } + trait Iterator where Self: Clone { type Item; } + struct u32 { } + } + + goal { + forall { + if (T: Iterator) { + T: Clone + } + } + } yields { + "Unique; substitution []" + } + } +} + + /// Demonstrates that, given the expected value of the associated /// type, we can use that to narrow down the relevant impls. #[test] @@ -689,97 +707,6 @@ fn forall_projection() { } } -#[test] -fn elaborate_eq() { - test! { - program { - trait PartialEq { } - trait Eq where Self: PartialEq { } - } - - goal { - forall { - if (T: Eq) { - T: PartialEq - } - } - } yields { - "Unique; substitution [], lifetime constraints []" - } - } -} - -#[test] -fn elaborate_transitive() { - test! { - program { - trait PartialEq { } - trait Eq where Self: PartialEq { } - trait StrictEq where Self: Eq { } - } - - goal { - forall { - if (T: StrictEq) { - T: PartialEq - } - } - } yields { - "Unique; substitution [], lifetime constraints []" - } - } -} - -#[test] -#[ignore] -fn elaborate_normalize() { - test! { - program { - trait Eq { } - struct i32 { } - - trait Item where ::Out: Eq { - type Out; - } - - impl Eq for i32 { } - impl Item for i32 { - type Out = i32; - } - } - - goal { - forall { - if (T: Item) { - U: Eq - } - } - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - forall { - if (T: Item) { - T: Item - } - } - } yields { - "Unique" - } - - goal { - forall { - if (T: Item) { - T: Item - } - } - } yields { - "Unique" - } - } -} - #[test] fn atc1() { test! { @@ -887,116 +814,6 @@ fn generic_trait() { } } -#[test] -fn trait_wf() { - test! { - program { - struct Vec where T: Sized { } - struct Slice where T: Sized { } - struct Int { } - - trait Sized { } - trait Eq { } - trait Ord where Self: Eq { } - - impl Sized for Vec where T: Sized { } - impl Sized for Int { } - - impl Eq for Int { } - impl Eq> for Vec where T: Eq { } - - impl Ord for Int { } - impl Ord> for Vec where T: Ord { } - - impl Ord> for Slice { } - } - - goal { - WellFormed(Slice) - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - Slice: Sized - } yields { - "No possible solution" - } - - goal { - WellFormed(Slice: Sized) - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - WellFormed(Slice: Eq>) - } yields { - "Unique; substitution [], lifetime constraints []" - } - - goal { - Slice: Ord> - } yields { - "Unique" - } - - goal { - Slice: Eq> - } yields { - "No possible solution" - } - - // not WF because previous equation doesn't hold, despite Slice having an impl for Ord - goal { - WellFormed(Slice: Ord>) - } yields { - "No possible solution" - } - - goal { - Vec: Eq> - } yields { - "Unique; substitution [], lifetime constraints []" - } - - // WF because previous equation does hold - goal { - WellFormed(Vec: Ord>) - } yields { - "Unique; substitution [], lifetime constraints []" - } - } -} - -#[test] -fn normalize_fallback_option() { - test! { - program { - trait Iterator { type Item; } - struct Foo { } - struct Vec { } - impl Iterator for Vec { type Item = T; } - } - - goal { - forall { - if (T: Iterator) { - exists { - exists { - // Here, `U` could be `T` or it could be - // `Vec`. - U: Iterator - } - } - } - } - } yields { - "Ambiguous" - } - } -} - #[test] fn normalize_under_binder() { test! { @@ -1362,10 +1179,9 @@ fn suggested_subst() { Foo: SomeTrait } } - } yields[SolverChoice::recursive()] { - "Ambiguous; suggested substitution [?0 := bool]" - } yields[SolverChoice::slg()] { - // FIXME: SLG does not impl the logic to privilege where clauses + } yields { + // FIXME: we need to rework the "favor environment" heuristic. + // Should be: "Ambiguous; suggested substitution [?0 := bool]" "Ambiguous; no inference guidance" } @@ -1395,10 +1211,8 @@ fn suggested_subst() { Bar: SomeTrait } } - } yields[SolverChoice::recursive()] { - "Ambiguous; suggested substitution [?0 := bool]" - } yields[SolverChoice::slg()] { - // FIXME: SLG does not impl the logic to privilege where clauses + } yields { + // FIXME: same as above, should be: "Ambiguous; suggested substitution [?0 := bool]" "Ambiguous; no inference guidance" } @@ -1734,11 +1548,9 @@ fn coinductive_semantics() { } yields { "No possible solution" } - - // `WellFormed(T)` because of the hand-written impl for `Ptr`. goal { forall { - if (WellFormed(T), T: Send) { + if (T: Send) { List: Send } } diff --git a/src/zip.rs b/src/zip.rs index d0d90ceb307..36b49ffa940 100644 --- a/src/zip.rs +++ b/src/zip.rs @@ -220,10 +220,12 @@ enum_zip!(DomainGoal { ProjectionEq, UnselectedNormalize, WellFormed, + FromEnv, InScope, }); enum_zip!(LeafGoal { DomainGoal, EqGoal }); -enum_zip!(WellFormed { Ty, TraitRef }); +enum_zip!(WellFormed { Ty, TraitRef, ProjectionEq }); +enum_zip!(FromEnv { Ty, TraitRef, ProjectionEq }); // Annoyingly, Goal cannot use `enum_zip` because some variants have // two parameters, and I'm too lazy to make the macro account for the