Stream: wg-traits

Topic: universes and #57639


nikomatsakis (Feb 12 2019 at 16:59, on Zulip):

Hello @WG-compiler-traits ! (oh, and @Aaron Turon, who I don't think is on that alias yet) As discussed yesterday, we'll be doing a kind of walkthrough on this topic + problem today

nikomatsakis (Feb 12 2019 at 17:00, on Zulip):

as ever :P I didn't get as much time to prepare as I would like, so i'm spending a few minutes dropping notes into a paper document

nikomatsakis (Feb 12 2019 at 17:00, on Zulip):

However, part of the point of having people involved, is that this is supposed to be a bit of an interactive walk

nikomatsakis (Feb 12 2019 at 17:00, on Zulip):

with you the audience helping control the flow of instruction :)

nikomatsakis (Feb 12 2019 at 17:00, on Zulip):

so that's sort of by design I guess...

nikomatsakis (Feb 12 2019 at 17:01, on Zulip):

Meeting link: https://zoom.us/j/417259692

Jake Goulding (Feb 12 2019 at 17:04, on Zulip):

/me wishes there was a free service that transcribed this in real time in order to follow along at home

Jake Goulding (Feb 12 2019 at 17:04, on Zulip):

have fun! :heart:

Josh Huber (Feb 12 2019 at 17:53, on Zulip):

surprisingly, I'm available!

Josh Huber (Feb 12 2019 at 17:53, on Zulip):

if i can figure out how to use software.

Josh Huber (Feb 12 2019 at 17:57, on Zulip):

(Oops, I'll just watch the video later :)

nikomatsakis (Feb 12 2019 at 19:29, on Zulip):

dang it, I forgot to use my microphone

nikomatsakis (Feb 12 2019 at 19:30, on Zulip):

voice quality is so much worse when using the headphone mic

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

I'll try to get the video up today but also we need to schedule a follow-up session

tmandry (Feb 13 2019 at 18:01, on Zulip):

tomorrow is pretty open for me, I think

nikomatsakis (Feb 13 2019 at 19:11, on Zulip):

I'll try to get the video up today but also we need to schedule a follow-up session

editing video on windows has proven kind of annoying

Jake Goulding (Feb 13 2019 at 19:44, on Zulip):

@nikomatsakis FWIW, we use Davinci Resolve for our video series. It's pretty amazing and free. It supports at least Mac and Windows

Sunjay Varma (Feb 13 2019 at 19:46, on Zulip):

editing video on windows has proven kind of annoying

Is Windows Movie Maker still a thing? I remember that being easy for simple edits like trimming video, etc.

Laurențiu Nicola (Feb 13 2019 at 21:03, on Zulip):

maybe virtualdub, but I don't know about the codec support

nikomatsakis (Feb 14 2019 at 14:45, on Zulip):

The "Universes" video is now available on YouTube, although I think processing is not yet complete. I also created a Playlist there.

nikomatsakis (Feb 14 2019 at 18:03, on Zulip):

For the next session: How about tomorrow at 14:00 EST?

(cc @Aaron Turon, @Sunjay Varma, @tmandry, who participated in last video)

Aaron Turon (Feb 14 2019 at 18:04, on Zulip):

perfect!

tmandry (Feb 14 2019 at 18:04, on Zulip):

That won't work for me, but I can always watch the video

nikomatsakis (Feb 14 2019 at 18:04, on Zulip):

ok. I'm actually pretty flexible that day.

Aaron Turon (Feb 14 2019 at 18:05, on Zulip):

same

tmandry (Feb 14 2019 at 18:05, on Zulip):

For me, earlier in the morning (before 11am EST) or perhaps late in the afternoon is pretty free

tmandry (Feb 14 2019 at 18:16, on Zulip):

..that's probably not great given everyone's time zones, so I'll sit this one out

Aaron Turon (Feb 14 2019 at 18:23, on Zulip):

earlier is just fine for me!

nikomatsakis (Feb 14 2019 at 22:32, on Zulip):

@tmandry @Aaron Turon I'd really prefer to have both of you if possible -- would 10am or 10:30am work for either of you?

nikomatsakis (Feb 14 2019 at 22:32, on Zulip):

I'm actually quite flexible, it's more @Aaron Turon that I'm concerned about, as that is 7am west coast time

nikomatsakis (Feb 14 2019 at 22:32, on Zulip):

I could also do the afternoon tbh

tmandry (Feb 14 2019 at 22:36, on Zulip):

That works for me, I just might have to leave by 11:30

Sunjay Varma (Feb 14 2019 at 22:46, on Zulip):

10 am or 10:30 work for me :)

tmandry (Feb 15 2019 at 00:31, on Zulip):

If not does 4:30pm or (preferably) 5pm work for you @nikomatsakis?

tmandry (Feb 15 2019 at 00:35, on Zulip):

