Stream: wg-traits

Topic: RPIT Lifetime issues


Alexander Regueiro (Jan 14 2019 at 19:25, on Zulip):

@Taylor Cramer @nikomatsakis and I discussed this previously (and @eddyb chipped in a bit). I think we want to use for<'a> (or a new keyword, but preferably reuse that one) to bind such lifetimes.

Taylor Cramer (Jan 14 2019 at 19:25, on Zulip):

@Alexander Regueiro

Alexander Regueiro (Jan 14 2019 at 19:26, on Zulip):

^

Alexander Regueiro (Jan 14 2019 at 19:27, on Zulip):

I guess the semantics would be quite simple: capturing the variables and doing nothing.

nikomatsakis (Jan 14 2019 at 19:27, on Zulip):

Maybe paste in the issues for context here?

Alexander Regueiro (Jan 14 2019 at 19:27, on Zulip):

appropriate diagnostics might be a bit harder

nikomatsakis (Jan 14 2019 at 19:27, on Zulip):

I want to be sure I know which issues you are talking about

Alexander Regueiro (Jan 14 2019 at 19:27, on Zulip):

Here they are.

Alexander Regueiro (Jan 14 2019 at 19:27, on Zulip):

1. https://github.com/rust-lang/rust/issues/34511#issuecomment-373423999 (@eddyb has some thoughts about this, but he hasn't been around for a while now, and @nikomatsakis understands it anyway)
2. https://github.com/rust-lang/rust/issues/42940
3. Possibly https://github.com/rust-lang/rust/issues/55929 is related to or even the same as 1?

Taylor Cramer (Jan 14 2019 at 19:28, on Zulip):

I'm not sure what the "issue" with (1) is

Taylor Cramer (Jan 14 2019 at 19:29, on Zulip):

It was addressed in https://github.com/rust-lang/rust/pull/49041

Taylor Cramer (Jan 14 2019 at 19:30, on Zulip):

in order to capture lifetimes, you have to add a Captures trait in order to pick up the lifetime in the bounds

Taylor Cramer (Jan 14 2019 at 19:31, on Zulip):

Is there something else going on there that you think we should resolve?

Alexander Regueiro (Jan 14 2019 at 19:31, on Zulip):

"The key thing here is that TyCtxt is invariant w/r/t 'tcx and 'gcx, so they must appear in the return type. And yet only 'cx and 'tcx appear in the impl trait bounds, so only those two lifetimes are supposed to be "captured". The old compiler was accepting this because 'gcx: 'cx, but that's not really correct if you think about the desugaring we have in mind. That desugaring would create an abstract type like this:"

Alexander Regueiro (Jan 14 2019 at 19:31, on Zulip):

that's the key bit

Alexander Regueiro (Jan 14 2019 at 19:31, on Zulip):

@Taylor Cramer I started doing that, but @nikomatsakis doesn't like it, and prefers a language-based solution.

Taylor Cramer (Jan 14 2019 at 19:32, on Zulip):

What sort of "language-based" solution?

Taylor Cramer (Jan 14 2019 at 19:34, on Zulip):

(I'm curious because some kind of language-level LUB('a, 'b, ...) would also fix my issues with async fn)

Taylor Cramer (Jan 14 2019 at 19:34, on Zulip):

as well as fixing (2), I believe

Taylor Cramer (Jan 14 2019 at 19:34, on Zulip):

(or at least giving a workaround)

Alexander Regueiro (Jan 14 2019 at 19:34, on Zulip):

See my first comment in this thread. :-)

Alexander Regueiro (Jan 14 2019 at 19:34, on Zulip):

At least, that's what we talked about before.

Alexander Regueiro (Jan 14 2019 at 19:34, on Zulip):

It need not be the only possible solution though...

Taylor Cramer (Jan 14 2019 at 19:35, on Zulip):

using for<'a>?

Alexander Regueiro (Jan 14 2019 at 19:35, on Zulip):

/me waits for @nikomatsakis to chip in.

Alexander Regueiro (Jan 14 2019 at 19:35, on Zulip):

yeah

Taylor Cramer (Jan 14 2019 at 19:35, on Zulip):

