Stream: wg-traits

Topic: meeting 2019-10-21


nikomatsakis (Oct 21 2019 at 16:31, on Zulip):

Hey @WG-traits --

So do we want to have a design meeting today? It hasn't been long since our last one, and I was traveling much of that time, so I didn't have time to "prepare" anything. However, here are some things I think we could talk about:

I'm going to go for a bit but I'll see what people think when I get back =)

Alexander Regueiro (Oct 21 2019 at 16:38, on Zulip):

Sounds fair

Alexander Regueiro (Oct 21 2019 at 16:38, on Zulip):

I can make tonight for once!

Sunjay Varma (Oct 21 2019 at 16:42, on Zulip):

I will probably be in another meeting today at 2 pm, but yes very excited to start on specialization again!

nikomatsakis (Oct 21 2019 at 17:39, on Zulip):

Some other possible topics I thought of later:

nikomatsakis (Oct 21 2019 at 17:40, on Zulip):

or maybe:

nikomatsakis (Oct 21 2019 at 18:04, on Zulip):

OK, @WG-traits hello =)

nikomatsakis (Oct 21 2019 at 18:05, on Zulip):

So as I wrote above, I'm not 100% sure what to talk about today, but open to suggestions. I mostly just want us to keep talking more than anything. =)

nikomatsakis (Oct 21 2019 at 18:06, on Zulip):

I guess it depends a bit on who's around

nikomatsakis (Oct 21 2019 at 18:08, on Zulip):

I think I would probably narrow down to 2 things that seem best to me:

All the topics above seem imp't, but I think I'd rather do the "planning" part a bit separately.

nikomatsakis (Oct 21 2019 at 18:09, on Zulip):

OK, let's just start in on the first one a bit

nikomatsakis (Oct 21 2019 at 18:09, on Zulip):

The basic problem is that Chalk doesn't understand anything about dyn Trait -- or didn't

nikomatsakis (Oct 21 2019 at 18:10, on Zulip):

@Keith Yeung added a new sort of type for that (link)

nikomatsakis (Oct 21 2019 at 18:10, on Zulip):

It looks like this:

    /// A "dyn" type is a trait object type created via the "dyn Trait" syntax.
    /// In the chalk parser, the traits that the object represents is parsed as
    /// a QuantifiedInlineBound, and is then changed to a list of where clauses
    /// during lowering.
    ///
    /// See the `Opaque` variant for a discussion about the use of
    /// binders here.
    Dyn(Binders<Vec<QuantifiedWhereClause>>),
nikomatsakis (Oct 21 2019 at 18:11, on Zulip):

(I'm going to skip past impl trait for a section, but we can loop back to that)

nikomatsakis (Oct 21 2019 at 18:11, on Zulip):

This type definition is sort of interesting I think because it looks very different from other types; it embeds "where clauses"

nikomatsakis (Oct 21 2019 at 18:12, on Zulip):

this comes back to the idea of dyn Trait being a kind of "existential type" -- i.e., shorthand for a type like exists<T> { T: Trait }. i.e., "some type that implements Trait"

nikomatsakis (Oct 21 2019 at 18:12, on Zulip):

(make sense so far?)

tmandry (Oct 21 2019 at 18:13, on Zulip):

I thought that was a bit odd, but guess it makes sense if you do Self: Trait

tmandry (Oct 21 2019 at 18:14, on Zulip):

(my internet is flaking so sorry if this comes out of order)

detrumi (Oct 21 2019 at 18:15, on Zulip):

Not sure about the Self, but the exists makes sense

nikomatsakis (Oct 21 2019 at 18:15, on Zulip):

(er, sorry! afk for 2 minutes)

tmandry (Oct 21 2019 at 18:16, on Zulip):

yeah nevermind, the Self part doesn't seem right

tmandry (Oct 21 2019 at 18:16, on Zulip):

I sent that before niko's better explanation ;)

nikomatsakis (Oct 21 2019 at 18:19, on Zulip):

ok, back

nikomatsakis (Oct 21 2019 at 18:19, on Zulip):

I'm not sure what you meant by Self but

nikomatsakis (Oct 21 2019 at 18:19, on Zulip):

I guess that worked out :)

