substitute answers into pending goals without using unification

This is not only more efficient, but it also sidesteps the problems that
led to the SLG solver recursing infinitely when unifying goals involving
projections.

This also uncovers a potential flaw with the truncation operation, in
that it does not concern itself with internal binders. For example, we
might truncate a type like `for<'a> fn(Vec<&'a u32>)` into `for<'a>
fn(?X)`. This is problematic because there is no value of `?X` that
could reference `'a`. For now, the SLG solver will panic in this
scenario, but probably truncation needs to truncate the binder as well.

src/solve/infer/unify.rs

@@ -343,23 +343,11 @@ impl<'t> Zipper for Unifier<'t> {
         self.unify_lifetime_lifetime(a, b)
     }
 
-    fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
+    fn zip_binders<T>(&mut self, _: &Binders<T>, _: &Binders<T>) -> Fallible<()>
     where
         T: Zip + Fold<Result = T>,
     {
-        {
-            let a = &self.table.instantiate_binders_universally(a);
-            let b = &self.table.instantiate_binders_existentially(b);
-            let () = self.sub_unify(a, b)?;
-        }
-
-        {
-            let b = &self.table.instantiate_binders_universally(b);
-            let a = &self.table.instantiate_binders_existentially(a);
-            let () = self.sub_unify(a, b)?;
-        }
-
-        Ok(())
+        panic!("cannot unify things with binders (other than types)")
     }
 }
 

src/solve/slg/mod.rs

@@ -2164,18 +2164,6 @@ impl DepthFirstNumber {
     }
 }
 
-impl ExClause {
-    fn with_constraints<I>(mut self, constraints: I) -> Self
-    where
-        I: IntoIterator<Item = InEnvironment<Constraint>>,
-    {
-        self.constraints.extend(constraints);
-        self.constraints.sort();
-        self.constraints.dedup();
-        self
-    }
-}
-
 impl<T> Satisfiable<T> {
     fn yes(self) -> Option<T> {
         match self {