can you give an example?

Alexander Regueiro (Jan 14 2019 at 19:36, on Zulip):

I think something like fn foo(self) -> impl for<'gcx> Iterator<Item = &'tcx Foo> + 'cx {

Taylor Cramer (Jan 14 2019 at 19:37, on Zulip):

that seems misleading to me

Alexander Regueiro (Jan 14 2019 at 19:37, on Zulip):

alternatively, we build it into the impl syntax, e.g. impl<'gcx> Iterator...

Taylor Cramer (Jan 14 2019 at 19:37, on Zulip):

because for there looks like part of the bound

centril (Jan 14 2019 at 19:37, on Zulip):

it is part of the bound

Taylor Cramer (Jan 14 2019 at 19:37, on Zulip):

and I'd expect the bound to be quantified over 'gcx

Taylor Cramer (Jan 14 2019 at 19:38, on Zulip):

sorry, your thumb indicates that you agree, but I think the feature that is being suggested here is different?

Alexander Regueiro (Jan 14 2019 at 19:38, on Zulip):

okay, move it outside the impl then? or take my alternative syntax?

Taylor Cramer (Jan 14 2019 at 19:38, on Zulip):

that it actually makes it part of the extistentail type<...> rather than the bound on the RHS of :

Taylor Cramer (Jan 14 2019 at 19:39, on Zulip):

@Alexander Regueiro maybe?

centril (Jan 14 2019 at 19:39, on Zulip):

I'd expect impl<'a> Foo<'a> + Bar<'a> to be equivalent to impl for<'a> (Foo<'a> + Bar<'a>)

centril (Jan 14 2019 at 19:39, on Zulip):

(which you cannot express)

Alexander Regueiro (Jan 14 2019 at 19:39, on Zulip):

yes...

Alexander Regueiro (Jan 14 2019 at 19:41, on Zulip):

@nikomatsakis thoughts on syntax? options:
1. impl for<'a> Foo<'a>
2. for<'a> impl Foo<'a>
3. impl<'a> Foo<'a>
4. other?

Alexander Regueiro (Jan 14 2019 at 19:42, on Zulip):

@Taylor Cramer should I put you down for these things in the meeting notes; is that okay? (I think you know what needs to be tackle, syntax pending)

Alexander Regueiro (Jan 14 2019 at 19:42, on Zulip):

and 2. doesn't require any syntactical enhancements

Alexander Regueiro (Jan 14 2019 at 19:42, on Zulip):

that is, issue 2. https://github.com/rust-lang/rust/issues/42940

Alexander Regueiro (Jan 14 2019 at 19:58, on Zulip):

So...?

Taylor Cramer (Jan 14 2019 at 20:02, on Zulip):

i'm not sure I agree that something needs to happen here

Taylor Cramer (Jan 14 2019 at 20:02, on Zulip):

and certainly not without an RFC

Taylor Cramer (Jan 14 2019 at 20:02, on Zulip):

although we could possibly justify it as "experimentation"

Taylor Cramer (Jan 14 2019 at 20:03, on Zulip):

but the motivation (not using Captures<...>) seems unclear to me

Taylor Cramer (Jan 14 2019 at 20:03, on Zulip):

Also there's an interesting parallel here between Captures and PhantomData

Taylor Cramer (Jan 14 2019 at 20:03, on Zulip):

I wonder if there's room for PhantomTrait or something

centril (Jan 14 2019 at 20:04, on Zulip):

can someone TL;DR the lifetime issues under discussion here?

Taylor Cramer (Jan 14 2019 at 20:04, on Zulip):

https://github.com/rust-lang/rust/issues/42940 is the more interesting one to me

Taylor Cramer (Jan 14 2019 at 20:04, on Zulip):

I think that's the only one that just needs "fixing"

centril (Jan 14 2019 at 20:05, on Zulip):

for<'a> impl Foo<'a> would be a higher ranked type; impl<'a> Foo<'a> would just be sugar for impl for<'a> Foo<'a>

Taylor Cramer (Jan 14 2019 at 20:05, on Zulip):

It's just a bug

