Stream: wg-traits

Topic: region constraints


nikomatsakis (Mar 22 2019 at 20:55, on Zulip):

Hey @scalexm do you happen to be around? If so, do you have a link to what happens if you remove the FIXMEs and uncomment this code?

nikomatsakis (Mar 22 2019 at 20:56, on Zulip):

Like, what prompted you to do that in the first place again?

scalexm (Mar 22 2019 at 20:57, on Zulip):

@nikomatsakis this one is actually fine and I think I uncommented it in the fixup PR

nikomatsakis (Mar 22 2019 at 20:57, on Zulip):

Ah. Which one causes problems then?

scalexm (Mar 22 2019 at 20:58, on Zulip):

It was just that, before that PR, we were not forwarding region constraints at all in program_clauses_for; now we do with the fixup PR

scalexm (Mar 22 2019 at 20:58, on Zulip):

@nikomatsakis the ones that pose problem are those coming from unification

scalexm (Mar 22 2019 at 20:59, on Zulip):

@nikomatsakis there is an helper function called into_ex_clause I think

nikomatsakis (Mar 22 2019 at 20:59, on Zulip):

Yeah

nikomatsakis (Mar 22 2019 at 20:59, on Zulip):

What sorts of problems do they cause?

scalexm (Mar 22 2019 at 20:59, on Zulip):

In that function, I commented the line which collects region constraints for unification

nikomatsakis (Mar 22 2019 at 20:59, on Zulip):
crate fn into_ex_clause(result: UnificationResult<'tcx>, ex_clause: &mut ChalkExClause<'tcx>) {
    ex_clause.subgoals.extend(
        result.goals.into_iter().map(Literal::Positive)
    );

    // FIXME: restore this later once we get better at handling regions
    let _ = result.constraints.len(); // trick `-D dead-code`
    // ex_clause.constraints.extend(result.constraints);
}
scalexm (Mar 22 2019 at 21:00, on Zulip):

Well, they end up creating multiple identical solutions but with different region constraints

scalexm (Mar 22 2019 at 21:00, on Zulip):

different syntactically but actually equivalent

scalexm (Mar 22 2019 at 21:00, on Zulip):

But enough for the solver to answer ambiguity

scalexm (Mar 22 2019 at 21:01, on Zulip):

@nikomatsakis I’ve written down a precise example here in some stream, I’ll try to find it

nikomatsakis (Mar 22 2019 at 21:01, on Zulip):

That would be great

scalexm (Mar 22 2019 at 21:05, on Zulip):

@nikomatsakis check the « chalk-integration » stream, November 29th

nikomatsakis (Mar 22 2019 at 21:22, on Zulip):

I see these messages, giving evidence that I've asked you to refresh my memory before :stuck_out_tongue_wink:

nikomatsakis (Mar 22 2019 at 21:22, on Zulip):

I guess this is the initial comment

Last update: Nov 12 2019 at 15:30UTC