Merge pull request #463 from flodiebold/generalize-for-builtin-impls

Handle bound vars in builtin trait impls

Author: jackh726

chalk-solve/src/clauses.rs

@@ -225,13 +225,7 @@ fn program_clauses_that_could_match<I: Interner>(
             }
 
             if let Some(well_known) = trait_datum.well_known {
-                builtin_traits::add_builtin_program_clauses(
-                    db,
-                    builder,
-                    well_known,
-                    trait_ref,
-                    self_ty.data(interner),
-                );
+                builtin_traits::add_builtin_program_clauses(db, builder, well_known, trait_ref);
             }
         }
         DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => match &alias_eq.alias {

chalk-solve/src/clauses/builtin_traits.rs

@@ -1,6 +1,6 @@
-use super::builder::ClauseBuilder;
+use super::{builder::ClauseBuilder, generalize};
 use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
-use chalk_ir::{Substitution, Ty, TyData};
+use chalk_ir::{Substitution, Ty};
 
 mod clone;
 mod copy;
@@ -13,22 +13,35 @@ pub fn add_builtin_program_clauses<I: Interner>(
     builder: &mut ClauseBuilder<'_, I>,
     well_known: WellKnownTrait,
     trait_ref: &TraitRef<I>,
-    ty: &TyData<I>,
 ) {
-    if let Some(force_impl) = db.force_impl_for(well_known, ty) {
-        if force_impl {
-            builder.push_fact(trait_ref.clone());
+    // If `trait_ref` contains bound vars, we want to universally quantify them.
+    // `Generalize` collects them for us.
+    let generalized = generalize::Generalize::apply(db.interner(), trait_ref);
+
+    builder.push_binders(&generalized, |builder, trait_ref| {
+        let self_ty = trait_ref.self_type_parameter(db.interner());
+        let ty = self_ty.data(db.interner());
+        if let Some(force_impl) = db.force_impl_for(well_known, ty) {
+            if force_impl {
+                builder.push_fact(trait_ref.clone());
+            }
+            return;
         }
-        return;
-    }
 
-    match well_known {
-        WellKnownTrait::SizedTrait => sized::add_sized_program_clauses(db, builder, trait_ref, ty),
-        WellKnownTrait::CopyTrait => copy::add_copy_program_clauses(db, builder, trait_ref, ty),
-        WellKnownTrait::CloneTrait => clone::add_clone_program_clauses(db, builder, trait_ref, ty),
-        // Drop impls are provided explicitly
-        WellKnownTrait::DropTrait => (),
-    }
+        match well_known {
+            WellKnownTrait::SizedTrait => {
+                sized::add_sized_program_clauses(db, builder, &trait_ref, ty)
+            }
+            WellKnownTrait::CopyTrait => {
+                copy::add_copy_program_clauses(db, builder, &trait_ref, ty)
+            }
+            WellKnownTrait::CloneTrait => {
+                clone::add_clone_program_clauses(db, builder, &trait_ref, ty)
+            }
+            // Drop impls are provided explicitly
+            WellKnownTrait::DropTrait => (),
+        }
+    });
 }
 
 /// Given a trait ref `T0: Trait` and a list of types `U0..Un`, pushes a clause of the form

chalk-solve/src/clauses/generalize.rs

@@ -67,7 +67,7 @@ impl<'i, I: Interner> Folder<'i, I> for Generalize<'i, I> {
         let binder_vec = &mut self.binders;
         let new_index = self.mapping.entry(bound_var).or_insert_with(|| {
             let i = binder_vec.len();
-            binder_vec.push(VariableKind::Ty);
+            binder_vec.push(VariableKind::Lifetime);
             i
         });
         let new_var = BoundVar::new(outer_binder, *new_index);

tests/test/misc.rs

@@ -515,3 +515,43 @@ fn non_enumerable_traits_reorder() {
         }
     }
 }
+
+#[test]
+fn builtin_impl_enumeration() {
+    test! {
+        program {
+            #[lang(copy)]
+            trait Copy { }
+
+            #[lang(sized)]
+            trait Sized { }
+
+            #[lang(clone)]
+            trait Clone { }
+
+            impl Copy for u8 {}
+            impl Clone for u8 {}
+        }
+
+        goal {
+            exists<T> { T: Copy }
+        } yields {
+            // FIXME: wrong, e.g. &u8 is also Copy
+            "Unique; substitution [?0 := Uint(U8)]"
+        }
+
+        goal {
+            exists<T> { T: Clone }
+        } yields {
+            // FIXME: wrong, e.g. &u8 is also Clone
+            "Unique; substitution [?0 := Uint(U8)]"
+        }
+
+        goal {
+            exists<T> { T: Sized }
+        } yields {
+            // FIXME: wrong, most of the built-in types are Sized
+            "No possible solution"
+        }
+    }
+}

tests/test/tuples.rs

@@ -82,13 +82,41 @@ fn tuples_are_sized() {
         } yields {
             "Unique; substitution [], lifetime constraints []"
         }
+
+        goal {
+            exists<T> { (T, u8): Sized }
+        } yields {
+            "Unique; for<?U0> { substitution [?0 := ^0.0], lifetime constraints [] }"
+        }
+
+        goal {
+            forall<T> { (T, u8): Sized }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            forall<T> { (u8, T): Sized }
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            forall<T> { if (T: Sized) { (u8, T): Sized } }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
     }
 }
 
 #[test]
 fn tuples_are_copy() {
     test! {
         program {
+            // FIXME: If we don't declare Copy non-enumerable, `exists<T> { T:
+            // Copy }` gives wrong results, because it doesn't consider the
+            // built-in impls.
+            #[non_enumerable]
             #[lang(copy)]
             trait Copy { }
 
@@ -132,13 +160,26 @@ fn tuples_are_copy() {
         } yields {
             "Unique; substitution [], lifetime constraints []"
         }
+
+        goal {
+            exists<T> { (T, u8): Copy }
+        } yields {
+            "Ambiguous"
+        }
+
+        goal {
+            forall<T> { if (T: Copy) { (T, u8): Copy } }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
     }
 }
 
 #[test]
 fn tuples_are_clone() {
     test! {
         program {
+            #[non_enumerable] // see above
             #[lang(clone)]
             trait Clone { }
 
@@ -182,5 +223,17 @@ fn tuples_are_clone() {
         } yields {
             "Unique; substitution [], lifetime constraints []"
         }
+
+        goal {
+            exists<T> { (T, u8): Clone }
+        } yields {
+            "Ambiguous"
+        }
+
+        goal {
+            forall<T> { if (T: Clone) { (T, u8): Clone } }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
     }
 }