Taylor Cramer (Jan 14 2019 at 20:05, on Zulip):

@centril I think you're getting mixed up--none of this has to do with higher-rankedness

Taylor Cramer (Jan 14 2019 at 20:06, on Zulip):

that's why I don't want to use this syntax

Taylor Cramer (Jan 14 2019 at 20:06, on Zulip):

IIUC @Alexander Regueiro is trying to get another way to spell Captures<...>

Taylor Cramer (Jan 14 2019 at 20:06, on Zulip):

which is more about variance than about higher-rankedness

centril (Jan 14 2019 at 20:06, on Zulip):

@Taylor Cramer I'm not mixing up anything, I'm giving expected semantics to the syntaxes @Alexander Regueiro referenced

centril (Jan 14 2019 at 20:07, on Zulip):

(i.e. 1-3)

Taylor Cramer (Jan 14 2019 at 20:07, on Zulip):

I'm saying those aren't the semantics he's looking for

centril (Jan 14 2019 at 20:07, on Zulip):

@Taylor Cramer sure, that's my point :P

Taylor Cramer (Jan 14 2019 at 20:07, on Zulip):

unless I'm confused (which is possible)

Taylor Cramer (Jan 14 2019 at 20:07, on Zulip):

Okay, so we're on the same page that we shouldn't reuse for or impl to add captured lifetimes to impl Trait

centril (Jan 14 2019 at 20:08, on Zulip):

yep

centril (Jan 14 2019 at 20:08, on Zulip):

when was Captures<...> needed again?

Taylor Cramer (Jan 14 2019 at 20:08, on Zulip):

@Alexander Regueiro does that make sense to you? or did I get mixed up?

Taylor Cramer (Jan 14 2019 at 20:09, on Zulip):

@centril when you have a return type that is quantified over a lifetime but you don't want to require that the type outlive that lifetime

Taylor Cramer (Jan 14 2019 at 20:09, on Zulip):

it can't live longer than that lifetime

Taylor Cramer (Jan 14 2019 at 20:09, on Zulip):

but not as long as

Taylor Cramer (Jan 14 2019 at 20:10, on Zulip):

e.g. fn foo<'a, 'b: 'a>(x: &'a str, y: &'b str) -> impl Debug + Captures<'b> + 'a { (x, y) }

Taylor Cramer (Jan 14 2019 at 20:10, on Zulip):

it doesn't live as long as 'b

Taylor Cramer (Jan 14 2019 at 20:10, on Zulip):

but it captures 'b

centril (Jan 14 2019 at 20:28, on Zulip):

@Taylor Cramer hmm, is this Captures<'a> a common need?

Taylor Cramer (Jan 14 2019 at 20:29, on Zulip):

not super common, but it happens

Taylor Cramer (Jan 14 2019 at 20:29, on Zulip):

it's in rustc in several places

centril (Jan 14 2019 at 20:31, on Zulip):

@Taylor Cramer hmm remind me again... what is the variance of Captures<'b> ?

Alexander Regueiro (Jan 14 2019 at 21:03, on Zulip):

@centril I already linked to them above.

Alexander Regueiro (Jan 14 2019 at 21:04, on Zulip):

@Taylor Cramer I wasn't against using Captures, but it seems Niko wanted to avoid it.

Alexander Regueiro (Jan 14 2019 at 21:04, on Zulip):

So let's get his reasoning

Alexander Regueiro (Jan 14 2019 at 21:21, on Zulip):

@Taylor Cramer are you good to work on issue 2 until we decide that?

Alexander Regueiro (Jan 14 2019 at 21:23, on Zulip):

also, https://github.com/rust-lang/rust/pull/56047

Alexander Regueiro (Jan 15 2019 at 00:15, on Zulip):

@centril Captures<'a> would surely be covariant, since it's an empty trait

Alexander Regueiro (Jan 16 2019 at 04:22, on Zulip):

@nikomatsakis Could we kindly get your reasoning on 1 and why you want a solution built into the language rather than a Captures trait or such? I know you expressed this on my closed PR, but I think elaboration would be nice, especially for @Taylor Cramer.

