Stream: wg-traits

Topic: planning meeting 2018-10-09


nikomatsakis (Oct 09 2018 at 14:04, on Zulip):

Hello all, so we were going to try and do some planning

nikomatsakis (Oct 09 2018 at 14:05, on Zulip):

I'm not sure whether to do this on Zulip or on appear.in, but @scalexm says their network is sort of slow today, so maybe we'll give Zulip a try :)

nikomatsakis (Oct 09 2018 at 14:06, on Zulip):

So let's see

nikomatsakis (Oct 09 2018 at 14:06, on Zulip):

(cc @tmandry, you also were saying you'd be able to attend)

nikomatsakis (Oct 09 2018 at 14:06, on Zulip):

Some lnks:

tmandry (Oct 09 2018 at 14:07, on Zulip):

:wave:

nikomatsakis (Oct 09 2018 at 14:08, on Zulip):

I forget, @tmandry and @scalexm, did we have some "final" set of notes for the steps we had planned to take?

nikomatsakis (Oct 09 2018 at 14:08, on Zulip):

I found various Dropbox papers

tmandry (Oct 09 2018 at 14:09, on Zulip):

I think the Upcoming Traits Work doc was it

nikomatsakis (Oct 09 2018 at 14:10, on Zulip):

ok

nikomatsakis (Oct 09 2018 at 14:11, on Zulip):

so that was focused on "Preliminary chalk integration", we can start there

nikomatsakis (Oct 09 2018 at 14:11, on Zulip):

there is a check-list for integrate chalk under a flag (#48049)

nikomatsakis (Oct 09 2018 at 14:12, on Zulip):

@scalexm has been working on that list

nikomatsakis (Oct 09 2018 at 14:12, on Zulip):

it's maybe worth elaborating these two items a bit:

which I think are the "next two" items beyond what @scalexm is actively doing

nikomatsakis (Oct 09 2018 at 14:12, on Zulip):

@scalexm is there a rust issue for "implement very naive procedure to find the lowered rules for a given domain goal"?

scalexm (Oct 09 2018 at 14:13, on Zulip):

I think there is one

scalexm (Oct 09 2018 at 14:13, on Zulip):

https://github.com/rust-lang/rust/issues/49600

nikomatsakis (Oct 09 2018 at 14:14, on Zulip):

ok, I'm going to start taking some "finalized" notes in the Planning Meeting Minutes doc for now

nikomatsakis (Oct 09 2018 at 14:14, on Zulip):

but I think it'd be best to move these to GH as the "central roadmap planning space"

nikomatsakis (Oct 09 2018 at 14:16, on Zulip):

I guess to step back

nikomatsakis (Oct 09 2018 at 14:16, on Zulip):

one question is the set of lowering rules

nikomatsakis (Oct 09 2018 at 14:16, on Zulip):

I think we're "more or less" on top of this part for now, right? (e.g., #49177)

scalexm (Oct 09 2018 at 14:17, on Zulip):

@nikomatsakis rules Implied-Bound-From-AssocTy and Implied-WC-From-AssocTy are not relevant without GATs for now

scalexm (Oct 09 2018 at 14:17, on Zulip):

rule ProjectionEq-Normalize is blocked by the support of bound tys

scalexm (Oct 09 2018 at 14:17, on Zulip):

and the three remaining ones are in my PR

Sunjay Varma (Oct 09 2018 at 14:18, on Zulip):

Should we add the rules for coherence at some point?

nikomatsakis (Oct 09 2018 at 14:18, on Zulip):

ok so bound tys

nikomatsakis (Oct 09 2018 at 14:18, on Zulip):

@Sunjay Varma good question; probably eventually but I feel like it's not needed for this preliminary goal

nikomatsakis (Oct 09 2018 at 14:18, on Zulip):

we should maybe make explicit what program we want to work

nikomatsakis (Oct 09 2018 at 14:19, on Zulip):

I was imagining something like

#![no_std]

trait Foo { }

impl Foo for i32 { }

impl Foo for u32 { }

fn gimme<F: Foo>() { }

fn main() {
    gimme::<i32>();
    gimme::<u32>();
    gimme::<f32>(); //~ ERROR
}
nikomatsakis (Oct 09 2018 at 14:19, on Zulip):

about as simple as it gets :)

nikomatsakis (Oct 09 2018 at 14:21, on Zulip):

(sounds good?)

scalexm (Oct 09 2018 at 14:21, on Zulip):

yes :)

Sunjay Varma (Oct 09 2018 at 14:21, on Zulip):

