Merge pull request #82 from scalexm/implied-bounds-ok

Implied bounds, second take

Author: nikomatsakis

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<ParameterKind>, Box<Goal>),
     Exists(Vec<ParameterKind>, Box<Goal>),
-
-    // The `bool` flag indicates whether we should elaborate where clauses or not
-    Implies(Vec<WhereClause>, Box<Goal>, bool),
-
+    Implies(Vec<WhereClause>, Box<Goal>),
     And(Box<Goal>, Box<Goal>),
     Not(Box<Goal>),
 

chalk-parse/src/parser.lalrpop

@@ -29,17 +29,12 @@ pub Goal: Box<Goal> = {
 Goal1: Box<Goal> = {
     "forall" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::ForAll(p, g)),
     "exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
-    <i:IfKeyword> "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, i)),
+    "if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
     "not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
     <w:WhereClause> => Box::new(Goal::Leaf(w)),
     "(" <Goal> ")",
 };
 
-IfKeyword: bool = {
-    "if" => true,
-    "if_raw" => false,
-};
-
 StructDefn: StructDefn = {
     "struct" <n:Id><p:Angle<ParameterKind>> <w:WhereClauses> "{" <f:Fields> "}" => StructDefn {
         name: n,
@@ -187,9 +182,11 @@ WhereClause: WhereClause = {
 
     "WellFormed" "(" <t:Ty> ")" => WhereClause::TyWellFormed { ty: t },
 
-    "WellFormed" "(" <t:TraitRef<":">> ")" => WhereClause::TraitRefWellFormed {
-             trait_ref: t
-    },
+    "WellFormed" "(" <t:TraitRef<":">> ")" => WhereClause::TraitRefWellFormed { trait_ref: t },
+
+    "FromEnv" "(" <t:Ty> ")" => WhereClause::TyFromEnv { ty: t },
+
+    "FromEnv" "(" <t:TraitRef<":">> ")" => WhereClause::TraitRefFromEnv { trait_ref: t },
 
     <a:Ty> "=" <b:Ty> => WhereClause::UnifyTys { a, b },
 

src/cast.rs

@@ -111,13 +111,32 @@ impl Cast<LeafGoal> for WellFormed {
     }
 }
 
+impl Cast<DomainGoal> for FromEnv {
+    fn cast(self) -> DomainGoal {
+        DomainGoal::FromEnv(self)
+    }
+}
+
+impl Cast<LeafGoal> for FromEnv {
+    fn cast(self) -> LeafGoal {
+        LeafGoal::DomainGoal(self.cast())
+    }
+}
+
 impl Cast<Goal> for WellFormed {
     fn cast(self) -> Goal {
         let wcg: LeafGoal = self.cast();
         wcg.cast()
     }
 }
 
+impl Cast<Goal> for FromEnv {
+    fn cast(self) -> Goal {
+        let wcg: LeafGoal = self.cast();
+        wcg.cast()
+    }
+}
+
 impl Cast<Goal> for Normalize {
     fn cast(self) -> Goal {
         let wcg: LeafGoal = self.cast();

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")

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),

src/ir/could_match.rs

@@ -17,12 +17,7 @@ impl<T: Zip> CouldMatch<T> 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

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)

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<Item = U>) expands to (T: Foo<Item = U>), T: Foo, WF(T: Foo).
-    crate fn expanded(self, program: &Program) -> impl Iterator<Item = DomainGoal> {
-        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<Item = Foo>` maps to `WellFormed(T: Trait<Item = Foo>)`
+    /// * 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<K> where K: Hash {
+///     ...
+/// }
+/// ```
+///
+/// then we have the following rule: `WellFormed(Set<K>) :- (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<T> {
+///     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<T> UCanonical<T> {
 }
 
 impl UCanonical<InEnvironment<Goal>> {
-    /// 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,
         }
     }

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()