Well-formedness dev guide page#2889
Conversation
rustbot
added
the
S-waiting-on-review
|
|
||
| During wfck we encounter the obligation for `Vec<T>` that `T: Sized`. For `Vec<str>` we encounter the obligation `str: Sized`, and as `str` is not `Sized` the term is not well-formed. | ||
|
|
||
| ### We Don't Need Normalization (Yet) |
There was a problem hiding this comment.
when i talk about normalization im referring to the process of replacing aliases with the aliased type (see https://rustc-dev-guide.rust-lang.org/normalization.html), which is orthogonal from whether a term has generic parameters in it or not.
There was a problem hiding this comment.
Right, got wires crossed with monomorphization. This makes why this is problematic make a lot more sense ^^
|
|
||
| Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). | ||
|
|
||
| ## Generating Obligations |
There was a problem hiding this comment.
I think this makes more sense as being part of the wfness of terms section, item wfck doesn't really start by doing this
|
|
||
| This produces an obligation that still has a generic in it. While more normalized versions of `Struct<T>` may not be `Ord`, we can say that `Set<Struct<T>>` is well-formed when `T: Ord`. | ||
|
|
||
| ### Const Generic Arguments |
There was a problem hiding this comment.
|
|
||
| Here we have a trivial bound that does not hold, because `String` is not `Copy`. | ||
|
|
||
| ## When We Don't Fully Do Wfck |
There was a problem hiding this comment.
i think as a general rule we should never just say "wfck" on its own in this, we should always explicitly say if we're talking about wfness of terms or checking wf of items.
| @@ -0,0 +1,166 @@ | |||
| # Well-Formedness of Terms and Items | |||
|
|
|||
| The area of the analysis pipeline that deals with questions like "does `T: Debug` hold true for some data structure that uses T?" or "is this const generic parameter `const B: bool` being handed a value of the right type?" | |||
There was a problem hiding this comment.
this feels slightly off to me, i would say the trait solver deals with those questions. though i guess that kind of makes sense since the trait solver is also responsible for proving wf obligations (i.e. checking terms are wf when we require them to be)
Co-authored-by: Boxy <rust@boxyuwu.dev>
3 participants
Initial work off of discussions with boxy + chasing hyperlinks.
Few unsolved items here:
I've also ended up doing some syntax here "from scratch", which I could use some input on. Specifically for showing off obligations I've done:
If this works fine, cool. Otherwise, open to being told to do it a different way :)
Finally, I'm putting this in an
analysissubfolder as I've been told we need to do some structural reordering of the mdbook directory, and this should eventually live in ananalysissubfolder so might as well have it there now.Footnotes
This was "Type-Level Term" in these files before I find-replaced it all to Term, which is maybe too vague to our target audience. ↩