Auto merge of #607 - Areredify:coerce_unsized, r=jackh726

Add CoerceUnsized builtin rules

So uhh either Im missing an obvious implementation option or we are missing a necessary abstraction to do things in a reasonable manner. The problem I ran into is that there is no way to extend sequent signature and clauses *and* query the solver about them. Consider this:
```
let forall_goals: Binders<Goal<I>> = ...;

gb.forall(forall_goals, |goals| {
    // here, the binders of `forall_goals` are "in environment", but to query the solver, you need to
    // return from `GoalBuilder::forall` and call the solver with the result, you can't query the solver from inside.
    // So, if you want to branch depending on the result of solving the `forall_goal` inside the `GoalBuilder::forall`,
    // you need to return (popping binders from environment), call the solver, and then reenter binders again.
    // At this point, it's easier to manipulate bound vars by hand (what I did in the pr).
})
```
I think an an abstraction similar to goal builder where you can call `forall` and `implies` (and these alone) to push new things to the environment, and then call solver with the goals about vars inside the environment, would be nice, (but Im not sure).

Author: bors

book/src/clauses/well_known_traits.md

@@ -28,26 +28,26 @@ Some common examples of auto traits are `Send` and `Sync`.
 [coinductive_section]: ../engine/logic/coinduction.html#coinduction-and-refinement-strands
 
 # Current state 
