Well-formedness dev guide page by fallible-algebra · Pull Request #2889 · rust-lang/rustc-dev-guide

fallible-algebra · 2026-06-03T11:12:55Z

Initial work off of discussions with boxy + chasing hyperlinks. Part of #2663.

Few unsolved items here:

Conceptual: Items "contain" Terms? Is this the right way to say this? I imagine so, syntactically, but I need a vibe check.
Remove the "boxy said so" citations
"Term"¹ needs to be better specified as a concept. Maybe added to the glossary.
- May end up as "Type-Level Term"
Wfck doesn't appear on its own, but as item-wfck or term-wfck.
Run the formatter that deals with maximum line length.
Remove unused links

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:

<Items or Terms>
---
<Obligations and (relevant) Substitutions>

If this works fine, cool. Otherwise, open to being told to do it a different way :)

Finally, I'm putting this in an analysis subfolder as I've been told we need to do some structural reordering of the mdbook directory, and this should eventually live in an analysis subfolder so might as well have it there now.

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

BoxyUwU · 2026-06-04T17:38:02Z

+
+Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md).
+
+## Generating Obligations


I think this makes more sense as being part of the wfness of terms section, item wfck doesn't really start by doing this

View changes since the review

BoxyUwU · 2026-06-04T17:44:30Z

+
+Here we have a trivial bound that does not hold, because `String` is not `Copy`.
+
+## When We Don't Fully Do Wfck


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.

View changes since the review

BoxyUwU · 2026-06-04T17:46:09Z

@@ -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?"


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)

View changes since the review

Co-authored-by: Boxy <rust@boxyuwu.dev>

BoxyUwU

another round of feedback, I think slightly more nitpicky than last time? though still mostly just based around the general structure rather than too much about individual sentences/paragraphs/whatever

View changes since this review

BoxyUwU · 2026-06-08T23:06:13Z

+
+Well-formedness checking is not a coherent "stage" of type checking. It gets called from various contexts, and there are places where it gets skipped partially or entirely.
+
+### Trait Objects


Another example to illustrate this:

trait Trait where for<'a> [u8]: Sized {} fn foo(_: &dyn Trait) {}

this compiles even though [u8]: Sized doesn't hold. But if you try to actually construct an &dyn Trait we'll wind up checking all the where clauses hold and get an error.

probably a nicer example to lead with so you can separate out discussion of trait object wf jank from the const generics jank working around trait object wf jank lol

BoxyUwU · 2026-06-08T23:08:49Z

+
+Here we have a trivial bound that does not hold, because `String` is not `Copy`.
+
+## When We Don't Fully Do Well-Formedness Checking


Structurally it feels weird to lump this all under one header instead of wellformedness of terms and wellformedness of items having its own separate lists of "jank". Though I realise some things (e.g. const generics jank) would appear in both sections

It's a bit difficult. I like having them all here so there's a stronger emphasis on them as collective jank, but I'll see if I can rework them into the two major sections.

BoxyUwU · 2026-06-08T23:10:38Z

+
+Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md).
+
+## Type-Level Terms


would in theory like this header to be "Well-Formedness of Type-Level Terms" to mirror the following "Well-Formedness of Items" header 🤔 I realise you use this name as a subheader of Type-Level terms but that feels a bit weird to me.

I don't think the primary point of this page is to explain what a "type level term" is so I wouldn't structure it too heavily around that, rather than what it means for one to be well formed

Yeah agreed, this is a weird glossary out of nowhere. Restructuring 🫡

BoxyUwU · 2026-06-08T23:15:14Z

+    - "Items wfck" can call into "Term-wfck" as Items contain Terms.
+    - Sometimes normalize their inner Terms first.
+
+Wfck is not "number of parameters" or "parameter type" checking (AKA "kind checking"), as we might see in languages like Haskell. Neither term-wfck nor item-wfck is concerned with if a type with 2 parameters has 1 or 3 types applied to it (assuming no defaults), or if a const generic parameter has a type applied to it. These kinds of problems will get handled during HIR-ty Lowering[^hir-ty-lower], not wfck.


I wonder if it'd make sense to have a more general header at the end like "what isn't covered by well formedness" so that this sort-of tangent doesn't get in the way, and also we can talk about other things which one might expect is covered by wfck but actually isnt

i guess problem statement: not a huge fan of having this big paragraph here at the very start of the page :3 it feels like it takes up a lot of space and is kinda scary (talks about haskell and "kind checking") while not being all that important for probably the average reader

That's reasonable! I figured "problems I ran into while narrowing down what well-formedness is" just had to live somewhere, and that an earlier correction made more sense than a late one. But I'll move it down and replace this with a smaller "what this isn't" link.

BoxyUwU · 2026-06-08T23:19:54Z

@@ -0,0 +1,163 @@
+# Well-Formedness of Items and Type-Level Terms
+
+The area of analysis that produces 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?" for the trait solver to answer.


something about this paragraph feels odd to me and im not sure I can place why. it might just be that it feels like it makes more sense in the "Well-Formedness of Type-Level Terms" section, but also that would feel a bit weird too.

I think leading with the second paragraph "Items and Type-Level Terms are 'well formed' when they ..." feels like it would work fine and also feels better to me for some reason?

I guess concretely leading with this feels weird because:

item wfck does more than just produce obligations

