Stream: wg-traits

Topic: weekly meeting 2019-01-21


nikomatsakis (Jan 20 2019 at 02:19, on Zulip):

@WG-compiler-traits:

I just realized that this Monday is a holiday here in the US -- not sure if I can make the meeting or not. I could probably make it to the same time but on Tuesday. Should we consider rescheduling?

(@scalexm was going to talk about how to handle trait objects in chalk)

scalexm (Jan 20 2019 at 09:05, on Zulip):

I think Tuesday same time is fine for me

Sunjay Varma (Jan 20 2019 at 14:12, on Zulip):

I won't be able to attend, but feel free to go on without me. My update is that I'm currently at a conference with Manish. Manish is leaving on Wednesday after which I will start work on specialization in chalk.

tmandry (Jan 20 2019 at 15:23, on Zulip):

That works for me

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

So will we do the meeting today, @WG-compiler-traits? In ~90 minutes, I suppose.

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

Any thoughts on how we should do this? :)

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

I'm trying to pull together my thoughts from reading https://github.com/rust-lang-nursery/chalk/issues/203

nikomatsakis (Jan 22 2019 at 19:00, on Zulip):

I'm not sure if we had planned to do a chat over video or just stick with Zulip

nikomatsakis (Jan 22 2019 at 19:00, on Zulip):

I feel like we talked about it but I forget the answer :)

scalexm (Jan 22 2019 at 19:02, on Zulip):

@nikomatsakis just Zulip is a bit easier for me this evening, also I could do video

nikomatsakis (Jan 22 2019 at 19:02, on Zulip):

ok that works for me

scalexm (Jan 22 2019 at 19:02, on Zulip):

I answered on the issue about the RFC you cited

nikomatsakis (Jan 22 2019 at 19:02, on Zulip):

I see that, yes, I was thinking something similar

nikomatsakis (Jan 22 2019 at 19:03, on Zulip):

@WG-compiler-traits — guess we'll get started

scalexm (Jan 22 2019 at 19:03, on Zulip):

mmh no actually that wouldn't work because we also require WellFormed(dyn Foo) :- WellFormed(dyn Foo: Foo)

scalexm (Jan 22 2019 at 19:04, on Zulip):

and we somehow need this to prevent the possibility of naming types like dyn Foo<&'a i32> where trait Foo<X>: 'static

nikomatsakis (Jan 22 2019 at 19:04, on Zulip):

something else to file for follow-up: we should discuss associatd item projection (e.g., dyn Foo<T = Bar>)

nikomatsakis (Jan 22 2019 at 19:04, on Zulip):

so, the RFC, I was wondering if we want some in between

nikomatsakis (Jan 22 2019 at 19:05, on Zulip):

i.e., if the trait is not object safe, maybe we permit the dyn type, but we don't add all the "implied bounds" rules

nikomatsakis (Jan 22 2019 at 19:05, on Zulip):

er, I guess I mean the impls

nikomatsakis (Jan 22 2019 at 19:05, on Zulip):

but I think we are getting ahead of ourselves

scalexm (Jan 22 2019 at 19:06, on Zulip):

@nikomatsakis I think dyn Foo<T = Bar> would just add some Normalize rules

scalexm (Jan 22 2019 at 19:06, on Zulip):

well basically in what I call the "generated impls", we would forward the specified associated type values

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

the heart of your proposal is this rule, basically:

impl<T1...Tk> SuperTrait<...> for dyn Foo<T1...Tk> where SuperWC1[...], ..., SuperWCr[...]
{
}
nikomatsakis (Jan 22 2019 at 19:07, on Zulip):

and I guess the WF rule:

WellFormed(dyn Foo<X1...Xk>) :-
    ObjectSafe(Foo),
    WellFormed(dyn Foo<X1...Xk>: Foo<X1...Xk>).
scalexm (Jan 22 2019 at 19:07, on Zulip):

