Auto merge of #579 - nathanwhit:opaque-wf, r=nikomatsakis

Check well-formedness of opaque type declarations

chalk-integration/src/query.rs

@@ -177,6 +177,10 @@ fn checked_program(db: &dyn LoweringDatabase) -> Result<Arc<Program>, ChalkError
             solver.verify_adt_decl(id)?;
         }
 
+        for &opaque_ty_id in program.opaque_ty_data.keys() {
+            solver.verify_opaque_ty_decl(opaque_ty_id)?;
+        }
+
         for &impl_id in program.impl_data.keys() {
             solver.verify_trait_impl(impl_id)?;
         }

chalk-solve/src/wf.rs

@@ -16,6 +16,7 @@ use tracing::debug;
 #[derive(Debug)]
 pub enum WfError<I: Interner> {
     IllFormedTypeDecl(chalk_ir::AdtId<I>),
+    IllFormedOpaqueTypeDecl(chalk_ir::OpaqueTyId<I>),
     IllFormedTraitImpl(chalk_ir::TraitId<I>),
 }
 
@@ -27,6 +28,11 @@ impl<I: Interner> fmt::Display for WfError<I> {
                 "type declaration `{:?}` does not meet well-formedness requirements",
                 id
             ),
+            WfError::IllFormedOpaqueTypeDecl(id) => write!(
+                f,
+                "opaque type declaration `{:?}` does not meet well-formedness requirements",
+                id
+            ),
             WfError::IllFormedTraitImpl(id) => write!(
                 f,
                 "trait impl for `{:?}` does not meet well-formedness requirements",
@@ -262,6 +268,63 @@ where
             Err(WfError::IllFormedTraitImpl(trait_id))
         }
     }
+
+    pub fn verify_opaque_ty_decl(&self, opaque_ty_id: OpaqueTyId<I>) -> Result<(), WfError<I>> {
+        // Given an opaque type like
+        // ```notrust
+        // opaque type Foo<T>: Clone where T: Bar = Baz;
+        // ```
+        let interner = self.db.interner();
+
+        let mut gb = GoalBuilder::new(self.db);
+
+        let datum = self.db.opaque_ty_data(opaque_ty_id);
+        let bound = &datum.bound;
+
+        // We make a goal like
+        //
+        // forall<T>
+        let goal = gb.forall(&bound, opaque_ty_id, |gb, _, bound, opaque_ty_id| {
+            let interner = gb.interner();
+
+            let subst = Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id));
+
+            let bounds = bound.bounds.substitute(interner, &subst);
+            let where_clauses = bound.where_clauses.substitute(interner, &subst);
+
+            let clauses = where_clauses
+                .iter()
+                .cloned()
+                .map(|wc| wc.into_from_env_goal(interner));
+
+            // if (WellFormed(T: Bar))
+            gb.implies(clauses, |gb| {
+                let interner = gb.interner();
+
+                // all(WellFormed(Baz: Clone))
+                gb.all(
+                    bounds
+                        .iter()
+                        .cloned()
+                        .map(|b| b.into_well_formed_goal(interner)),
+                )
+            })
+        });
+
+        debug!("WF opaque type goal: {:#?}", goal);
+
+        let mut new_solver = (self.solver_builder)();
+        let is_legal = match new_solver.solve(self.db, &goal.into_closed_goal(interner)) {
+            Some(sol) => sol.is_unique(),
+            None => false,
+        };
+
+        if is_legal {
+            Ok(())
+        } else {
+            Err(WfError::IllFormedOpaqueTypeDecl(opaque_ty_id))
+        }
+    }
 }
 
 fn impl_header_wf_goal<I: Interner>(

tests/test/opaque_types.rs

@@ -7,6 +7,9 @@ fn opaque_bounds() {
             struct Ty { }
 
             trait Clone { }
+
+            impl Clone for Ty { }
+
             opaque type T: Clone = Ty;
         }
 
@@ -27,6 +30,7 @@ fn opaque_reveal() {
             impl Trait for Ty { }
 
             trait Clone { }
+            impl Clone for Ty { }
             opaque type T: Clone = Ty;
         }
 
@@ -53,11 +57,16 @@ fn opaque_where_clause() {
             struct Ty { }
 
             trait Clone { }
+            impl Clone for Ty { }
+
             trait Trait { }
             impl Trait for Ty { }
+
             opaque type T: Clone where T: Trait = Ty;
 
             struct Vec<U> { }
+
+            impl<V> Clone for Vec<V> { }
             impl<U> Trait for Vec<U> { }
 
             opaque type S<U>: Clone where U: Trait = Vec<U>;
@@ -130,6 +139,10 @@ fn opaque_generics() {
             struct Vec<T> { }
             struct Bar { }
 
+            impl<T> Iterator for Vec<T> {
+                type Item = T;
+            }
+
             opaque type Foo<X>: Iterator<Item = X> = Vec<X>;
         }
 
@@ -167,6 +180,9 @@ fn opaque_auto_traits() {
             struct Baz { }
             trait Trait { }
 
+            impl Trait for Bar { }
+            impl Trait for Baz { }
+
             #[auto]
             trait Send { }
 

tests/test/wf_lowering.rs

@@ -1103,3 +1103,29 @@ fn no_unsize_impls() {
         }
     }
 }
+
+#[test]
+fn ill_formed_opaque_ty() {
+    lowering_error! {
+        program {
+            trait Foo {}
+            struct Bar {}
+
+            opaque type T: Foo = Bar;
+        } error_msg {
+            "opaque type declaration `T` does not meet well-formedness requirements"
+        }
+    }
+
+    lowering_error! {
+        program {
+            trait Foo { }
+            struct NotFoo { }
+            struct IsFoo { }
+            impl Foo for IsFoo { }
+            opaque type T: Foo = NotFoo;
+        } error_msg {
+            "opaque type declaration `T` does not meet well-formedness requirements"
+        }
+    }
+}