Lower opaque type kind

Author: detrumi

chalk-integration/src/lowering.rs

@@ -614,13 +614,11 @@ impl LowerTypeKind for TraitDefn {
 
 impl LowerTypeKind for OpaqueTyDefn {
     fn lower_type_kind(&self) -> LowerResult<TypeKind> {
+        let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect();
         Ok(TypeKind {
             sort: TypeSort::Opaque,
             name: self.identifier.str,
-            binders: chalk_ir::Binders::new(
-                vec![], //TODO do we need binders here?
-                (),
-            ),
+            binders: chalk_ir::Binders::new(binders.anonymize(), ()),
         })
     }
 }

chalk-solve/src/clauses/program_clauses.rs

@@ -142,8 +142,7 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
             ApplicationTy {
                 name: TypeName::OpaqueType(self.opaque_ty_id),
                 substitution,
-            }
-            .cast(interner),
+            },
         );
 
         builder.push_binders(&self.bound, |builder, opaque_ty_bound| {

tests/test/existential_types.rs

@@ -6,31 +6,42 @@ use super::*;
 fn opaque_bounds() {
     test! {
         program {
-            trait Direct { }
-            trait Indirect { }
             struct Ty { }
-            impl Direct for Ty { }
-            impl Indirect for Ty { }
 
-            opaque type T: Direct = Ty;
+            trait Clone { }
+            opaque type T: Clone = Ty;
         }
 
         goal {
-            T: Direct
+            T: Clone
         } yields {
             "Unique; substitution []"
         }
+    }
+}
+
+#[test]
+fn opaque_reveal() {
+    test! {
+        program {
+            struct Ty { }
+            trait Trait { }
+            impl Trait for Ty { }
+
+            trait Clone { }
+            opaque type T: Clone = Ty;
+        }
 
         goal {
             if (Reveal) {
-                T: Indirect
+                T: Trait
             }
         } yields {
             "Unique; substitution []"
         }
 
         goal {
-            T: Indirect
+            T: Trait
         } yields {
             "No possible solution"
         }