nikomatsakis (Jan 17 2019 at 14:16, on Zulip):

sorry y'all I was late on this thread, catching up now

nikomatsakis (Jan 17 2019 at 14:17, on Zulip):

to go back, the problem is when you have some function like fn foo(..) -> impl Iterator<Item = &'a Blah> but it references some lifetime like 'tcx

nikomatsakis (Jan 17 2019 at 14:17, on Zulip):

my preference here would be to just accept the code as is

nikomatsakis (Jan 17 2019 at 14:17, on Zulip):

but I want to figure out how we justify that :)

nikomatsakis (Jan 17 2019 at 14:18, on Zulip):

as I wrote.. somewhere... you can hide lifetimes using a dyn type

nikomatsakis (Jan 17 2019 at 14:18, on Zulip):

(you do need some common "denominator", though)

nikomatsakis (Jan 17 2019 at 14:18, on Zulip):

i.e., a bound

nikomatsakis (Jan 17 2019 at 14:19, on Zulip):

but I am now looking at #42940 and trying to catch up with what @Taylor Cramer was saying

nikomatsakis (Jan 17 2019 at 14:20, on Zulip):

it seems like we should split the discussion a bit further

nikomatsakis (Jan 17 2019 at 14:51, on Zulip):

OK, re: #42940, I posted a comment with my thoughts. The TL;DR is "seems like a bug" and the fix, while non-trivial, is straight-forward-ish I think. @Taylor Cramer maybe you want to work on it?

Taylor Cramer (Jan 17 2019 at 16:11, on Zulip):

Yeah, I can work on it, thanks for your comments. And wrt #42940 I agree that it should "just work" but I don't know how to make that clear in the existential type desugaring. It reminds me a bit of the closure type replacement issue where you could imagine that we just replaced all lifetimes with the explicitly-mentioned bound and that the change due to invalid variance was just "unobservable", but that seems like quite a hack and not really a good justification in any formal-ish sense

nikomatsakis (Jan 17 2019 at 16:11, on Zulip):

right, I've been hoping to put off that question

nikomatsakis (Jan 17 2019 at 16:11, on Zulip):

which reminds me that I thought of a better variant of the captures trait...

nikomatsakis (Jan 17 2019 at 16:12, on Zulip):

right now I think it is Captures<'a>, but that leads to trouble if you have more than one lifetime

nikomatsakis (Jan 17 2019 at 16:12, on Zulip):

I think if we did Captures<T> instead, it would be better

nikomatsakis (Jan 17 2019 at 16:12, on Zulip):

and then you could do e.g. impl Foo + Captures<(&'a (), &'b ())>

nikomatsakis (Jan 17 2019 at 16:12, on Zulip):

still a horrible hack

nikomatsakis (Jan 17 2019 at 16:12, on Zulip):

but could be useful in rustc anyway

Alexander Regueiro (Jan 17 2019 at 17:10, on Zulip):

@Taylor Cramer So the idea is to fix both of these problems by making the code “just work”?

Taylor Cramer (Jan 17 2019 at 17:44, on Zulip):

Yeah, #42940 was always just a bug (albeit a subtle one), and the other thing I think niko and I agree that we should just allow the code without having to explicitly mention the lifetimes. Still not sure exactly what it should desugar to or how we should explain the fact that it works, though

Alexander Regueiro (Jan 18 2019 at 21:20, on Zulip):

@Taylor Cramer Yeah, I've been thinking about that too, and it's a tricky one... maybe it can be justified in an analogous way to dyn Trait though? Anyway, do please let me know if you and Niko decide on anything, just out of curiosity.

nikomatsakis (Jan 18 2019 at 21:37, on Zulip):

I feel like the answer is that we'd have some kind of exists<'a> Type notion

nikomatsakis (Jan 18 2019 at 21:38, on Zulip):

and just try to convince ourselves that it will work out ;)

nikomatsakis (Jan 18 2019 at 21:38, on Zulip):

it feels like it has to be ok

Alexander Regueiro (Jan 18 2019 at 21:39, on Zulip):

@nikomatsakis why would you have that for impl Trait but not for dyn Trait?

