Many lifetimes one universe

[leoyvens]

This makes it so that for<'a, 'b> or forall<'a, 'b> are represented as two lifetimes in the same universe, denoted !1'0 and !1'1. This should not change any semantics.

The end goal is to later make u-canonicalization more powerful by putting parameters bound in the same binder in a canonical order (e.g. order of appearance) so that forall<T, U> { Goal(T, U) } and forall<T, U> { Goal(U, T) } get u-canonicalized to the same thing, so hopefully that means this change makes sense.

This fixes #147, I think, though there is followup work to be done for types to also use a UniversalIndex and improving u-canonicalization.

[nikomatsakis]

Cool! Originally, I expected this to be the "everything is a debruijn index" change that we talked about, which I still think is a reasonable end-point to consider shooting for. But this change also makes sense. I'm trying to think if there is a way to observe the difference, but I haven't thought of one yet. I would like to see the representation of types/lifetimes made analogous though.

[nikomatsakis]

I think that types should also use UniversalIndex, no? That is, we should handle lifetimes/types in equivalent ways.

[nikomatsakis]

Nit: maybe {}_{}? e.g., '!1_0 or something? The double ' feels a bit hard for me to read.

[leoyvens]

@nikomatsakis I got curious about this check, I feel like there are assumptions related to regions that are not being spelled out, do you remember what's going on here?

[nikomatsakis]

Huh, it sure doesn't look right to me. We should try to concoct some test. I imagine that this equality would come out as true:

for<'a, 'b> fn(&'a u32, &'b u32) = for<'a> fn(&'a u32, &'a u32)

It's actually debatable whether this is correct -- as described in rust-lang/rust#33684, I think we actually should consider those two types as equal, which may require changes to the unification algorithm implemented here.

But something like this is clearly false, and I imagine that some ordering of it may succeed today?

for<'a, 'b> fn(&'a u32) -> &'b u32 = for<'a> fn(&'a u32) -> &'a u32

[leoyvens]

I don't think either of those equalities would hold under this algorithm since they require 'a = 'b, and didn't understand why we'd want the first one to hold.

[nikomatsakis]

The first one is tricky. I at first thought it should not hold as well, but I now think that this is wrong. The starting point is that if T <: U and U <: T then T = U. And "clearly" the more general form should be a "subtype" of the less general form (since you can trivially instantiate it that way):

for<'a, 'b> fn(&'a u32, &'b u32) <: for<'c> fn(&'c u32, &'c u32)

But what about the reverse? Here, because 'a and 'b only appear in contravariant positions, we can actually consider for<'c> fn(&'c, &'c) to be a subtype of for<'a, 'b> fn(&'a, &'b) because, no matter what regions 'a and 'b are instantated with when the function is called, 'c will just be the intersection of them. Put another way, consider that functions with those two signatures can freely call one another:

fn foo<'a>(x: &'a u32, y: &'a u32) {
    bar(x, y) // OK: 'b and 'c can both be bound to `'a` (or, in fact, the call site)
}

fn bar<'b, 'c>(x: &'b u32, y: &'c u32) {
    foo(x, y) // OK: 'a is inferred to the call site
}

(This is the same argument I made before here)

[leoyvens]

Ah thanks for reviving that comment, the unification is too restrictive then, do we even have that differentiation between a late-bound and early-bound universal in chalk? Should I open an issue to track this?

[nikomatsakis]

OK so there are two separate things, right @leodasvacas? The first is the case where we want equality to be true and the second is one where we do not... I still think this algorithm is incomplete as impl'd, but it'd be nice to find examples of both where it fails.

do we even have that differentiation between a late-bound and early-bound universal in chalk?

We do, yes:

https://github.com/rust-lang-nursery/chalk/blob/62038e04b1cd19a77b3dd2a51903435617c1c333/src/ir.rs#L435

At least if I understood your question.

[leoyvens]

I'm not sure how to call it, but I mean that difference between an universal lifetime in inputs vs in outputs of a function. Can we construct a type in chalk that represents that difference?

[nikomatsakis]

Ah, I see. Well, the difference there arises from variance, and you're right that Chalk just doesn't model that at all, which is part of the problem here I suppose. We may have to start.

[leoyvens]

Thanks for the quick review! I've changed the debug output (new one is really better) and used the same representation for types.

[nikomatsakis]

Heh:

Thanks for the quick review!

and then I dropped it on the floor for 22 days. Sorry about that.

[nikomatsakis]

So... I kind of destroying this PR with my latest one ;) but I am planning to rebase the heart of the changes, I think.

[nikomatsakis]

Wow, I'm impressed with git here. A rebase actually worked.