subtyping and type equality

[nikomatsakis]

Chalk currently has a notion of type unification, but it doesn't have a notion of subtyping. Since trait matching is always invariant, and thus never uses subtyping, you might not think this is important, but it turns out it is when you consider higher-ranked types and variance (annoyingly).

The key invariant is that T1 = T2 if T1 <: T2 and T2 <: T1. The way we handle this equality for higher-ranked types in the rust repo is to translate T1 = T2 into two subtyping requirements. (In fact, rustc has two bits of code that handle this sort of thing, the other one is defined here, and is probably more the model I would want us to use in chalk -- it too translates equality into two subtyping checks.)

The reason that this is specific to higher-ranked types is that:

for<'a> A <: for<'b> B

if forall<'b> { exists<'a> { A <: B } }. In other words, you instantiate one side with forall and one with exists. For now I will leave it an exercise to the reader, but if you work through T1 = for<'a, 'b> fn(&'a u32, &'b u32) and T2 = for<'c> fn(&'c u32), you will find that T1 <: T2 and T2 <: T1 both hold, and therefore T1 = T2 should hold. (I wrote some notes on why this is here.) But chalk wouldn't handle that today.

The work here is to create a "semantic type relator", probably similar to nll_relate in rustc. The way that nll_relate works is that it tracks an "ambient" variance (i.e., are we computing that T1 = T2, T1 <: T2, etc), and when it winds up relating regions, it uses that variance.

[nikomatsakis]

I think the steps here are something like the following

• Generalize our handling of lifetime constraints to consider outlives ('a: 'b) relations and not just equality
• Separate semantic from syntactic equality
• Generalize the semantic equality code so that it carries a variance around and handles higher-ranked equality correctly
• Create Subtype goals (which rustc wants anyway)

[jackh726]

We discussed this in today's meeting: https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits/topic/meeting.2006.2E02.2E2020/near/199548856

[jackh726]

Gonna go ahead and say that #609 closes this