-| Type            | Copy | Clone | Sized | Unsize | Drop | FnOnce/FnMut/Fn  | Unpin  | Generator | auto traits |
-| ---             | ---  | ---   | ---   | ---    | ---  | --- | ---    |  ---      |  ---        |
-| tuple types     | ✅    | ✅    | ✅     | ✅     | ⚬    | ⚬  |  ⚬      |  ⚬       |   ✅         |
-| structs         | ⚬    | ⚬    |  ✅    | ✅     | ⚬    | ⚬  |  ⚬      |  ⚬       |   ✅         |
-| scalar types    | 📚    | 📚    | ✅     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |     ✅       |
-| str             | 📚    | 📚    | ⚬     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |     ✅       |
-| never type      | 📚   |  📚   |  ✅   |  ⚬    |  ⚬    | ⚬   |   ⚬    |  ⚬       |  ✅       |
-| trait objects   | ⚬    | ⚬    | ⚬     |  ✅    | ⚬    | ⚬   | ⚬      |  ⚬       |    ⚬        |
-| functions defs  | ✅    | ✅    | ✅     | ⚬     | ⚬    |  ❌  | ⚬      |  ⚬       |     ✅        |
-| functions ptrs  | ✅    | ✅    | ✅     | ⚬     | ⚬    |  ✅  | ⚬      |  ⚬       |     ✅        |
-| raw ptrs        | 📚   |  📚  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |       ✅     |
-| immutable refs  | 📚   |  📚  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |       ✅     |
-| mutable refs    | ⚬    |  ⚬   |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |       ✅     |
-| slices          | ⚬     | ⚬    | ⚬     |   ✅    | ⚬   | ⚬   | ⚬      |  ⚬       |     ✅      |
-| arrays          | ✅     | ✅    | ✅     |   ❌    | ⚬   | ⚬   | ⚬      |  ⚬       |     ✅       |
-| closures❌       | ❌     | ❌    | ❌     | ⚬      | ⚬   | ❌   | ⚬      |  ⚬       |     ✅       |
-| generators❌     |  ⚬    |  ⚬  | ❌     |  ⚬     | ⚬    | ⚬  | ❌      |   ❌       |    ❌       |
-| gen. witness❌   |  ⚬    |   ⚬  |  ⚬   |   ⚬    |  ⚬   |  ⚬ |  ⚬    |   ⚬       |    ❌       |
-| -----------     |       |      |       |        |      |     |        |           |             |
-| well-formedness |  ✅   |  ⚬   | ✅     | ⚬     | ✅    |  ⚬  | ⚬      |  ⚬       |   ⚬         |
+| Type            | Copy | Clone | Sized | Unsize | CoerceUnsized | Drop | FnOnce/FnMut/Fn  | Unpin  | Generator | auto traits |
+| ---             | ---  | ---   | ---   | ---   |      ---       | ---  | --- | ---    |  ---      |  ---        |
+| tuple types     | ✅    | ✅    | ✅     | ✅     |  ⚬             | ⚬    | ⚬  |  ⚬      |  ⚬       |   ✅         |
+| structs         | ⚬    | ⚬    |  ✅    | ✅     |  ⚬             | ⚬    | ⚬  |  ⚬      |  ⚬       |   ✅         |
+| scalar types    | 📚    | 📚    | ✅     | ⚬     | ⚬             | ⚬   |  ⚬  |  ⚬     |  ⚬       |    ✅        |
+| str             | 📚    | 📚    | ⚬     | ⚬     | ⚬            | ⚬    |  ⚬  |  ⚬     |  ⚬       |    ✅        |
+| never type      | 📚   |  📚   |  ✅   |  ⚬    |  ⚬            | ⚬     | ⚬   |   ⚬    |  ⚬       |   ✅       |
+| trait objects   | ⚬    | ⚬    | ⚬     |  ✅    | ⚬            | ⚬     | ⚬   | ⚬      |  ⚬       |    ⚬        |
+| functions defs  | ✅    | ✅    | ✅     | ⚬     | ⚬            | ⚬     |  ❌  | ⚬      |  ⚬       |    ✅         |
+| functions ptrs  | ✅    | ✅    | ✅     | ⚬     | ⚬            | ⚬     |  ✅  | ⚬      |  ⚬       |    ✅         |
+| raw ptrs        | 📚   |  📚  |   ✅   |  ⚬    |   ⚬            | ⚬    |  ⚬  |   ⚬    |   ⚬      |      ✅      |
+| immutable refs  | 📚   |  📚  |   ✅   |  ⚬    |   ⚬            | ⚬    |  ⚬  |   ⚬    |   ⚬      |      ✅      |
+| mutable refs    | ⚬    |  ⚬   |   ✅   |  ⚬    |   ⚬            | ⚬    |  ⚬  |   ⚬    |   ⚬      |      ✅      |
+| slices          | ⚬     | ⚬    | ⚬     |   ✅    | ⚬            | ⚬    | ⚬   | ⚬      |  ⚬       |    ✅       |
+| arrays          | ✅     | ✅    | ✅     |   ❌    | ⚬            | ⚬    | ⚬   | ⚬      |  ⚬       |    ✅        |
+| closures❌       | ❌     | ❌    | ❌     | ⚬      | ⚬            | ⚬    | ❌   | ⚬      |  ⚬       |    ✅        |
+| generators❌     |  ⚬    |  ⚬  | ❌     |  ⚬     | ⚬            | ⚬     | ⚬  | ❌      |   ❌       |    ❌       |
+| gen. witness❌   |  ⚬    |   ⚬  |  ⚬   |   ⚬    |  ⚬            | ⚬    |  ⚬ |  ⚬    |   ⚬       |    ❌       |
+| -----------     |       |      |       |        |             |       |     |        |           |             |
+| well-formedness |  ✅   |  ⚬   | ✅     | ⚬     | ✅            | ✅     |  ⚬  | ⚬      |  ⚬       |   ⚬         |
 
 legend:  
 ⚬ - not applicable  

chalk-integration/src/lowering.rs

@@ -1156,6 +1156,7 @@ impl Lower for WellKnownTrait {
             WellKnownTrait::Fn => rust_ir::WellKnownTrait::Fn,
             WellKnownTrait::Unsize => rust_ir::WellKnownTrait::Unsize,
             WellKnownTrait::Unpin => rust_ir::WellKnownTrait::Unpin,
+            WellKnownTrait::CoerceUnsized => rust_ir::WellKnownTrait::CoerceUnsized,
         }
     }
 }

chalk-ir/src/interner.rs

@@ -726,6 +726,16 @@ where
     type Interner = I;
 }
 
+impl<A, B, C, I> HasInterner for (A, B, C)
+where
+    A: HasInterner<Interner = I>,
+    B: HasInterner<Interner = I>,
+    C: HasInterner<Interner = I>,
+    I: Interner,
+{
+    type Interner = I;
+}
+
 impl<'a, T: HasInterner> HasInterner for std::slice::Iter<'a, T> {
     type Interner = T::Interner;
 }

chalk-ir/src/lib.rs