nikomatsakis (Jan 18 2019 at 21:42, on Zulip):

dyn Trait does have that, in some sense. That is, dyn Trait is basically exists T: Trait

Alexander Regueiro (Jan 18 2019 at 21:42, on Zulip):

oh, true

nikomatsakis (Jan 18 2019 at 21:42, on Zulip):

so what I am saying is -- conceptually -- impl Trait would be inferred not to Foo<'a, 'gcx> but exists<'gcx> Foo<'gcx>

nikomatsakis (Jan 18 2019 at 21:42, on Zulip):

actually chalk already has this kind of type, iirc

nikomatsakis (Jan 18 2019 at 21:43, on Zulip):

well, not exactly

Alexander Regueiro (Jan 18 2019 at 21:43, on Zulip):

@nikomatsakis oh right, so there would be no syntactical additions?

nikomatsakis (Jan 18 2019 at 21:43, on Zulip):

but I mean that forall types are distinct from fns

nikomatsakis (Jan 18 2019 at 21:43, on Zulip):

yeah I don't mean that the syntax changes

Alexander Regueiro (Jan 18 2019 at 21:43, on Zulip):

sounds reasonable

Alexander Regueiro (Jan 18 2019 at 21:54, on Zulip):

@nikomatsakis so correct me if I'm wrong, this still wouldn't make impl Trait existential in nature, but it would (just) implicitly existentially quantify invariant lifetimes?

nikomatsakis (Jan 18 2019 at 22:07, on Zulip):

@Alexander Regueiro correct, this is what I have in mind

Alexander Regueiro (Jan 18 2019 at 22:09, on Zulip):

@nikomatsakis okay, great. the question then is: is @Taylor Cramer comfortable enough with Chalk to tackle this too, or should it be assigned to someone else? (Sadly I'm definitely not comfortable enough, but maybe that will change some day.)

Taylor Cramer (Jan 18 2019 at 22:26, on Zulip):

I definitely don't know enough to model this today

Taylor Cramer (Jan 18 2019 at 22:26, on Zulip):

but I'd be happy to work on learning

Alexander Regueiro (Jan 18 2019 at 22:26, on Zulip):

@Taylor Cramer I want to learn about Chalk too. the "technical deep dive" should be coming up soon... maybe one (or both) of us can take it on after then?

Alexander Regueiro (Jan 18 2019 at 22:26, on Zulip):

at least, if it's next week (as I believe it is)

nikomatsakis (Jan 18 2019 at 22:31, on Zulip):

well, next week we were going to focus on trait objects, but not "all of chalk" -- still, I'd be happy to schedule some time to talk this stuff through in an exploratory fashion (probably with both of y'all and whomever else wants to)

nikomatsakis (Jan 18 2019 at 22:31, on Zulip):

(we could record and post too)

nikomatsakis (Jan 18 2019 at 22:33, on Zulip):

I suspect the end result of all of this is that we'll basically just wind up removing the check we added to make the existing code an error ...

Taylor Cramer (Jan 18 2019 at 22:40, on Zulip):

Yeah, that was sort of what I was wondering ;)

Taylor Cramer (Jan 18 2019 at 22:40, on Zulip):

@nikomatsakis It seems like the actual task here is to just open a PR reverting that change

Taylor Cramer (Jan 18 2019 at 22:41, on Zulip):

now that we're comfortable that there exists some way to model this more formally

Taylor Cramer (Jan 18 2019 at 22:41, on Zulip):

(provided you actually do believe that now)

centril (Jan 18 2019 at 22:44, on Zulip):

@nikomatsakis ostensibly fn foo(x: impl Trait) { ... } ==> fn foo(x: exists<T: Trait> T) ==> fn foo<T: Trait>(x: T) whereas fn foo() -> impl Trait ==> exists<T: Trait> fn foo() but not fn foo() -> exists<T: Trait> T

Alexander Regueiro (Jan 18 2019 at 23:06, on Zulip):

@nikomatsakis @Taylor Cramer sounds fair. so we don't need to model this in Chalk then? :-)

Taylor Cramer (Jan 18 2019 at 23:39, on Zulip):