yes :)

nikomatsakis (Oct 09 2018 at 14:21, on Zulip):

so what do we need to support "bound types" exactly

nikomatsakis (Oct 09 2018 at 14:22, on Zulip):

I think our intention was basically to add a BoundTy variant

nikomatsakis (Oct 09 2018 at 14:22, on Zulip):

something like BoundTy(DebruijnIndex, usize)

nikomatsakis (Oct 09 2018 at 14:22, on Zulip):

arguably not needed for that initial program

nikomatsakis (Oct 09 2018 at 14:22, on Zulip):

but otoh kind of hard to make things even work without it

scalexm (Oct 09 2018 at 14:23, on Zulip):

yes, there is some work already in https://github.com/rust-lang/rust/pull/52984 I believe

nikomatsakis (Oct 09 2018 at 14:23, on Zulip):

right

scalexm (Oct 09 2018 at 14:23, on Zulip):

which I forgot to review btw, the author was blocked on how to determine the debruijn index

nikomatsakis (Oct 09 2018 at 14:23, on Zulip):

ok

nikomatsakis (Oct 09 2018 at 14:25, on Zulip):

we had a pre-existing issue: https://github.com/rust-lang/rust/issues/49810

nikomatsakis (Oct 09 2018 at 14:25, on Zulip):

we are basically there though, if that PR works out

nikomatsakis (Oct 09 2018 at 14:25, on Zulip):

you still up to review it @scalexm ?

nikomatsakis (Oct 09 2018 at 14:25, on Zulip):

(I can also take a look)

nikomatsakis (Oct 09 2018 at 14:25, on Zulip):

now that I'm budgetting a bit more traits time :)

scalexm (Oct 09 2018 at 14:26, on Zulip):

well I was suggesting to just assume for now that types always live in a specific root universe, so basically just put 0 for the debruijn index and land that PR

scalexm (Oct 09 2018 at 14:27, on Zulip):

so that we can adjust that later once we support bound tys in all places

nikomatsakis (Oct 09 2018 at 14:28, on Zulip):

sounds reasonable

nikomatsakis (Oct 09 2018 at 14:28, on Zulip):

ideally, add some assertions that this is the case =)

nikomatsakis (Oct 09 2018 at 14:28, on Zulip):

(if applicable)

nikomatsakis (Oct 09 2018 at 14:29, on Zulip):

ok, so, I think the next thing is "implement very naive procedure to find the lowered rules for a given domain goal", which I think is what you are working on

nikomatsakis (Oct 09 2018 at 14:29, on Zulip):

not sure if we have an open issue for that

scalexm (Oct 09 2018 at 14:30, on Zulip):

@nikomatsakis I gave a link to this: https://github.com/rust-lang/rust/issues/49600

nikomatsakis (Oct 09 2018 at 14:30, on Zulip):

oh right, thanks

nikomatsakis (Oct 09 2018 at 14:30, on Zulip):

I was just skimming the old issues and found it as well :)

nikomatsakis (Oct 09 2018 at 14:30, on Zulip):

I will assign to you, then

nikomatsakis (Oct 09 2018 at 14:31, on Zulip):

next up: "implement unification procedures in integration"

nikomatsakis (Oct 09 2018 at 14:31, on Zulip):

I don't see an issue for this

nikomatsakis (Oct 09 2018 at 14:32, on Zulip):

For reference, here is a link to chalk_context.rs, our impl of the chalk traits

nikomatsakis (Oct 09 2018 at 14:32, on Zulip):

I am referring then to unify_parameters

nikomatsakis (Oct 09 2018 at 14:33, on Zulip):

is that it? I thought there was something else too...

nikomatsakis (Oct 09 2018 at 14:33, on Zulip):

ah, yes, and the ResolventOps methods

nikomatsakis (Oct 09 2018 at 14:34, on Zulip):

I'll open an issue on this I guess ā€” probably to cover all 3... I have to refresh my memory, but it seems unlikely to be worthwhile doing them independently

nikomatsakis (Oct 09 2018 at 14:34, on Zulip):

(also, the WG-compiler-traits list is pretty decent, we might want to prune it a bit but it seems good-ish)

Sunjay Varma (Oct 09 2018 at 14:35, on Zulip):

Is there a section in the rustc-guide about the work that has currently been done to integrate chalk into rustc? It would be good to have at least a short section about where to find things, how they map to similar concepts/files from the chalk repo, etc.

nikomatsakis (Oct 09 2018 at 14:36, on Zulip):