@@ -477,6 +477,17 @@ impl<I: Interner> Ty<I> {
         }
     }
 
+    /// Returns `Some(adt_id)` if this is an ADT, `None` otherwise
+    pub fn adt_id(&self, interner: &I) -> Option<AdtId<I>> {
+        match self.data(interner) {
+            TyData::Apply(ApplicationTy {
+                name: TypeName::Adt(adt_id),
+                ..
+            }) => Some(*adt_id),
+            _ => None,
+        }
+    }
+
     /// True if this type contains "bound" types/lifetimes, and hence
     /// needs to be shifted across binders. This is a very inefficient
     /// check, intended only for debug assertions, because I am lazy.

chalk-parse/src/ast.rs

@@ -127,6 +127,7 @@ pub enum WellKnownTrait {
     Fn,
     Unsize,
     Unpin,
+    CoerceUnsized,
 }
 
 #[derive(Clone, PartialEq, Eq, Debug)]

chalk-parse/src/parser.lalrpop

@@ -63,6 +63,7 @@ WellKnownTrait: WellKnownTrait = {
      "#" "[" "lang" "(" "fn" ")" "]" => WellKnownTrait::Fn,
      "#" "[" "lang" "(" "unsize" ")" "]" => WellKnownTrait::Unsize,
      "#" "[" "lang" "(" "unpin" ")" "]" => WellKnownTrait::Unpin, 
+     "#" "[" "lang" "(" "coerce_unsized" ")" "]" => WellKnownTrait::CoerceUnsized,
 };
 
 AdtRepr: Atom = "#" "[" "repr" "(" <name:Id> ")" "]" => name.str;

chalk-solve/src/clauses/builtin_traits.rs

@@ -41,12 +41,8 @@ pub fn add_builtin_program_clauses<I: Interner>(
             WellKnownTrait::Unsize => {
                 unsize::add_unsize_program_clauses(db, builder, &trait_ref, ty)
             }
-
-            // Drop impls are provided explicitly
-            WellKnownTrait::Drop => (),
-
-            // There are no special rules for Unpin
-            WellKnownTrait::Unpin => (),
+            // There are no builtin impls provided for the following traits:
+            WellKnownTrait::Unpin | WellKnownTrait::Drop | WellKnownTrait::CoerceUnsized => (),
         }
         Ok(())
     })

chalk-solve/src/coherence/solve.rs

@@ -251,10 +251,7 @@ impl<I: Interner> CoherenceSolver<'_, I> {
 
         let canonical_goal = &goal.into_closed_goal(interner);
         let mut fresh_solver = (self.solver_builder)();
-        let result = match fresh_solver.solve(self.db, canonical_goal) {
-            Some(sol) => sol.is_unique(),
-            None => false,
-        };
+        let result = fresh_solver.has_unique_solution(self.db, canonical_goal);
 
         debug!("specializes: result = {:?}", result);
 

chalk-solve/src/display/items.rs

@@ -194,6 +194,7 @@ impl<I: Interner> RenderAsRust<I> for TraitDatum<I> {
                 WellKnownTrait::Fn => "fn",
                 WellKnownTrait::Unsize => "unsize",
                 WellKnownTrait::Unpin => "unpin",
+                WellKnownTrait::CoerceUnsized => "coerce_unsized",
             };
             writeln!(f, "#[lang({})]", name)?;
         }

chalk-solve/src/rust_ir.rs

@@ -270,6 +270,7 @@ pub enum WellKnownTrait {
     Fn,
     Unsize,
     Unpin,
+    CoerceUnsized,
 }
 
 chalk_ir::const_visit!(WellKnownTrait);

chalk-solve/src/solve.rs

@@ -203,4 +203,17 @@ where
         goal: &UCanonical<InEnvironment<Goal<I>>>,
         f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool,
     ) -> bool;
+
+    /// A convenience method for when one doesn't need the actual solution,
+    /// only whether or not one exists.
+    fn has_unique_solution(
+        &mut self,
+        program: &dyn RustIrDatabase<I>,
+        goal: &UCanonical<InEnvironment<Goal<I>>>,
+    ) -> bool {
+        match self.solve(program, goal) {
+            Some(sol) => sol.is_unique(),
+            None => false,
+        }
+    }
 }