(sorry, tomorrow's not the best day for me; mon and tues are also bad but I have some availability over the weekend)

nikomatsakis (Feb 15 2019 at 16:07, on Zulip):

Welp, having not heard from @Aaron Turon, I guess we're not doing it at 11 am =)

nikomatsakis (Feb 15 2019 at 16:07, on Zulip):

But also I wound up with some last minute meetings and things

Aaron Turon (Feb 15 2019 at 17:31, on Zulip):

bah, sorry! wouldn't've been able to do that time anyway

Aaron Turon (Feb 15 2019 at 18:03, on Zulip):

@nikomatsakis are we sticking with the currently-scheduled invite, or gonna shoot for next week to catch @tmandry?

nikomatsakis (Feb 15 2019 at 18:50, on Zulip):

@Aaron Turon, @tmandry -- I'm debating about moving that to early next week

nikomatsakis (Feb 15 2019 at 18:50, on Zulip):

today proved to be a lot more full than expected

nikomatsakis (Feb 15 2019 at 18:50, on Zulip):

and I'm only sitting down now to do some of the work I had planned to do earlier

nikomatsakis (Feb 15 2019 at 18:51, on Zulip):

but also I at the co-working space and don't have the good microphone I wanted to use :P

Aaron Turon (Feb 15 2019 at 18:51, on Zulip):

are you thinking you'll pursue a stop-gap fix for the time being?

nikomatsakis (Feb 15 2019 at 18:51, on Zulip):

well, I'm trying to decide what work to do now actually

nikomatsakis (Feb 15 2019 at 18:51, on Zulip):

I think the first thing is to catalog the problems

nikomatsakis (Feb 15 2019 at 18:51, on Zulip):

but also maybe to try and game out a possible stop-gap fix

nikomatsakis (Feb 15 2019 at 18:52, on Zulip):

I guess to that end, I would be game to do a video chat now-ish (even recorded, doesn't matter) just to "rubber duck" and talk out the situation

Aaron Turon (Feb 15 2019 at 18:52, on Zulip):

i'm down for that if it seems helpful :+1:

nikomatsakis (Feb 15 2019 at 18:52, on Zulip):

though I do think a dedicated call trying to more thoroughly explain "how current system works" is a good idea

Aaron Turon (Feb 15 2019 at 18:52, on Zulip):

agreed

nikomatsakis (Feb 15 2019 at 18:52, on Zulip):

(but that can wait a day or two)

nikomatsakis (Feb 15 2019 at 18:52, on Zulip):

ok, what the heck, let me see if there's a 'phonebooth' available

nikomatsakis (Feb 15 2019 at 18:56, on Zulip):

actually, @Aaron Turon, there isn't right now, but I bet we could do this just as well on zulip

Aaron Turon (Feb 15 2019 at 18:56, on Zulip):

wfm!

nikomatsakis (Feb 15 2019 at 18:58, on Zulip):

I believe there are three universe related errors:

nikomatsakis (Feb 15 2019 at 18:58, on Zulip):

I think the middle one is not particularly bothersome

nikomatsakis (Feb 15 2019 at 18:58, on Zulip):

though I have 24 messages still to read in that thread, where @lqd and @tmandry were digging into it some

nikomatsakis (Feb 15 2019 at 18:59, on Zulip):

but I am like 99% sure the problem is a in the region error reporting code, basically that it wasn't fully generalized to account for universes (we had a similar bug in NLL)

nikomatsakis (Feb 15 2019 at 18:59, on Zulip):

let me refresh my memory a bit about #57639...

nikomatsakis (Feb 15 2019 at 19:00, on Zulip):

Ah, right. So the basic problem here is an old one

nikomatsakis (Feb 15 2019 at 19:00, on Zulip):

I summarized it here

nikomatsakis (Feb 15 2019 at 19:01, on Zulip):

in short, we have a where-clause in scope, but that where clause is less general than the impl

nikomatsakis (Feb 15 2019 at 19:01, on Zulip):

well, in this case, it's not the impl

nikomatsakis (Feb 15 2019 at 19:01, on Zulip):

but we have a candidate from the where clause, and one from the trait definition

nikomatsakis (Feb 15 2019 at 19:01, on Zulip):

example test:

nikomatsakis (Feb 15 2019 at 19:02, on Zulip):
trait Foo<'a> {}

trait Bar {
    type Item: for<'a> Foo<'a>;
}

fn foo<'a, T>(_: T)
where
    T: Bar,
    T::Item: Foo<'a>
{}
nikomatsakis (Feb 15 2019 at 19:04, on Zulip):

in this case, the trait definition supplies for<'a> <X as Bar>::Item: Foo<'a>, basically

nikomatsakis (Feb 15 2019 at 19:04, on Zulip):

in the older system that predates universes -- the "leak check" -- we used to wind up with a "unification failure" when considering the where clause

Aaron Turon (Feb 15 2019 at 19:05, on Zulip):

because it would refuse to instantiate the HRTB?

nikomatsakis (Feb 15 2019 at 19:06, on Zulip):

@Aaron Turon do you remember how the leak check worked?

nikomatsakis (Feb 15 2019 at 19:07, on Zulip):

basically the idea was that we would scan the resulting region obligations

nikomatsakis (Feb 15 2019 at 19:07, on Zulip):

you can kind of reframe it in universe terms

nikomatsakis (Feb 15 2019 at 19:07, on Zulip):

effectively it would find all the things that a placeholder was "related" to -- the code (incorrectly) didn't distinguish between R: P and P: R, where P is a placeholder

nikomatsakis (Feb 15 2019 at 19:08, on Zulip):

if any of those regions R were from an "outer universe" -- the way the actual code worked, this meant "pre-existed the region computation", more or less -- it would report a unification error

nikomatsakis (Feb 15 2019 at 19:08, on Zulip):

so in this case, since we are trying to prove that for<'a> T::Item: Foo<'a>...

nikomatsakis (Feb 15 2019 at 19:08, on Zulip):

we would create a placeholder for 'a...

nikomatsakis (Feb 15 2019 at 19:09, on Zulip):

resulting in a where-clause of T::Item: Foo<'!1>

nikomatsakis (Feb 15 2019 at 19:09, on Zulip):

we would then try to unify with the where clause, T::Item: Foo<'a>

nikomatsakis (Feb 15 2019 at 19:09, on Zulip):

then we would scan the reuslting region obligation and observe that 'a == '!1 was required, and give a hard error

Aaron Turon (Feb 15 2019 at 19:09, on Zulip):

got it

nikomatsakis (Feb 15 2019 at 19:09, on Zulip):

so basically we could do something similar

nikomatsakis (Feb 15 2019 at 19:10, on Zulip):

the question is just kind of .. where to do it

nikomatsakis (Feb 15 2019 at 19:10, on Zulip):

this is also why the coherence rules changed

nikomatsakis (Feb 15 2019 at 19:10, on Zulip):

certainly one of my goals with this PR was to change the way this worked

Aaron Turon (Feb 15 2019 at 19:10, on Zulip):

right, i was going to ask, i don't quite understand why we'd want to make the unification fail

nikomatsakis (Feb 15 2019 at 19:10, on Zulip):

(oh, I think that's another "regression report", though I'm not sure it has an issue number)

nikomatsakis (Feb 15 2019 at 19:11, on Zulip):

there are some reasons we don't

nikomatsakis (Feb 15 2019 at 19:11, on Zulip):

among them, it means that -- in principle, at least -- we can have a more efficient type check

nikomatsakis (Feb 15 2019 at 19:11, on Zulip):

since it can ignore regions, bound or unbound

nikomatsakis (Feb 15 2019 at 19:11, on Zulip):

also, there are some other concerns

nikomatsakis (Feb 15 2019 at 19:11, on Zulip):

e.g., eventually I want us to get smarter and extend the system to include implication

nikomatsakis (Feb 15 2019 at 19:12, on Zulip):

so e.g. for<'a> { if ('a: 'b) { 'a: 'b } } should be provable

nikomatsakis (Feb 15 2019 at 19:12, on Zulip):

the idea being that if you have a function type like for<'a> fn(&'b &'a u32), we might infer that if ('b: 'a) { .. } as part of its WF condition or whatever

nikomatsakis (Feb 15 2019 at 19:12, on Zulip):

because that's what it takes for the fn arugments to be WF

nikomatsakis (Feb 15 2019 at 19:13, on Zulip):

this obviously realtes to that bug you found way back when :)

Aaron Turon (Feb 15 2019 at 19:13, on Zulip):

yup, was just thinking about that

nikomatsakis (Feb 15 2019 at 19:13, on Zulip):

all of that said, the current trait checker is pretty dumb here

nikomatsakis (Feb 15 2019 at 19:13, on Zulip):

so it's behavior is not very good

nikomatsakis (Feb 15 2019 at 19:13, on Zulip):

I had hoped that in a chalk-enabled future,

Aaron Turon (Feb 15 2019 at 19:13, on Zulip):

ok so just to be clear, the issue here currently is that the less general where clause ends up obstructing the trait's internal bound, but that in turn makes WF fail?

nikomatsakis (Feb 15 2019 at 19:13, on Zulip):

we would figure out that the reuslting region constraint is actually more complex, and includes an || basically

nikomatsakis (Feb 15 2019 at 19:14, on Zulip):

ok so just to be clear, the issue here currently is that the less general where clause ends up obstructing the trait's internal bound, but that in turn makes WF fail?

right

nikomatsakis (Feb 15 2019 at 19:14, on Zulip):

so what chalk would do here is explore both, and -- if suitably extended -- we could produce a region constraint like 'a == '0 || for<'b> { '0 == 'b }, where only the second half fails

Aaron Turon (Feb 15 2019 at 19:14, on Zulip):

and is that roughly because, since we're trying to push region checking stuff to a separate phase, the where clause looks "good enough" to unify, but then turns out not to be good enough when regions are being checked?

nikomatsakis (Feb 15 2019 at 19:15, on Zulip):

right

nikomatsakis (Feb 15 2019 at 19:15, on Zulip):

I feel like it might be worth digging a bit into what is going on with #46989

nikomatsakis (Feb 15 2019 at 19:15, on Zulip):

since that seems a bit odd, and mabe just flat out wrong

nikomatsakis (Feb 15 2019 at 19:15, on Zulip):

i.e., not a "completeness" problem but a "soundness" problem

Aaron Turon (Feb 15 2019 at 19:16, on Zulip):

OK

nikomatsakis (Feb 15 2019 at 19:17, on Zulip):

I'm going to try to make a more self-contained example real quick

Aaron Turon (Feb 15 2019 at 19:17, on Zulip):

i'm still chewing a bit on the other -- it seems tricky to find a better solution that fits into our general algorithmic approach here. basically we'd need to be more conservative about deciding that a given source of facts is the one to choose if it entails region constraints

Aaron Turon (Feb 15 2019 at 19:17, on Zulip):

but it seems really hard to do that without going all the way to full search

Aaron Turon (Feb 15 2019 at 19:17, on Zulip):

like i'm wondering to what extent this might just be a fundamental issue with treating region checking entirely separately

Aaron Turon (Feb 15 2019 at 19:18, on Zulip):

i can see ways to special-case this particular scenario heuristically

nikomatsakis (Feb 15 2019 at 19:18, on Zulip):

self-contained example (playground):

trait Foo {

}

impl<A> Foo for fn(A) { }

fn assert_foo<T: Foo>() {}

fn main() {
    assert_foo::<fn(&i32)>();
}
Aaron Turon (Feb 15 2019 at 19:18, on Zulip):

like, before we decide on a particular source of a fact (here, the where clause), we search for a more general version of the fact

nikomatsakis (Feb 15 2019 at 19:19, on Zulip):

hmm

Aaron Turon (Feb 15 2019 at 19:19, on Zulip):

(i'm not sure if my terminology here is clear -- i remember things like "candidates" and "confirmation" steps, not sure how current that is)

nikomatsakis (Feb 15 2019 at 19:19, on Zulip):

so I was going to say that going to full search is more-or-less what I was proposing

nikomatsakis (Feb 15 2019 at 19:19, on Zulip):

that's kind of roughly what chalk does

nikomatsakis (Feb 15 2019 at 19:19, on Zulip):

but there are some implications I don't love from that :)

Aaron Turon (Feb 15 2019 at 19:19, on Zulip):

hm

Aaron Turon (Feb 15 2019 at 19:19, on Zulip):

well so, to be more explicit

Aaron Turon (Feb 15 2019 at 19:20, on Zulip):

generally if we find a candidate that seems to work to prove something, modulo region constraints, we just choose it and stop looking elsewhere

Aaron Turon (Feb 15 2019 at 19:20, on Zulip):

but there may be other candidates that also prove that thing while giving different region constraints

nikomatsakis (Feb 15 2019 at 19:20, on Zulip):

to clarify, are you saying that it will be hard to adapt the current solver here?

nikomatsakis (Feb 15 2019 at 19:20, on Zulip):

(the candidate etc stuff is definitely still how things work)

Aaron Turon (Feb 15 2019 at 19:21, on Zulip):

no, i'm thinking more generally in terms of my understanding of greedy search plus separating out region checking

Aaron Turon (Feb 15 2019 at 19:21, on Zulip):

like fundamentally we don't want region checking to inform our search

Aaron Turon (Feb 15 2019 at 19:21, on Zulip):

but to handle this case, we might want to look for the "best" proof of a fact

nikomatsakis (Feb 15 2019 at 19:21, on Zulip):

right -- although I'm not 100% convinced of this also

Aaron Turon (Feb 15 2019 at 19:21, on Zulip):

rather than accepting the first one that looks plausible

nikomatsakis (Feb 15 2019 at 19:22, on Zulip):

but to handle this case, we might want to look for the "best" proof of a fact

well, this is what I meant by disjunction

nikomatsakis (Feb 15 2019 at 19:22, on Zulip):

so what I meant was

Aaron Turon (Feb 15 2019 at 19:22, on Zulip):

ok, i thought maybe, though i don't fully grasp how that would look

Aaron Turon (Feb 15 2019 at 19:23, on Zulip):

are you suggesting that we basically bundle up all possible proofs of a fact, tracking the needed region constraints?

nikomatsakis (Feb 15 2019 at 19:24, on Zulip):

imagine you have two rules to prove something. I'll go a "touch" more abstract.

Foo('a). // for some "free" region 'a
for<'a> Foo('a).

and you have a goal to prove for<'b> Foo('b).

Trying the first option gives you a region constraint of for<'b> { 'a = 'b }. Trying the second option gives you a region constraint of for<'b> { exists<'a> { 'b = 'a } }. You could then say that the result is yes, if the constraint:

for<'b> { 'a = 'b } OR for<'b> { exists<'a> { 'b = 'a } }

is solved.

nikomatsakis (Feb 15 2019 at 19:24, on Zulip):

There are other things that can give rise to this too

nikomatsakis (Feb 15 2019 at 19:24, on Zulip):

for example, where T: Foo<'a>, T: Foo<'b>

nikomatsakis (Feb 15 2019 at 19:24, on Zulip):

now, dealing with OR is annoying

nikomatsakis (Feb 15 2019 at 19:24, on Zulip):

though in this particular case not that annoying

Aaron Turon (Feb 15 2019 at 19:24, on Zulip):

ok so, that's what i thought you were suggesting, but i have questions

Aaron Turon (Feb 15 2019 at 19:25, on Zulip):

most importantly: in general deciding to go with a particular candidate may entail other proof obligations, beyond just the region constraints, right?

nikomatsakis (Feb 15 2019 at 19:25, on Zulip):

yes

Aaron Turon (Feb 15 2019 at 19:25, on Zulip):

or are you imagining limiting this disjunctive combination to "base" facts somehow?

nikomatsakis (Feb 15 2019 at 19:25, on Zulip):

well

nikomatsakis (Feb 15 2019 at 19:26, on Zulip):

no

nikomatsakis (Feb 15 2019 at 19:26, on Zulip):

I mean, yes, that is correct, but

nikomatsakis (Feb 15 2019 at 19:26, on Zulip):

in the chalk solver, at least, there isn't like a "single thread" of proof obligations

nikomatsakis (Feb 15 2019 at 19:26, on Zulip):

so it's not that we have to commit to one choice before we've explored those further proof obligations

nikomatsakis (Feb 15 2019 at 19:26, on Zulip):

or are you imagining limiting this disjunctive combination to "base" facts somehow?

not sure what a "base" fact is

nikomatsakis (Feb 15 2019 at 19:27, on Zulip):

I guess maybe by "base fact" you mean a region constriant?

Aaron Turon (Feb 15 2019 at 19:27, on Zulip):

just one that you get without introducting any additional non-region obligations

nikomatsakis (Feb 15 2019 at 19:27, on Zulip):

yeah

nikomatsakis (Feb 15 2019 at 19:27, on Zulip):

in some sense, there isn't much special about region constraints

Aaron Turon (Feb 15 2019 at 19:27, on Zulip):

so the thing is, in general we could end up with a disjunction that has some region constraints, and some trait constraints, right?

Aaron Turon (Feb 15 2019 at 19:27, on Zulip):

but to "finish" the trait side we need to pick one proof and set of region obligations

Aaron Turon (Feb 15 2019 at 19:28, on Zulip):

but we don't know which one to pick, since the deciding factor is the region constraints

nikomatsakis (Feb 15 2019 at 19:28, on Zulip):

right.

nikomatsakis (Feb 15 2019 at 19:28, on Zulip):

certainly this is the problem with present solver strategy

nikomatsakis (Feb 15 2019 at 19:28, on Zulip):

and it's generally a tricky scenario

nikomatsakis (Feb 15 2019 at 19:29, on Zulip):

but to "finish" the trait side we need to pick one proof and set of region obligations

this part I am not sure is true

nikomatsakis (Feb 15 2019 at 19:29, on Zulip):

it depends on what you mean by "need" and "pick" and "one" :)

Aaron Turon (Feb 15 2019 at 19:29, on Zulip):

hahahaha

nikomatsakis (Feb 15 2019 at 19:29, on Zulip):

ok, one is pretty clear

Aaron Turon (Feb 15 2019 at 19:29, on Zulip):

ok so, i was imagining a relatively strict phase separation

Aaron Turon (Feb 15 2019 at 19:30, on Zulip):

between trait checking and region checking

nikomatsakis (Feb 15 2019 at 19:30, on Zulip):

hmm so i think maybe a way to think of it is like a "value" being a "Fully evaluated expression "in lambda calculus

nikomatsakis (Feb 15 2019 at 19:30, on Zulip):

i.e., the region constraint is a contraint just as a "value" is an expression

Aaron Turon (Feb 15 2019 at 19:30, on Zulip):

sure

nikomatsakis (Feb 15 2019 at 19:31, on Zulip):

so like in a typical prolog solver it basically does a DFS over the proof tree

Aaron Turon (Feb 15 2019 at 19:31, on Zulip):

i guess my question is, are we OK with doing trait solving, then winnowing proofs using region solving, then going back to do more trait solving?

nikomatsakis (Feb 15 2019 at 19:31, on Zulip):

I don't think we have to do that

Aaron Turon (Feb 15 2019 at 19:31, on Zulip):

(i thought we were trying to avoid that interleaving in favor of a strict phase split)

nikomatsakis (Feb 15 2019 at 19:31, on Zulip):

that's what I'm trying to say

Aaron Turon (Feb 15 2019 at 19:32, on Zulip):

ok, but i don't see how to avoid that if we allow trait solving to produce arbitrary disjunctions that mix both trait and region constraints

nikomatsakis (Feb 15 2019 at 19:32, on Zulip):

( though I think one could imagine doing that )

nikomatsakis (Feb 15 2019 at 19:32, on Zulip):

the idea is that you would explore fully the trait constraints

Aaron Turon (Feb 15 2019 at 19:32, on Zulip):

ahhhh

nikomatsakis (Feb 15 2019 at 19:32, on Zulip):

producing a (potentially complex) region constraint

Aaron Turon (Feb 15 2019 at 19:32, on Zulip):

so exhaustively search and "bottom out" in region constraints

nikomatsakis (Feb 15 2019 at 19:32, on Zulip):

right

nikomatsakis (Feb 15 2019 at 19:32, on Zulip):

that said

Aaron Turon (Feb 15 2019 at 19:32, on Zulip):

basically work out the entire proof tree in all possible cases

nikomatsakis (Feb 15 2019 at 19:33, on Zulip):

given that region constraints -- at least some of the time -- can be seen to be unsolveable

Aaron Turon (Feb 15 2019 at 19:33, on Zulip):

are you worried about efficiency though?

nikomatsakis (Feb 15 2019 at 19:33, on Zulip):

maybe it'd be useful to take advatnage of that

Aaron Turon (Feb 15 2019 at 19:33, on Zulip):

yeahok

nikomatsakis (Feb 15 2019 at 19:33, on Zulip):

are you worried about efficiency though?

I am

nikomatsakis (Feb 15 2019 at 19:33, on Zulip):

:)

Aaron Turon (Feb 15 2019 at 19:33, on Zulip):

like we can incorporate shortcut heuristics

Aaron Turon (Feb 15 2019 at 19:33, on Zulip):

to prune things that are "obviously dumb"

nikomatsakis (Feb 15 2019 at 19:33, on Zulip):

yeah

nikomatsakis (Feb 15 2019 at 19:33, on Zulip):

this is why I said:

Aaron Turon (Feb 15 2019 at 19:33, on Zulip):

ok

Aaron Turon (Feb 15 2019 at 19:34, on Zulip):

this is now making sense to me

nikomatsakis (Feb 15 2019 at 19:34, on Zulip):

though in this particular case not that annoying

nikomatsakis (Feb 15 2019 at 19:34, on Zulip):

referring to

nikomatsakis (Feb 15 2019 at 19:34, on Zulip):
for<'b> { 'a = 'b } OR for<'b> { exists<'a> { 'b = 'a } }
nikomatsakis (Feb 15 2019 at 19:34, on Zulip):

because in some sense the left-hand side obviously yields no sol'n

Aaron Turon (Feb 15 2019 at 19:34, on Zulip):

right

nikomatsakis (Feb 15 2019 at 19:34, on Zulip):

one annoying thing about this

Aaron Turon (Feb 15 2019 at 19:34, on Zulip):

we can basically have a highly approximated version of region checking embedded in the trait solver

nikomatsakis (Feb 15 2019 at 19:34, on Zulip):

which is not true in chalk today

Aaron Turon (Feb 15 2019 at 19:34, on Zulip):

to help quickly prune

nikomatsakis (Feb 15 2019 at 19:35, on Zulip):

well basically

nikomatsakis (Feb 15 2019 at 19:35, on Zulip):

it just makes it harder to know when to stop

nikomatsakis (Feb 15 2019 at 19:35, on Zulip):

i.e., if you've found some sol'n with a region constraint like 'a: 'b -- you don't know if maybe there is a better one to be found with a more minimal RC

Aaron Turon (Feb 15 2019 at 19:35, on Zulip):

right

nikomatsakis (Feb 15 2019 at 19:35, on Zulip):

so that is a concern of mine

nikomatsakis (Feb 15 2019 at 19:36, on Zulip):

it's also true that, at least today, we do know the "binder" information in the type check

Aaron Turon (Feb 15 2019 at 19:36, on Zulip):

somewhat related: it feels like we'd want a DAG-ish structure for the proof "forest" we produce -- maybe that falls out from caching though?

Aaron Turon (Feb 15 2019 at 19:36, on Zulip):

(like if multiple avenues of proof wind up generating the same sub-obligations)

nikomatsakis (Feb 15 2019 at 19:36, on Zulip):

that should fall out from caching

nikomatsakis (Feb 15 2019 at 19:36, on Zulip):

if I understand you

nikomatsakis (Feb 15 2019 at 19:36, on Zulip):

I don't think you wre at the chalk session at all hands, right?

nikomatsakis (Feb 15 2019 at 19:37, on Zulip):

I kind of gave a brief overview of how chalk solver works

Aaron Turon (Feb 15 2019 at 19:37, on Zulip):

i wasn't; i have some recollection of how it used to work when i was hacking on it, not sure how much it's changed

nikomatsakis (Feb 15 2019 at 19:37, on Zulip):

a lot ;)

Aaron Turon (Feb 15 2019 at 19:37, on Zulip):

haha ok

nikomatsakis (Feb 15 2019 at 19:37, on Zulip):

I rewrote it completely

nikomatsakis (Feb 15 2019 at 19:37, on Zulip):

based on some papers I was reading

nikomatsakis (Feb 15 2019 at 19:37, on Zulip):

the thing is though

Aaron Turon (Feb 15 2019 at 19:37, on Zulip):

is the rewrite explained on your blog?

nikomatsakis (Feb 15 2019 at 19:38, on Zulip):

I did write a blog post on it

Aaron Turon (Feb 15 2019 at 19:38, on Zulip):

i plan to go re-read all the posts at some point soon

Aaron Turon (Feb 15 2019 at 19:38, on Zulip):

hm

Aaron Turon (Feb 15 2019 at 19:38, on Zulip):

how much do you know about SMT solving?

nikomatsakis (Feb 15 2019 at 19:38, on Zulip):

"an on-demand SLG solver for chalk"

nikomatsakis (Feb 15 2019 at 19:38, on Zulip):

heh, not a lot, but I've been wondering whether I should go try to learn more

Aaron Turon (Feb 15 2019 at 19:38, on Zulip):

it feels related

Aaron Turon (Feb 15 2019 at 19:38, on Zulip):

i don't have a full grasp on the details of how it's done,

nikomatsakis (Feb 15 2019 at 19:38, on Zulip):

I've read a lot into prolog solving techniques but I feel like there are very related techniques in other areas that I am not versed in

nikomatsakis (Feb 15 2019 at 19:39, on Zulip):

I also feel like -- I feel sort of uneasy about the whole approach to region solving

nikomatsakis (Feb 15 2019 at 19:39, on Zulip):

like I'd like a crisp explanation for why it is quite this way and I find it hard to produce it

Aaron Turon (Feb 15 2019 at 19:39, on Zulip):

but the setup is like: you have a core SAT solver which understands logical operators, but not domain-specific facts; you then have various "theory solvers" that can deal with specific kinds of constraints. the SMT solver coordinates back and forth between doing SAT solving and theory solving to find its way quickly to a proof

Aaron Turon (Feb 15 2019 at 19:40, on Zulip):

so you're interleaving different kinds of proof/constraint solving, in a hopefully smart way

nikomatsakis (Feb 15 2019 at 19:40, on Zulip):

that said, I was exploring this in a series of blog posts (polonius + region errors and polonius + hereditary harrop) and I feel like a phase separation is in some sense very useful for interfacing between "polonius" plus "trait solving"

nikomatsakis (Feb 15 2019 at 19:40, on Zulip):

interesting

Aaron Turon (Feb 15 2019 at 19:41, on Zulip):

now, my recollection from a long while ago is that you were hoping to get a strict separation, somewhere, between trait and region solving so that for trait solving we could work on erased regions, basically

nikomatsakis (Feb 15 2019 at 19:41, on Zulip):

right, so that is part of it

nikomatsakis (Feb 15 2019 at 19:41, on Zulip):

but it feels like it's not strictly necessary

Aaron Turon (Feb 15 2019 at 19:41, on Zulip):

right

Aaron Turon (Feb 15 2019 at 19:41, on Zulip):

but it's tied up with whether we "interleave", right?

Aaron Turon (Feb 15 2019 at 19:41, on Zulip):

like, if we could interleave, then instead of bottoming out "all the proofs" we could just jump into region solving to help narrow

nikomatsakis (Feb 15 2019 at 19:42, on Zulip):

yeah, right. We have to be able to convince ourselves that region solving is not influencing our decisions in some way that would go differently at codegen time

nikomatsakis (Feb 15 2019 at 19:42, on Zulip):

like, if we could interleave, then instead of bottoming out "all the proofs" we could just jump into region solving to help narrow

the thing is...

nikomatsakis (Feb 15 2019 at 19:42, on Zulip):

...what exactly is region solving?

nikomatsakis (Feb 15 2019 at 19:42, on Zulip):

But also, if the solving we are talking about is mostly about higher-ranked things

nikomatsakis (Feb 15 2019 at 19:42, on Zulip):

e.g., universe-style violations

nikomatsakis (Feb 15 2019 at 19:42, on Zulip):

we can actually detect it earlier

Aaron Turon (Feb 15 2019 at 19:42, on Zulip):

right

nikomatsakis (Feb 15 2019 at 19:42, on Zulip):

which is what we do today, just poorly

nikomatsakis (Feb 15 2019 at 19:43, on Zulip):

er, pre-universe I mean

Aaron Turon (Feb 15 2019 at 19:43, on Zulip):

yeah

nikomatsakis (Feb 15 2019 at 19:43, on Zulip):

"yesterday"

nikomatsakis (Feb 15 2019 at 19:43, on Zulip):

I think this example is also quite relevant

nikomatsakis (Feb 15 2019 at 19:43, on Zulip):

since we're talking about this topic at a pretty general elvel

nikomatsakis (Feb 15 2019 at 19:43, on Zulip):

level

Aaron Turon (Feb 15 2019 at 19:43, on Zulip):

ok so i think we understand each other, and i think i agree with your instincts about "bottom out all potential proofs into a 'residue' of region constraints, which may include disjunction"

nikomatsakis (Feb 15 2019 at 19:44, on Zulip):
fn foo<T>()
where T: Foo<'a> + Foo<'b>
{
    <T as Foo<'_>>::bar(...) // what do we infer the `'_` to be? `'a` or `'b`?
}
nikomatsakis (Feb 15 2019 at 19:44, on Zulip):

ok so i think we understand each other, and i think i agree with your instincts about "bottom out all potential proofs into a 'residue' of region constraints, which may include disjunction"

yeah, it's at least a viable path. it may be inefficient.

Aaron Turon (Feb 15 2019 at 19:44, on Zulip):

(it seems ok in part because i think it will generally be fairly unusual to have multiple, substantially different ways of proving a given obligation, so the extra searching here will be minimal in practice)

nikomatsakis (Feb 15 2019 at 19:44, on Zulip):

that is my guess, yes

nikomatsakis (Feb 15 2019 at 19:44, on Zulip):

that said

nikomatsakis (Feb 15 2019 at 19:44, on Zulip):

if we pop the stack

nikomatsakis (Feb 15 2019 at 19:44, on Zulip):

and we look at #46989, and the example I produced for it

nikomatsakis (Feb 15 2019 at 19:45, on Zulip):

it seems pretty clear that the universe code itself has a bug

nikomatsakis (Feb 15 2019 at 19:45, on Zulip):

i.e., I don't expect this code to typecheck (playground)

nikomatsakis (Feb 15 2019 at 19:45, on Zulip):
trait Foo {

}

impl<A> Foo for fn(A) { }

fn assert_foo<T: Foo>() {}

fn main() {
    assert_foo::<fn(&i32)>();
}
nikomatsakis (Feb 15 2019 at 19:45, on Zulip):

let me double check my thinking

nikomatsakis (Feb 15 2019 at 19:46, on Zulip):

specifically this would require that exists<A> { (for<'a> fn(&'a i32)) = fn(A) }

Aaron Turon (Feb 15 2019 at 19:46, on Zulip):

yes

nikomatsakis (Feb 15 2019 at 19:46, on Zulip):

and it feels like that should fail because the binders are nested wrong

nikomatsakis (Feb 15 2019 at 19:46, on Zulip):

oh wait

Aaron Turon (Feb 15 2019 at 19:46, on Zulip):

yes

nikomatsakis (Feb 15 2019 at 19:46, on Zulip):

I have a pending PR

nikomatsakis (Feb 15 2019 at 19:46, on Zulip):

that I think fixes this

nikomatsakis (Feb 15 2019 at 19:47, on Zulip):

https://github.com/rust-lang/rust/pull/58056

nikomatsakis (Feb 15 2019 at 19:47, on Zulip):

I had kind of forgotten about that

nikomatsakis (Feb 15 2019 at 19:48, on Zulip):

let me double check that

nikomatsakis (Feb 15 2019 at 19:48, on Zulip):

that would be a relief, since I'd hate for things to be unsound

Aaron Turon (Feb 15 2019 at 19:48, on Zulip):

indeed

nikomatsakis (Feb 15 2019 at 19:48, on Zulip):

though I still think it's worth talking about how to restore the old behavior, perhaps with a warning period

nikomatsakis (Feb 15 2019 at 19:48, on Zulip):

e.g., I think some code in servo was relying on the old behavior

nikomatsakis (Feb 15 2019 at 19:48, on Zulip):

which actually I knew about

nikomatsakis (Feb 15 2019 at 19:48, on Zulip):

and meant to reach out to Simon Sapin

nikomatsakis (Feb 15 2019 at 19:48, on Zulip):

but forgot, in the moment

Aaron Turon (Feb 15 2019 at 19:49, on Zulip):

relies on it for coherence in particular?

nikomatsakis (Feb 15 2019 at 19:49, on Zulip):

yeah, but I forgot the details of exactly why

nikomatsakis (Feb 15 2019 at 19:49, on Zulip):

it was kind of hack

nikomatsakis (Feb 15 2019 at 19:49, on Zulip):

a workaround for some other thing

Aaron Turon (Feb 15 2019 at 19:49, on Zulip):

gotcha

nikomatsakis (Feb 15 2019 at 19:49, on Zulip):

some other time we broke their code ;)

nikomatsakis (Feb 15 2019 at 19:50, on Zulip):

I think it was from when method dispatch was rewritten

Aaron Turon (Feb 15 2019 at 19:50, on Zulip):

lol

nikomatsakis (Feb 15 2019 at 19:58, on Zulip):

@Aaron Turon ok I'm building that branch from that PR, which apparently I no longer had an active checkout for

nikomatsakis (Feb 15 2019 at 19:58, on Zulip):

so I will test that it fixes this example

nikomatsakis (Feb 15 2019 at 19:58, on Zulip):

(and perhaps try to figure out what is blocking the PR in the first place)

nikomatsakis (Feb 15 2019 at 19:58, on Zulip):

but now we can return to the question of what to do about the region checking etc in the shorter term...

Aaron Turon (Feb 15 2019 at 19:58, on Zulip):

OK, sounds good

nikomatsakis (Feb 15 2019 at 19:59, on Zulip):

let me see if I can fish up a comment from Simon

nikomatsakis (Feb 15 2019 at 19:59, on Zulip):

but basically what I am imagining

nikomatsakis (Feb 15 2019 at 19:59, on Zulip):

is that you could definitely imagine re-introducing the "leak check" but built atop the universes formulation

nikomatsakis (Feb 15 2019 at 19:59, on Zulip):

there are a few points where we could do this

nikomatsakis (Feb 15 2019 at 19:59, on Zulip):

I'm not like super eager to do it

nikomatsakis (Feb 15 2019 at 20:00, on Zulip):

otoh a compatibility grace period at minimum seems wise

Aaron Turon (Feb 15 2019 at 20:01, on Zulip):

so, to be clear, this leak check would (sort of by luck) rule out the where clause as a candidate, so that the trait's direct bound on the associated type would be used instead?

Aaron Turon (Feb 15 2019 at 20:02, on Zulip):

re: compatibility warning, it seems like in the long run we'll want to accept this code (as we do on stable today)

Aaron Turon (Feb 15 2019 at 20:02, on Zulip):

NB i'm talking about:

trait Foo<'a> {}

trait Bar {
    type Item: for<'a> Foo<'a>;
}

fn foo<'a, T>(_: T)
where
    T: Bar,
    T::Item: Foo<'a>
{}
Aaron Turon (Feb 15 2019 at 20:03, on Zulip):

so with what's on master right now, we reject this due to being overly greedy; but in the long run if we follow the disjunction strategy we talked about above, we will accept this again

Aaron Turon (Feb 15 2019 at 20:03, on Zulip):

which is all to say: a compatbility warning doesn't actually seem like what we want here

nikomatsakis (Feb 15 2019 at 20:05, on Zulip):

re: compatibility warning, it seems like in the long run we'll want to accept this code (as we do on stable today)

confirm

nikomatsakis (Feb 15 2019 at 20:05, on Zulip):

which is all to say: a compatbility warning doesn't actually seem like what we want here

yes, sorry, I was thinking more about coherence

nikomatsakis (Feb 15 2019 at 20:05, on Zulip):

so this is actually an interesting point though

nikomatsakis (Feb 15 2019 at 20:05, on Zulip):

i.e., we might be able to use these "universe tests" to inform the trait selection aspect of things

nikomatsakis (Feb 15 2019 at 20:05, on Zulip):

without worry

Aaron Turon (Feb 15 2019 at 20:06, on Zulip):

as quick-pruning heuristics? i agree --

Aaron Turon (Feb 15 2019 at 20:06, on Zulip):

and that could be a stopgap for doing the complete search

nikomatsakis (Feb 15 2019 at 20:06, on Zulip):

right, in the "candidate" phase

nikomatsakis (Feb 15 2019 at 20:06, on Zulip):

that would fix #57639

Aaron Turon (Feb 15 2019 at 20:06, on Zulip):

but to be clear, the old tests here were too aggressive

nikomatsakis (Feb 15 2019 at 20:06, on Zulip):

interestingly, we could ALSO do this check in coherence, but issue warnings

nikomatsakis (Feb 15 2019 at 20:07, on Zulip):

but to be clear, the old tests here were too aggressive

yes, they were, but I don't think that's relevant to this example

Aaron Turon (Feb 15 2019 at 20:07, on Zulip):

ok

nikomatsakis (Feb 15 2019 at 20:07, on Zulip):

an example where they were wrong

nikomatsakis (Feb 15 2019 at 20:07, on Zulip):

actually a pretty interesting one to me :)

nikomatsakis (Feb 15 2019 at 20:07, on Zulip):
T1: for<'a, 'b> fn(&'a u32, &'b u32)
T2: for<'c> fn(&'c u32, &'c u32)
nikomatsakis (Feb 15 2019 at 20:07, on Zulip):

those two types are actually equal

nikomatsakis (Feb 15 2019 at 20:08, on Zulip):

if I got that right ;)

nikomatsakis (Feb 15 2019 at 20:08, on Zulip):

but the old code didn't think so

Aaron Turon (Feb 15 2019 at 20:08, on Zulip):

wait so these are equated in master?

nikomatsakis (Feb 15 2019 at 20:08, on Zulip):

yeah, I think so

nikomatsakis (Feb 15 2019 at 20:09, on Zulip):

let's work it out together ;)

Aaron Turon (Feb 15 2019 at 20:09, on Zulip):

that seems bad...

nikomatsakis (Feb 15 2019 at 20:09, on Zulip):

just to double check

nikomatsakis (Feb 15 2019 at 20:09, on Zulip):

well, they are actually equivalent in every way

Aaron Turon (Feb 15 2019 at 20:09, on Zulip):

really? because the LUB always works?

Aaron Turon (Feb 15 2019 at 20:10, on Zulip):

i guess that makes sense

Aaron Turon (Feb 15 2019 at 20:10, on Zulip):

but like, if you added -> &'a u32 and -> 'c u32 respectively, they would not be equal in master?

nikomatsakis (Feb 15 2019 at 20:10, on Zulip):

confirm

Aaron Turon (Feb 15 2019 at 20:10, on Zulip):

ok :+1:

nikomatsakis (Feb 15 2019 at 20:11, on Zulip):
T1 <: T2

forall<'c> {
  exists<'a, 'b> {
    'c: 'a && 'c: 'b
  }
}

T2 <: T1

forall<'a, 'b> {
  exists<'c> {
    'a: 'c && 'b: 'c
  }
}
nikomatsakis (Feb 15 2019 at 20:11, on Zulip):

I think those are the region constraints? I should have "shown my work" prob

nikomatsakis (Feb 15 2019 at 20:11, on Zulip):

it depensd on whether you consider an "emptyregion" valid though

nikomatsakis (Feb 15 2019 at 20:11, on Zulip):

the code sort of does

Aaron Turon (Feb 15 2019 at 20:11, on Zulip):

that makes sense

nikomatsakis (Feb 15 2019 at 20:11, on Zulip):

but I think it also makes sense because, intuitively

Aaron Turon (Feb 15 2019 at 20:12, on Zulip):

like if you can cough up both arguments, there has to be some (nonempty?) lifetime that contains both of them

nikomatsakis (Feb 15 2019 at 20:12, on Zulip):
fn foo(x: &'a u32, y: &'b u32) { bar(x, y) } // OK 'c is the intersecton
fn bar(x: &'c u32, y: &'c u32) { foo(x, y) } // OK == 'a ='c, 'b = 'c
nikomatsakis (Feb 15 2019 at 20:12, on Zulip):

right

Aaron Turon (Feb 15 2019 at 20:12, on Zulip):

yeah

Aaron Turon (Feb 15 2019 at 20:12, on Zulip):

ok i'm with you

nikomatsakis (Feb 15 2019 at 20:12, on Zulip):

anyway this comes up in toehr cases

nikomatsakis (Feb 15 2019 at 20:12, on Zulip):

similar things

nikomatsakis (Feb 15 2019 at 20:12, on Zulip):

where we used to error out instead of inferring 'static

nikomatsakis (Feb 15 2019 at 20:12, on Zulip):

etc

Aaron Turon (Feb 15 2019 at 20:12, on Zulip):

yes

Aaron Turon (Feb 15 2019 at 20:12, on Zulip):

i remember that came up during our Zoom call

nikomatsakis (Feb 15 2019 at 20:13, on Zulip):

anyway so -- backing up -- one option might be to add some check into the candidate evaluation

nikomatsakis (Feb 15 2019 at 20:13, on Zulip):

as well as (potentially )a check in coherence

nikomatsakis (Feb 15 2019 at 20:14, on Zulip):

I am a bit nervous about the latter

nikomatsakis (Feb 15 2019 at 20:14, on Zulip):

well it requires the former

nikomatsakis (Feb 15 2019 at 20:14, on Zulip):

i.e., if we permit impl<'a> fn(&'a u32) and impl for<'a> fn(&'a u32)

nikomatsakis (Feb 15 2019 at 20:14, on Zulip):

we will have to be able to distinguish between them during trait selection

Aaron Turon (Feb 15 2019 at 20:15, on Zulip):

yes. and if we don't permit them, we have an expressivity gap

nikomatsakis (Feb 15 2019 at 20:16, on Zulip):

say more?

nikomatsakis (Feb 15 2019 at 20:16, on Zulip):

well, I mean we permit one "exclusive or" the other today

nikomatsakis (Feb 15 2019 at 20:16, on Zulip):

but not both

nikomatsakis (Feb 15 2019 at 20:16, on Zulip):

yes. and if we don't permit them, we have an expressivity gap

but perhaps you meant like .. long term, one could want both

Aaron Turon (Feb 15 2019 at 20:16, on Zulip):

well so earlier we were talking about the fn case, and how impl<A> Foo for fn(A) doesn't imply (for<'a> fn(&'a u32)): Foo

nikomatsakis (Feb 15 2019 at 20:16, on Zulip):

it's definitely an "awkward area"

Aaron Turon (Feb 15 2019 at 20:17, on Zulip):

so what i'm thinking about is

nikomatsakis (Feb 15 2019 at 20:17, on Zulip):

ah, yes. that's a problem also today

Aaron Turon (Feb 15 2019 at 20:17, on Zulip):

if you're forced to choose

nikomatsakis (Feb 15 2019 at 20:17, on Zulip):

i.e., there is actually no way to write the impls in question the way you want to

Aaron Turon (Feb 15 2019 at 20:17, on Zulip):

then you can find yourself in a situation where you want to use the HRTB version

Aaron Turon (Feb 15 2019 at 20:17, on Zulip):

but you can't because coherence prevents you

Aaron Turon (Feb 15 2019 at 20:18, on Zulip):

basically different parts of the type system would disagree about whether there is overlap

nikomatsakis (Feb 15 2019 at 20:18, on Zulip):

ok yeah so today at least, you could have one impl for all A, and then more impls that are specific but contain bound regions

Aaron Turon (Feb 15 2019 at 20:18, on Zulip):

so hm

nikomatsakis (Feb 15 2019 at 20:18, on Zulip):

basically different parts of the type system would disagree about whether there is overlap

definitely this is what I'm trying to think through and avoid, if we try to loosen any rules here

nikomatsakis (Feb 15 2019 at 20:18, on Zulip):

Im feeling a bit confused about what you are saying though

Aaron Turon (Feb 15 2019 at 20:19, on Zulip):

well so imagine you have fn foo<T: Foo>(t: T) -> T

nikomatsakis (Feb 15 2019 at 20:19, on Zulip):

that is, are you saying "it is GOOD to permit both fn(&'a u32) and for<'a> fn(&'a u32), because otherwise we have an expressiveness gap"?

nikomatsakis (Feb 15 2019 at 20:19, on Zulip):

if so, my feeling is sort of... I would rather close that gap another way

nikomatsakis (Feb 15 2019 at 20:19, on Zulip):

but I don't have a specific proposal :)

Aaron Turon (Feb 15 2019 at 20:19, on Zulip):

that is not what i'm saying

nikomatsakis (Feb 15 2019 at 20:19, on Zulip):

ok

nikomatsakis (Feb 15 2019 at 20:19, on Zulip):

/me listens

Aaron Turon (Feb 15 2019 at 20:19, on Zulip):

i think what i'm saying is, we need the ability to have the trait implemented for both the HRTB and the "ground" version

Aaron Turon (Feb 15 2019 at 20:20, on Zulip):

otherwise you can get yourself trapped

Aaron Turon (Feb 15 2019 at 20:20, on Zulip):

but HOW we do that is up for grabs

nikomatsakis (Feb 15 2019 at 20:20, on Zulip):

i think what i'm saying is, we need the ability to have the trait implemented for both the HRTB and the "ground" version

let me rephrase

nikomatsakis (Feb 15 2019 at 20:20, on Zulip):

from a lang design perspective

nikomatsakis (Feb 15 2019 at 20:20, on Zulip):

we want the ability to say "I implement this for any fn of 1 argument"

Aaron Turon (Feb 15 2019 at 20:20, on Zulip):

so for example, i think i'd prefer that if you do impl <'a> Foo for fn(&'a u32) that also implies that (for<'a> fn(&'a u32)): Foo

nikomatsakis (Feb 15 2019 at 20:21, on Zulip):

and/or probably a way to say "I implement this for any fn of any number of arguments"?

nikomatsakis (Feb 15 2019 at 20:21, on Zulip):

I actually am not sure if the first thing is true

nikomatsakis (Feb 15 2019 at 20:21, on Zulip):

I think the second thing is definitely true

nikomatsakis (Feb 15 2019 at 20:21, on Zulip):

so for example, i think i'd prefer that if you do impl <'a> Foo for fn(&'a u32) that also implies that (for<'a> fn(&'a u32)): Foo

yes, I've wondered about this.

nikomatsakis (Feb 15 2019 at 20:21, on Zulip):

it feels like it ... almost does

nikomatsakis (Feb 15 2019 at 20:21, on Zulip):

maybe it actually does, so long as the 'a doesn't appear anywhere else

nikomatsakis (Feb 15 2019 at 20:22, on Zulip):

i.e.., clearly impl<'a> Foo<'a> for fn(&'a u32) is not sound to do that

Aaron Turon (Feb 15 2019 at 20:22, on Zulip):

put differently: for<'a> (T: Foo) versus (for<'a> T): Foo

Aaron Turon (Feb 15 2019 at 20:22, on Zulip):

it seems like these should be equivalent

nikomatsakis (Feb 15 2019 at 20:23, on Zulip):

I am trying to decide if that is correct

nikomatsakis (Feb 15 2019 at 20:23, on Zulip):

in particular, the for part

nikomatsakis (Feb 15 2019 at 20:23, on Zulip):

i.e.., clearly impl<'a> Foo<'a> for fn(&'a u32) is not sound to do that

you see what I mean about this?

Aaron Turon (Feb 15 2019 at 20:24, on Zulip):

yes

nikomatsakis (Feb 15 2019 at 20:24, on Zulip):

(on a related note, i would like us to think about what it means to have exists and for attached to arbitrary types -- exists in particular feels like it could be useful around thinking about impl trait and some of the associated lifetime issues)

Aaron Turon (Feb 15 2019 at 20:24, on Zulip):

it's a scope violation

nikomatsakis (Feb 15 2019 at 20:24, on Zulip):

right so I guess I'm thinking about like

nikomatsakis (Feb 15 2019 at 20:25, on Zulip):

hmm

nikomatsakis (Feb 15 2019 at 20:25, on Zulip):

I can't figure out how to talk about this :)

nikomatsakis (Feb 15 2019 at 20:25, on Zulip):

but let's move to a very "operational" view

nikomatsakis (Feb 15 2019 at 20:25, on Zulip):

when you have impl<'a> ..., we basically instantiate the region parameter 'a before unifying the types

nikomatsakis (Feb 15 2019 at 20:26, on Zulip):

this then becomes a problem because when you have a for<...> type, we create placeholders

nikomatsakis (Feb 15 2019 at 20:26, on Zulip):

and thus 'a cannot be inferred to those placeholders

Aaron Turon (Feb 15 2019 at 20:26, on Zulip):

yes

nikomatsakis (Feb 15 2019 at 20:27, on Zulip):

ok so i'm seeing part of the challenge here

Aaron Turon (Feb 15 2019 at 20:27, on Zulip):

oh hm, i'm having doubts about equating these, lemme think for a sec

nikomatsakis (Feb 15 2019 at 20:27, on Zulip):

if impl<'a> ... was sort of equated with for<'a> fn(&'a u32) in the self type

nikomatsakis (Feb 15 2019 at 20:27, on Zulip):

oh hm, i'm having doubts about equating these, lemme think for a sec

I too have doubts ;)

nikomatsakis (Feb 15 2019 at 20:28, on Zulip):

I'm trying to put them into words though.

nikomatsakis (Feb 15 2019 at 20:28, on Zulip):

The code as it is today would (e.g.) assume that 'a outlives the fn body of each fn in the impl

nikomatsakis (Feb 15 2019 at 20:28, on Zulip):

because we assume it is "free"

nikomatsakis (Feb 15 2019 at 20:28, on Zulip):

i'm not sure quite where that goes wrong

Aaron Turon (Feb 15 2019 at 20:28, on Zulip):

well so, if you impl for for<'a> T: Foo as a type, the impl can use T at different choices of 'a

nikomatsakis (Feb 15 2019 at 20:28, on Zulip):

or, alternatively, if you have impl ... for for<'a> fn(&'a u32), then you have a fn that you can give references to which do NOT outlive your fn body

nikomatsakis (Feb 15 2019 at 20:29, on Zulip):

well so, if you impl for for<'a> T: Foo as a type, the impl can use T at different choices of 'a

yes, that's what I mean

nikomatsakis (Feb 15 2019 at 20:29, on Zulip):

I feel like there must be some way to create some incoherent setup

Aaron Turon (Feb 15 2019 at 20:29, on Zulip):

yes

Aaron Turon (Feb 15 2019 at 20:29, on Zulip):

but i think that

Aaron Turon (Feb 15 2019 at 20:29, on Zulip):

there should be an implication

Aaron Turon (Feb 15 2019 at 20:29, on Zulip):

that is, if you have impl<'a> Foo for T you should get that (for<'a> T): Foo

Aaron Turon (Feb 15 2019 at 20:29, on Zulip):

but not the other way around

nikomatsakis (Feb 15 2019 at 20:32, on Zulip):

intuitively, because the for can be opened

Aaron Turon (Feb 15 2019 at 20:32, on Zulip):

right

nikomatsakis (Feb 15 2019 at 20:32, on Zulip):

I was wondering about it

nikomatsakis (Feb 15 2019 at 20:32, on Zulip):

it feels like there has to be a problem

Aaron Turon (Feb 15 2019 at 20:32, on Zulip):

hahaha yeah

nikomatsakis (Feb 15 2019 at 20:32, on Zulip):

but let's see if we can find it somehow

nikomatsakis (Feb 15 2019 at 20:33, on Zulip):

I mean maybe not

nikomatsakis (Feb 15 2019 at 20:33, on Zulip):

but we would have to ensure

nikomatsakis (Feb 15 2019 at 20:33, on Zulip):

that e.g. if Self type appears in various places

nikomatsakis (Feb 15 2019 at 20:33, on Zulip):

probably it has to be the .. opened version?

nikomatsakis (Feb 15 2019 at 20:33, on Zulip):

or something?

nikomatsakis (Feb 15 2019 at 20:34, on Zulip):

i.e., in some sense, the "upcast" here is not in the trait system

nikomatsakis (Feb 15 2019 at 20:34, on Zulip):

but rather in the one using the trait system

Aaron Turon (Feb 15 2019 at 20:34, on Zulip):

right, i think like Self appearing in multiple places is likely to pose the key problem

nikomatsakis (Feb 15 2019 at 20:34, on Zulip):

like, if I am trying to prove that fn(&u32): Trait -- why am I doing that? It probably comes from some method call like Trait::foo(x) where x: fn(&u32)

nikomatsakis (Feb 15 2019 at 20:35, on Zulip):

and I could certainly upcast x there to exists<'a> fn(&'a u32)

nikomatsakis (Feb 15 2019 at 20:35, on Zulip):

right now, the compiler fails to do that for a variety of reasons

Aaron Turon (Feb 15 2019 at 20:44, on Zulip):
trait Foo {
  type Output;
}

impl<'a> Foo for fn(&'a u32) {
  type Output = &'a u32;
}

// this CANNOT imply that `(for<'a> fn(&'a u32)): Foo`,
// because we have no way to normalize
// `<(for<'a> fn(&'a u32)) as Foo>::Output`
Aaron Turon (Feb 15 2019 at 20:45, on Zulip):

@nikomatsakis i'm gonna run to lunch, but lemme know your thoughts on ^ when you have a chance

nikomatsakis (Feb 15 2019 at 20:46, on Zulip):

@Aaron Turon yes so this intersects a separate thing

nikomatsakis (Feb 15 2019 at 20:49, on Zulip):

In RFC 1214, we specified that lifetime parameters like 'a can only appear in an associated type if they also appear (syntactically) in an input type. That would mean that the above impl is accepted. However, I have come to regret that decision. I think we should have said that a lifetime parameter like 'a can only appear in an associated type value if it is constrained by an input type, where constrained would exclude fn parameter arguments and other contravariant positions (e.g., trait objects).

nikomatsakis (Feb 15 2019 at 20:49, on Zulip):

Actually variance is an "imperfect" fit

nikomatsakis (Feb 15 2019 at 20:50, on Zulip):

but basically the motivation is that it would be nice if fn(&'a u32): 'static were true

nikomatsakis (Feb 15 2019 at 20:50, on Zulip):

presently it is not, and this is because of the above rule

nikomatsakis (Feb 15 2019 at 20:50, on Zulip):

specifically because we want to know that T::Output: 'x if T: 'x

nikomatsakis (Feb 15 2019 at 20:51, on Zulip):

but e.g. in your example if fn(&'a u32): 'static, we could conclude that <fn(&'a u32) as Trait>::Output: 'static, which is wrong

nikomatsakis (Feb 15 2019 at 20:51, on Zulip):

I've wondered -- but not tried to evaluate -- if we could get away with changing this rule

nikomatsakis (Feb 15 2019 at 20:51, on Zulip):

Seems probable but not guaranteed

nikomatsakis (Feb 15 2019 at 20:51, on Zulip):

but basically the motivation is that it would be nice if fn(&'a u32): 'static were true

but the fact that this is untrue in current Rust feels sorta like a bug

Aaron Turon (Feb 15 2019 at 22:02, on Zulip):

yeah that's annoying

tmandry (Feb 18 2019 at 02:39, on Zulip):

(I followed most of this, fyi)

Last update: Nov 12 2019 at 17:00UTC