document trait bounds and candidate preference behavior #7
Conversation
joshtriplett
left a comment
joshtriplett
left a comment
There was a problem hiding this comment.
A couple of nits and a question, but the overall structure and organization of this seems potentially reasonable.
|
🤷 idk how to make progress here, would be nice if someone could look over this again. |
jackh726
left a comment
jackh726
left a comment
There was a problem hiding this comment.
Okay, here are lot of a comments. I started to realize that I think this is still meant to be fairly "outline-y".
Overall, I'm feeling weird - I don't think describing how trait solving works is actually fitting well into the existing structure. The existing structure feels very "syntax-focused", but I think to describe well trait solving, we need to be able to describe more precisely the underlying formal procedures. It's not impossible, but it's hard.
| } | ||
| ``` | ||
|
|
||
| r[items.generics.instantiation] |
There was a problem hiding this comment.
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.
| r[items.generics.instantiation] | ||
| 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 unconstrained inference variable. | ||
|
|
||
| Instantiating the generic parameters of an item generally requires proving its where clauses. |
There was a problem hiding this comment.
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.
|
|
||
| r[type.alias.rigid] | ||
|
|
||
| Aliases might be treated as *rigid* in their current environment. In this case they behave like other types. |
There was a problem hiding this comment.
Definitely need to define what qualifies an alias as rigid, and what it means to "behave like other types"
| r[type.alias.rigid] | ||
|
|
||
| Aliases might be treated as *rigid* in their current environment. In this case they behave like other types. | ||
| Their equality is structural, *rigid* aliases are only equal if both have the same type constructor and equal corresponding arguments. |
There was a problem hiding this comment.
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 |
There was a problem hiding this comment.
Certainly this could use a concrete code example.
|
|
||
| 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. |
There was a problem hiding this comment.
I'd probably reword this like:
"Global bounds must be satisfiable without relying on any where clauses."
|
|
||
| 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. |
There was a problem hiding this comment.
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.
|
|
||
| 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. |
There was a problem hiding this comment.
Ah, great! Probably should just link the other section to this, then split this across aliases and trait bounds.
| 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. |
There was a problem hiding this comment.
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.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. |
There was a problem hiding this comment.
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.
specify s390x target features
Having just "Struct" as the link makes it look like the target is about structs and not just struct expressions
const_eval.md: be more clear where link leads to
These don't really belong where they are, and are just generally helpful things about the attribute.
The current text was a little bit of a mess and had some subtle inaccuracies. This reworks so that the intro follows the template, and just generally introduces the attribute. `allowed-positions` now just specifies the allowed positions. I reworked the behavior changes caused by no_std into proper separate rules. `std` is not injected into the crate root anymore starting with edition 2018.
I do not know how this was missing, I've looked at it a million times. I feel like I was maybe missing something, but I really can't find anything that directly refers to this, nor can I find any open issues. I believe this is now done with this relatively subtle bit: https://github.com/rust-lang/rust/blob/4d08223c054cf5a56d9761ca925fd46ffebe7115/compiler/rustc_builtin_macros/src/standard_library_imports.rs#L42 In the past it used to use a different approach of emulating `extern crate std as _;`: https://github.com/rust-lang/rust/blob/c8cf9f5a025bb475804b5a90f54aca310b952526/src/libsyntax_ext/standard_library_imports.rs#L42-L46
More closely align with the template, and some minor word tweaks.
We had said here that the `no_std` attribute is used to "prevent the automatic linking of the std crate", but then further down we say, "using `no_std` does not prevent the standard library from being linked in". The important distinction here is the word "automatically", but that gets a bit lost due to reusing the "prevent" phrasing. Probably "prevent" is just too strong a word to use when what we're really saying is that we're causing something to not happen automatically. Let's make that more clear and increase sentence parallelism.
Some sentences here could be improved with more sentence parallelism and a bit of reordering, so let's do that.
We had text in the intro about "deferring to the core crate instead", but it may not have been sufficiently clear what we mean exactly by that. Let's talk specifically about how `no_std` causes us to use the `core` crate for the standard library prelude and for the `macro_use` prelude.
We want to highlight how using `no_std` doesn't prevent `std` from being linked. Let's revise and elaborate this text for clarity.
The text here could be read in such a way as to imply that `no_std` affected whether or not `core` was added to the extern prelude, but that isn't the case. Let's make it clear that this section is about what is added to the `macro_use` prelude and speak to that directly.
Update `no_std` to use the attribute template
This is to follow the attribute template.
This rewrites the intro to be a little more general, and moves the description of the behavior to a specific rule that can be cited.
More closely align with the template, and some minor word tweaks.
… text This follows our style guide where the main text should document the current edition, and the edition blocks should note the differences to previous editions.
One of the comments in the example stretched out a bit far; let's wrap that and reword the comments in the example for clarity and flow.
It's more clear to say either that something can be applied "at the crate level" or "to the crate" than "to the crate level". Let's pick the latter and adjust for better grammatical parallelism.
Rather than saying "or any of its descendants", we can say "and its descendants" to express the same thing more concisely. Let's do that.
The remainder of this note is in the present tense, so saying that something "will" happen starting in the 2018 edition makes it sound as though that will happen in the future, even if what we mean is that the compiler "will" do it in the 2018 edition and later. Let's use the present tense here in emphatic form to distinguish this, and let's expand "it" for clarity.
Update `no_implicit_prelude` to use the attribute template
Guarantee the binary representation of `isize` explicitly
8 participants
cc https://github.com/joshtriplett/project-goal-reference-expansion/issues/3
documents http://github.com/rust-lang/rust/pull/120752
would be nice for somebody to quickly skim over this to detect
how to talk about X
how to talk about relating higher ranked types. "instantiating the
forof the subtype with inference variables and theforof the supertype with placeholders before relating them as normal" seems quite cumbersome. This is where using judgements/actual code is actually ncier than text.concepts which I don't know how to avoid
rigid types: a type which cannot be normalized in teh current context, whose equality is implemented by equating the type constructor and then recursively their corresponding generic arguments