I mean, it should probably be done at some point

Taylor Cramer (Jan 18 2019 at 23:39, on Zulip):

but it's not a blocker for resolving the issue IMO

Alexander Regueiro (Jan 18 2019 at 23:44, on Zulip):

@Taylor Cramer from what I've just heard, I agree, yes.

Alexander Regueiro (Jan 18 2019 at 23:44, on Zulip):

had any luck with the other issue yet?

Alexander Regueiro (Jan 18 2019 at 23:45, on Zulip):

or still trying to find time to look at it?

Taylor Cramer (Jan 18 2019 at 23:46, on Zulip):

I haven't had time yet

Taylor Cramer (Jan 18 2019 at 23:46, on Zulip):

If you have time, feel free to go at it

Taylor Cramer (Jan 18 2019 at 23:46, on Zulip):

but I have a several day latency on actually having time to do anything :)

centril (Jan 18 2019 at 23:47, on Zulip):

@Taylor Cramer I know the feeling :P

Alexander Regueiro (Jan 19 2019 at 00:06, on Zulip):

hehe, yeah, that's not uncommon I also find! I feel you're legitimately in a better position to make this fix, so let's touch base on the wg-traits meeting on Monday, and decide then (if you haven't started by then) :-)

nikomatsakis (Jan 22 2019 at 20:41, on Zulip):

now that we're comfortable that there exists some way to model this more formally

I mean I always believed that, but that's not the same as sort of doing it and convincing ourselves we're not messing something up. I guess though I could be persuaded to go ahead and revert the check on the premise that it seems almost certainly correct, and we'll deal with any unsoundness as we ever do :P

Alexander Regueiro (Jan 24 2019 at 01:02, on Zulip):

@Taylor Cramer I see your PR for issue (1). Good stuff. I think that covers (3) too. Will you be tackling (2) afterwards, out of curiosity?

Taylor Cramer (Jan 24 2019 at 03:47, on Zulip):

@Alexander Regueiro yeah I was going to

Taylor Cramer (Jan 24 2019 at 03:47, on Zulip):

but I haven't had time yet

Alexander Regueiro (Jan 24 2019 at 03:57, on Zulip):

@Taylor Cramer Okay cool. :-)

Alexander Regueiro (Jan 28 2019 at 17:57, on Zulip):

@Taylor Cramer @nikomatsakis Does @Matthew Jasper's bug report and my suggestion make sense on https://github.com/rust-lang/rust/pull/57870 ?

Alexander Regueiro (Mar 23 2019 at 15:45, on Zulip):

@nikomatsakis so, it turns out I might need to speak to you about this after all... if you have time. the fix isn't as obvious as I'd hoped!

nikomatsakis (Mar 25 2019 at 18:22, on Zulip):

So, @Alexander Regueiro, what I was imagining is that we need some sort of "bound"

nikomatsakis (Mar 25 2019 at 18:23, on Zulip):

In other words, when you "hide" lifetimes with dyn Trait, you can only do it because we have a lifetime bound 'b on dyn Trait (i.e., dyn Trait + 'b) and the hidden type must outlive 'b

nikomatsakis (Mar 25 2019 at 18:23, on Zulip):

It sounds like you were roughly coming to the same conclusion in that PR

Alexander Regueiro (Mar 25 2019 at 18:23, on Zulip):

yeah

Alexander Regueiro (Mar 25 2019 at 18:23, on Zulip):

though didn't quite eget there

nikomatsakis (Mar 25 2019 at 18:23, on Zulip):

which I agree with

nikomatsakis (Mar 25 2019 at 18:24, on Zulip):

I'm not exactly sure what form this should take

nikomatsakis (Mar 25 2019 at 18:24, on Zulip):

but basically we can't "ignore' lifetimes unless there is some named lifetime that is captured which they outlive

Alexander Regueiro (Mar 25 2019 at 18:24, on Zulip):

did you see matthewjasper's tricky way to create unsound behaviour?

Alexander Regueiro (Mar 25 2019 at 18:24, on Zulip):

(a new one)

Alexander Regueiro (Mar 25 2019 at 18:24, on Zulip):

