coercion becomes order dependent for higher-ranked functions

[nikomatsakis]

#72493 revealed an interesting interaction between coercion, the universe transition (#56105), and the transition to NLL (#57895). What happens in the old-lub-glb-hr-noteq[12].rs tests introduced by that PR is:

• We have to compute the "coercion LUB" of fn('a, 'b) -> 'a and fn('a, 'a) -> 'a. The "correct answer" is fn('a, 'a) -> 'a. With NLL migration mode, we get a hard error always, but once we enable the NLL mode, our answer depends on the order of the match arms.
• The reason is that the coercion code finds that it can create a subtype for either order, so it produces a result that depends on the ordering. That same code introduces a "equality" requirement in migration mode that results in an error no matter what. But when those errors are suppressed, we generate NLL, and we only enforce subtyping, which either works or doesn't, depending on what type was chosen.

How should we fix this?

• Keep the error? Unfortunate.
• Extend the leak check so it can distinguish these two types correctly and make the coercion code do a "evaluate" that includes a leak check.

[Aaron1011]

@nikomatsakis: I'm interested in working on this. Can you elaborate on how the leak check needs to be modified?

[nikomatsakis]

@Aaron1011 obviously I missed that message -- are you still interested? Can you schedule a slot at https://calendly.com/nikomatsakis to talk it through? I'll need to bring this back in cache.

[nikomatsakis]

So I was just talking to @jackh726 about this bug. The work that @lcnr, @oli-obk and I are doing to implement the newer subtyping algorithm suggested by a-mir-formality will address this problem, I believe, or at least it is a step in the right direction. The key idea of that work that is relevant here is that the job for doing the "leak check" will move into the trait resolver -- this I think is the right home. It's also a new home: today, it lives in the borrow checker, and the problem with this bug is that this comes too late. It used to live in the subtyping code specifically, which was too early, especially with lazy normalization and other more complex topics come into play.

The idea is that when you have an outlives obligation that relates to a placeholder lifetime (e.g., !a: 'b) we can (a) find all each bound 'c0...'cN on !a from the environment (which are always known) and then translate this into an obligation to prove Any('c0: 'b, ..., 'cN: 'b).

The way that this affects this bug is as follows: the coercion LUB code, when it attempts to coerce from fn('a, 'a) -> 'a into fn('a, 'b) -> 'a will generate an unsolveable lifetime requirement. This used to get detected as part of the subtyping check, but that changed when we moved to the current leak-check model (i.e., leak-check occurring in the borrow checker), and hence it was seen as successful, leading to the current situation. If the coercion code allows the fulfillment context to run to completion, that will eventually be detected, and so we can pick the current result (fn('a, 'a) -> 'a) as the more general one (i.e., a fn that returns one of its parameters).

A couple of things need to come together for this to work, but I believe it should be possible.

[nikomatsakis]

In the meantime, what we could do in the coercion code is to extend our check.

Instead of saying, can A be cast to B and -- if so -- making B be the target, we could ask:

• Let A->B be true if A can be cast to B
• Let B->A be true if B can be cast to A

then

• If A->B && !B->A then we want to make B the target
• If B->A && !A->B then we want to make A the target
• Else the two types are equal, which .. is weird because here they are not equal, so we could error, but it seems suboptimal. =)