Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions src/items/generics.md
Original file line number Diff line number Diff line change
Expand Up @@ -310,6 +310,12 @@ struct Foo<#[my_flexible_clone(unbounded)] H> {
}
```

r[items.generics.instantiation]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This section feels hard :/

Do we define "instantiation" anywhere? I feel like could just be worded as

When using an item all occurrences of the its generics parameters are replaced with either the explicitly provided argument or a new inference variable.

Though, this is very imprecise, and kind of overlaps with other statements (e.g. items.fn.generics.mono).

(Quite note, but " with either the explicitly provided argument" isn't quite right? We substitute with all new inference variables, but some are later unified with known arguments? Certainly, there's a semantic identity and I think it's more clear to talk about it this way. I bring it up because I'll use it below.)

I almost kind of would expect a bit more of a baseline definition - what is monomorphization and that all generics must be defined for monomorphization to occur. Then, discuss how this happens: substitution. And for that, I would like go more technical (and, my example doesn't quite align with the technical wording we use elsewhere, but I imagine we want to it, just giving a rough example):

For an item with generic parameters `<P0..Pn>`, we define a _substitution_ `[S0, ..., Sn]` consisting of a new inference variable for each generic parameter. Then, occurrences of each parameter are substituted with the variable defined in the substitution: `P0 => S0, ..., Pn => Sn`.

Explicitly provided arguments are unified with their respective inference variables. 

When using an item its generic parameters have to get instantiated. This replaces all occurances of the parameter with either the explicitly provided argument or a new inference variable.

Instantiating the generic parameters of an item generally requires proving its where clauses.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Likely, the word "generally" here will want to be elaborated here - or the statement should be changed around a bit.

I could imagine us wanting to change this around a bit - focusing instead of what we want to ensure happens by proving its where clauses. I.e. what are the invariants we want to hold by proving its where clauses. Where clause solving during impl selection is also probably a specific thing we want to call out.



[array repeat expression]: ../expressions/array-expr.md
[arrays]: ../types/array.md
[slices]: ../types/slice.md
Expand Down
115 changes: 68 additions & 47 deletions src/trait-bounds.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,68 +44,89 @@ certain common cases:
`trait A { type B: Copy; }` is equivalent to
`trait A where Self::B: Copy { type B; }`.

r[bound.global]

Bounds 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.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd probably reword this like:

"Global bounds must be satisfiable without relying on any where clauses."


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.

r[bound.satisfaction.impl]

A trait bound can be satisfied by using an implementation of that trait. An implementation is applicable if,
after instantiating its generic parameters with new inference variables, the self type and trait arguments are
equal to the trait bound and the where-bounds of the impl can be recursively satisfied.

r[bound.satisfaction.impl.builtin]

There exist impls which are automatically generated by the compiler.

- `Sized`,`Copy`, `Clone`,...


- alternative: mention this in item-kind impl

r[bound.satisfaction.impl.builtin.trait-object]

Trait objects implement their trait if TODO: lookup conditions, something something project bounds make sense

r[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.

r[bound.satisfaction.alias-bounds]

If an alias type is rigid in the current environment, trait bounds using this alias as a self type can be satisfied by using its item bounds.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, these are some of the code examples I had mentioned above. Would probably want to see this discussed outside of a "when an alias is rigid" example.


```rust
# type Surface = i32;
trait Shape {
fn draw(&self, surface: Surface);
fn name() -> &'static str;
trait Trait {
type Assoc: Clone;
}

fn draw_twice<T: Shape>(surface: Surface, sh: T) {
sh.draw(surface); // Can call method because T: Shape
sh.draw(surface);
fn foo<T: Trait>(x: &T::Assoc) -> T::Assoc {
// The where-bound `T::Assoc: Clone` is satisfied using the `Clone` item-bound.
x.clone()
}
```

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
}
r[bound.satisfaction.alias-bounds.nested]

struct Figure<S: Shape>(S, S);
We also consider the item bounds of the self type of aliases to satisfy trait bounds.

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
);
```rust
trait Trait {
type Assoc: Iterator
where
<Self::Assoc as Iterator>::Item: Clone;
// equivalent to
// type Assoc: Iterator<Item: 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,
fn item_is_clone<T: Trait>(iter: T::Assoc) {
for item in iter {
let _ = item.clone();
}
}
struct UsesA<'a, T>(A<'a, T>);
```


r[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.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, great! Probably should just link the other section to this, then split this across aliases and trait bounds.


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. ...

r[bound.trait-object]
Trait and lifetime bounds are also used to name [trait objects].

Expand Down
25 changes: 25 additions & 0 deletions src/types.md
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,31 @@ enum List<T> {
let a: List<i32> = List::Cons(7, Box::new(List::Cons(13, Box::new(List::Nil))));
```

## Equality of types

r[types.equality]

Equality and subtyping of types is generally structural; if the outermost type constructors are the same,
their corresponding generic arguments are pairwise compared. We say types with this equality behavior are *rigid*. The only exceptions from this rule are higher ranked types and alias types.
Comment on lines +157 to +158
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, okay, this is sort of what I meant in a previous comment on wanting to see this split out.

I'd probably just rephrase this as:

Two types are structurally equal if the following conditions are met:
- their type constructors are the same
- each generic parameter are pair-wise structurally equal

(q: is this second point too strong - do we structurally equate parameters, or do general equality?)

We say types with this equality behavior are rigid.

Kind of weird use of this terminology, but I guess not incorrect. It's pretty confusing that we refer to this as both "rigid" and "structural". We should probably decide on the precise definitions of these as a team.

The only exceptions from this rule are higher ranked types and alias types.

This probably deserves to be in an "intro" paragraph (and leave the definition of structural equality as it's own paragraph.


r[types.equality.rigid]

r[types.equality.aliases]

Aliases are compared by first normalizing them to a *rigid* type and then equating their type constructors and recursing into their generic arguments.

r[types.equality.higher-ranked]

Function pointers and trait objects may be higher-ranked.

r[types.equality.higher-ranked.sub]

Subtyping is checked by instantiating the `for` of the subtype with inference variables and the `for` of the supertype with placeholders before relating them as normal.

r[types.equality.higher-ranked.eq]

Equality is checked by both instantiating the `for` of the lhs with inference variables and the `for` of the rhs with placeholders before equating them, and also doing the opposite.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we define "placeholders" anywhere? I'm really afraid that these are kind of "just" words without a lot of "meaning" of what someone unfamiliar without the specifics of how our type system works would understand.


[Array]: types/array.md
[Boolean]: types/boolean.md
[Closures]: types/closure.md
Expand Down
35 changes: 35 additions & 0 deletions src/types/alias-types.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
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 types.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Definitely need to define what qualifies an alias as rigid, and what it means to "behave like other types"

Their equality is structural, *rigid* aliases are only equal if both have the same type constructor and equal corresponding arguments.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess that second part is this. Wording here is a bit weird. I would kind of want to be more precise, but I'm wondering if this needs to be elsewhere in a more generic "type equality" section - where we define equality as the equality of both the type constructor and the pair-wise equality of the parameters.


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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Certainly this could use a concrete code example.

- 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
Comment on lines +23 to +25
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably want code examples of each


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
Comment on lines +32 to +35
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this something we want to commit to (as a team)? I think I'd personally prefer weaker language here. Though, I don't know what that quite looks like (I do personally sort of want to try to move away from picking candidates through some arbitrary ordering.)

Loading