add WellKnownTraits chapter to the book

book/src/SUMMARY.md

@@ -17,6 +17,7 @@
     - [Type equality and unification](./clauses/type_equality.md)
     - [Implied bounds](./clauses/implied_bounds.md)
     - [Lowering rules](./clauses/lowering_rules.md)
+    - [Well known traits](./clauses/well_known_traits.md)
     - [Well-formedness checking](./clauses/wf.md)
 - [Canonical queries](./canonical_queries.md)
     - [Canonicalization](./canonical_queries/canonicalization.md)

book/src/clauses/well_known_traits.md

@@ -0,0 +1,52 @@
+# Well known traits
+
+For most traits, the question of whether some type T implements the trait is determined by 
+looking solely at the impls that exist for the trait. But there are some well-known traits 
+where we have "built-in" impls that are never expressly written in the compiler, they are 
+built-in to the language itself. In some cases, these impls also encode complex conditions
+that an ordinary impl cannot express. To address this, chalk has a notion of a `WellKnownTrait` 
+-- basically, a trait which is inherent to the language and where we will generate custom logic.
+
+As an example, consider the logic for `Sized` in regards to structs: A struct can have
+at most one `!Sized` field, and it must be the last. And the last field isn't `Sized`, 
+then neither is the struct itself. 
+
+Chalk has two main places that deal with well known trait logic:
+1) [`chalk-solve\clauses\builtin_traits`][builtin_traits_mod], which generates built-in implementations
+for well-known traits.
+2) [well-formedness](wf.md) checks, some of which need to know about well known traits.
+
+[builtin_traits_mod]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/clauses/builtin_traits.rs
+
+# Auto traits
+
+Auto traits, while not exactly well known traits, do also have special logic. 
+The idea is that the type implements an auto trait if all data owned by that type implements it, 
+with an ability to specifically opt-out or opt-in. Additionally, auto traits are [coinductive][coinductive_section]. 
+Some common examples of auto traits are `Send` and `Sync`.
+
+[coinductive_section]: ../engine/logic/coinduction.html#coinduction-and-refinement-strands
+
+# Current state 
+| Type            | Copy | Clone | Sized | Unsize | Drop | Fn  | Unpin  | Generator | auto traits |
+| ---             | ---  | ---   | ---   | ---    | ---  | --- | ---    |  ---      |  ---        |
+| tuple types     | ✅    | ✅    | ✅     | ✅     | ⚬    | ⚬  |  ⚬      |  ⚬       |   ❌         |
+| structs         | ⚬    | ⚬    |  ✅    | ✅     | ⚬    | ⚬  |  ⚬      |  ⚬       |   ✅         |
+| scalar types    | 📚    | 📚    | ✅     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |    ❌        |
+| trait objects   | ⚬    | ⚬    | ⚬     |  ✅    | ⚬    | ⚬   | ⚬      |  ⚬       |    ⚬        |
+| functions ptrs  | ✅    | ✅    | ✅     | ⚬     | ⚬    | ❌   | ⚬      |  ⚬       |    ❌         |
+| arrays❌         | ❌     | ❌    | ❌     | ❌      | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌        |
+| slices❌         | ❌     | ❌    | ⚬     | ❌      | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌       |
+| closures❌       | ❌     | ❌    | ❌     | ⚬      | ⚬   | ❌   | ⚬      |  ⚬       |    ❌        |
+| generators❌     |  ⚬    |  ⚬  | ❌     |  ⚬     | ⚬    | ⚬  | ❌      |   ❌       |    ❌       |
+| gen. witness❌   |  ⚬    |   ⚬  |  ⚬   |   ⚬    |  ⚬   |  ⚬ |  ⚬    |   ⚬       |    ❌       |
+| -----------     |       |      |       |        |      |     |        |           |             |
+| well-formedness |  ✅   |  ⚬   | ✅     | ⚬     | ✅    |  ⚬  | ⚬      |  ⚬       |   ⚬         |
+
+legend:  
+⚬ - not applicable  
+✅ - implemented  
+📚 - implementation provided in libcore  
+❌ - not implemented  
+
+❌ after a type name means that type is not yet in chalk