@nikomatsakis right, but actually I believe the where clauses are not even needed (at least under an implied bounds setting), the real heart is the WF rule

nikomatsakis (Jan 22 2019 at 19:08, on Zulip):

it's an interesting rule

nikomatsakis (Jan 22 2019 at 19:08, on Zulip):

so you'll have to refresh my memory

nikomatsakis (Jan 22 2019 at 19:08, on Zulip):

when we prove that WF(T: Trait), does that assume that WF(T) is true?

nikomatsakis (Jan 22 2019 at 19:08, on Zulip):

I know we talked about various different approaches to where to put the "recursion"

scalexm (Jan 22 2019 at 19:08, on Zulip):

@nikomatsakis yes kind of, basically WF(T: Trait) does not care at all about the well-formedness of types

nikomatsakis (Jan 22 2019 at 19:09, on Zulip):

(meta-question: who else is around? Is it just @scalexm and I?)

centril (Jan 22 2019 at 19:09, on Zulip):

/me is reading

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

I'm around briefly

tmandry (Jan 22 2019 at 19:10, on Zulip):

me

nikomatsakis (Jan 22 2019 at 19:10, on Zulip):

cool :)

nikomatsakis (Jan 22 2019 at 19:10, on Zulip):

I am feeling a desire to briefly reiterate how the WF rules work again @scalexm =)

centril (Jan 22 2019 at 19:11, on Zulip):

that's a very curious typing rule... which should never terminate unless WF(T: Trait) doesn't require WF(T)... right?

nikomatsakis (Jan 22 2019 at 19:11, on Zulip):

correct, @centril, that's partly why I was asking

scalexm (Jan 22 2019 at 19:11, on Zulip):

@centril WF(T: Trait) does not assume anything

scalexm (Jan 22 2019 at 19:11, on Zulip):

and it does not try to prove any WF(T) either

scalexm (Jan 22 2019 at 19:11, on Zulip):

well-formedness for types comes from "outside", that is when the type checker see some type Type named somewhere, it will try to prove WF(Type)

Alexander Regueiro (Jan 22 2019 at 19:12, on Zulip):

what does well-formedness even mean?

Alexander Regueiro (Jan 22 2019 at 19:12, on Zulip):

seems like a kind of vague term

nikomatsakis (Jan 22 2019 at 19:12, on Zulip):

@scalexm is the rustc-guide up to date, do you now? (e.g., this section)

nikomatsakis (Jan 22 2019 at 19:12, on Zulip):

what does well-formedness even mean?

it means what we say it means :)

scalexm (Jan 22 2019 at 19:12, on Zulip):

@nikomatsakis the rustc-guide is up to date, except for the slight flaw I discovered

nikomatsakis (Jan 22 2019 at 19:12, on Zulip):

yeah, ok

scalexm (Jan 22 2019 at 19:13, on Zulip):

(which btw I discovered by studying well-formedness for trait objects since you have some weird rule like struct S<T> where S<T>: Trait)

nikomatsakis (Jan 22 2019 at 19:13, on Zulip):

except I linked to the wrong part

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

the wf rules for traits are here, in the lowering section

nikomatsakis (Jan 22 2019 at 19:14, on Zulip):
// Rule WellFormed-TraitRef
forall<Self, P1..Pn> {
  WellFormed(Self: Trait<P1..Pn>) :-
    Implemented(Self: Trait<P1..Pn>) &&
    WellFormed(WC)
}
scalexm (Jan 22 2019 at 19:14, on Zulip):

right

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

so basically @Alexander Regueiro saying that T: Trait is "well-formed" says that (a) it is implemented and (b) all the where clauses on the trait are satisfied

centril (Jan 22 2019 at 19:15, on Zulip):

(the prolog form of stating things feels so backwards stating the premises before the result... as compared to gentzen style...)

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

okay. that means something totally different to logic hah. I thought it was some type-theoretical notion which had a correspondence to logic.

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

