Stream: wg-traits

Topic: QuantifiedApply


nikomatsakis (Dec 06 2019 at 23:58, on Zulip):

Hey @detrumi I was taking a look at your QuantifiedApply branch

nikomatsakis (Dec 06 2019 at 23:58, on Zulip):

I'm starting to think that the right thing is to not make any attempt to be "general" and to rename QuantifiedApply to just Fn

nikomatsakis (Dec 06 2019 at 23:58, on Zulip):

I'm going to push a bit of a "messy" commit that doesn't quite pass tests but fixes your recursion problem

nikomatsakis (Dec 07 2019 at 00:01, on Zulip):

the commit message explains a bit more what's going on

nikomatsakis (Dec 07 2019 at 00:02, on Zulip):

the reason you were getting infinite recursion had to do with the definition of substitute that you had--

nikomatsakis (Dec 07 2019 at 00:03, on Zulip):

the idea with substitute was that it would take for<'p0...'pn> T, along with some lifetimes 'x0...'xn, and return ['p0=>'x0...'pn=>'xn] T

nikomatsakis (Dec 07 2019 at 00:03, on Zulip):

i.e., it "removed" one level of binder

nikomatsakis (Dec 07 2019 at 00:03, on Zulip):

but in your formulation it didn't do that

nikomatsakis (Dec 07 2019 at 00:03, on Zulip):

it preserved the levels of binders

nikomatsakis (Dec 07 2019 at 00:03, on Zulip):

hence the infinite recursion

nikomatsakis (Dec 07 2019 at 00:03, on Zulip):

however, the only need for that function in the first place was so that we could do unify_forall_other -- i.e., unify a type like for<'a> T and U

nikomatsakis (Dec 07 2019 at 00:04, on Zulip):

but in practice all for<'a> types in Rust are tied to fn types of some ABI or another. And in fact that's exactly the point of this change, to kind of "fuse" together the quantification with the fn type, versus having them separated as chalk was originally intending -- this matches better Rust and just generally matches the syntax of Rust types better

nikomatsakis (Dec 07 2019 at 00:04, on Zulip):

(note that the other place you get for is dyn types, and they have a binder baked in already (in both rustc and chalk))

nikomatsakis (Dec 07 2019 at 00:05, on Zulip):

anyway so what this means is that if you think of for<'a> T as really being like for<'a> fn(T)-- then it makes no sense to unify a for<'a> fn(T) with some other non-forall type U

nikomatsakis (Dec 07 2019 at 00:05, on Zulip):

that's like unifying a Vec and a fn

nikomatsakis (Dec 07 2019 at 00:05, on Zulip):

so if just make that an error, we don't need the function, but we have to patch up a few random tests

nikomatsakis (Dec 07 2019 at 00:06, on Zulip):

I'm not actually sure if I did the right thing patching up the forall_projection tests the way I did

nikomatsakis (Dec 07 2019 at 00:06, on Zulip):

maybe I should have added some for<> into the impl instead

nikomatsakis (Dec 07 2019 at 00:06, on Zulip):

I'm a bit confused what the intent of those tests was

nikomatsakis (Dec 07 2019 at 00:06, on Zulip):

let me tinker with that...

nikomatsakis (Dec 07 2019 at 00:08, on Zulip):

ok, yeah, I think I did that wrong...

nikomatsakis (Dec 07 2019 at 00:08, on Zulip):

/me fixes

nikomatsakis (Dec 07 2019 at 00:09, on Zulip):

fixed

detrumi (Dec 08 2019 at 06:58, on Zulip):

Makes sense

detrumi (Dec 08 2019 at 07:02, on Zulip):

Though I'm confused as to why the for<> was introduced in tests like this:

for<'a> <Unit as DropLt<'a>>::Item: Eq<for<> Unit>

There's no functions involved in these tests?

detrumi (Dec 08 2019 at 07:07, on Zulip):

You mentioned that forall types will only be created for function types, but here they're used around associated types?

nikomatsakis (Dec 09 2019 at 18:58, on Zulip):

@detrumi well in effect the for<> notation should be read as fn()

nikomatsakis (Dec 09 2019 at 18:59, on Zulip):

so e.g., the for<'a> <Unit as DropLt<'a>>::Item is kind of for<'a> fn(<Unit as DropLt<'a>>::Item)

nikomatsakis (Dec 09 2019 at 18:59, on Zulip):

(at least, with the changes I made)

nikomatsakis (Dec 09 2019 at 18:59, on Zulip):

so in order to unify, then, we had to add a fn(Unit) on the other side

nikomatsakis (Dec 09 2019 at 18:59, on Zulip):

but if we go this road, we would presumably (a) change the name to Fn or something and then (b) change the syntax

detrumi (Dec 09 2019 at 19:02, on Zulip):

Ah, I see. That got really confusing, but I see what you mean now

nikomatsakis (Dec 09 2019 at 19:02, on Zulip):

@detrumi yeah it kind of confused me too for a bit, as I was working on the patch :)

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

in particular one thing I was confused about was:

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

there are two places in rust types where for<'a> comes into play

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

one of them is fn types, the other is dyn types

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

I think I originally imagined chalk would factor that out into a common place (hence the current design)

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

but in fact dyn already includes the binders in its setup

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

so really the only thing left for for is fn

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

I think in the end, just specializing to fn makes the type easier to understand anyway

nikomatsakis (Dec 09 2019 at 19:03, on Zulip):

more connected to rust

detrumi (Dec 09 2019 at 19:04, on Zulip):

Yeah, being less general here makes it clearer and easier to solve

nikomatsakis (Dec 09 2019 at 21:51, on Zulip):

Oh, I am re-reading our notes from last time,

nikomatsakis (Dec 09 2019 at 21:52, on Zulip):

I see there is one more case I had overlooked -- generator witnesses

nikomatsakis (Dec 09 2019 at 21:52, on Zulip):

maybe we'll just extend chalk with that concept directly, though

detrumi (Jan 02 2020 at 14:51, on Zulip):

@nikomatsakis I've rebased and updated the parser, so it should be good to go. I've renamed TyData::ForAll to TyData::Function as well. Was about to ask whether that Box was still needed, but seems like that was already removed in the meantime :slight_smile:

nikomatsakis (Jan 06 2020 at 18:52, on Zulip):

Nice, @detrumi

nikomatsakis (Jan 06 2020 at 19:40, on Zulip):

Left one minor nit, otherwise ready to merge I think

detrumi (Jan 06 2020 at 20:13, on Zulip):

@nikomatsakis Nit fixed!

nikomatsakis (Jan 06 2020 at 20:13, on Zulip):

nice

nikomatsakis (Jan 06 2020 at 20:14, on Zulip):

merged!

Last update: Jan 21 2020 at 09:45UTC