Check well-formedness of opaque type declarations

rust-lang · Jul 22, 2020 · 34a2a66 · 34a2a66
1 parent 173ebcd
commit 34a2a66
Show file tree

Hide file tree

Showing 2 changed files with 74 additions and 0 deletions.
diff --git a/chalk-integration/src/query.rs b/chalk-integration/src/query.rs
@@ -151,6 +151,10 @@ fn checked_program(db: &impl LoweringDatabase) -> Result<Arc<Program>, ChalkErro
             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)?;
         }

diff --git a/chalk-solve/src/wf.rs b/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",
@@ -269,6 +275,70 @@ 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| {
+            // exists<Self>
+            gb.exists(
+                &bound.where_clauses,
+                (opaque_ty_id, &bound.bounds),
+                |gb, _, where_clauses, (opaque_ty_id, bounds)| {
+                    let interner = gb.interner();
+                    let clauses = where_clauses
+                        .iter()
+                        .cloned()
+                        .map(|wc| wc.into_from_env_goal(interner));
+                    let subst =
+                        Substitution::from1(interner, gb.db().hidden_opaque_type(opaque_ty_id));
+
+                    // if (WellFormed(T: Bar))
+                    gb.implies(clauses, |gb| {
+                        let interner = gb.interner();
+
+                        // all(WellFormed(Baz: Clone))
+                        gb.all(
+                            bounds
+                                .substitute(interner, &subst)
+                                .iter()
+                                .cloned()
+                                .map(|b| b.into_well_formed_goal(interner)),
+                        )
+                    })
+                },
+            )
+        });
+
+        debug!("WF opaque type goal: {:#?}", goal);
+
+        let is_legal = match self
+            .solver_choice
+            .into()
+            .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>(