ok, so to bring that back to the trait object rule:

WellFormed(dyn Foo<X1...Xk>) :-
    ObjectSafe(Foo),
    WellFormed(dyn Foo<X1...Xk>: Foo<X1...Xk>).

it certainly relies on the Implemented rule that we generate

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

and what does "implemented" mean here?

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

you mean the trait bound is satisfied?

nikomatsakis (Jan 22 2019 at 19:16, on Zulip):

more or less. It means that we believe an impl exists (it may come from an in-scope where-clause, in some contexts)

centril (Jan 22 2019 at 19:16, on Zulip):

(or "witness" in type theory)

scalexm (Jan 22 2019 at 19:17, on Zulip):

@nikomatsakis yes: thanks to the Implemented rules we generate, only the where clauses that talk about lifetimes or type parameters may turn out to be false, all the other where clauses of the form where Self: Trait<...> are somehow "assumed" to be true because of the generated impls

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

(perhaps it's worth mentioning trivial-where-clauses, where some of this breaks down)

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

the impl rule we generate being as follows, I think?

forall<T1..Tk> {
  Implemented(dyn Foo<T1..Tk>: SuperTrait<..>) :-
    Implemented(SuperWC1[...]), ..., Implemented(SuperWCr[...])
}

ah, so, @scalexm, to what extent are we relying on things being acyclic here..?

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

since it allows assuming some things that aren't true globally-- but ignore me if I'm just distracting

scalexm (Jan 22 2019 at 19:18, on Zulip):

@Taylor Cramer I believe trivial-where-clauses are naturally handled in the new-style trait solving, basically we just always assume all where clauses to be true, we never check for "inconsistent" where clauses

scalexm (Jan 22 2019 at 19:19, on Zulip):

@nikomatsakis yes this is what we generate

scalexm (Jan 22 2019 at 19:20, on Zulip):

mmh I think cyclic traits are handled correctly, provided that we can get all the super-traits via some fixed point algorithm

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

so e.g. if we have

trait Foo: Bar { }
trait Bar: Foo { }

today, that's an error, but I'd like to remove that requirement.

scalexm (Jan 22 2019 at 19:20, on Zulip):

but as I noted this must be done outside of the logic

scalexm (Jan 22 2019 at 19:20, on Zulip):

I mean we must have some code in rustc that retrieves all the super-traits and generate the impls

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

so let's walk through that example, maybe? just for my edification :)

nikomatsakis (Jan 22 2019 at 19:21, on Zulip):

basically we would make two rules, lke so, right?

Implemented(dyn Foo: Foo) :- Implemented(dyn Foo: Bar).
Implemented(dyn Foo: Bar) :- Implemented(dyn Foo: Foo).
nikomatsakis (Jan 22 2019 at 19:22, on Zulip):

er, I guess we would also have

Implemented(dyn Bar: Foo) :- Implemented(dyn Bar: Bar).
Implemented(dyn Bar: Bar) :- Implemented(dyn Bar: Foo).

coming from the trait Bar declaration

centril (Jan 22 2019 at 19:22, on Zulip):

@scalexm so if WF(T: Trait) :- WF(T), ... doesn't hold, then won't that make [u8; "hello"] legal and other such nonsense...? or do you check WF(T) later for [u8; "hello"] ?

scalexm (Jan 22 2019 at 19:22, on Zulip):

@nikomatsakis yeah ok it seems like it would not work with the where clauses on the generated impls

scalexm (Jan 22 2019 at 19:22, on Zulip):

however, as I said, I think they are not necessary especially in the implied bounds setting

nikomatsakis (Jan 22 2019 at 19:22, on Zulip):

ok, yeah, maybe we can drill into that a bit

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

@centril cool. that's in terminology I'm familiar with

scalexm (Jan 22 2019 at 19:22, on Zulip):

basically I've written these where clauses at first so that these synthetic impls are well-formed (well-formedness of impls defined in the rustc-guide)

nikomatsakis (Jan 22 2019 at 19:23, on Zulip):

(I kind of can't answer the question of what role they play exactly, I think)

scalexm (Jan 22 2019 at 19:23, on Zulip):

@nikomatsakis but with the reverse rules FromEnv(dyn Foo: Foo) :- FromEnv(dyn Foo) and since we do impl Trait for dyn Foo, we have dyn Foo in our env

nikomatsakis (Jan 22 2019 at 19:24, on Zulip):

OK.

scalexm (Jan 22 2019 at 19:24, on Zulip):

@centril all types appearing in, say, a function are WF-checked in a separate pass indeed

centril (Jan 22 2019 at 19:25, on Zulip):

makes sense

scalexm (Jan 22 2019 at 19:25, on Zulip):

@nikomatsakis but basically the sentence I wrote on the issue:

Note that, in the rules described earlier, we added where clauses from the super traits on every generated impl only so that the impl is well-formed even without implied bounds, I am not sure they are strictly needed.

sums up the idea

nikomatsakis (Jan 22 2019 at 19:25, on Zulip):

(ps, maybe we should find another name for WellFormed(T: Trait) -- even WellFormedImpl might be more obvious)

nikomatsakis (Jan 22 2019 at 19:26, on Zulip):

(actually not sure that's more obvious ;)

scalexm (Jan 22 2019 at 19:26, on Zulip):

yeah bike-shedding is welcome :)

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

can we come up with better terminology than well-formed, btw? it doesn't really give an intuitive idea of what it means... unless it's standard terminology, I guess. "witnessed" sounds good.

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

oh

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

heh

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

just saw your message

scalexm (Jan 22 2019 at 19:27, on Zulip):

@Alexander Regueiro WellFormed for types has been a terminology floating around in the compiler for some time, and we just basically reused it for traits without thinking too much about it :p

centril (Jan 22 2019 at 19:27, on Zulip):

it's standard terminology

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

(in particular, the goals of the "well-formedness checking" section are different from the "well formed" predicate)

scalexm (Jan 22 2019 at 19:27, on Zulip):

recent developments on implied bounds etc have basically been niko, @Ariel Ben-Yehuda and myself

nikomatsakis (Jan 22 2019 at 19:28, on Zulip):

maybe FullyImplemented or something...

Alexander Regueiro (Jan 22 2019 at 19:28, on Zulip):

yeah. god knows how it became standard though. "well-formed" has syntactical connotations (both to the intuitive mind, and in formal logic)

Alexander Regueiro (Jan 22 2019 at 19:28, on Zulip):

which is why I dislike it.

Alexander Regueiro (Jan 22 2019 at 19:28, on Zulip):

FullyImplemented kind of works

tmandry (Jan 22 2019 at 19:28, on Zulip):

(in particular, the goals of the "well-formedness checking" section are different from the "well formed" predicate)

I remember this being confusing for sure

nikomatsakis (Jan 22 2019 at 19:28, on Zulip):

the latter section might also be called "legality" or something

nikomatsakis (Jan 22 2019 at 19:28, on Zulip):

i.e., it's the rules that make an impl legal

scalexm (Jan 22 2019 at 19:28, on Zulip):

"legality" is good I think

nikomatsakis (Jan 22 2019 at 19:29, on Zulip):

and other forms of declarations

centril (Jan 22 2019 at 19:29, on Zulip):

can we stick to standard terminology (especially that used by Philip Wadler)...? :P

Alexander Regueiro (Jan 22 2019 at 19:29, on Zulip):

no, because it's shit? ;-)

centril (Jan 22 2019 at 19:30, on Zulip):

in gentzen style you might say:

Γ ⊢ σ type
Γ ⊢ x: usize
------------------
Γ ⊢ [σ; x] type
scalexm (Jan 22 2019 at 19:30, on Zulip):

@centril I'm not even sure we're really using WellFormed(Type) according to the standard terminology signification, do we?

Alexander Regueiro (Jan 22 2019 at 19:30, on Zulip):

^^

centril (Jan 22 2019 at 19:31, on Zulip):

@scalexm not sure either... but I can read a wadler paper and... ;)

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

@centril that's not what we're talking about here though I think

centril (Jan 22 2019 at 19:31, on Zulip):

σ type meaning "σ is well-formed"

scalexm (Jan 22 2019 at 19:31, on Zulip):

basically WF rules are something like:

struct S<T> where T: Debug { }
WellFormed(S<T>) :- Implemented(T: Debug)
scalexm (Jan 22 2019 at 19:31, on Zulip):

so I don't even know if there is a connection to type theory or whatever (not my field of knowledge at all lol)

centril (Jan 22 2019 at 19:32, on Zulip):

I recommend reading https://homepages.inf.ed.ac.uk/wadler/papers/quantcc/quantcc.pdf

Alexander Regueiro (Jan 22 2019 at 19:32, on Zulip):

I would say "the type S<T> has a witness"

Alexander Regueiro (Jan 22 2019 at 19:33, on Zulip):

or "has a type instance", maybe better

tmandry (Jan 22 2019 at 19:33, on Zulip):

FWIW I find "legal" fairly intuitive

Alexander Regueiro (Jan 22 2019 at 19:33, on Zulip):

"legal" doesn't work for me, because it looks legal at first sight, it just happens not to have an instance.

Alexander Regueiro (Jan 22 2019 at 19:33, on Zulip):

i.e. it's empty

scalexm (Jan 22 2019 at 19:33, on Zulip):

@tmandry I think "legal" for type/trait/impl declarations is good indeed

scalexm (Jan 22 2019 at 19:34, on Zulip):

@Alexander Regueiro we're talking about declarations here, e.g. "is this impl block I wrote legal"

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

so maybe NonEmpty works, unless I'm misunderstanding?

centril (Jan 22 2019 at 19:34, on Zulip):

legal is a synonym for well-formed... you haven't changed anything ;)

nikomatsakis (Jan 22 2019 at 19:34, on Zulip):

I think legal is good for the goals that declare whether a declaration is accepted or whether an error is reported.

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

@scalexm concrete example?

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

that's not what I was talking about

scalexm (Jan 22 2019 at 19:35, on Zulip):

@Alexander Regueiro

trait Foo: Copy { }

impl Foo for String {
// This impl is not legal
}
scalexm (Jan 22 2019 at 19:35, on Zulip):

today we say "this impl is not WF", which I agree is confusing :p

scalexm (Jan 22 2019 at 19:35, on Zulip):

because we already use WellFormed for so many things

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

ohh that's something else entirely

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

I think we're talking about two different things here

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

and not just me

nikomatsakis (Jan 22 2019 at 19:35, on Zulip):

yes, that's the point :)

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

sorry guys

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

I agree "legal" is good for that case :-)

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