right

Alexander Regueiro (Mar 25 2019 at 18:24, on Zulip):

that makes sense, I think....

nikomatsakis (Mar 25 2019 at 18:25, on Zulip):

I'm reading what they wrote now

nikomatsakis (Mar 25 2019 at 18:25, on Zulip):

well ok so the problem is

nikomatsakis (Mar 25 2019 at 18:25, on Zulip):

yeah, this makes sense

Alexander Regueiro (Mar 25 2019 at 18:25, on Zulip):

so basically we can only allow this hiding if opaque_defn.has_required_region_bounds?

Alexander Regueiro (Mar 25 2019 at 18:25, on Zulip):

that condition being necessary but not sufficient

Alexander Regueiro (Mar 25 2019 at 18:25, on Zulip):

I think if you combine it with the condition I currently have, that may be enough then?

nikomatsakis (Mar 25 2019 at 18:26, on Zulip):

so, when I was talking earlier, I mentioned that the way I wanted to think about this was basically "as if" we introduced an existential type construct

Alexander Regueiro (Mar 25 2019 at 18:26, on Zulip):

in what sense? RPIT is already "kind of" existential. :-)

nikomatsakis (Mar 25 2019 at 18:27, on Zulip):

not really

nikomatsakis (Mar 25 2019 at 18:27, on Zulip):

I mean not in the sense I mean

nikomatsakis (Mar 25 2019 at 18:27, on Zulip):

i.e., the hidden type in @Matthew Jasper's example is Rc<RefCell<&'b T>> -- but that doesn't work beacuse it names 'b

nikomatsakis (Mar 25 2019 at 18:27, on Zulip):

the hidden type would have to be exists<'b> Rc<RefCell<&'b T>>

nikomatsakis (Mar 25 2019 at 18:27, on Zulip):

er

nikomatsakis (Mar 25 2019 at 18:27, on Zulip):

exists<'b: 'a> Rc<RefCell<&'b T>>

nikomatsakis (Mar 25 2019 at 18:28, on Zulip):

and the key point here is that this would not implement Swap

nikomatsakis (Mar 25 2019 at 18:28, on Zulip):

because Swap is implemented for Rc<RefCell<&'b T>>, not exists<...> ...

nikomatsakis (Mar 25 2019 at 18:28, on Zulip):

anyway, this all feels tricky to me

nikomatsakis (Mar 25 2019 at 18:28, on Zulip):

which is why I've been discouraging us from pushing too hard :)

nikomatsakis (Mar 25 2019 at 18:28, on Zulip):