https://rust-lang-nursery.github.io/rustc-guide/traits/index.html

nikomatsakis (Oct 09 2018 at 14:36, on Zulip):

no doubt can be expanded

scalexm (Oct 09 2018 at 14:37, on Zulip):

yes the rustc guide should definitely be expanded

scalexm (Oct 09 2018 at 14:37, on Zulip):

that was something I wanted to work on eventually

Sunjay Varma (Oct 09 2018 at 14:37, on Zulip):

I think I may have been looking for: https://rust-lang-nursery.github.io/rustc-guide/traits/lowering-module.html

Sunjay Varma (Oct 09 2018 at 14:38, on Zulip):

Because the rest of the guide is pretty specific to the chalk repo, not rustc, right?

scalexm (Oct 09 2018 at 14:39, on Zulip):

@Sunjay Varma well we are basically moving most chalk rules in rustc so this will soon be about rustc too :)

scalexm (Oct 09 2018 at 14:39, on Zulip):

but even the chalk section needs to be completed, in particular the "new-style" well-formedness requirements are not detailed at all

Sunjay Varma (Oct 09 2018 at 14:39, on Zulip):

Oh I should clarify. I meant the specific files like "we are putting the rules in xx.rs" and "lowering happens in yy.rs" etc.

nikomatsakis (Oct 09 2018 at 14:40, on Zulip):

ok so the last thing on that list is "implement other bits of integration (fill in panics)"

nikomatsakis (Oct 09 2018 at 14:40, on Zulip):

let's see, what are those?

nikomatsakis (Oct 09 2018 at 14:41, on Zulip):
tmandry (Oct 09 2018 at 14:44, on Zulip):

Iā€™m guessing the best reference for these is their implementation in chalk

nikomatsakis (Oct 09 2018 at 14:44, on Zulip):

mm sort of

nikomatsakis (Oct 09 2018 at 14:44, on Zulip):

in many cases there exists comparbale code in rustc

nikomatsakis (Oct 09 2018 at 14:45, on Zulip):

so, I guess I can file issues for those, and try to give a few hints where to find the relevant code (I suspect of this bunch I would be best for that)

nikomatsakis (Oct 09 2018 at 14:46, on Zulip):

I guess that some of them depend on whether we plan to change the Goal etc

nikomatsakis (Oct 09 2018 at 14:46, on Zulip):

@scalexm we were talking about maybe moving away from ty::Predicate, right?

nikomatsakis (Oct 09 2018 at 14:46, on Zulip):

I'm looking specifically at is_coinductive

scalexm (Oct 09 2018 at 14:46, on Zulip):

@nikomatsakis yes

scalexm (Oct 09 2018 at 14:47, on Zulip):

but I think ty::Predicate is not used in chalk_context.rs apart from ParamEnv, which I'm replacing by a new type

nikomatsakis (Oct 09 2018 at 14:47, on Zulip):

ok, that's a good "to do" item for me, and I think those will be good "intro tasks"

nikomatsakis (Oct 09 2018 at 14:47, on Zulip):

but I think ty::Predicate is not used in chalk_context.rs apart from ParamEnv, which I'm replacing by a new type

isn't it used for DomainGoal or something?

scalexm (Oct 09 2018 at 14:49, on Zulip):

in DomainGoal we only use e.g. ty::TraitPredicate or ty::ProjectionPredicate

scalexm (Oct 09 2018 at 14:49, on Zulip):

which I think are ok

nikomatsakis (Oct 09 2018 at 14:50, on Zulip):

ok

nikomatsakis (Oct 09 2018 at 14:51, on Zulip):

so ā€” hmm, where does the "universe" work I've been doing fall on this spectrum.

nikomatsakis (Oct 09 2018 at 14:51, on Zulip):

feels like it will help on implementing some of those methods above (the ones I broke out)

nikomatsakis (Oct 09 2018 at 14:51, on Zulip):

may or may not be a blocker per se

nikomatsakis (Oct 09 2018 at 14:53, on Zulip):

OK, is there more to say about prelim chalk integration?

nikomatsakis (Oct 09 2018 at 14:54, on Zulip):

Seems like no

nikomatsakis (Oct 09 2018 at 14:54, on Zulip):

we may need to call it soon (because it's been ~1 hr and I've got other stuff to do), but it seems clear there is a need to break out more tasks

scalexm (Oct 09 2018 at 14:54, on Zulip):

I think that's it

tmandry (Oct 09 2018 at 14:54, on Zulip):

where is the tracking issue to rewrite rustc in lambda Prolog