better than "well-formed"

nikomatsakis (Jan 22 2019 at 19:36, on Zulip):

heh, not just you that is confused, never fear =)

scalexm (Jan 22 2019 at 19:36, on Zulip):

@Alexander Regueiro that's ok, at least we now see how confusing all these WellFormed everywhere are lol

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

yep!

nikomatsakis (Jan 22 2019 at 19:36, on Zulip):

so, to bring it back a bit to trait objects:

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

so my vote is "witnessed" or "instantiated" for the first meaning, and "legal" for that meaning... but do we have a consensus already?

nikomatsakis (Jan 22 2019 at 19:37, on Zulip):

I do not like either witnessed or instantiated :)

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

okay

nikomatsakis (Jan 22 2019 at 19:37, on Zulip):

but I'd rather we discuss that particular bikeshed later :)

nikomatsakis (Jan 22 2019 at 19:37, on Zulip):

I also don't like well-formed, mind you :)

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

In addition to checking the well-formedness of the method type,we ensure that the class context(C1,...,Cn)is also well-formed,extending the environment with the local variablea. In turn, thisimplies thatfv(Ci)⊆ {a}, in line with the Haskell standard.

Type & Constraint Well-ScopednessThe judgments for well-scopeness of types, constraints and axiom sets are denotedΓ⊢tyσ,Γ⊢ctCandΓ⊢axArespectively. Their definitions are straightforwardand can be found in Appendix A.