(though @Matthew Jasper's example is a very good one)

nikomatsakis (Mar 25 2019 at 18:29, on Zulip):

and basically highlights where using a "real" existential type would start to differ from just ignoring stuff

nikomatsakis (Mar 25 2019 at 18:29, on Zulip):

that said, there is a different but related area that might be worth pushing on

nikomatsakis (Mar 25 2019 at 18:29, on Zulip):

that was blocking some of the async-await stuff

Alexander Regueiro (Mar 25 2019 at 18:30, on Zulip):

yeah...

Alexander Regueiro (Mar 25 2019 at 18:30, on Zulip):

hmm

nikomatsakis (Mar 25 2019 at 18:30, on Zulip):

I spent a while outlining the problem/possible solutions to @Taylor Cramer over in #t-compiler/wg-async-await

Alexander Regueiro (Mar 25 2019 at 18:30, on Zulip):

do you have an example of where adding + 'b to the bounds isn't good enough?

Alexander Regueiro (Mar 25 2019 at 18:30, on Zulip):

okay

Alexander Regueiro (Mar 25 2019 at 18:30, on Zulip):

I'll take a look

nikomatsakis (Mar 25 2019 at 18:30, on Zulip):

do you have an example of where adding + 'b to the bounds isn't good enough?

well that is good enough

nikomatsakis (Mar 25 2019 at 18:31, on Zulip):

but that changes the whole problem

nikomatsakis (Mar 25 2019 at 18:31, on Zulip):

that is, the problem is to find a way where we can have a type that includes lifetimes

nikomatsakis (Mar 25 2019 at 18:31, on Zulip):

which are NOT part of the trait bounds

nikomatsakis (Mar 25 2019 at 18:31, on Zulip):

i.e., which don't appear in the capture list

nikomatsakis (Mar 25 2019 at 18:31, on Zulip):

and I think the answer is that, as @Matthew Jasper's example shows, we can't really do that very easily

Alexander Regueiro (Mar 25 2019 at 18:31, on Zulip):

oh yes, duh

Alexander Regueiro (Mar 25 2019 at 18:31, on Zulip):

hmm

Alexander Regueiro (Mar 25 2019 at 18:35, on Zulip):

@nikomatsakis I'll take a look at that one in a bit, but for this issue, how would go around creating an existential type, binding by lifetime?

Alexander Regueiro (Mar 25 2019 at 18:35, on Zulip):

in terms of implementation

Alexander Regueiro (Mar 25 2019 at 18:38, on Zulip):

I mean, we have for<'a: 'b> already today as HRLB

nikomatsakis (Mar 25 2019 at 18:44, on Zulip):

@Alexander Regueiro well, I don't quite know, to be totally honest =)

Alexander Regueiro (Mar 25 2019 at 18:44, on Zulip):

heh, yeah, it's tricky...

nikomatsakis (Mar 25 2019 at 18:45, on Zulip):

we'd have to figure out the rules for the type, which probably isn't too hard, but also define whre the "open and close" operations occur

nikomatsakis (Mar 25 2019 at 18:45, on Zulip):

those would presumably be connected to returning a value from a fn w/ an RPIT

Alexander Regueiro (Mar 25 2019 at 18:45, on Zulip):

open & close?

nikomatsakis (Mar 25 2019 at 18:46, on Zulip):

'close' refers to 'hiding' the existential lifetime

Alexander Regueiro (Mar 25 2019 at 18:46, on Zulip):

right

nikomatsakis (Mar 25 2019 at 18:46, on Zulip):

i.e., converting from Foo<'b> to exists<'b> Foo<'b>

Alexander Regueiro (Mar 25 2019 at 18:46, on Zulip):

that seems the more obvious (?) one: that could be done where I'm doing my checks now for hidden lifetimes

Alexander Regueiro (Mar 25 2019 at 18:47, on Zulip):

in constrain_type

Alexander Regueiro (Mar 25 2019 at 18:47, on Zulip):

or whatever it's called

Alexander Regueiro (Mar 25 2019 at 18:47, on Zulip):

opening... I'm not so sure!

Alexander Regueiro (Mar 25 2019 at 18:53, on Zulip):

@nikomatsakis I can try to throw something together if you give me a few tips about how/where to do the opening :-)

Alexander Regueiro (Mar 25 2019 at 18:53, on Zulip):

just experiment

Alexander Regueiro (Mar 26 2019 at 16:27, on Zulip):

@nikomatsakis so, I'm willing to pursue this, but I feel I'd need mentoring from someone who really understands the semantics and implementation... this could be informal, or in the form of an eRFC...

centril (Mar 27 2019 at 12:54, on Zulip):

I think the immediate next step here should be to add @Matthew Jasper's tests on both PRs as compile-fail tests to ensure that accidents don't occur.

centril (Mar 27 2019 at 12:56, on Zulip):

@nikomatsakis The notion of exists<'x: 'y> is appealing; It was discussed in https://medium.com/@GolDDranks/things-rust-doesnt-let-you-do-draft-f596a3c740a5 as a means of having "dependent lifetimes" which I found intriguing... Definitely worth exploring but will need deeper thinking + buy-in from the language team.

Alexander Regueiro (Apr 03 2019 at 14:29, on Zulip):

hey @nikomatsakis. got a bit of free time coming up to discuss RPIT existential lifetime issues more?

tmandry (Apr 03 2019 at 16:51, on Zulip):

I think niko is on vacation this week @Alexander Regueiro

Alexander Regueiro (Apr 03 2019 at 17:04, on Zulip):

@tmandry okay thanks

Last update: Nov 18 2019 at 01:25UTC