Merge pull request #563 from nathanwhit/opaque-where-clauses

Support where clauses on opaque types

Author: nikomatsakis

chalk-integration/src/lowering.rs

@@ -594,11 +594,11 @@ impl LowerProgram for Program {
                                         chalk_ir::VariableKind::Ty(TyKind::General),
                                         Atom::from(FIXME_SELF),
                                     )),
-                                    |env1| {
-                                        let interner = env1.interner();
+                                    |env| {
+                                        let interner = env.interner();
                                         Ok(opaque_ty
                                             .bounds
-                                            .lower(&env1)?
+                                            .lower(&env)?
                                             .iter()
                                             .flat_map(|qil| {
                                                 // Instantiate the bounds with the innermost bound variable, which represents Self, as the self type.
@@ -614,8 +614,19 @@ impl LowerProgram for Program {
                                             .collect())
                                     },
                                 )?;
-
-                            Ok(OpaqueTyDatumBound { bounds })
+                            let where_clauses: chalk_ir::Binders<Vec<chalk_ir::Binders<_>>> = env
+                                .in_binders(
+                                Some(chalk_ir::WithKind::new(
+                                    chalk_ir::VariableKind::Ty(TyKind::General),
+                                    Atom::from(FIXME_SELF),
+                                )),
+                                |env| opaque_ty.where_clauses.lower(env),
+                            )?;
+
+                            Ok(OpaqueTyDatumBound {
+                                bounds,
+                                where_clauses,
+                            })
                         })?;
 
                         opaque_ty_data.insert(

chalk-parse/src/ast.rs

@@ -142,6 +142,7 @@ pub struct OpaqueTyDefn {
     pub variable_kinds: Vec<VariableKind>,
     pub identifier: Identifier,
     pub bounds: Vec<QuantifiedInlineBound>,
+    pub where_clauses: Vec<QuantifiedWhereClause>,
 }
 
 #[derive(Clone, PartialEq, Eq, Debug)]

chalk-parse/src/parser.lalrpop

@@ -219,12 +219,14 @@ AssocTyDefn: AssocTyDefn = {
 };
 
 OpaqueTyDefn: OpaqueTyDefn = {
-    "opaque" "type" <identifier:Id> <p:Angle<VariableKind>> ":" <b:Plus<QuantifiedInlineBound>> "=" <ty:Ty> ";" => {
+    "opaque" "type" <identifier:Id> <p:Angle<VariableKind>> ":" <b:Plus<QuantifiedInlineBound>>
+        <w:QuantifiedWhereClauses> "=" <ty:Ty> ";" => {
         OpaqueTyDefn {
             ty,
             variable_kinds: p,
             identifier,
             bounds: b,
+            where_clauses: w,
         }
     }
 };
@@ -332,7 +334,7 @@ TyWithoutId: Ty = {
     "*" <m: RawMutability> <t:Ty> => Ty::Raw{ mutability: m, ty: Box::new(t) },
     "&" <l: Lifetime> "mut" <t:Ty> => Ty::Ref{ mutability: Mutability::Mut, lifetime: l, ty: Box::new(t) },
     "&" <l: Lifetime> <t:Ty> => Ty::Ref{ mutability: Mutability::Not, lifetime: l, ty: Box::new(t) },
-    "[" <t:Ty> "]" => Ty::Slice { ty: Box::new(t) }, 
+    "[" <t:Ty> "]" => Ty::Slice { ty: Box::new(t) },
     "[" <t:Ty> ";" <len:Const> "]" => Ty::Array { ty: Box::new(t), len },
 };
 

chalk-solve/src/clauses/program_clauses.rs

@@ -128,13 +128,14 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyValue<I> {
 }
 
 impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
-    /// Given `opaque type T<..>: A + B = HiddenTy;`, we generate:
+    /// Given `opaque type T<U>: A + B = HiddenTy where U: C;`, we generate:
     ///
     /// ```notrust
-    /// AliasEq(T<..> = HiddenTy) :- Reveal.
-    /// AliasEq(T<..> = !T<..>).
-    /// Implemented(!T<..>: A).
-    /// Implemented(!T<..>: B).
+    /// AliasEq(T<U> = HiddenTy) :- Reveal.
+    /// AliasEq(T<U> = !T<U>).
+    /// WF(T<U>) :- WF(U: C).
+    /// Implemented(!T<U>: A).
+    /// Implemented(!T<U>: B).
     /// ```
     /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`.
     #[instrument(level = "debug", skip(builder))]
@@ -180,7 +181,17 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
                 .cast(interner),
             ));
 
-            let substitution = Substitution::from1(interner, alias_placeholder_ty.clone());
+            // WF(!T<..>) :- WF(WC).
+            builder.push_binders(&opaque_ty_bound.where_clauses, |builder, where_clauses| {
+                builder.push_clause(
+                    WellFormed::Ty(alias_placeholder_ty.clone()),
+                    where_clauses
+                        .into_iter()
+                        .map(|wc| wc.into_well_formed_goal(interner)),
+                );
+            });
+
+            let substitution = Substitution::from1(interner, alias_placeholder_ty);
             for bound in opaque_ty_bound.bounds {
                 // Implemented(!T<..>: Bound).
                 let bound_with_placeholder_ty = bound.substitute(interner, &substitution);

chalk-solve/src/display/stub.rs

@@ -116,6 +116,7 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
             v.bound.binders,
             OpaqueTyDatumBound {
                 bounds: Binders::new(VariableKinds::empty(self.db.interner()), Vec::new()),
+                where_clauses: Binders::new(VariableKinds::empty(self.db.interner()), Vec::new()),
             },
         );
         Arc::new(v)

chalk-solve/src/rust_ir.rs

@@ -643,8 +643,12 @@ pub struct OpaqueTyDatum<I: Interner> {
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner, Visit)]
 pub struct OpaqueTyDatumBound<I: Interner> {
-    /// Trait bounds for the opaque type.
+    /// Trait bounds for the opaque type. These are bounds that the hidden type must meet.
     pub bounds: Binders<Vec<QuantifiedWhereClause<I>>>,
+    /// Where clauses that inform well-formedness conditions for the opaque type.
+    /// These are conditions on the generic parameters of the opaque type which must be true
+    /// for a reference to the opaque type to be well-formed.
+    pub where_clauses: Binders<Vec<QuantifiedWhereClause<I>>>,
 }
 
 #[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]

tests/test/opaque_types.rs

@@ -46,6 +46,57 @@ fn opaque_reveal() {
     }
 }
 
+#[test]
+fn opaque_where_clause() {
+    test! {
+        program {
+            struct Ty { }
+
+            trait Clone { }
+            trait Trait { }
+            impl Trait for Ty { }
+            opaque type T: Clone where T: Trait = Ty;
+
+            struct Vec<U> { }
+            impl<U> Trait for Vec<U> { }
+
+            opaque type S<U>: Clone where U: Trait = Vec<U>;
+        }
+
+        goal {
+            if (T: Trait) {
+                WellFormed(T)
+            }
+        } yields {
+            "Unique; substitution []"
+        }
+
+        goal {
+            WellFormed(T)
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            forall<U> {
+                if (U : Trait) {
+                    WellFormed(S<U>)
+                }
+            }
+        } yields {
+            "Unique; substitution []"
+        }
+
+        goal {
+            forall<U> {
+                WellFormed(S<U>)
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
 #[test]
 fn opaque_generics_simple() {
     test! {