We check the well-formedness of the instance contextAun-der the extended typing environment, and that each superclassconstraintCiis entailed by the instance context.

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

fair. we'll leave that later

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

so... well-formed is standard.

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

@centril Wadler isn't the oracle though, you know. ;-)

centril (Jan 22 2019 at 19:38, on Zulip):

He is, he invented this stuff we are talking about... =P

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

and standard doesn't mean good... though it does mean standard. anyway, we should weigh that against the fact most people who work on the compiler aren't type theorists

centril (Jan 22 2019 at 19:38, on Zulip):

(anyways...)

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

I sincerely doubt it. This stuff has been around forever.

nikomatsakis (Jan 22 2019 at 19:38, on Zulip):

ok, off topic :)

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

yep

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

back to Niko... next topic?

nikomatsakis (Jan 22 2019 at 19:39, on Zulip):

so @scalexm it seems like the "trait object implied bounds" is another key part

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

I think the confusion arises from not being clear about what WF is with respect to... e.g. WF type, WF environment, WF super-trait constrants, ...

nikomatsakis (Jan 22 2019 at 19:39, on Zulip):

but if I'm not mistaken, I don't see the FromEnv rules in your writeup... I must have missed them

scalexm (Jan 22 2019 at 19:40, on Zulip):

@nikomatsakis it's one very small paragraph I think