it implies that item wfck and wellformedness of terms are one singular analysis rather than two semi-separate things

refers to an area of analysis that hasn't previously been referred to I guess :3

I think I can see it? But also I'd like to put the high-level "input/output" of the processes described here somewhere close to the top. I think the following paragraph isn't concrete enough in comparison. I'll wiggle things around.

BoxyUwU · 2026-06-08T23:23:44Z

+
+HRBs also skip the wfck on their subjects.
+
+TODO: bit of background of why this doesn't happen.


u need us to chat about this or just haven't gotten around to writing down what's in your notes?

We gotta chat about this :') This is lightly mentioned but any details are missing from my notes.

BoxyUwU · 2026-06-08T23:24:40Z

+## Well-Formedness of Items
+
+Items[^items] are, generally speaking, "Things that get defined." Item-wfck[^item-wf-module] only happens at the signature level for types and functions, including the methods and implementations. This doesn't happen for Free Type Aliases other than Const Generic Argument type checking.
+


probably a concrete example here of a function and going "things here are item wfck'd" and "things here are handled by normal type checking" would be useful

BoxyUwU · 2026-06-08T23:29:35Z

+
+There are two different forms of well-formedness checking:
+
+- Type-Level Term[^terms] wfck (term-wfck).


I think we discussed this a little 1:1 but to note it down here too, I feel unsure about the term "Term wfck". I feel like it has strong implications of it being a particular analysis/pass/something.

This is the case for item wfck but not as much for wellformedness of terms which is more of a general "thing you can get the trait solver to check" and is done all over the place 🤔

I think things would be a lot closer to how I "expect" them to be if instead of saying, for example, "Item-wfck is one of the entry points where most term-wfck will get performed" we instead wrote like, "Item-wfck is one of the places where well-formedness of terms will get checked"

definitely slightly nitpicky and not entirely structural, but also I guess it's kind of a semi-big-picture framing choice so feels somewhat important :3

View changes since the review

This is a helpful nudge ^^ I think I misinterpreted this originally as "always specify item-wfck vs term-wfck", rather than "'ck' has specific suffix implications and isn't just an abbreviation of check"

didn't misinterpret :3 that was the point I was making but then seeing it written out made me unsure about term-wfck as a piece of terminology 😅 this is wholly nitpicky so feel free to ignore this and we can figure it out at a later point, just wanted to make sure i wrote it down and didnt forget

Gotcha 😌 I've been rotating this in my mind today regardless so I'm kinda fine with either I think?

fallible-algebra added 2 commits June 1, 2026 15:54

Initial wellformed commit

3cbb0e0

Elaborate more about wfck

6ffe465

BoxyUwU self-assigned this Jun 3, 2026

Initial editing pass before un-drafting the PR

3c3ca09

fallible-algebra marked this pull request as ready for review June 3, 2026 15:34

rustbot added the S-waiting-on-review Status: this PR is waiting for a reviewer to verify its content label Jun 3, 2026

Title change

bb9a515

BoxyUwU reviewed Jun 4, 2026

View reviewed changes

fallible-algebra and others added 2 commits June 5, 2026 09:33

Apply suggestions from code review

7a4a307

Co-authored-by: Boxy <rust@boxyuwu.dev>

Big editing round

d9f8e3a

fallible-algebra requested a review from BoxyUwU June 5, 2026 14:09

BoxyUwU reviewed Jun 8, 2026

View reviewed changes


		Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md).

		## Generating Obligations


		Here we have a trivial bound that does not hold, because `String` is not `Copy`.

		## When We Don't Fully Do Wfck

		@@ -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?"


		Well-formedness checking is not a coherent "stage" of type checking. It gets called from various contexts, and there are places where it gets skipped partially or entirely.

		### Trait Objects


		Here we have a trivial bound that does not hold, because `String` is not `Copy`.

		## When We Don't Fully Do Well-Formedness Checking


		Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md).

		## Type-Level Terms

		@@ -0,0 +1,163 @@
		# Well-Formedness of Items and Type-Level Terms

		The area of analysis that produces 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?" for the trait solver to answer.


		HRBs also skip the wfck on their subjects.

		TODO: bit of background of why this doesn't happen.

		## Well-Formedness of Items

		Items[^items] are, generally speaking, "Things that get defined." Item-wfck[^item-wf-module] only happens at the signature level for types and functions, including the methods and implementations. This doesn't happen for Free Type Aliases other than Const Generic Argument type checking.


		There are two different forms of well-formedness checking:

		- Type-Level Term[^terms] wfck (term-wfck).

Conversation

fallible-algebra commented Jun 3, 2026 • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Footnotes

Uh oh!

Uh oh!

BoxyUwU Jun 4, 2026 • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

BoxyUwU Jun 4, 2026 • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

BoxyUwU Jun 4, 2026 • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

BoxyUwU left a comment • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

BoxyUwU Jun 8, 2026 • edited by rustbot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

fallible-algebra commented Jun 3, 2026 •

edited by rustbot

Loading

BoxyUwU Jun 4, 2026 •

edited by rustbot

Loading

BoxyUwU Jun 4, 2026 •

edited by rustbot

Loading

BoxyUwU Jun 4, 2026 •

edited by rustbot

Loading

BoxyUwU left a comment •

edited by rustbot

Loading

BoxyUwU Jun 8, 2026 •

edited by rustbot

Loading