Write well-formedness checking chapter #222

scalexm · 2018-10-29T15:21:03Z

This covers types, traits and trait impls.

cc @nikomatsakis @tmandry

mark-i-m

LGTM. Thanks :)

I left a few nits and comments, but overall it looks good!

src/traits/wf.md

mark-i-m · 2018-10-29T20:52:37Z

Also, travis is failing.

Co-Authored-By: scalexm <[email protected]>

tmandry

Nice! I think this does a very good job of explaining the concepts. It would have been really helpful to have when I was first working on traits.

Added a few readability nits, otherwise looks good to me.

tmandry · 2018-10-30T17:14:01Z

src/traits/wf.md

+}
+```
+
+So where clauses on associated types work *exactly* like where clauses on


I was confused at first because I thought you were talking about WF rules for trait methods (which aren't mentioned here). It might be helpful to say "In Rust, where clauses on associated types work..." to make it clear you're talking about the semantics of Rust itself.

Also consider marking this paragraph as an "aside" with >, to emphasize that you don't need to be familiar with those semantics to understand the rest of the chapter.

tmandry · 2018-10-30T17:18:34Z

src/traits/wf.md

+            forall<P2...> {
+                if (FromEnv(WC_assoc)) {
+                    WellFormed(SomeValue<A3...>: Bounds_assoc) &&
+                        WellFormed(InputTypes(SomeValue<A3...>))


From a quick scan of the below text, I'm confused why this doesn't have WellFormed(InputTypes(WC_assoc)) as in the other goals.

There is indeed something missing but not exactly what you’re pointing :)

I stated that you could assume that the receiver type and its input types are well-formed.

This is correct but not complete: actually you can assume FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>)). We can do that because everywhere else we check that all types appearing in where clauses are WF. This is what we currently do in chalk, I just forgot about it.

Then, we already checked WC_assoc in the trait decl. In the impl, they are basically repeated, except that we substituted type parameters from the trait with the values provided by the impl, that is A1.... But since we already assume that the A1... are WF, no need to check again.

Then, we already checked WC_assoc in the trait decl. In the impl, they are basically repeated, except that we substituted type parameters from the trait with the values provided by the impl, that is A1.... But since we already assume that the A1... are WF, no need to check again.

Yeah, on second thought this seems clear, though it may be worth saying. Also, the text might want to mention (in the paragraph above) where the WC_assoc is verified to be equivalent to the trait decl. i.e. is it during lowering in chalk?

In chalk we have an easy solution for that: we just don’t write where clauses on associated type values, they are like auto-repeated from the trait :)

I don’t know yet where we’ll do that in rustc, especially because if we want to really mimic where clauses on trait methods, then it’s a bit more complex than just « omit it or write it »: on trait methods, you can actually write "new" where clauses provided that they are weaker than (= implied by) the original ones, for example you can do that:

trait Foo { fn foo<T> where T: Copy; } impl Foo for i32 { fn foo<T> where T: Clone { ... } }

Of course this is useless from a semantic POV, it just serves as a documentation that you are not using the full power of the original where clause. But to check that the where clauses you wrote are indeed weaker, you’d need to use the trait solver of course. So I decided to juste sidestep this in the text as this is anecdotic I think.

I think the idea would be that -- to prove the impl is well-formed -- we have to prove that the where-clauses from the trait imply the where-clauses from the impl. i.e., assuming the where-clauses from the trait hold, we show we can prove the where-clauses from the impl -- but I agree it can wait to be added.

tmandry · 2018-10-30T18:49:38Z

src/traits/wf.md

+`WellFormed(SomeType<A2...>: Trait<A1...>)` hold. That is, we want to prove
+that `SomeType<A2...>` verify all the where clauses that might transitively
+come from the `Trait` definition (see
+[this subsection](./implied-bounds.md#co-inductiveness-of-wellformed)).


This seems to skip over the WellFormed(InputTypes(WC_impl)) part.

Actually I was trying to factor out all the WellFormed(InputTypes(...)) in the previous paragraph (« assuming that the various where clauses hold, we prove that every type appearing in the impl is WF»)

Oh, I missed that, sorry. Maybe update the goal clauses to match the order that they are mentioned in the text?

Also, it does say something to the effect of "assuming that the various where clauses hold" twice, this might be slightly confusing.

Yeah I think when writing that paragraph I wasn’t entierely convinced by my formulation either :)

I’ll separate the if goals in two parts yes, it should be clearer.

tmandry · 2018-10-30T18:53:47Z

src/traits/wf.md

+Lastly, assuming that the where clauses on the associated type `WC_assoc` hold,
+we prove that `WellFormed(SomeValue<A3...>: Bounds_assoc)` hold. Again, we are
+not only proving `Implemented(SomeValue<A3...>: Bounds_assoc)`, but also
+all the facts that might transitively come from `Bounds_assoc`. This is because


Suggested change

all the facts that might transitively come from `Bounds_assoc`. This is because

all the facts that might transitively come from `Bounds_assoc` using only the

where clauses in scope. We must do this because

Mmh so we’re not only using the where clauses in fact, we can also rely on the various program clauses that don’t come from the environment but rather from the other impls,

Good point.

src/traits/wf.md

scalexm · 2018-10-30T20:14:53Z

@tmandry Thanks, I’ll fix what we discussed in the comments soon (on my phone now).

Co-Authored-By: scalexm <[email protected]>

scalexm · 2018-10-30T21:17:09Z

Ok @tmandry should be good now. Just waiting for @nikomatsakis to proofread it and we should be ok.

nikomatsakis

This all seems like a great start. I left some nits. I think we will wind up iterating but I'd prefer to land the text and refine over time.

nikomatsakis · 2018-11-02T20:10:39Z

src/traits/wf.md


+The new-style WF checking has not been implemented in rustc yet.
+
+[wf]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf.rs


Maybe we should link to the chalk rustdocs at http://rust-lang-nursery.github.io/chalk/doc/chalk/rules/wf/index.html instead? Not sure.

I think that the code is still a good documentation for that chapter as there are multiple subtle things happening.

nikomatsakis · 2018-11-02T20:11:20Z

src/traits/wf.md

+lowering rules, we'll introduce another notation: when checking WF of a
+declaration, we'll often have to prove that all types that appear are
+well-formed, except type parameters that we always assume to be WF. Hence,
+we'll use the following notation: for a type `SomeType<...>`, we denote


Nit: Instead of "we denote" maybe "we define InputTypes(SomeType<..>) to be the set of all non-parameter types..."

nikomatsakis · 2018-11-02T20:13:21Z

src/traits/wf.md

+* `InputTypes(Box<T>) = [Box<T>]`
+* `InputTypes(Box<Box<T>>) = [Box<T>, Box<Box<T>>]`
+
+We may naturally extend the `InputTypes` notation to where clauses, for example


Nit: "We also extend the InputTypes notation to where clauses in the natural way. So, for example, InputTypes(A0: ...)..."

nikomatsakis · 2018-11-02T20:14:12Z

src/traits/wf.md

+}
+```
+
+we generate the following goal:


Nit: we generate the following goal, which represents its well-formedness condition:

nikomatsakis · 2018-11-02T20:14:42Z

src/traits/wf.md

+
+Examples:
+* `InputTypes((u32, f32)) = [u32, f32, (u32, f32)]`
+* `InputTypes(Box<T>) = [Box<T>]`


I would add something like ", assuming that T is a type parameter"

Remind me btw why we pushed the "expansion" into the lowering step, versus defining a proper WellFormed(T) goal? (And then having struct Box<T> get to assume that WellFormed(T) in its "environment"?)

nikomatsakis · 2018-11-02T20:16:54Z

src/traits/wf.md

+}
+```
+
+which in English gives: assuming that the where clauses defined on the type


s/gives/states/

nikomatsakis · 2018-11-02T20:25:44Z

src/traits/wf.md

+the input types of `SomeType<A2...>` are well-formed, we prove that
+`WellFormed(SomeType<A2...>: Trait<A1...>)` hold. That is, we want to prove
+that `SomeType<A2...>` verify all the where clauses that might transitively
+come from the `Trait` definition (see


Nit: s/come/be required by/

scalexm added 2 commits October 29, 2018 14:38

Write well-formedness checking chapter

462b7c3

Add some examples for impls

b5dff2e

tmandry mentioned this pull request Oct 29, 2018

high-level rustc-guide docs on chalk-integration rust-lang/rust#55100

Closed

Fix code blocks

8365209

mark-i-m suggested changes Oct 29, 2018

View reviewed changes

Fix a few things

e20f283

Co-Authored-By: scalexm <[email protected]>

scalexm force-pushed the wf branch from 6d9f58f to e20f283 Compare October 29, 2018 21:44

tmandry requested changes Oct 30, 2018

View reviewed changes

scalexm force-pushed the wf branch from 432728a to cd92235 Compare October 30, 2018 21:13

Fix a few more things

fe9dc61

Co-Authored-By: scalexm <[email protected]>

scalexm force-pushed the wf branch from cd92235 to fe9dc61 Compare October 30, 2018 21:15

mark-i-m approved these changes Oct 30, 2018

View reviewed changes

tmandry approved these changes Oct 30, 2018

View reviewed changes

nikomatsakis approved these changes Nov 2, 2018

View reviewed changes

Fix nits

cbb021e

nikomatsakis merged commit 505c99f into rust-lang:master Nov 3, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Write well-formedness checking chapter #222

Write well-formedness checking chapter #222

scalexm commented Oct 29, 2018

mark-i-m left a comment

mark-i-m commented Oct 29, 2018

tmandry left a comment

tmandry Oct 30, 2018

tmandry Oct 30, 2018

scalexm Oct 30, 2018

tmandry Oct 30, 2018 •

edited

Loading

scalexm Oct 30, 2018

nikomatsakis Nov 2, 2018

tmandry Oct 30, 2018

scalexm Oct 30, 2018

tmandry Oct 30, 2018

scalexm Oct 30, 2018

tmandry Oct 30, 2018

scalexm Oct 30, 2018

tmandry Oct 30, 2018

scalexm commented Oct 30, 2018

scalexm commented Oct 30, 2018

nikomatsakis left a comment

nikomatsakis Nov 2, 2018

scalexm Nov 2, 2018

nikomatsakis Nov 2, 2018

nikomatsakis Nov 2, 2018

nikomatsakis Nov 2, 2018

nikomatsakis Nov 2, 2018

nikomatsakis Nov 2, 2018

nikomatsakis Nov 2, 2018

nikomatsakis Nov 2, 2018

	all the facts that might transitively come from `Bounds_assoc`. This is because
	all the facts that might transitively come from `Bounds_assoc` using only the
	where clauses in scope. We must do this because


		The new-style WF checking has not been implemented in rustc yet.

		[wf]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf.rs

Write well-formedness checking chapter #222

Write well-formedness checking chapter #222

Conversation

scalexm commented Oct 29, 2018

mark-i-m left a comment

Choose a reason for hiding this comment

mark-i-m commented Oct 29, 2018

tmandry left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tmandry Oct 30, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

scalexm commented Oct 30, 2018

scalexm commented Oct 30, 2018

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tmandry Oct 30, 2018 •

edited

Loading