Stream: wg-traits

Topic: unification under binders


tmandry (Nov 13 2019 at 14:13, on Zulip):

@nikomatsakis so, I was looking at your zip_binders PR

tmandry (Nov 13 2019 at 14:14, on Zulip):

and the issue it fixes, which links to the equality_binder test

nikomatsakis (Nov 13 2019 at 14:14, on Zulip):

yep

tmandry (Nov 13 2019 at 14:14, on Zulip):

I have a question about that test

nikomatsakis (Nov 13 2019 at 14:14, on Zulip):

(I'm reminded there was one comment that was niggling at me in that PR that I meant go back and adjust, but carry on)

tmandry (Nov 13 2019 at 14:14, on Zulip):

yes, I think that comment was confusing me as well :)

tmandry (Nov 13 2019 at 14:14, on Zulip):

but also

nikomatsakis (Nov 13 2019 at 14:15, on Zulip):

actually I believe it was referencing a different test

nikomatsakis (Nov 13 2019 at 14:15, on Zulip):

the issue, that is

nikomatsakis (Nov 13 2019 at 14:15, on Zulip):

I think that equality_binder test was behaving correctly before?

nikomatsakis (Nov 13 2019 at 14:15, on Zulip):

though I think I can also anticipate what your question is about it

tmandry (Nov 13 2019 at 14:15, on Zulip):

I see that it generates a constraint for ?0 (which is 'a in the exists<'a>) to equal '!2_0 (which I think corresponds to 'c in for<'c>)

tmandry (Nov 13 2019 at 14:16, on Zulip):

can such a constraint ever be satisfied?

nikomatsakis (Nov 13 2019 at 14:16, on Zulip):

Yes and no

nikomatsakis (Nov 13 2019 at 14:16, on Zulip):

In this example, no

nikomatsakis (Nov 13 2019 at 14:16, on Zulip):

However

nikomatsakis (Nov 13 2019 at 14:17, on Zulip):

you could imagine an example like this

tmandry (Nov 13 2019 at 14:17, on Zulip):

(..but in the equality_binder2 test it can?)

nikomatsakis (Nov 13 2019 at 14:17, on Zulip):
forall<'a> {
    forall<T> {
        forall<'b> {
            if ('a: 'b, 'b: 'a) {
                T = &'b u32
            }
        }
    }
}
nikomatsakis (Nov 13 2019 at 14:18, on Zulip):

Sorry, like that

nikomatsakis (Nov 13 2019 at 14:18, on Zulip):

In this case, 'b cannot be named by T

nikomatsakis (Nov 13 2019 at 14:18, on Zulip):

but 'a can

nikomatsakis (Nov 13 2019 at 14:18, on Zulip):

and 'b is equivalent to 'a

nikomatsakis (Nov 13 2019 at 14:18, on Zulip):

chalk can't really reason about that

nikomatsakis (Nov 13 2019 at 14:18, on Zulip):

this is actually a topic I would like to use as an upcoming design meeting

tmandry (Nov 13 2019 at 14:18, on Zulip):

right, okay

nikomatsakis (Nov 13 2019 at 14:19, on Zulip):

as I've not fully tried to write out all my thoughts about it

nikomatsakis (Nov 13 2019 at 14:19, on Zulip):

but I do not think it is chalk's job to solve these sorts of things, in short

nikomatsakis (Nov 13 2019 at 14:19, on Zulip):

or .. well, it's a mix

nikomatsakis (Nov 13 2019 at 14:19, on Zulip):

I want chalk to do some of this work, and export some of it to polonius :)

nikomatsakis (Nov 13 2019 at 14:20, on Zulip):

anyway, the setup as is is not I think quite perfect, but basically what it tries to do right now is to always generate a constraint, and not assume much of anything

tmandry (Nov 13 2019 at 14:20, on Zulip):

yeah, I'm a little confused by that.. clearly in the logic we have stuff that requires "reasoning about lifetimes," e.g. your example :)

nikomatsakis (Nov 13 2019 at 14:20, on Zulip):

well

nikomatsakis (Nov 13 2019 at 14:20, on Zulip):

I would draw the line there

nikomatsakis (Nov 13 2019 at 14:20, on Zulip):

the trait solver does not, for the most part, reason about lifetimes

nikomatsakis (Nov 13 2019 at 14:20, on Zulip):

nor does the type-checker

nikomatsakis (Nov 13 2019 at 14:20, on Zulip):

but I think it should be able to reason a bit about them, specifically in connection with universes

nikomatsakis (Nov 13 2019 at 14:21, on Zulip):

the trait solver does not, for the most part, reason about lifetimes

this statment is maybe too strong

nikomatsakis (Nov 13 2019 at 14:21, on Zulip):

what I mean is, it doesn't really know which lifetimes outlive which other ones

nikomatsakis (Nov 13 2019 at 14:21, on Zulip):

that is more of an output from trait solving

nikomatsakis (Nov 13 2019 at 14:21, on Zulip):

which lifetimes must outlive which other ones

