cool beans

Author: lcnr

src/trait-bounds.md

@@ -44,67 +44,64 @@ certain common cases:
   `trait A { type B: Copy; }` is equivalent to
   `trait A where Self::B: Copy { type B; }`.
 
+r[bound.global]
+
+A bound which does not use the item's parameters or any higher-ranked lifetimes are considered global.
+
+An error is emitted if a global bound cannot be satisfied in an empty environment.
+
 r[bound.satisfaction]
-Bounds on an item must be satisfied when using the item. When type checking and
-borrow checking a generic item, the bounds can be used to determine that a
-trait is implemented for a type. For example, given `Ty: Trait`
 
-* In the body of a generic function, methods from `Trait` can be called on `Ty`
-  values. Likewise associated constants on the `Trait` can be used.
-* Associated types from `Trait` can be used.
-* Generic functions and types with a `T: Trait` bounds can be used with `Ty`
-  being used for `T`.
+The bounds of an item must be satisfied when using that item.
 
-```rust
-# type Surface = i32;
-trait Shape {
-    fn draw(&self, surface: Surface);
-    fn name() -> &'static str;
-}
+r[bound.satisfaction.impl]
 
-fn draw_twice<T: Shape>(surface: Surface, sh: T) {
-    sh.draw(surface);           // Can call method because T: Shape
-    sh.draw(surface);
-}
+- a trait bound can be satisfied by using an implementation of that trait
+- an impl is applicable if, after instantiating its generic parameters with inference variables
+    - TODO: how to talk about "instantiate with infer vars"...
+    - the self type and trait arguments are equal to the trait bound,
+    - the where-bounds of the impl can be recursively satisfied
 
-fn copy_and_draw_twice<T: Copy>(surface: Surface, sh: T) where T: Shape {
-    let shape_copy = sh;        // doesn't move sh because T: Copy
-    draw_twice(surface, sh);    // Can use generic function because T: Shape
-}
+[bound.satisfaction.impl.builtin]
 
-struct Figure<S: Shape>(S, S);
+There exists impls which are automatically generated by the compiler.
 
-fn name_figure<U: Shape>(
-    figure: Figure<U>,          // Type Figure<U> is well-formed because U: Shape
-) {
-    println!(
-        "Figure of two {}",
-        U::name(),              // Can use associated function
-    );
-}
-```
+- `Sized`,`Copy`, `Clone`,...
 
-r[bound.trivial]
-Bounds that don't use the item's parameters or [higher-ranked lifetimes] are checked when the item is defined.
-It is an error for such a bound to be false.
-
-r[bound.special]
-[`Copy`], [`Clone`], and [`Sized`] bounds are also checked for certain generic types when using the item, even if the use does not provide a concrete type.
-It is an error to have `Copy` or `Clone` as a bound on a mutable reference, [trait object], or [slice].
-It is an error to have `Sized` as a bound on a trait object or slice.
-
-```rust,compile_fail
-struct A<'a, T>
-where
-    i32: Default,           // Allowed, but not useful
-    i32: Iterator,          // Error: `i32` is not an iterator
-    &'a mut T: Copy,        // (at use) Error: the trait bound is not satisfied
-    [T]: Sized,             // (at use) Error: size cannot be known at compilation
-{
-    f: &'a T,
-}
-struct UsesA<'a, T>(A<'a, T>);
-```
+
+- alternative: mention this in item-kind impl
+
+[bound.satisfaction.impl.builtin.trait-object]
+
+Trait objects implement their trait if TODO: lookup conditions, something something project bounds make sense
+
+[bound.satisfaction.bounds]
+
+While inside of a generic item, trait bounds can be satisfied by using the where-bounds of the current item as the item is able to assume that its bounds are satisfied. For this, higher-ranked where-bounds can be instantiated with inference variables. The where-bound is then equated with the trait bound that needs to be satisfied.
+
+[bound.satisfaction.alias-bounds]
+
+- if an alias cannot be normalized in the current environment, trait bounds using this alias as a self type can be proven by using its item bounds
+- TODO: alias bounds from nested self-types github.com/rust-lang/rust/pull/120752
+
+
+[bound.satisfaction.candidate-preference]
+
+> This is purely descriptive. Candidate preference behavior may change in future releases and must not be relied upon for correctness or soundness.
+
+If there are multiple ways to satisfy a trait bound, some groups of candidate are preferred over others. In case a single group has multiple different candidates, the bound remains ambiguous. Candidate preference has the following order
+- builtin implementations of `Sized`
+- if there are any non-global where-bounds, all where-bounds
+- alias-bounds
+- impls
+    - In case the goal trait bound does not contain any inference variables, we prefer builtin trait object impls over user-written impls. TODO: that's unsound jank
+- global where-bounds (only relevant if it does not hold)
+
+> note: this candidate preference can result in incorrect errors and type mismatches, e.g. ...
+
+[bound.satisfaction.cycles]
+
+In case satisfying a bound requires recursively satisfying the same bound, we've encountered a *cycle*. TODO: terminology is iffy here .... can just drop this again
 
 r[bound.trait-object]
 Trait and lifetime bounds are also used to name [trait objects].

src/types.md

@@ -150,6 +150,17 @@ enum List<T> {
 let a: List<i32> = List::Cons(7, Box::new(List::Cons(13, Box::new(List::Nil))));
 ```
 
+## Equality of types
+
+Equality and subtyping of types is generally structural. If the outermost type constructors are the same,
+the fields are pairwise related. The only exceptions from this rule are higher ranked types and alias types
+
+higher ranked types:
+uwu, instantiate binder with placeholders, eq
+
+aliases
+normalized to a rigid type, then equated as normal
+
 [Array]: types/array.md
 [Boolean]: types/boolean.md
 [Closures]: types/closure.md

src/types/alias-types.md

@@ -0,0 +1,34 @@
+r[type.alias]
+
+- associated types
+- opaque types
+    - link from "impl-trait type" to this or param
+
+r[type.alias.rigid]
+
+Aliases might be treated as rigid in their current environment. In this case they behave like other rigid types.
+
+r[type.alias.normalization]
+
+Alias types can be normalized to their underlying type.
+- for associated types this is the type provided by the corresponding impl
+- opaque types
+
+r[type.alias.normalization.assoc-type]
+
+Similar to how trait bounds get satisfied, associated types can be normalized via
+multiple different candidates
+
+- impl (also builtin)
+- projection bound in the environment TODO: where do we talk about them
+- alias bound of their self type
+
+candidate preference:
+- normalizing an alias relies on the candidate group used to prove their corresponding trait bound
+- if corresponding trait bound has been proven via a where-bound or an alias-bound, we do not consider impls
+    - if there is no remaining candidate, the associated type is rigid
+
+For all applicable candidates we
+- prefer where-bounds
+- then alias bounds
+- then impls