|
| 1 | +# Well known traits |
| 2 | + |
| 3 | +For most traits, the question of whether some type T implements the trait is determined by |
| 4 | +looking solely at the impls that exist for the trait. But there are some well-known traits |
| 5 | +where we have "built-in" impls that are never expressly written in the compiler, they are |
| 6 | +built-in to the language itself. In some cases, these impls also encode complex conditions |
| 7 | +that an ordinary impl cannot express. To address this, chalk has a notion of a `WellKnownTrait` |
| 8 | +-- basically, a trait which is inherent to the language and where we will generate custom logic. |
| 9 | + |
| 10 | +As an example, consider the logic for `Sized` in regards to structs: A struct can have |
| 11 | +at most one `!Sized` field, and it must be the last. And the last field isn't `Sized`, |
| 12 | +then neither is the struct itself. |
| 13 | + |
| 14 | +Chalk has two main places that deal with well known trait logic: |
| 15 | +1) [`chalk-solve\clauses\builtin_traits`][builtin_traits_mod], which generates built-in implementations |
| 16 | +for well-known traits. |
| 17 | +2) [well-formedness](wf.md) checks, some of which need to know about well known traits. |
| 18 | + |
| 19 | +[builtin_traits_mod]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/clauses/builtin_traits.rs |
| 20 | + |
| 21 | +# Auto traits |
| 22 | + |
| 23 | +Auto traits, while not exactly well known traits, do also have special logic. |
| 24 | +The idea is that the type implements an auto trait if all data owned by that type implements it, |
| 25 | +with an ability to specifically opt-out or opt-in. Additionally, auto traits are [coinductive][coinductive_section]. |
| 26 | +Some common examples of auto traits are `Send` and `Sync`. |
| 27 | + |
| 28 | +[coinductive_section]: ../engine/logic/coinduction.html#coinduction-and-refinement-strands |
| 29 | + |
| 30 | +# Current state |
| 31 | +| Type | Copy | Clone | Sized | Unsize | Drop | Fn | Unpin | Generator | auto traits | |
| 32 | +| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | |
| 33 | +| tuple types | ✅ | ✅ | ✅ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | |
| 34 | +| structs | ⚬ | ⚬ | ✅ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ✅ | |
| 35 | +| scalar types | 📚 | 📚 | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | |
| 36 | +| trait objects | ⚬ | ⚬ | ⚬ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | |
| 37 | +| functions ptrs | ✅ | ✅ | ✅ | ⚬ | ⚬ | ❌ | ⚬ | ⚬ | ❌ | |
| 38 | +| arrays❌ | ❌ | ❌ | ❌ | ❌ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | |
| 39 | +| slices❌ | ❌ | ❌ | ⚬ | ❌ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | |
| 40 | +| closures❌ | ❌ | ❌ | ❌ | ⚬ | ⚬ | ❌ | ⚬ | ⚬ | ❌ | |
| 41 | +| generators❌ | ⚬ | ⚬ | ❌ | ⚬ | ⚬ | ⚬ | ❌ | ❌ | ❌ | |
| 42 | +| gen. witness❌ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ | |
| 43 | +| ----------- | | | | | | | | | | |
| 44 | +| well-formedness | ✅ | ⚬ | ✅ | ⚬ | ✅ | ⚬ | ⚬ | ⚬ | ⚬ | |
| 45 | + |
| 46 | +legend: |
| 47 | +⚬ - not applicable |
| 48 | +✅ - implemented |
| 49 | +📚 - implementation provided in libcore |
| 50 | +❌ - not implemented |
| 51 | + |
| 52 | +❌ after a type name means that type is not yet in chalk |
0 commit comments