nikomatsakis (Jan 22 2019 at 19:40, on Zulip):

oh, I see

nikomatsakis (Jan 22 2019 at 19:41, on Zulip):
FromEnv(dyn Foo<T1...Tk>: Foo<T1...Tk>) :- FromEnv(dyn Foo<T1...Tk>)
scalexm (Jan 22 2019 at 19:43, on Zulip):

(btw if someone wants to know what FromEnv means and basically how implied bounds are supposed to work in the new style trait solver, I wrote a lot of things in the rustc guide, feedback on the understandability of what I wrote is welcome)

nikomatsakis (Jan 22 2019 at 19:44, on Zulip):

I was just re-reading some of that indeed

nikomatsakis (Jan 22 2019 at 19:44, on Zulip):

to bring it back in cache

centril (Jan 22 2019 at 19:45, on Zulip):

if I read that literally... then it says "if from the environment, we can assume dyn Foo<T1...Tk> is ????, we can prove that dyn Foo<T1...Tk>: Foo<T1...Tk> is ????"

tmandry (Jan 22 2019 at 19:46, on Zulip):

???? = legal?

scalexm (Jan 22 2019 at 19:46, on Zulip):

@centril seems like that yeah

centril (Jan 22 2019 at 19:46, on Zulip):

valid = WF ?

tmandry (Jan 22 2019 at 19:46, on Zulip):

oh gosh sorry

tmandry (Jan 22 2019 at 19:47, on Zulip):

I meant "legal"

nikomatsakis (Jan 22 2019 at 19:48, on Zulip):

to summarize, I guess:

Applied to this particular case, we are saying that dyn Foo has sort of implied "where clauses":

tmandry (Jan 22 2019 at 19:49, on Zulip):

actually, when we do WF checking in chalk (where we produce and check WF goals), is that meaning of WF also covered by "legal"?

scalexm (Jan 22 2019 at 19:50, on Zulip):

@tmandry in chalk, src/rules/wf.rs is where we check if trait/type/impl declarations are legal