nikomatsakis (Oct 09 2018 at 14:55, on Zulip):

looking over the list of WG-compiler-traits issues, I see various things that would be worth going into, not all of which are directly chalk related

nikomatsakis (Oct 09 2018 at 14:56, on Zulip):

ah, @scalexm, that reminds me ā€” once we support bound types, we also need to support placeholder types (which obviously overlap with TyParam, but anyway). That would be quite useful for some of the work that @mikeyhew was doing in https://github.com/rust-lang/rust/pull/54383

nikomatsakis (Oct 09 2018 at 14:57, on Zulip):

also, I found "refactor structure of ty::Predicate" #48539, but I'm guessing that's out of date and not worth pursuing, particularly if we're going to build up a parallel replacement structure

scalexm (Oct 09 2018 at 14:57, on Zulip):

mmh

scalexm (Oct 09 2018 at 14:57, on Zulip):

what are "placeholder" types? Not related to what we used to call skolemized types before I guess?

nikomatsakis (Oct 09 2018 at 14:57, on Zulip):

same thing

nikomatsakis (Oct 09 2018 at 14:57, on Zulip):

e.g., when you have for<T> { ... }

scalexm (Oct 09 2018 at 14:58, on Zulip):

ah ok

nikomatsakis (Oct 09 2018 at 14:58, on Zulip):

and you open the binder...

scalexm (Oct 09 2018 at 14:58, on Zulip):

yes I was basically including that in "bound types support" then :)

nikomatsakis (Oct 09 2018 at 14:58, on Zulip):

agreed, I had just overlooked it

scalexm (Oct 09 2018 at 14:58, on Zulip):

and as for TyParam I guess it will just be a "named" BoundTy

nikomatsakis (Oct 09 2018 at 14:58, on Zulip):

it would follow the structure of RePlaceholder presumably

nikomatsakis (Oct 09 2018 at 14:58, on Zulip):

yes, so, in regions we also have this split

nikomatsakis (Oct 09 2018 at 14:58, on Zulip):

I don't love it but it's ok

nikomatsakis (Oct 09 2018 at 14:59, on Zulip):

basically "higher-ranked trait bounds" and "higher-ranked types" wind up with RePlaceholder

nikomatsakis (Oct 09 2018 at 14:59, on Zulip):

but otherwise you get other variants

nikomatsakis (Oct 09 2018 at 15:00, on Zulip):

ok, well, we should probably stop for now, maybe we ought to reconvene again though

nikomatsakis (Oct 09 2018 at 15:00, on Zulip):

we reached a logical stopping point, anyway

tmandry (Oct 09 2018 at 15:00, on Zulip):

the placeholders conversation is a bit confusing to me, because I always associate it with associated types only

nikomatsakis (Oct 09 2018 at 15:01, on Zulip):

the concept of placeholders is more general

nikomatsakis (Oct 09 2018 at 15:01, on Zulip):

e.g., if you are proving forall<T> { T: Debug }

nikomatsakis (Oct 09 2018 at 15:01, on Zulip):

then you do that by instantiating T with a "placeholder" meant to represent "any type"

nikomatsakis (Oct 09 2018 at 15:01, on Zulip):

we usually write these as !1

nikomatsakis (Oct 09 2018 at 15:01, on Zulip):

whereas if you were proving exists<T> { ... }, you would instantiate T with an inference variable (?1)

nikomatsakis (Oct 09 2018 at 15:02, on Zulip):

in the case of an associated type, the "placeholder" is again meant to represent "any type used as the value of this associated type" :)

tmandry (Oct 09 2018 at 15:02, on Zulip):

right ok

tmandry (Oct 09 2018 at 15:03, on Zulip):

makes sense. thanks

nikomatsakis (Oct 09 2018 at 15:05, on Zulip):

OK, great, thanks all! <3

I think that tomorrow I would be up to do a bit more of this planning, though probably a bit later, maybe 11 (vs 10 today)? I wanted to dig into a few non-chalk things. No need to be present but feel free to show up, I'll probably open a thread and talk out loud in Zulip. =)

Diogo Sousa (Oct 10 2018 at 00:26, on Zulip):

@Sunjay Varma I added a couple links to the "Context & Background About Chalk" in the dropbox paper about the SLG solver. I'm not entirely sure if they deserve to be there, so I'm just letting you know :)

Sunjay Varma (Oct 10 2018 at 00:34, on Zulip):

Yup! That's great! Thanks

Last update: Nov 18 2019 at 01:20UTC