high-level rustc-guide docs on chalk-integration

[nikomatsakis]

The existing rustc-guide docs need some organization and love. Let's start with a high-level overview on the various moving parts and their relationship to one another.

[sunjay]

Hello! I am available to help work on this! 😄

[tmandry]

Here are some topics we could cover in a high-level overview...

• what is trait solving? which things does it do, which things does it not?
• introduce trait solving goals in terms of logical (prose) statements
• introduce queries, what they are used for

Basically, cover the motivation and most basic concepts in the introduction, and the further chapters can flesh out those ideas in much greater detail (like they already do).

Glossary terms: (many of these may link back to a page with more details)

• canonical type
• inference variable
• bound type
• bound variable
• environment
• clause
• program clause
• goal
• domain goal
• universe
• placeholder

As @nikomatsakis was saying, we may want to hop on a call to talk it over soon.

[sunjay]

Thanks for writing that up! These are great things to cover!

what is trait solving? which things does it do, which things does it not?

This is somewhat covered here:
https://rust-lang-nursery.github.io/rustc-guide/traits/resolution.html

introduce trait solving goals in terms of logical (prose) statements

We somewhat do this here, though not as much in prose:
https://rust-lang-nursery.github.io/rustc-guide/traits/lowering-to-logic.html

introduce queries, what they are used for

I actually don't think we do this! Which is somewhat surprising given how fundamental it is. Great idea!

Glossary terms:

I definitely think these need to be defined. All of these are fundamental to understanding the way we communicate about chalk.

high-level rustc-guide docs on chalk-integration

This is the issue title. Are we focusing on docs about chalk itself and its concepts, or about documenting the way that chalk is being integrated into the compiler so more people can contribute to it?

[tmandry]

Regarding where things are already covered, I did see those (thanks for adding pointers). IMHO one problem right now is that most of the knowledge is there, but split up in a way that it's hard to grasp the big picture. I think it makes sense to put them all together in a single introduction at a very high level of abstraction (hence my emphasis on prose – but I could be convinced otherwise).

The old-style traits is eventually going away, so I personally think it's okay to repeat some stuff from there.

Good point re: issue title! I may have misunderstood the original goal. In any case, those are my thoughts on how to better cover chalk concepts 😄

[nikomatsakis]

introduce queries, what they are used for

By this, do you mean the compiler's queries, or "trait queries"? The compiler's query system is introduced here:

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

I think that the intended interaction between the compiler query system and the chalk trait engine is something we should talk through and document. To some extent, it's a work-in-progress =)

[tmandry]

By this, do you mean the compiler's queries, or "trait queries"?

Yes, trait queries is what I meant.

On second thought, there should really be a focus on any “public” API (query or otherwise) that other parts of the compiler can use. IME, knowing exactly what the boundaries of a component are is just as important for understanding as knowing what’s in it.

[tmandry]

I just posted a PR to do some light editing and refactoring of the traits chapter: rust-lang/rustc-dev-guide#219

[tmandry]

Okay, I put together a list of all the tasks I can think of. Some of these are quite simple, as they're just moving content around or copying it from @nikomatsakis blog posts :)

If you want to work on something, simply edit this comment and put your name at the end of the line.

• WF Checking — @scalexm (Write well-formedness checking chapter rustc-dev-guide#222)
• SLG Solver (see this blog post) – @tmandry (Add traits SLG solver section rustc-dev-guide#228)
  • I think this could be easily done by copying from the blog post, perhaps with light edits and/or additions for context
• Context trait: see this paper doc
  • this could be part of the SLG section
• Unification: see blog1, blog2
• FInd a home for Universes (currently documented under region inference)
• Coherence (please add pointers if you have them!)
• Chalk Overview additions – @tmandry (Update chalk overview rustc-dev-guide#223)
  • add new module structure
  • add “elaborate test harness” concept which @nikomatsakis always uses to describe chalk
• Glossary: see chalk glossary, this comment
• The lowering module in rustc
  • add info about how rules are represented, e.g. Normalize, with links to code

---

I think it helps to know what we're shooting for. Here's a strawman for the eventual structure. Please let me know what you think!

0. Intro
1. Lowering to logic
   i. Goals and clauses
   ii. Equality and associated types
   iii. Implied bounds
   iv. Coherence
   v. Region constraints
   vi. The lowering module in rustc
   vii. Lowering rules
   viii. Well-formedness checking
2. Solving logic programs
   i. Unification
   ii. Universes
   iii. Canonicalization (maybe, or part of SLG Solver)
   iv. The SLG Solver (sub-sub-sections: Context trait)
3. Canonical queries (rustc-specific stuff can go here)
4. An Overview of Chalk
5. Glossary
6. Bibliography