unification under binders is broken

[nikomatsakis]

The current logic for unifying under binders as broken in two ways. First off, it's specific (rather unnecessarily) to for<'a> types, when it should be applicable to any zippable things. Secondly, it only tests one half of the necessary conditions! In fact, we've got a comment to this effect, somehow:

chalk/chalk-solve/src/infer/unify.rs

Lines 201 to 209 in 3ea7a60

	// for<'a...> T == for<'b...> U
	//
	// if:
	//
	// for<'a...> exists<'b...> T == U &&
	// for<'b...> exists<'a...> T == U
	//
	// Here we only check for<'a...> exists<'b...> T == U,
	// can someone smart comment why this is sufficient?

What I think we should do is two things.

First, we need to instantiate in both directions, as the comment suggests. We should be able to add a "sibling test" to this existing test

chalk/src/test/unify.rs

Lines 122 to 123 in 3ea7a60

	#[test]
	fn equality_binder() {

that looks like this one:

#[test]
fn equality_binder2() {
    test! {
        program {
            struct Ref<'a, 'b> { }
        }

        goal {
            for<'b, 'c> Ref<'b, 'c> = for<'a> Ref<'a, 'a>
        } yields {
            "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }]"
        }

        goal {
            for<'a> Ref<'a, 'a> = for<'b, 'c> Ref<'b, 'c>
        } yields {
            "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }]"
        }
    }
}

Right now, the second test fails for me -- I get lifetime constraints [], which is clearly wrong. We want to be generating constraints like the ones above, which are in fact not reconcilable. (Those constraints say "this is equal if 'b == 'c", which cannot be proven.)

Second, move this logic to zip_binders and remove unify_forall_tys (or make it just invoke zip on its arguments).:

chalk/chalk-solve/src/infer/unify.rs

Lines 384 to 389 in 3ea7a60

	fn zip_binders<T>(&mut self, _: &Binders<T>, _: &Binders<T>) -> Fallible<()>
	where
	T: Zip<ChalkIr> + Fold<ChalkIr, Result = T>,
	{
	panic!("cannot unify things with binders (other than types)")
	}

This should then allow us to support zipping the binders and things inside dyn and impl types using the same routines.

Finally, third, if we like, we could optimize the case where you are zipping two forall with a single argument -- in that case, we could just instantiate with a placeholder on both sides and skip the existentials, I believe. But that's just an optimization.