nikomatsakis (Nov 13 2019 at 14:21, on Zulip):

that is fed into polonius to see if it is satisfiable

tmandry (Nov 13 2019 at 14:22, on Zulip):

okay, right

nikomatsakis (Nov 13 2019 at 14:22, on Zulip):

(but Polonius shouldn't have the job of figuring out the hgiher-ranked relationships, that's something we can figure out)

nikomatsakis (Nov 13 2019 at 14:22, on Zulip):

this is related to some pending rustc PRs too

tmandry (Nov 13 2019 at 14:22, on Zulip):

I guess one thing I'm missing is, what does chalk do with the 'a: 'b, 'b: 'a condition above?

nikomatsakis (Nov 13 2019 at 14:22, on Zulip):

right now, nothing

nikomatsakis (Nov 13 2019 at 14:23, on Zulip):

in fact, we can't even express that right now I don't think

nikomatsakis (Nov 13 2019 at 14:23, on Zulip):

but I think eventually it would use that

nikomatsakis (Nov 13 2019 at 14:23, on Zulip):

specifically when it sees a 'a: 'b that is must prove, it would use logic like this:

nikomatsakis (Nov 13 2019 at 14:23, on Zulip):
nikomatsakis (Nov 13 2019 at 14:24, on Zulip):
nikomatsakis (Nov 13 2019 at 14:24, on Zulip):

in which case, we can try to prove 'a: 'x

nikomatsakis (Nov 13 2019 at 14:24, on Zulip):

the goal would be eventually to find root regions we can convert to outputs

nikomatsakis (Nov 13 2019 at 14:24, on Zulip):

I've mocked this up in lambda prolog

nikomatsakis (Nov 13 2019 at 14:24, on Zulip):

I've been meaning to mock it up in chalk...

nikomatsakis (Nov 13 2019 at 14:25, on Zulip):

there would also be a base rule that forall<'x> { 'static: 'x }

nikomatsakis (Nov 13 2019 at 14:25, on Zulip):

anway if you apply it to this example, the output would be some constraints like 'a: 'a, which is clearly true

nikomatsakis (Nov 13 2019 at 14:25, on Zulip):

(And we could just filter them out)

nikomatsakis (Nov 13 2019 at 14:25, on Zulip):

does that make sense?

tmandry (Nov 13 2019 at 14:25, on Zulip):

hmm I think so

nikomatsakis (Nov 13 2019 at 14:26, on Zulip):

you are motivating me to try and write this up

tmandry (Nov 13 2019 at 14:26, on Zulip):

so it seems like, very naively, you could end up with complex constraints which introduced their own binders

nikomatsakis (Nov 13 2019 at 14:26, on Zulip):

yes can have complex constraints, but they will not have their own binders

nikomatsakis (Nov 13 2019 at 14:26, on Zulip):

our current constraints do

nikomatsakis (Nov 13 2019 at 14:26, on Zulip):

but this is a shift from that approach

tmandry (Nov 13 2019 at 14:26, on Zulip):

and are basically a "subset of chalk goals involving only lifetimes"

nikomatsakis (Nov 13 2019 at 14:27, on Zulip):

the idea is that chalk can handle the binders, in short, but it can't figure out the root constraints

tmandry (Nov 13 2019 at 14:27, on Zulip):

okay, I see

nikomatsakis (Nov 13 2019 at 14:27, on Zulip):

one downside is

nikomatsakis (Nov 13 2019 at 14:27, on Zulip):

that we wll get cosnrtaints like 'a: 'b || 'a: 'c

tmandry (Nov 13 2019 at 14:27, on Zulip):

that's nonobvious to me, but interesting

nikomatsakis (Nov 13 2019 at 14:27, on Zulip):

i.e., one of these must be true, but not both

nikomatsakis (Nov 13 2019 at 14:27, on Zulip):

but that is already true

nikomatsakis (Nov 13 2019 at 14:27, on Zulip):

we have to deal with it somehow, i'm not sure the best way to handle it

tmandry (Nov 13 2019 at 14:27, on Zulip):

right, I remember us talking about that

nikomatsakis (Nov 13 2019 at 14:27, on Zulip):

today's rustc sometimes just gives ambiguous results

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

I would like to get to the point where we have that problem

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

and then worry about it :)

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

for now I think we can be conservative, rustc presently is

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

at least I think so :)

tmandry (Nov 13 2019 at 14:28, on Zulip):

:)

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

in short I want to isolate that problem to the "interface" betwen chalk and polonius

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

chalk can generate the precise constraint

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

maybe we simplify it, or make it more conservative, and then hand it off to polonius

nikomatsakis (Nov 13 2019 at 14:28, on Zulip):

or maybe we even run polonius many times (one for each ||)

nikomatsakis (Nov 13 2019 at 14:29, on Zulip):

until we find a sol'n

nikomatsakis (Nov 13 2019 at 14:29, on Zulip):

that's the worst case

Last update: Dec 12 2019 at 01:25UTC