nikomatsakis (Oct 21 2019 at 18:19, on Zulip):

in any case, I think the binders etc there are interesting

nikomatsakis (Oct 21 2019 at 18:19, on Zulip):
Binders<Vec<QuantifiedWhereClause>>)

kind of expands to

Binders<Vec<Binders<WhereClause>>>
nikomatsakis (Oct 21 2019 at 18:20, on Zulip):

the notation exists<T> { T: Trait } -- that exists is the first round of Binders

nikomatsakis (Oct 21 2019 at 18:20, on Zulip):

the second round is to allow for things like

nikomatsakis (Oct 21 2019 at 18:20, on Zulip):
dyn FnOnce(&u8)
dyn for<'a> Trait<'a>
nikomatsakis (Oct 21 2019 at 18:21, on Zulip):

which would correspond to a type like

exists<T> { forall<'a> { T: FnOnce<(&'a u8,)> } }
exists<T> { forall<'a> { T: Trait<'a> } }
nikomatsakis (Oct 21 2019 at 18:21, on Zulip):

you can see now where the "inner binders" comes from, maybe

nikomatsakis (Oct 21 2019 at 18:23, on Zulip):

ok, any questions on that? (I was pausing, but didn't say so)

nikomatsakis (Oct 21 2019 at 18:23, on Zulip):

ok so besides the type def'n

nikomatsakis (Oct 21 2019 at 18:23, on Zulip):

how do we integrate these "dyn Trait" types into trait solving?

nikomatsakis (Oct 21 2019 at 18:24, on Zulip):

there is an imp't caveat here, which is that we're wrestling with these rules in rustc proper

nikomatsakis (Oct 21 2019 at 18:24, on Zulip):

but I'm going to give the simple version to start

nikomatsakis (Oct 21 2019 at 18:25, on Zulip):

the basic rule that we want is that dyn Foo: Foo for any Foo

Keith Yeung (Oct 21 2019 at 18:25, on Zulip):

Hmm, that reminds me, solving for impl Trait is different from dyn Trait

nikomatsakis (Oct 21 2019 at 18:25, on Zulip):

this is an implication of a trait being "dyn safe" (which we don't presently choose to model)

nikomatsakis (Oct 21 2019 at 18:25, on Zulip):

Hmm, that reminds me, solving for impl Trait is different from dyn Trait

hmm, I'm not 100% sure what yo mean but let's come back to that

tmandry (Oct 21 2019 at 18:26, on Zulip):

ok, any questions on that? (I was pausing, but didn't say so)

it's been awhile since I worked in chalk, but I thought Binders only corresponded to forall quantifiers

nikomatsakis (Oct 21 2019 at 18:26, on Zulip):

no, Binders correspond to any sort of quantifier; whether it is forall or exists comes from the surrounding context

detrumi (Oct 21 2019 at 18:26, on Zulip):

Maybe only one of them was used initially in Chalk?

tmandry (Oct 21 2019 at 18:26, on Zulip):

okay, I find the docs confusing in that case

nikomatsakis (Oct 21 2019 at 18:27, on Zulip):

Maybe only one of them was used initially in Chalk?

nope

nikomatsakis (Oct 21 2019 at 18:27, on Zulip):

but forall is far more common

nikomatsakis (Oct 21 2019 at 18:27, on Zulip):

see e.g. this part of the Goal definition

nikomatsakis (Oct 21 2019 at 18:27, on Zulip):
   Quantified(QuantifierKind, Binders<Box<Goal>>),
nikomatsakis (Oct 21 2019 at 18:27, on Zulip):

that encodes both forall<T> { .. } and exists<T> { ... } goals

nikomatsakis (Oct 21 2019 at 18:27, on Zulip):

I think the best way to thikn about Binders is as the <T> { .. } part

nikomatsakis (Oct 21 2019 at 18:27, on Zulip):

without the forall or exists

nikomatsakis (Oct 21 2019 at 18:28, on Zulip):

for completeness, QuantifiedKind is:

pub enum QuantifierKind {
    ForAll,
    Exists,
}
nikomatsakis (Oct 21 2019 at 18:28, on Zulip):

okay, I find the docs confusing in that case

that...seems quite likely

tmandry (Oct 21 2019 at 18:28, on Zulip):

docs for Binders

detrumi (Oct 21 2019 at 18:29, on Zulip):

Hmm, why not something like Quantified(QuantifierKind, Binders, Box<Goal>) then?

nikomatsakis (Oct 21 2019 at 18:29, on Zulip):

@detrumi the Binders<T> encloses the value that is bound

nikomatsakis (Oct 21 2019 at 18:29, on Zulip):

this is useful because you often want to have operations like

instantiate<T>(x: &Binders<T>) -> T
nikomatsakis (Oct 21 2019 at 18:30, on Zulip):

that will take all the bound variables and replace them with inference variables, returning the T inside

nikomatsakis (Oct 21 2019 at 18:30, on Zulip):

it is also useful because it's kind of a bug to access the T inside without considering the new binders

nikomatsakis (Oct 21 2019 at 18:30, on Zulip):

so it makes sense for it to be "owned"

nikomatsakis (Oct 21 2019 at 18:30, on Zulip):

rustc is actually stricter on this point than chalk is, which is something I think we should improve

nikomatsakis (Oct 21 2019 at 18:30, on Zulip):

well, I can't remember, actually

nikomatsakis (Oct 21 2019 at 18:30, on Zulip):

at some point in rustc I had a branch that made the "value" of a Binders private

nikomatsakis (Oct 21 2019 at 18:31, on Zulip):

so that all accesses to it had to go through some suitable API

nikomatsakis (Oct 21 2019 at 18:31, on Zulip):

which made for easier auditing

nikomatsakis (Oct 21 2019 at 18:31, on Zulip):

should prob do the same with chalk eventually

nikomatsakis (Oct 21 2019 at 18:31, on Zulip):

ok, move on?

tmandry (Oct 21 2019 at 18:31, on Zulip):

at some point in rustc I had a branch that made the "value" of a Binders private

I remember doing that refactor in rustc, I believe it's still the case =)

nikomatsakis (Oct 21 2019 at 18:32, on Zulip):

docs for Binders

"Indicates that the value is universally quantified over N parameters of the given kinds, where N == self.binders.len(). A variable with depth i < N refers to the value at self.binders[i]. Variables with depth >= N are free."

nikomatsakis (Oct 21 2019 at 18:32, on Zulip):

yeah, that's just wrong

nikomatsakis (Oct 21 2019 at 18:32, on Zulip):

heh, awesome

nikomatsakis (Oct 21 2019 at 18:32, on Zulip):

yeah I think I did a branch for it and then it bitrotted

nikomatsakis (Oct 21 2019 at 18:32, on Zulip):

and then I made you do it :P

nikomatsakis (Oct 21 2019 at 18:33, on Zulip):

the basic rule that we want is that dyn Foo: Foo for any Foo

so this rule

nikomatsakis (Oct 21 2019 at 18:33, on Zulip):

the question is, how do we handle this?

Keith Yeung (Oct 21 2019 at 18:33, on Zulip):

at some point in rustc I had a branch that made the "value" of a Binders private

good thing you are restricting that for chalk now, otherwise i really would've just used that field to do computation upon

nikomatsakis (Oct 21 2019 at 18:33, on Zulip):

in "old school chalk", we had a premise that we lowered all the impls/traits to a fixed set of program clauses

nikomatsakis (Oct 21 2019 at 18:33, on Zulip):

but this doesn't work well for dyn and impl trait types

nikomatsakis (Oct 21 2019 at 18:33, on Zulip):

because the set of rules is kind of open ended and huge

nikomatsakis (Oct 21 2019 at 18:34, on Zulip):

especially once you consider things like dyn Write + Send

nikomatsakis (Oct 21 2019 at 18:34, on Zulip):

there we want two rules:

dyn (Write + Send): Write
dyn (Write + Send): Send
nikomatsakis (Oct 21 2019 at 18:34, on Zulip):

(note that chalk rules work with equality, not subtyping, so you can't just say dyn Write: Write -- and anyway dyn (Write + Send) is not a subtype of dyn Write in Rust)

nikomatsakis (Oct 21 2019 at 18:35, on Zulip):

(which touches on the upcasting work that @Alexander Regueiro has been pursuing :)

nikomatsakis (Oct 21 2019 at 18:35, on Zulip):

however, the good thing is that chalk has been moving towards this more "on demand" model anyway

nikomatsakis (Oct 21 2019 at 18:36, on Zulip):

which fits better with rust-analyzer, rustc, incremental, etc

nikomatsakis (Oct 21 2019 at 18:36, on Zulip):

so basically there is this callback for the core engine where it says:

I have to prove the goal G, what are the relevant program clauses?

nikomatsakis (Oct 21 2019 at 18:36, on Zulip):

@detrumi will remember this, as they did a lot of the core refactoring work here :)

Keith Yeung (Oct 21 2019 at 18:37, on Zulip):

i'm a bit lost here, does a QuantifiedWhereClause have a corresponding Goal definition associated with it?

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

a "where clause" corresponds to a Rust where clause -- it is neither a goal nor a "clause"

Alexander Regueiro (Oct 21 2019 at 18:37, on Zulip):

@nikomatsakis Speaking off which, how should we proceed with codegen?

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

a "where clause" corresponds to a Rust where clause -- it is neither a goal nor a "clause"

let me glossary those:

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

there is a collision of terminology here, which I hadn't fully realized, in that goal/clause come from prolog solvers

nikomatsakis (Oct 21 2019 at 18:39, on Zulip):

and 'where clause' is just some thing I invented for RFC XXX

nikomatsakis (Oct 21 2019 at 18:39, on Zulip):

whichever one it was that introducd where clauses ;)

nikomatsakis (Oct 21 2019 at 18:41, on Zulip):

in particular though where clauses are a subset of goals etc

nikomatsakis (Oct 21 2019 at 18:41, on Zulip):

(@Alexander Regueiro -- let's discuss that later)

Alexander Regueiro (Oct 21 2019 at 18:41, on Zulip):

Okay

nikomatsakis (Oct 21 2019 at 18:41, on Zulip):

i'm a bit lost here, does a QuantifiedWhereClause have a corresponding Goal definition associated with it?

that is, you can convert a WC to a goal

nikomatsakis (Oct 21 2019 at 18:41, on Zulip):

sorry, I feel like I'm rambling, not sure if I'm really answering your question @Keith Yeung

tmandry (Oct 21 2019 at 18:42, on Zulip):

(bikeshed: we could start calling them "where bounds" -- as opposed to "inline bounds"? but I don't want to derail further)

Keith Yeung (Oct 21 2019 at 18:42, on Zulip):

i'm just wondering if a where-clause is a goal -- something that we want to prove

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

(bikeshed: we could start calling them "where bounds" -- as opposed to "inline bounds"? but I don't want to derail further)

yeah, maybe

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

I usually say "bound" to mean the thing on the right-hand side of a :

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

e.g., the Debug in T: Foo -- it's kind of a where-clause without the "self" part

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

i'm just wondering if a where-clause is a goal -- something that we want to prove

ok -- well, the answer is "sometimes"

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

e.g.,

fn foo<T>() where T: Send {  }
nikomatsakis (Oct 21 2019 at 18:43, on Zulip):

when you call foo, you have to prove that T: Send for whichever value of T you chose (so it's a goal)

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

but you type-check the body of Foo, you get to assume T: Foo for some placeholder T (so it's a "clause")

detrumi (Oct 21 2019 at 18:44, on Zulip):

that is, you can convert a WC to a goal

Isn't a WC context sensitive? Because it's just part of a type

nikomatsakis (Oct 21 2019 at 18:44, on Zulip):

in the case of dyn Send, the same is true -- when you create an instance of a dyn Send type, you have to prove that T: Send

nikomatsakis (Oct 21 2019 at 18:44, on Zulip):

(but that sort of happens outside the purview of chalk)

nikomatsakis (Oct 21 2019 at 18:44, on Zulip):

but when we are trying to prove dyn Send: Send, we get to assume things

nikomatsakis (Oct 21 2019 at 18:45, on Zulip):

anyway let's talk through that exact mechanism a bit? maybe it becomes clearer?

nikomatsakis (Oct 21 2019 at 18:46, on Zulip):

I'm trying to find the dang callback right now

nikomatsakis (Oct 21 2019 at 18:46, on Zulip):

ok well there is this function:

nikomatsakis (Oct 21 2019 at 18:46, on Zulip):
pub(crate) fn program_clauses_for_goal<'db>(
    db: &'db dyn RustIrDatabase,
    environment: &Arc<Environment<ChalkIr>>,
    goal: &DomainGoal<ChalkIr>,
) -> Vec<ProgramClause<ChalkIr>> { .. }
nikomatsakis (Oct 21 2019 at 18:47, on Zulip):

from clauses.rs

nikomatsakis (Oct 21 2019 at 18:47, on Zulip):

so what's happening here is that the solver is saying "I have to prove goal, what are the 'program clauses' I might use to do it"

nikomatsakis (Oct 21 2019 at 18:47, on Zulip):

a program clause is just a clause that's globally true and widely know; perhaps a meaningless piece of jargon we should remove

nikomatsakis (Oct 21 2019 at 18:48, on Zulip):

( it comes from prolog -- i.e., it's the clauses you wrote in your prolog program. )

detrumi (Oct 21 2019 at 18:50, on Zulip):

Huh, didn't know it was that simple

nikomatsakis (Oct 21 2019 at 18:54, on Zulip):

anyway so the point is, suppose we are trying to prove something like

dyn Foo: XXX
nikomatsakis (Oct 21 2019 at 18:54, on Zulip):

or rather

nikomatsakis (Oct 21 2019 at 18:54, on Zulip):

well, yes

nikomatsakis (Oct 21 2019 at 18:54, on Zulip):

we are going to synthesize rules of the form dyn Foo: Foo

nikomatsakis (Oct 21 2019 at 18:54, on Zulip):

as possible clauses

nikomatsakis (Oct 21 2019 at 18:54, on Zulip):

we are actually rather inefficient about this

nikomatsakis (Oct 21 2019 at 18:55, on Zulip):

this is because we don't consider what the XXX is

nikomatsakis (Oct 21 2019 at 18:55, on Zulip):

we just say "ah, you are trying to prove something of the form dyn XXX: YYY? I will make some rules like dyn XXX: XXX -- if it so happens that XXX = YYY, that would be useful to you; otherwise, it's not"

nikomatsakis (Oct 21 2019 at 18:56, on Zulip):

this is ok because the callback is basically allowed to return "extra" rules that don't really apply to the goal at hand

nikomatsakis (Oct 21 2019 at 18:56, on Zulip):

it should perhaps be improved at some point, but not imp't

nikomatsakis (Oct 21 2019 at 18:56, on Zulip):

so where does that happen, you ask?

nikomatsakis (Oct 21 2019 at 18:56, on Zulip):

in the function program_clauses_that_could_match

nikomatsakis (Oct 21 2019 at 18:57, on Zulip):

first we check if the thing you are trying to prove is Implemented(TraitRef) for some TraitRef (here)

nikomatsakis (Oct 21 2019 at 18:57, on Zulip):

in there we check if the self-type is dyn Foo

nikomatsakis (Oct 21 2019 at 18:57, on Zulip):
            match trait_ref.self_type_parameter() {
                Some(Ty::Opaque(qwc)) | Some(Ty::Dyn(qwc)) => {
                    ...
                }
                _ => {}
            }
nikomatsakis (Oct 21 2019 at 18:58, on Zulip):

here the qwc are those "quantified where clauses" we talked about before, so they have the type Binder<Vec<Binder<WhereClause>>>

nikomatsakis (Oct 21 2019 at 18:58, on Zulip):

really they are kind of "qqwc" -- quantified twice :)

nikomatsakis (Oct 21 2019 at 18:58, on Zulip):

so if our goal were dyn (Write + Send): Send (say)

nikomatsakis (Oct 21 2019 at 18:59, on Zulip):

then the self-type would be dyn (Write + Send), and hence qwc would be something like

exists<T> { forall<> { T: Write }, forall<> { T: Send } }
nikomatsakis (Oct 21 2019 at 18:59, on Zulip):

(where the forall<> indicates "empty" binders)

nikomatsakis (Oct 21 2019 at 19:00, on Zulip):

what we want to produce are two program clauses:

dyn (Write + Send): Write
dyn (Write + Send): Send
nikomatsakis (Oct 21 2019 at 19:00, on Zulip):

as it happens, only the second one will be useful for the goal at hand, but as I said, we don't consider that

nikomatsakis (Oct 21 2019 at 19:00, on Zulip):

so we basically take the qwc and we substitute dyn (Write + Send) for that "self-type" T

nikomatsakis (Oct 21 2019 at 19:00, on Zulip):
                    let self_ty = trait_ref.self_type_parameter().unwrap(); // This cannot be None
                    let wc = qwc.substitute(&[self_ty.cast()]);
nikomatsakis (Oct 21 2019 at 19:01, on Zulip):

this gives us a value wc -- slightly misnamed, as these are actually still quantified where clauses

nikomatsakis (Oct 21 2019 at 19:01, on Zulip):

so wc would be

 vec![
    forall<> { (dyn Write + Send): Write },
    forall<> { dyn (Write + Send): Send }
]
nikomatsakis (Oct 21 2019 at 19:02, on Zulip):

on the final line we convert those into program clauses by using the cast() function

nikomatsakis (Oct 21 2019 at 19:02, on Zulip):
                    clauses.extend(wc.into_iter().casted());
nikomatsakis (Oct 21 2019 at 19:02, on Zulip):

argh, I ust realized it's 3pm ..

nikomatsakis (Oct 21 2019 at 19:02, on Zulip):

sorry, I gotta run to another mtg :)

nikomatsakis (Oct 21 2019 at 19:02, on Zulip):

sorry for the occasional delay today, I had some "local" interruptions

nikomatsakis (Oct 21 2019 at 19:03, on Zulip):

anyway, I'll try to answer questions async, hope that was helpful so far to explain what @Keith Yeung did :)

tmandry (Oct 21 2019 at 19:04, on Zulip):

I thought it was helpful, thanks

tmandry (Oct 21 2019 at 19:04, on Zulip):

also, it might be worth taking your "more general" example here and adding it as a comment in the implementation

tmandry (Oct 21 2019 at 19:06, on Zulip):

as a reminder of why we're working with a vec of clauses, for instance

detrumi (Oct 21 2019 at 19:09, on Zulip):

Ooh, so we're substituting the T, and that removes the exists<T>, leaving us with a vec instead. Was wondering where the vec came from

tmandry (Oct 21 2019 at 19:10, on Zulip):

(I would make the docs/comments changes myself but I also have to run)

detrumi (Oct 21 2019 at 19:10, on Zulip):

That's a lot of implicit steps

nikomatsakis (Oct 21 2019 at 20:25, on Zulip):

(I would make the docs/comments changes myself but I also have to run)

yep I was thinking the same

nikomatsakis (Oct 21 2019 at 20:25, on Zulip):

I'll open a small PR

Keith Yeung (Oct 21 2019 at 22:30, on Zulip):

@nikomatsakis I was thinking in terms of unification for dyn and impl Trait

Keith Yeung (Oct 21 2019 at 22:30, on Zulip):

they seem to have different rules as I understand it

Keith Yeung (Oct 21 2019 at 22:32, on Zulip):

namely, dyn Trait doesn't just mean exists<T> { forall<> { T: Trait } }, it also carries an assumption that the T is behind a pointer

Keith Yeung (Oct 21 2019 at 22:34, on Zulip):

although on second thought, that doesn't seem to be a concern, since all chalk needs to do is to generate another goal to prove that dyn Trait: Pointer or something

nikomatsakis (Oct 22 2019 at 00:30, on Zulip):

namely, dyn Trait doesn't just mean exists<T> { forall<> { T: Trait } }, it also carries an assumption that the T is behind a pointer

indeed I don't think this is really chalk's concern; there are some interactions with the Sized trait

Last update: Nov 12 2019 at 16:20UTC