nikomatsakis (Jan 22 2019 at 19:51, on Zulip):

I am thinking about a few things:

scalexm (Jan 22 2019 at 19:51, on Zulip):

@tmandry and proving that something is legal ends up generating WellFormed(...) goals :)

tmandry (Jan 22 2019 at 19:52, on Zulip):

@scalexm ok. so to clarify, have we decided to rename the WellFormed(...) goal, or not?

scalexm (Jan 22 2019 at 19:52, on Zulip):

@tmandry not yet

scalexm (Jan 22 2019 at 19:53, on Zulip):

@tmandry but we may decide to rename to "legality checking" the process that is happening in e.g. src/rules/wf.rs in chalk

tmandry (Jan 22 2019 at 19:53, on Zulip):

okay, thanks, makes sense now.

nikomatsakis (Jan 22 2019 at 19:53, on Zulip):

ok. so to clarify, have we decided to rename the WellFormed(...) goal, or not?

I think we have decided to rename it, but not what to rename it to

nikomatsakis (Jan 22 2019 at 19:54, on Zulip):

also, there are really two distinct goals (WellFormed(Ty) and WellFormed(TraitReference)) and likely they should not have the same name

centril (Jan 22 2019 at 19:54, on Zulip):

I'd write WFType(...), WFConstraint(...), WFOtherThing(...)

centril (Jan 22 2019 at 19:54, on Zulip):

to make it clear what sort of well-formedness we're talking about

nikomatsakis (Jan 22 2019 at 19:54, on Zulip):

(sure)

scalexm (Jan 22 2019 at 19:55, on Zulip):

we can spin-off a new channel for bike-shedding

nikomatsakis (Jan 22 2019 at 19:55, on Zulip):

I'm feeling a desire @scalexm to try and draw up a kind of diagram for implied bounds

nikomatsakis (Jan 22 2019 at 19:55, on Zulip):

(and object types, to some extent)

nikomatsakis (Jan 22 2019 at 19:55, on Zulip):

trying to show "this thing can be assumed to be true" because "so and so proves it here"

nikomatsakis (Jan 22 2019 at 19:56, on Zulip):

anyway, I probably gotta go, but this was definitely helpful. Re: naming, a separate topic sounds like a good idea

scalexm (Jan 22 2019 at 19:57, on Zulip):

@nikomatsakis I see

scalexm (Jan 22 2019 at 19:57, on Zulip):

that may help indeed, although I'm not sure what said diagram would look like

nikomatsakis (Jan 22 2019 at 19:58, on Zulip):

me either :)

nikomatsakis (Jan 22 2019 at 19:59, on Zulip):

it may prove hard to do

nikomatsakis (Jan 22 2019 at 19:59, on Zulip):

I spun out the "bikeshedding well formed" topic btw

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

@scalexm just to check, the writeup in the rustc guide suggests that when lowering a struct declaration like

struct Foo<T: Eq> { ... }

we would make a rule:

forall<T> {
  WellFormed(Foo<T>) :- Implemented(T: Eq)
}

but actually it's a tad unclear to me, because we write WellFormed(Type<P1..Pn>) :- WC (I guess that here when we "paste in" WC we map to Implemented, right?)

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

(in particular I was wondering if we needed the stronger WellFormed(T: Eq))

scalexm (Jan 22 2019 at 20:02, on Zulip):

@nikomatsakis we need it

scalexm (Jan 22 2019 at 20:02, on Zulip):

Because of the flaw indeed

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

yes ok I see

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

well that is mildly gratifying, in that my "intuition" was that we likely wanted it, but I can't honestly say why :)

scalexm (Jan 22 2019 at 20:04, on Zulip):

It was just an « optimization » at first, but turns out it was wrong

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

Thanks @scalexm for the writeup btw =) :heart:

Last update: Nov 12 2019 at 17:00UTC