From 3cbb0e02daa8704506974c658a8b818f1ec3084b Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Mon, 1 Jun 2026 15:54:29 +0100 Subject: [PATCH 01/18] Initial wellformed commit --- src/SUMMARY.md | 1 + src/analysis/well-formed.md | 91 +++++++++++++++++++++++++++++++++++++ 2 files changed, 92 insertions(+) create mode 100644 src/analysis/well-formed.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 9a98611860..9b59170de4 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -191,6 +191,7 @@ - [Sharing the trait solver with rust-analyzer](./solve/sharing-crates-with-rust-analyzer.md) - [`Unsize` and `CoerceUnsized` traits](./traits/unsize.md) - [Having separate `Trait` and `Projection` bounds](./traits/separate-projection-bounds.md) +- [Well-Formedness](./analysis/well-formed.md) - [Variance](./variance.md) - [Coherence checking](./coherence.md) - [HIR Type checking](./hir-typeck/summary.md) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md new file mode 100644 index 0000000000..82f719e518 --- /dev/null +++ b/src/analysis/well-formed.md @@ -0,0 +1,91 @@ +# Well-Formed Terms and Items + +Terms and items are "well formed" when they "follow rules" AKA "they meet the constraints." When we're doing a well-formedness check (wfck) we're usually concerned about if Trait requirements are met, but this also covers "requirements" of the types broadly. This is the area where Const Generics are "typechecked" as "this const generic argument must be a u8" is the responsibility of wfck. + +There's two different forms of well-formedness checking that happen, first for "Type Level Terms" and second for Items. "Items wfck" can call into "Type Level Terms wfck". + +Wfck is not "Kindedness" checking, as we might see in languages like Haskell. Wfck is not 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 errors will get handled during HIR-ty Lowering[^hir-ty-lower], not wfck. + +## Requirements + +The wfck module[^tlt-wf-module] contains an `obligations` function that takes type level terms and returns `PredicateObligation` that term must satisfy in order to be well-formed. The satisfaction of those obligations is performed + +## Well-Formedness of Type-Level Terms + +Well-Formed Type-Level Terms + +Type-Level Terms are Well-formed when trait constraints within them are satisfied. As an example, the following is not well-formed: + +```rust,no_compile +Vec +``` + +Because an implicit constraint on `T` in `Vec` is `T: Sized`, and `str` is not `Sized`. During wfck we would receive the requirement `str: Sized` This would not pass wfck, which passes the requirements off to the trait solver. + +### We Don't Need Normalization (Yet) + +This doesn't only happen with fully normalized types. For a type `struct Struct(T)` that gets used in `Vec>` and a where clause `Vec>: Send + Sync` we would also encounter the requirement `Struct: Send + Sync` and `T: Send + Sync`. + +TODO: Actually double check this with someone. + +## Well-Formedness of Items + +What's an Item? See the [Glossary](../appendix/glossary.md). We can imagine Items here as "Things that get defined." Wfck for Items[^item-wf-module] only happens at the signature level, for types and functions. This doesn't happen for Free Type Aliases beyond Const Generic Argument typechecking. + +### Calling Type Level Term Wfck from Item Wfck + +Item-level wfck can invoke Type-level term wfck[^boxy]. + +### Normalizing then checking well-formedness + +For Type-Level Terms, we don't need to normalize anything first. Items are different, and may require normalization before + +## Const Generic Arguments + +Const generics have special cases in wfck. + +## Trait Objects + +Trait objects of traits with where clauses (i.e. `trait MyTrait) + +```rust +trait Trait {} +fn foo(_: &dyn Trait) {} +``` + +## Trivial Bounds + +Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to be evaluated, go through wfck, etc. A + +## Binders + +```rust +fn foo() { + // legal even though slices aren't sized + // (in future, this SHOULD error.) + let _: for<'a> fn(Vec<[&'a ()]>); + // illegal + let _: for<'a> fn(&'a (), Vec<[()]>); +} +``` + +## Free Type Aliases + +The Rhs of Free Type Aliases[^fta] are an exception to Well Formedness checking. They don't get checked, with the exception of shallowly "type checking" the arguments of const generic parameters. + +This means the following _currently_ passes typechecking, assuming you don't actually use it in a non-FTA Item: + +```rust,no_compile +type WorksButShouldNot = Vec; +``` + +This shouldn't work, as `T: Sized`, `str: Sized` being implied by `Vec`. + +[^fta]: Type aliases not associated with anything, i.e. a top-level `type Alias = Vec`. +[^boxy]: Boxy said so. +[^hir-ty-lower]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/hir_ty_lowering/index.html +[^tlt-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html +[^item-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html +[^wf-ctx-construction]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/fn.enter_wf_checking_ctxt.html +[^item-wf-ctx]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/struct.WfCheckingCtxt.html +[^item-wf-global-bounds]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/struct.WfCheckingCtxt.html#method.check_false_global_bounds \ No newline at end of file From 6ffe46541fafffc5d736e5dd0cef85c8279a353b Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Wed, 3 Jun 2026 12:04:54 +0100 Subject: [PATCH 02/18] Elaborate more about wfck --- src/analysis/well-formed.md | 122 +++++++++++++++++++++++++----------- 1 file changed, 86 insertions(+), 36 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 82f719e518..5d232d6339 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -1,88 +1,138 @@ # Well-Formed Terms and Items -Terms and items are "well formed" when they "follow rules" AKA "they meet the constraints." When we're doing a well-formedness check (wfck) we're usually concerned about if Trait requirements are met, but this also covers "requirements" of the types broadly. This is the area where Const Generics are "typechecked" as "this const generic argument must be a u8" is the responsibility of wfck. +Terms and Items are "well formed" when they "follow rules" AKA "they fulfill obligations" or "they meet the necessary constraints." When we're doing a well-formedness check (wfck) we're usually concerned about if Trait obligations are met, but this also covers obligations of the types broadly, including making sure that the types of const generic terms type check. -There's two different forms of well-formedness checking that happen, first for "Type Level Terms" and second for Items. "Items wfck" can call into "Type Level Terms wfck". +There are two different forms of wfck that happen, first for Terms[^terms] and second for Items[^items]. "Items wfck" can call into "Terms wfck". Wfck is not "Kindedness" checking, as we might see in languages like Haskell. Wfck is not 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 errors will get handled during HIR-ty Lowering[^hir-ty-lower], not wfck. -## Requirements +## Generating Obligations -The wfck module[^tlt-wf-module] contains an `obligations` function that takes type level terms and returns `PredicateObligation` that term must satisfy in order to be well-formed. The satisfaction of those obligations is performed +The first step of wfck is generating the list of things for a subject of the wfck that need to be true for that subject to be well-formed. -## Well-Formedness of Type-Level Terms +These end up being referred to as Obligations, Requirements, or Constraints. Prefer to call them obligations for now, as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the Polonius term "Goal"[^boxy]. -Well-Formed Type-Level Terms +The Term wfck module[^tlt-wf-module] contains an `obligations` function that takes type-level terms and returns `PredicateObligations`, a set of obligations that Term must satisfy in order to be well-formed. The satisfaction of those obligations is performed by the Trait Solver[^trait-solver][^boxy], and if they are satisfied then the term is Well-Formed. -Type-Level Terms are Well-formed when trait constraints within them are satisfied. As an example, the following is not well-formed: +## Well-Formedness of Terms -```rust,no_compile +Terms are Well-Formed when trait obligations within them are satisfied. As an example, the following is not well-formed: + +```rust Vec +--- +// Obligations to fulfill +Vec where T: Sized +Vec where str: Sized ``` -Because an implicit constraint on `T` in `Vec` is `T: Sized`, and `str` is not `Sized`. During wfck we would receive the requirement `str: Sized` This would not pass wfck, which passes the requirements off to the trait solver. +This isn't well-formed an implicit obligation on `T` in `Vec` is `T: Sized`, and `str` is not `Sized`. + +During wfck we would receive the requirement `str: Sized` This would not pass wfck once those obligations are passed off to the trait solver. ### We Don't Need Normalization (Yet) -This doesn't only happen with fully normalized types. For a type `struct Struct(T)` that gets used in `Vec>` and a where clause `Vec>: Send + Sync` we would also encounter the requirement `Struct: Send + Sync` and `T: Send + Sync`. +Terms are not necessarily normalized, so wfck on these entities doesn't require . For a type `struct Struct(T)` that gets used in `Vec>` with a where clause `Vec>: Send + Sync` we would also encounter the requirement `Struct: Send + Sync` and `T: Send + Sync`. -TODO: Actually double check this with someone. +TODO: Actually double-check this with someone[^boxy]. ## Well-Formedness of Items -What's an Item? See the [Glossary](../appendix/glossary.md). We can imagine Items here as "Things that get defined." Wfck for Items[^item-wf-module] only happens at the signature level, for types and functions. This doesn't happen for Free Type Aliases beyond Const Generic Argument typechecking. +We can imagine Items[^items] here as "Things that get defined." Wfck for Items[^item-wf-module] only happens at the signature level, for types and functions. This doesn't happen for Free Type Aliases beyond Const Generic Argument type checking. -### Calling Type Level Term Wfck from Item Wfck +### Calling Term Wfck from Item Wfck -Item-level wfck can invoke Type-level term wfck[^boxy]. +Because Items contain Terms, Item-level wfck can invoke Term wfck[^boxy]. -### Normalizing then checking well-formedness +### Normalizing Then Checking Well-Formedness -For Type-Level Terms, we don't need to normalize anything first. Items are different, and may require normalization before +Items may require normalization before performing wfck on the terms that make them up. + +TODO: list a couple of places where this happens ## Const Generic Arguments -Const generics have special cases in wfck. +Wfck is responsible for getting obligations of _types of const generic arguments_ to match. Let's look at the following use of const generics: + +```rust +fn use_const_generics() { /* ... */ } +// call site +use_const_generics::<6>(); +--- +const U: usize +const 6: usize +``` + +Applying wfck to the call site will provide us with the obligation `6: usize`. + +## Trivial Bounds + +Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to be evaluated, go through wfck, etc. Consider the following: -## Trait Objects +```rust +fn apartment_complex(block: T, name: String) where String: Clone { /* ... */ } +--- +String: Clone // Trivial bound! We don't have to wfck T or any sub-terms to know this holds. +``` + +This produces the trivial bound `String: Clone`. This is something we can check without instantiating any other information in this Item. + +## Exceptions to Wfck + +Wfck is not a coherent "stage" of type checking. It gets called from various contexts, has special cases to consider, and there are places where it gets skipped partially or entirely. + +### Trait Objects -Trait objects of traits with where clauses (i.e. `trait MyTrait) +Trait objects of traits with where clauses / const generics do not undergo wfck until the type is coerced back into a concrete type. ```rust trait Trait {} fn foo(_: &dyn Trait) {} +--- +// This doesn't end up being generated, because it happens within a trait object. +const N: usize +const B: bool +N = B // implied substitution +const B: usize ``` -## Trivial Bounds +The above shouldn't compile, `foo`s const generic argument is a boolean, while `Trait`'s is a `usize`. But because the wfck of trait objects doesn't happen until coercion into a concrete type, the above makes it through wfck. + + +### Binders / Higher-Ranked Bounds -Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to be evaluated, go through wfck, etc. A +HRBs also skip the wfck on their subjects. -## Binders +TODO: bit of background of why this doesn't happen. ```rust -fn foo() { - // legal even though slices aren't sized - // (in future, this SHOULD error.) - let _: for<'a> fn(Vec<[&'a ()]>); - // illegal - let _: for<'a> fn(&'a (), Vec<[()]>); -} +let _: for<'a> fn(Vec<[&'a ()]>); +--- +// This doesn't end up being generated, because it happens within a HRB +[&'a ()]: Sized // slices aren't sized. ``` -## Free Type Aliases -The Rhs of Free Type Aliases[^fta] are an exception to Well Formedness checking. They don't get checked, with the exception of shallowly "type checking" the arguments of const generic parameters. +### Free Type Aliases -This means the following _currently_ passes typechecking, assuming you don't actually use it in a non-FTA Item: +The rhs[^rhs] of Free Type Aliases[^fta] do not go through full a full wfck. They don't get checked, with the exception of shallowly "type checking" only const generic parameters of the rhs. -```rust,no_compile +This means the following _currently_ passes type checking, assuming you don't actually use it in a non-FTA Item: + +```rust type WorksButShouldNot = Vec; +--- +// This should fail! But we skip the rhs of free type aliases +str: Sized ``` -This shouldn't work, as `T: Sized`, `str: Sized` being implied by `Vec`. +This shouldn't work, as `T: Sized`, `str: Sized` being implied by `Vec`, but because the rhs of a free type alias doesn't go through well-formedness checking unless it's used this doesn't error. -[^fta]: Type aliases not associated with anything, i.e. a top-level `type Alias = Vec`. -[^boxy]: Boxy said so. +[^trait-solver]: Despite being called a trait solver, it solves other things too[^boxy]. +[^fta]: Type aliases not associated with anything, i.e. a module-level `type Alias = Vec;`. +[^boxy]: Boxy said so. TODO: don't have any of these references :) +[^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md) +[^terms]: Type expressions? TODO: this needs to be nailed down, and maybe inserted into the glossary. [^hir-ty-lower]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/hir_ty_lowering/index.html [^tlt-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html [^item-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html From 3c3ca09cc53eb1581e0d5cfcf6a2a44fdc347283 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Wed, 3 Jun 2026 16:33:34 +0100 Subject: [PATCH 03/18] Initial editing pass before un-drafting the PR --- src/analysis/well-formed.md | 97 +++++++++++++++++++++++-------------- 1 file changed, 61 insertions(+), 36 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 5d232d6339..84c1e2f990 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -1,11 +1,20 @@ # Well-Formed 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?" + Terms and Items are "well formed" when they "follow rules" AKA "they fulfill obligations" or "they meet the necessary constraints." When we're doing a well-formedness check (wfck) we're usually concerned about if Trait obligations are met, but this also covers obligations of the types broadly, including making sure that the types of const generic terms type check. -There are two different forms of wfck that happen, first for Terms[^terms] and second for Items[^items]. "Items wfck" can call into "Terms wfck". +There are two different forms of wfck: + +- Term[^terms] wfck. +- Items[^items] wfck. + - "Items wfck" can call into "Terms wfck" as Items contain Terms. + - Sometimes normalize their inner Terms first. Wfck is not "Kindedness" checking, as we might see in languages like Haskell. Wfck is not 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 errors will get handled during HIR-ty Lowering[^hir-ty-lower], not wfck. +Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). + ## Generating Obligations The first step of wfck is generating the list of things for a subject of the wfck that need to be true for that subject to be well-formed. @@ -16,70 +25,86 @@ The Term wfck module[^tlt-wf-module] contains an `obligations` function that tak ## Well-Formedness of Terms -Terms are Well-Formed when trait obligations within them are satisfied. As an example, the following is not well-formed: +Terms are Well-Formed when trait obligations within them are satisfied when passed to the trait solver. As an example, the following is not well-formed: ```rust Vec --- // Obligations to fulfill Vec where T: Sized -Vec where str: Sized +Vec where str: Sized // This is not true, therefore the term is not well-formed. ``` -This isn't well-formed an implicit obligation on `T` in `Vec` is `T: Sized`, and `str` is not `Sized`. - -During wfck we would receive the requirement `str: Sized` This would not pass wfck once those obligations are passed off to the trait solver. +During wfck we encounter the obligation for `Vec` that `T: Sized`. For `Vec` we encounter the obligation `str: Sized`, and as `str` is not `Sized` the term is not well-formed. ### We Don't Need Normalization (Yet) -Terms are not necessarily normalized, so wfck on these entities doesn't require . For a type `struct Struct(T)` that gets used in `Vec>` with a where clause `Vec>: Send + Sync` we would also encounter the requirement `Struct: Send + Sync` and `T: Send + Sync`. - -TODO: Actually double-check this with someone[^boxy]. - -## Well-Formedness of Items - -We can imagine Items[^items] here as "Things that get defined." Wfck for Items[^item-wf-module] only happens at the signature level, for types and functions. This doesn't happen for Free Type Aliases beyond Const Generic Argument type checking. +We wfck terms regardless of their normalization state. Consider a struct `Struct` and another struct `Set` that has a where clause in it[^where-clause-in-type]: -### Calling Term Wfck from Item Wfck - -Because Items contain Terms, Item-level wfck can invoke Term wfck[^boxy]. - -### Normalizing Then Checking Well-Formedness - -Items may require normalization before performing wfck on the terms that make them up. +```rust +// Ord if T: Ord +#[derive(PartialEq, Eq, PartialOrd, Ord)] +struct Struct(T); +struct Set(A) where A: Ord; +Set> where T: Ord +--- +Struct: Ord // This is true / well-formed if T: Ord (which it is here) +``` -TODO: list a couple of places where this happens +This produces an obligation that still has a generic in it. While more normalized versions of `Struct` may not be `Ord`, we can say that `Set>` is well-formed when `T: Ord`. -## Const Generic Arguments +### Const Generic Arguments -Wfck is responsible for getting obligations of _types of const generic arguments_ to match. Let's look at the following use of const generics: +Wfck is also responsible for getting obligations of const generic terms. Let's look at the following use of const generics: ```rust fn use_const_generics() { /* ... */ } // call site use_const_generics::<6>(); --- -const U: usize +// call site wfck obligations const 6: usize ``` -Applying wfck to the call site will provide us with the obligation `6: usize`. +Applying wfck to the call site will provide us with the obligation `6: usize`. This obligation will be passed off to the trait solver just like any trait-style obligation, as the trait solver has more responsibilities than its name suggests. -## Trivial Bounds +## Well-Formedness of Items + +We can consider Items[^items] as "Things that get defined." Wfck for Items[^item-wf-module] only happens at the signature level, for types and functions. This doesn't happen for Free Type Aliases beyond Const Generic Argument type checking. + +Because Items contain Terms, Item-level wfck can invoke Term wfck[^boxy]. -Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to be evaluated, go through wfck, etc. Consider the following: +### We (Sometimes) Need Normalization + +Currently, there are places where normalization of an Item happens before its Terms have gone through wfck. This is considered problematic as this allows some terms to [bypass wfck entirely](https://github.com/rust-lang/rust/issues/100041). + +### Trivial Bounds + +Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to be evaluated, go through wfck, etc. These are also sometimes called Global Bounds. Consider the following: ```rust fn apartment_complex(block: T, name: String) where String: Clone { /* ... */ } --- String: Clone // Trivial bound! We don't have to wfck T or any sub-terms to know this holds. +// Maybe there's obligations on T but we don't care about them here. +// ... ``` -This produces the trivial bound `String: Clone`. This is something we can check without instantiating any other information in this Item. +This produces the trivial bound `String: Clone`. This is something we can check without instantiating any other information in this Item. We don't need to know any information about `T` to be able to make a judgment on the well-formedness of `String: Clone`. -## Exceptions to Wfck +False trivial bounds are things like: -Wfck is not a coherent "stage" of type checking. It gets called from various contexts, has special cases to consider, and there are places where it gets skipped partially or entirely. +```rust +fn apartment_simple(block: T, name: String) where String: Copy { /* ... */ } +--- +String: Copy // Trivial bound again, but this one is false! +``` + +Here we have a trivial bound that does not hold, because `String` is not `Copy`. + +## When We Don't Fully Do Wfck + +Wfck 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 @@ -92,12 +117,13 @@ fn foo(_: &dyn Trait) {} // This doesn't end up being generated, because it happens within a trait object. const N: usize const B: bool -N = B // implied substitution -const B: usize +N = B // Substitution +// This fails once we coerce out of a trait object to a concrete type. +// But because we don't coerce, it passes wfck. +const B: usize + bool ``` -The above shouldn't compile, `foo`s const generic argument is a boolean, while `Trait`'s is a `usize`. But because the wfck of trait objects doesn't happen until coercion into a concrete type, the above makes it through wfck. - +The above shouldn't compile, and yet it does. `foo`s const generic argument is a `bool`, while `Trait`'s is a `usize`. But because the wfck of trait objects doesn't happen until coercion into a concrete type, the above compiles just fine. ### Binders / Higher-Ranked Bounds @@ -112,10 +138,9 @@ let _: for<'a> fn(Vec<[&'a ()]>); [&'a ()]: Sized // slices aren't sized. ``` - ### Free Type Aliases -The rhs[^rhs] of Free Type Aliases[^fta] do not go through full a full wfck. They don't get checked, with the exception of shallowly "type checking" only const generic parameters of the rhs. +The rhs of Free Type Aliases[^fta] do not go through a full wfck. They don't get checked, with the exception of shallowly "type checking" const generic parameters of the rhs. This means the following _currently_ passes type checking, assuming you don't actually use it in a non-FTA Item: From bb9a51591a6ee9e30afac8f6d1a6a4fd6a6e2ba0 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Wed, 3 Jun 2026 16:43:56 +0100 Subject: [PATCH 04/18] Title change --- src/analysis/well-formed.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 84c1e2f990..1b10ffa638 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -1,4 +1,4 @@ -# Well-Formed Terms and Items +# 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?" From 7a4a307c6d48343185e8f57b29830416d164179e Mon Sep 17 00:00:00 2001 From: Fallible Algebra <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 5 Jun 2026 09:33:16 +0100 Subject: [PATCH 05/18] Apply suggestions from code review Co-authored-by: Boxy --- src/analysis/well-formed.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 1b10ffa638..b54067f2e5 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -19,7 +19,7 @@ Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-che The first step of wfck is generating the list of things for a subject of the wfck that need to be true for that subject to be well-formed. -These end up being referred to as Obligations, Requirements, or Constraints. Prefer to call them obligations for now, as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the Polonius term "Goal"[^boxy]. +These end up being referred to as Obligations, Requirements, or Constraints. Prefer to call them obligations for now, as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal"[^boxy]. The Term wfck module[^tlt-wf-module] contains an `obligations` function that takes type-level terms and returns `PredicateObligations`, a set of obligations that Term must satisfy in order to be well-formed. The satisfaction of those obligations is performed by the Trait Solver[^trait-solver][^boxy], and if they are satisfied then the term is Well-Formed. From d9f8e3a37f572193bce6e72e301fc0d9ceaf838b Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 5 Jun 2026 14:58:24 +0100 Subject: [PATCH 06/18] Big editing round --- src/analysis/well-formed.md | 83 ++++++++++++++++++------------------- 1 file changed, 40 insertions(+), 43 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index b54067f2e5..07c0a99270 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -1,33 +1,38 @@ -# Well-Formedness of Terms and Items +# Well-Formedness of Items and Type-Level Terms -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?" +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. -Terms and Items are "well formed" when they "follow rules" AKA "they fulfill obligations" or "they meet the necessary constraints." When we're doing a well-formedness check (wfck) we're usually concerned about if Trait obligations are met, but this also covers obligations of the types broadly, including making sure that the types of const generic terms type check. +Items and Type-Level Terms[^terms][^terms-abbreviated] are "well formed" when they "follow rules" AKA "fulfill obligations" or "meet the necessary constraints." When we're doing a well-formedness check (wfck) we're usually concerned about if Trait obligations are met, but this also covers obligations of the types broadly, including making sure that the types of const generic terms type check. -There are two different forms of wfck: +There are two different forms of well-formedness checking: -- Term[^terms] wfck. -- Items[^items] wfck. - - "Items wfck" can call into "Terms wfck" as Items contain Terms. +- Type-Level Term[^terms] wfck (term-wfck). + - This is the primary subject of "Well-Formedness Checking." +- Items[^items] wfck (item-wfck). + - "Items wfck" can call into "Term-wfck" as Items contain Terms. - Sometimes normalize their inner Terms first. -Wfck is not "Kindedness" checking, as we might see in languages like Haskell. Wfck is not 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 errors will get handled during HIR-ty Lowering[^hir-ty-lower], not wfck. +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. Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). -## Generating Obligations +## Type-Level Terms -The first step of wfck is generating the list of things for a subject of the wfck that need to be true for that subject to be well-formed. +Type-Level Terms are the data structures that well-formedness checking is focused on analyzing. Item-wfck is one of the entry points where most term-wfck will get performed. -These end up being referred to as Obligations, Requirements, or Constraints. Prefer to call them obligations for now, as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal"[^boxy]. +### Obligations -The Term wfck module[^tlt-wf-module] contains an `obligations` function that takes type-level terms and returns `PredicateObligations`, a set of obligations that Term must satisfy in order to be well-formed. The satisfaction of those obligations is performed by the Trait Solver[^trait-solver][^boxy], and if they are satisfied then the term is Well-Formed. +Term-wfck begins with generating the list of things that need to be true for the thing-being-wfck'd to be well-formed. -## Well-Formedness of Terms +These predicates end up being referred to as Obligations, Requirements, or Constraints. Preferred term is "obligations", as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal". + +The term-wfck module[^tlt-wf-module] contains an `obligations` function that takes type-level terms and returns `PredicateObligations`, a list of obligations that Type-Level Term must satisfy in order to be well-formed. The satisfaction of those obligations is performed by the Trait Solver[^trait-solver], and if they are satisfied then the term is Well-Formed. + +### Well-Formedness of Type-Level Terms Terms are Well-Formed when trait obligations within them are satisfied when passed to the trait solver. As an example, the following is not well-formed: -```rust +```rust,ignore Vec --- // Obligations to fulfill @@ -35,29 +40,19 @@ Vec where T: Sized Vec where str: Sized // This is not true, therefore the term is not well-formed. ``` -During wfck we encounter the obligation for `Vec` that `T: Sized`. For `Vec` we encounter the obligation `str: Sized`, and as `str` is not `Sized` the term is not well-formed. +During term-wfck we encounter the obligation for `Vec` that `T: Sized`. For `Vec` we encounter the obligation `str: Sized`, and as `str` is not `Sized` the term is not well-formed. ### We Don't Need Normalization (Yet) -We wfck terms regardless of their normalization state. Consider a struct `Struct` and another struct `Set` that has a where clause in it[^where-clause-in-type]: - -```rust -// Ord if T: Ord -#[derive(PartialEq, Eq, PartialOrd, Ord)] -struct Struct(T); -struct Set(A) where A: Ord; -Set> where T: Ord ---- -Struct: Ord // This is true / well-formed if T: Ord (which it is here) -``` +[Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type, this is because a type alias is considered well-formed if its underlying type is well-formed. The underlying type is undergoes well-formedness checking at most definition and instantiation sites. -This produces an obligation that still has a generic in it. While more normalized versions of `Struct` may not be `Ord`, we can say that `Set>` is well-formed when `T: Ord`. +We don't need to perform normalization to perform term-wfck. ### Const Generic Arguments -Wfck is also responsible for getting obligations of const generic terms. Let's look at the following use of const generics: +Term-wfck is also responsible for getting "type-checking" obligations of const generic terms[^tyck-const-generics]. Let's look at the following use of const generics: -```rust +```rust,ignore fn use_const_generics() { /* ... */ } // call site use_const_generics::<6>(); @@ -66,23 +61,23 @@ use_const_generics::<6>(); const 6: usize ``` -Applying wfck to the call site will provide us with the obligation `6: usize`. This obligation will be passed off to the trait solver just like any trait-style obligation, as the trait solver has more responsibilities than its name suggests. +Applying term-wfck to the call site will provide us with the obligation `6: usize`. This obligation will be passed off to the trait solver just like any trait-style obligation, as the trait solver has more responsibilities than its name suggests. ## Well-Formedness of Items -We can consider Items[^items] as "Things that get defined." Wfck for Items[^item-wf-module] only happens at the signature level, for types and functions. This doesn't happen for Free Type Aliases beyond Const Generic Argument type checking. +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. -Because Items contain Terms, Item-level wfck can invoke Term wfck[^boxy]. +Items are a major entry point for performing term-wfck. Because Items contain Terms, item-wfck can invoke term-wfck. ### We (Sometimes) Need Normalization -Currently, there are places where normalization of an Item happens before its Terms have gone through wfck. This is considered problematic as this allows some terms to [bypass wfck entirely](https://github.com/rust-lang/rust/issues/100041). +Currently, there are places where normalization of an Item happens before its Terms have gone through wfck. This is considered problematic as this allows some terms to [bypass term-wfck entirely](https://github.com/rust-lang/rust/issues/100041). ### Trivial Bounds -Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to be evaluated, go through wfck, etc. These are also sometimes called Global Bounds. Consider the following: +Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to go through wfck. These are also sometimes called Global Bounds. Consider the following: -```rust +```rust,ignore fn apartment_complex(block: T, name: String) where String: Clone { /* ... */ } --- String: Clone // Trivial bound! We don't have to wfck T or any sub-terms to know this holds. @@ -94,7 +89,7 @@ This produces the trivial bound `String: Clone`. This is something we can check False trivial bounds are things like: -```rust +```rust,ignore fn apartment_simple(block: T, name: String) where String: Copy { /* ... */ } --- String: Copy // Trivial bound again, but this one is false! @@ -102,15 +97,15 @@ String: Copy // Trivial bound again, but this one is false! Here we have a trivial bound that does not hold, because `String` is not `Copy`. -## When We Don't Fully Do Wfck +## When We Don't Fully Do Well-Formedness Checking -Wfck 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. +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 Trait objects of traits with where clauses / const generics do not undergo wfck until the type is coerced back into a concrete type. -```rust +```rust,ignore trait Trait {} fn foo(_: &dyn Trait) {} --- @@ -131,7 +126,7 @@ HRBs also skip the wfck on their subjects. TODO: bit of background of why this doesn't happen. -```rust +```rust,ignore let _: for<'a> fn(Vec<[&'a ()]>); --- // This doesn't end up being generated, because it happens within a HRB @@ -140,11 +135,11 @@ let _: for<'a> fn(Vec<[&'a ()]>); ### Free Type Aliases -The rhs of Free Type Aliases[^fta] do not go through a full wfck. They don't get checked, with the exception of shallowly "type checking" const generic parameters of the rhs. +The rhs of Free Type Aliases[^fta] do not go through a full wfck at the definition site, with the exception of shallowly "type checking" const generic parameters of the rhs. This means the following _currently_ passes type checking, assuming you don't actually use it in a non-FTA Item: -```rust +```rust,ignore type WorksButShouldNot = Vec; --- // This should fail! But we skip the rhs of free type aliases @@ -158,9 +153,11 @@ This shouldn't work, as `T: Sized`, `str: Sized` being implied by `Vec`, but [^boxy]: Boxy said so. TODO: don't have any of these references :) [^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md) [^terms]: Type expressions? TODO: this needs to be nailed down, and maybe inserted into the glossary. +[^terms-abbreviated]: Abbreviated as "Terms" on this page in some areas. [^hir-ty-lower]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/hir_ty_lowering/index.html [^tlt-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html [^item-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html [^wf-ctx-construction]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/fn.enter_wf_checking_ctxt.html [^item-wf-ctx]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/struct.WfCheckingCtxt.html -[^item-wf-global-bounds]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/struct.WfCheckingCtxt.html#method.check_false_global_bounds \ No newline at end of file +[^item-wf-global-bounds]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/struct.WfCheckingCtxt.html#method.check_false_global_bounds +[^tyck-const-generics]: https://rustc-dev-guide.rust-lang.org/const-generics.html#checking-types-of-const-arguments \ No newline at end of file From b18833893178609947d4ad197c76fbfcc3be3d14 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Mon, 15 Jun 2026 13:25:58 +0100 Subject: [PATCH 07/18] unwise to spend so much time stewing on changes between git commits --- src/analysis/well-formed.md | 107 +++++++++++++++++++++++------------- src/appendix/glossary.md | 1 + 2 files changed, 70 insertions(+), 38 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 07c0a99270..7424589b05 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -2,35 +2,35 @@ 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. -Items and Type-Level Terms[^terms][^terms-abbreviated] are "well formed" when they "follow rules" AKA "fulfill obligations" or "meet the necessary constraints." When we're doing a well-formedness check (wfck) we're usually concerned about if Trait obligations are met, but this also covers obligations of the types broadly, including making sure that the types of const generic terms type check. +Items and Type-Level Terms[^terms][^terms-abbreviated] are "well formed" when they "follow rules" AKA "fulfill obligations" or "meet the necessary constraints." When we're doing a well-formedness check we're usually concerned about if Trait obligations are met, but this also covers obligations of the types broadly, including making sure that the types of const generic terms type check. There are two different forms of well-formedness checking: -- Type-Level Term[^terms] wfck (term-wfck). - - This is the primary subject of "Well-Formedness Checking." -- Items[^items] wfck (item-wfck). - - "Items wfck" can call into "Term-wfck" as Items contain Terms. - - Sometimes normalize their inner Terms first. +- Type-Level Term[^terms] well-formedness check. + - Primary subject of "Well-Formedness Checking." + - Abbreviated here to "Term well-formedness" or "Term well-formedness checking." + - Not a distinct analysis pass. +- Items[^items] well-formedness check (item-wfck). + - "Item-wfck" can call into "Term well-formedness checking" as Items contain Terms. + - Inner "Terms" can get normalized 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. +See: [What Well-Formedness Is Not](#what-well-formedness-isnt) -Wfck doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). +## Well-Formedness of Type-Level Terms -## Type-Level Terms - -Type-Level Terms are the data structures that well-formedness checking is focused on analyzing. Item-wfck is one of the entry points where most term-wfck will get performed. +Type-Level Terms are the data structures that well-formedness checking is focused on analyzing. Item-wfck is one of the entry points where term well-formedness checking will get performed. ### Obligations -Term-wfck begins with generating the list of things that need to be true for the thing-being-wfck'd to be well-formed. +Term well-formedness begins with generating the list of things that need to be true for the term-being-checked to be well-formed. These predicates end up being referred to as Obligations, Requirements, or Constraints. Preferred term is "obligations", as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal". -The term-wfck module[^tlt-wf-module] contains an `obligations` function that takes type-level terms and returns `PredicateObligations`, a list of obligations that Type-Level Term must satisfy in order to be well-formed. The satisfaction of those obligations is performed by the Trait Solver[^trait-solver], and if they are satisfied then the term is Well-Formed. +The term well-formedness module[^tlt-wf-module] contains an `obligations` function that takes type-level terms and returns `PredicateObligations`, a list of obligations that Type-Level Term must satisfy in order to be well-formed. The satisfaction of those obligations is performed by the Trait Solver[^trait-solver], and if they are satisfied then the term is Well-Formed. -### Well-Formedness of Type-Level Terms +### When Type-Level Terms Are Well Formed -Terms are Well-Formed when trait obligations within them are satisfied when passed to the trait solver. As an example, the following is not well-formed: +Terms are Well-Formed when trait obligations within them are considered satisfied by the trait solver. As an example, the following is not well-formed: ```rust,ignore Vec @@ -40,17 +40,15 @@ Vec where T: Sized Vec where str: Sized // This is not true, therefore the term is not well-formed. ``` -During term-wfck we encounter the obligation for `Vec` that `T: Sized`. For `Vec` we encounter the obligation `str: Sized`, and as `str` is not `Sized` the term is not well-formed. +From term well-formedness we find the obligation for `Vec` that `T: Sized`. For `Vec` we encounter the obligation `str: Sized`, and as `str` is not `Sized` the term is not well-formed. ### We Don't Need Normalization (Yet) -[Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type, this is because a type alias is considered well-formed if its underlying type is well-formed. The underlying type is undergoes well-formedness checking at most definition and instantiation sites. - -We don't need to perform normalization to perform term-wfck. +[Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type. A type alias is considered well-formed if its underlying type is well-formed. The underlying type is undergoes well-formedness checking at most definition and instantiation sites. ### Const Generic Arguments -Term-wfck is also responsible for getting "type-checking" obligations of const generic terms[^tyck-const-generics]. Let's look at the following use of const generics: +Term well-formedness is also responsible for getting "type-checking" obligations of const generic terms[^tyck-const-generics]. Let's look at the following use of const generics: ```rust,ignore fn use_const_generics() { /* ... */ } @@ -61,31 +59,37 @@ use_const_generics::<6>(); const 6: usize ``` -Applying term-wfck to the call site will provide us with the obligation `6: usize`. This obligation will be passed off to the trait solver just like any trait-style obligation, as the trait solver has more responsibilities than its name suggests. +The call site will provide us with the obligation `6: usize` during well-formedness checking. This obligation will be passed off to the trait solver just like any trait-style obligation, as the trait solver has more responsibilities than its name suggests. ## 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. +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. -Items are a major entry point for performing term-wfck. Because Items contain Terms, item-wfck can invoke term-wfck. +Items are a major entry point for term well-formedness. Because Items contain Terms, item-wfck can invoke term well-formedness checking. ### We (Sometimes) Need Normalization -Currently, there are places where normalization of an Item happens before its Terms have gone through wfck. This is considered problematic as this allows some terms to [bypass term-wfck entirely](https://github.com/rust-lang/rust/issues/100041). +Currently, there are places where normalization of an Item happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). + +### Global & Trivial Bounds -### Trivial Bounds +Trait bounds are a common Obligation. -Trivial bounds[^item-wf-global-bounds] are bounds that don't need any further normalization to go through wfck. These are also sometimes called Global Bounds. Consider the following: +Global bounds[^global-where-bound] are post-normalization bounds that don't contain any generic parameters (like `` or `'a`) or bound variables (like `for<'a>`). + +Trivial bounds are bounds that do not need further normalization to determine if they're well-formed or not. + +Consider the following: ```rust,ignore fn apartment_complex(block: T, name: String) where String: Clone { /* ... */ } --- -String: Clone // Trivial bound! We don't have to wfck T or any sub-terms to know this holds. +String: Clone // Trivial & Global bound! There's no aliases to resolve. // Maybe there's obligations on T but we don't care about them here. // ... ``` -This produces the trivial bound `String: Clone`. This is something we can check without instantiating any other information in this Item. We don't need to know any information about `T` to be able to make a judgment on the well-formedness of `String: Clone`. +This produces the global (no generic parameters), trivial (didn't require normalization to be well-formedness checked) bound `String: Clone`. This is something we can check without instantiating any other information in this Item. We don't need to know any information about `T` to be able to make a judgment on the well-formedness of `String: Clone`. False trivial bounds are things like: @@ -97,13 +101,17 @@ String: Copy // Trivial bound again, but this one is false! Here we have a trivial bound that does not hold, because `String` is not `Copy`. +#### Trivial Bounds Are Not Always Global + +Trivial Bounds are not a subset of Global Bounds. A trivial bound that isn't Global is `for<'a> String: Clone` (trivially true, has a bound variable) or `&'a str: Copy` (trivially false, has a generic parameter). + ## When We Don't Fully Do Well-Formedness Checking 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 -Trait objects of traits with where clauses / const generics do not undergo wfck until the type is coerced back into a concrete type. +Trait objects of traits with where clauses / const generics do not undergo well-formedness checking until the type is coerced back into a concrete type. ```rust,ignore trait Trait {} @@ -118,26 +126,34 @@ N = B // Substitution const B: usize + bool ``` -The above shouldn't compile, and yet it does. `foo`s const generic argument is a `bool`, while `Trait`'s is a `usize`. But because the wfck of trait objects doesn't happen until coercion into a concrete type, the above compiles just fine. - -### Binders / Higher-Ranked Bounds +The above shouldn't compile, but it does. `foo`s const generic argument is a `bool`, while `Trait`'s is a `usize`. But because the wfck of trait objects doesn't happen until coercion into a concrete type, the above compiles just fine. -HRBs also skip the wfck on their subjects. +### Higher-Ranked Bounds -TODO: bit of background of why this doesn't happen. +Higher-Ranked Bounds skip well-formedness checking, leaving well-formedness checking to when the bound is instantiated: ```rust,ignore let _: for<'a> fn(Vec<[&'a ()]>); --- // This doesn't end up being generated, because it happens within a HRB -[&'a ()]: Sized // slices aren't sized. +[&'a ()]: Sized // slices aren't sized, this would fail! ``` +A lot of unsoundness surrounds this behavior. See: [#25860](https://github.com/rust-lang/rust/issues/25860), [#84591](https://github.com/rust-lang/rust/issues/84591). + +Let's consider the following: + +```rust,ignore +for<'a, 'b> fn(&'a &'b ()) +``` + +TODO: Consider the above + ### Free Type Aliases The rhs of Free Type Aliases[^fta] do not go through a full wfck at the definition site, with the exception of shallowly "type checking" const generic parameters of the rhs. -This means the following _currently_ passes type checking, assuming you don't actually use it in a non-FTA Item: +The following free type alias passes type checking, at time of writing: ```rust,ignore type WorksButShouldNot = Vec; @@ -146,14 +162,29 @@ type WorksButShouldNot = Vec; str: Sized ``` -This shouldn't work, as `T: Sized`, `str: Sized` being implied by `Vec`, but because the rhs of a free type alias doesn't go through well-formedness checking unless it's used this doesn't error. +This shouldn't work, as both `T: Sized`, `str: Sized` are implied by `Vec`. This "passes" item-wfck because the rhs of a free type alias doesn't go through well-formedness checking _until it's used_. Item-wfck is **deferred until use** for this specific case. + +--- + +## Well-Formed or Wellformed? + +Prefer "well-formed" over "wellformed," as this is consistent with logic literature. This also gets abbreviated to WF in other parts of the dev guide / docs. + +## What Well-Formedness Isn't + +Well-formedness checking is not "number of parameters" or "parameter type" checking[^kind-checking]. Neither term well-formedness checking 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. + +Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). [^trait-solver]: Despite being called a trait solver, it solves other things too[^boxy]. [^fta]: Type aliases not associated with anything, i.e. a module-level `type Alias = Vec;`. [^boxy]: Boxy said so. TODO: don't have any of these references :) -[^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md) +[^lcnr]: Lcnr said so. TODO: don't have any of these references :) +[^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md). [^terms]: Type expressions? TODO: this needs to be nailed down, and maybe inserted into the glossary. [^terms-abbreviated]: Abbreviated as "Terms" on this page in some areas. +[^kind-checking]: AKA "kind checking", as we might see in languages like Haskell. +[^global-where-bound]: See: [next-gen trait solving candidate preferences](../solve/candidate-preference.md). [^hir-ty-lower]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/hir_ty_lowering/index.html [^tlt-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html [^item-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html diff --git a/src/appendix/glossary.md b/src/appendix/glossary.md index 30959f4b39..0c86ae391f 100644 --- a/src/appendix/glossary.md +++ b/src/appendix/glossary.md @@ -102,6 +102,7 @@ Term | Meaning trans 👎 | Short for _translation_, the code to translate MIR into LLVM IR. **Renamed to** [codegen](#codegen). `Ty` | The internal representation of a type. ([see more](../ty.md)) `TyCtxt` | The data structure often referred to as [`tcx`](#tcx) in code which provides access to session data and the query system. +Type-Level Term | Type terms we're reasoning about and manipulating in an analysis context. Comparable/related to type expressions etc. UFCS 👎 | Short for _universal function call syntax_, this is an unambiguous syntax for calling a method. **Term no longer in use!** Prefer _fully-qualified path / syntax_. ([see more](../hir-typeck/summary.md), [see the reference](https://doc.rust-lang.org/reference/expressions/call-expr.html#disambiguating-function-calls)) uninhabited type | A type which has _no_ values. This is not the same as a ZST, which has exactly 1 value. An example of an uninhabited type is `enum Foo {}`, which has no variants, and so, can never be created. The compiler can treat code that deals with uninhabited types as dead code, since there is no such value to be manipulated. `!` (the never type) is an uninhabited type. Uninhabited types are also called _empty types_. upvar | A variable captured by a closure from outside the closure. From 74621b9b5c543a584c095f25f74d8932d1ea28a1 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Wed, 17 Jun 2026 10:58:09 +0100 Subject: [PATCH 08/18] Expand trait objects some more --- src/analysis/well-formed.md | 39 ++++++++++++++++++++++++++++++++++--- 1 file changed, 36 insertions(+), 3 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 7424589b05..d1eeebb9ec 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -111,7 +111,40 @@ Well-formedness checking is not a coherent "stage" of type checking. It gets cal ### Trait Objects -Trait objects of traits with where clauses / const generics do not undergo well-formedness checking until the type is coerced back into a concrete type. +Trait objects of traits do not undergo well-formedness checking until the construction / coercion points of that trait object. That is, the following will compile because we don't have any point where we're constructing the trait object or coercing it back to a concrete type: + +```rust,ignore +trait Trait +where for<'a> [u8]: Sized {} + +fn foo(_: &dyn Trait) {} +--- +// This doesn't end up being generated, because it happens within a trait object. +[u8]: Sized +``` + +The above should not compile because `[u8]: Sized`, but this won't be checked until actual use: + +```rust +trait Trait +where for<'a> [u8]: Sized {} + +fn foo(_: &dyn Trait) {} + +// We still need to specify the bound here, otherwise `[u8]: Sized` _is_ +// checked as an obligation as a global bound. +impl Trait for u8 where for<'a> [u8]: Sized {} + +fn main() { + // But no matter what we do, this boundary between concrete type and trait + // object will produce the obligation `[u8]: Sized`, which will fail when + // handed over to the trait solver. + let object: Box = Box::new(42u8); + foo(&object); +} +``` + +This also applies to Const Generic Arguments in trait objects: ```rust,ignore trait Trait {} @@ -126,7 +159,7 @@ N = B // Substitution const B: usize + bool ``` -The above shouldn't compile, but it does. `foo`s const generic argument is a `bool`, while `Trait`'s is a `usize`. But because the wfck of trait objects doesn't happen until coercion into a concrete type, the above compiles just fine. +The above shouldn't compile, but it does. `foo`s const generic argument is a `bool`, while `Trait`'s is a `usize`. But because the well-formedness check of trait objects doesn't happen until we hit the boundary of concrete types, the above compiles just fine. ### Higher-Ranked Bounds @@ -147,7 +180,7 @@ Let's consider the following: for<'a, 'b> fn(&'a &'b ()) ``` -TODO: Consider the above +The above HRB implies `'b: 'a`, rather than two separate lifetimes. This is normal lifetime behavior, but we don't check it here. ### Free Type Aliases From d257f8067b2ca042b96a0d9f7325458326f1ce76 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 19 Jun 2026 15:33:12 +0100 Subject: [PATCH 09/18] Big editing pass --- src/analysis/well-formed.md | 114 +++++++++++++++++++++--------------- 1 file changed, 66 insertions(+), 48 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index d1eeebb9ec..c5b9732a20 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -1,36 +1,53 @@ # 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. +"Well-formedness" is 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?" These questions are then handed off to the trait solver to answer. -Items and Type-Level Terms[^terms][^terms-abbreviated] are "well formed" when they "follow rules" AKA "fulfill obligations" or "meet the necessary constraints." When we're doing a well-formedness check we're usually concerned about if Trait obligations are met, but this also covers obligations of the types broadly, including making sure that the types of const generic terms type check. +Items and Type-Level Terms are "well formed" when they "follow rules" AKA "fulfill obligations" or "meet the necessary constraints." When we're performing well-formedness checks we're usually concerned about if Trait obligations are met, but this also includes making sure that the types of const generic parameters "type check." There are two different forms of well-formedness checking: -- Type-Level Term[^terms] well-formedness check. +- **Type-Level Term**[^terms][^terms-abbreviated] well-formedness check. - Primary subject of "Well-Formedness Checking." - Abbreviated here to "Term well-formedness" or "Term well-formedness checking." - Not a distinct analysis pass. -- Items[^items] well-formedness check (item-wfck). +- **Item**[^items] well-formedness check (item-wfck.) - "Item-wfck" can call into "Term well-formedness checking" as Items contain Terms. - Inner "Terms" can get normalized first. + - Can be considered a more coherent "pass" in the compiler than "term well-formedness" (which is performed in many places.) -See: [What Well-Formedness Is Not](#what-well-formedness-isnt) +See: [What Well-Formedness Isn't](#what-well-formedness-isnt) ## Well-Formedness of Type-Level Terms -Type-Level Terms are the data structures that well-formedness checking is focused on analyzing. Item-wfck is one of the entry points where term well-formedness checking will get performed. +Type-Level Terms are the fundamental subject of well-formedness checking. We are also concerned with [Items](#well-formedness-of-items), but as a downstream consumer of type-level term well-formedness. -### Obligations +### Obligations for Well-Formedness -Term well-formedness begins with generating the list of things that need to be true for the term-being-checked to be well-formed. +Term well-formedness begins with generating a list of things that need to be true for a term to be well-formed. -These predicates end up being referred to as Obligations, Requirements, or Constraints. Preferred term is "obligations", as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal". +These predicates are referred to as Obligations, Requirements, or Constraints. Preferred term is "obligations", as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal." -The term well-formedness module[^tlt-wf-module] contains an `obligations` function that takes type-level terms and returns `PredicateObligations`, a list of obligations that Type-Level Term must satisfy in order to be well-formed. The satisfaction of those obligations is performed by the Trait Solver[^trait-solver], and if they are satisfied then the term is Well-Formed. +Specific obligations might be things like `String: Clone`, `A: usize`, or `::Item: Debug`. -### When Type-Level Terms Are Well Formed +This page shows the term/item and obligation split as: -Terms are Well-Formed when trait obligations within them are considered satisfied by the trait solver. As an example, the following is not well-formed: +```rust,ignore + +--- + +``` + +#### Determining Obligations + +In the compiler, obligations of terms are found through the `obligations` function in the well-formedness module[^tlt-wf-module]. + +#### Other Obligations + +Obligations are more than just trait and const generic bounds, but we've only mentioned these specific obligations so far as they are what we care about when we do "well-formedness checking". For example, lifetime bounds (`'b: 'a` / `'b` outlives `'a`) can be part of the obligation output but _is not relevant to well-formedness_. This information is saved to part of the compiler's internal state for later use, rather than used during well-formedness checks. See: [`PredicateKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.PredicateKind.html) and [`ClauseKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.ClauseKind.html) for a full list of obligations. + +### When Type-Level Terms Are Well-Formed + +Type-Level Terms are considered Well-Formed when trait obligations within them are satisfied by the trait solver. As an example, the following is not well-formed: ```rust,ignore Vec @@ -40,15 +57,15 @@ Vec where T: Sized Vec where str: Sized // This is not true, therefore the term is not well-formed. ``` -From term well-formedness we find the obligation for `Vec` that `T: Sized`. For `Vec` we encounter the obligation `str: Sized`, and as `str` is not `Sized` the term is not well-formed. +We find the obligation for `Vec` that `T: Sized`. For `Vec` we find the obligation `str: Sized`, which cannot be satisfied/is false. ### We Don't Need Normalization (Yet) -[Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type. A type alias is considered well-formed if its underlying type is well-formed. The underlying type is undergoes well-formedness checking at most definition and instantiation sites. +[Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type. A type alias is considered well-formed if its underlying type is well-formed. The underlying type undergoes well-formedness checking at most definition and instantiation sites, but there are exceptions. ### Const Generic Arguments -Term well-formedness is also responsible for getting "type-checking" obligations of const generic terms[^tyck-const-generics]. Let's look at the following use of const generics: +Term well-formedness is responsible for getting "type checking" obligations of const generic terms[^tyck-const-generics]. Let's look at the following use of const generics: ```rust,ignore fn use_const_generics() { /* ... */ } @@ -69,17 +86,18 @@ Items are a major entry point for term well-formedness. Because Items contain Te ### We (Sometimes) Need Normalization -Currently, there are places where normalization of an Item happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). +There are places where normalization of an Item happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). -### Global & Trivial Bounds +### Global and Trivial Bounds -Trait bounds are a common Obligation. + -Global bounds[^global-where-bound] are post-normalization bounds that don't contain any generic parameters (like `` or `'a`) or bound variables (like `for<'a>`). +Trait bounds are a common Obligation. Global and Trivial trait bounds are kinds of trait bounds where we already have enough information to determine if they are true or false. -Trivial bounds are bounds that do not need further normalization to determine if they're well-formed or not. +- **Global bounds** are post-normalization bounds that don't contain any generic parameters (like `` or `'a`) or bound variables (like `for<'b>`). +- **Trivial bounds** are bounds that do not need further normalization to determine if they're well-formed or not. -Consider the following: +Consider the following function definition: ```rust,ignore fn apartment_complex(block: T, name: String) where String: Clone { /* ... */ } @@ -89,9 +107,9 @@ String: Clone // Trivial & Global bound! There's no aliases to resolve. // ... ``` -This produces the global (no generic parameters), trivial (didn't require normalization to be well-formedness checked) bound `String: Clone`. This is something we can check without instantiating any other information in this Item. We don't need to know any information about `T` to be able to make a judgment on the well-formedness of `String: Clone`. +This produces a trait bound obligation `String: Clone` that is _Global_ (no generic parameters) and _Trivial_ (didn't require normalization to be well-formedness checked). The trait solver doesn't need to be given any additional information for it to be able to make a judgment on the well-formedness of `String: Clone`. -False trivial bounds are things like: +False trivial bounds are simply trivial bounds that do not hold. The following is a basic example: ```rust,ignore fn apartment_simple(block: T, name: String) where String: Copy { /* ... */ } @@ -111,12 +129,15 @@ Well-formedness checking is not a coherent "stage" of type checking. It gets cal ### Trait Objects -Trait objects of traits do not undergo well-formedness checking until the construction / coercion points of that trait object. That is, the following will compile because we don't have any point where we're constructing the trait object or coercing it back to a concrete type: +Trait objects do not undergo well-formedness checking except at the boundaries of coercion into being a trait object or being downcast into a concrete type. + +As an example, the following will compile because we don't have a point where we're constructing the trait object or coercing it back to a concrete type: ```rust,ignore trait Trait -where for<'a> [u8]: Sized {} - +where + for<'a> [u8]: Sized {} + fn foo(_: &dyn Trait) {} --- // This doesn't end up being generated, because it happens within a trait object. @@ -127,12 +148,13 @@ The above should not compile because `[u8]: Sized`, but this won't be checked un ```rust trait Trait -where for<'a> [u8]: Sized {} +where + for<'a> [u8]: Sized {} fn foo(_: &dyn Trait) {} // We still need to specify the bound here, otherwise `[u8]: Sized` _is_ -// checked as an obligation as a global bound. +// checked as an obligation. impl Trait for u8 where for<'a> [u8]: Sized {} fn main() { @@ -159,7 +181,7 @@ N = B // Substitution const B: usize + bool ``` -The above shouldn't compile, but it does. `foo`s const generic argument is a `bool`, while `Trait`'s is a `usize`. But because the well-formedness check of trait objects doesn't happen until we hit the boundary of concrete types, the above compiles just fine. +The above shouldn't compile, but it does. The const generic argument of `foo` is a `bool`, while `Trait`'s is a `usize`. But because the well-formedness check of trait objects doesn't happen until we hit the boundary of concrete types, the above compiles just fine. ### Higher-Ranked Bounds @@ -180,26 +202,24 @@ Let's consider the following: for<'a, 'b> fn(&'a &'b ()) ``` -The above HRB implies `'b: 'a`, rather than two separate lifetimes. This is normal lifetime behavior, but we don't check it here. +The above HRB implies `'b: 'a` (a lifetime bound), rather than two completely separate lifetimes. This is normal lifetime behavior, but during well-formedness checking we cannot prove that this bound is generally true[^horrible], so we skip it. ### Free Type Aliases -The rhs of Free Type Aliases[^fta] do not go through a full wfck at the definition site, with the exception of shallowly "type checking" const generic parameters of the rhs. +The right-hand side of Free Type Aliases[^fta] do not go through a full well-formedness check at the definition site, with the exception of shallowly[^shallow] "type checking" const generic parameters of the RHS. The following free type alias passes type checking, at time of writing: ```rust,ignore type WorksButShouldNot = Vec; --- -// This should fail! But we skip the rhs of free type aliases +// This should fail! But we skip the RHS of free type aliases str: Sized ``` -This shouldn't work, as both `T: Sized`, `str: Sized` are implied by `Vec`. This "passes" item-wfck because the rhs of a free type alias doesn't go through well-formedness checking _until it's used_. Item-wfck is **deferred until use** for this specific case. - ---- +This shouldn't work, as both `T: Sized`, `str: Sized` are implied by `Vec`. This "passes" item-wfck because the RHS of a free type alias doesn't go through well-formedness checking _until it's used_. Item-wfck is **deferred until use** for this specific case. -## Well-Formed or Wellformed? +## "Well-Formed" or "Wellformed"? Prefer "well-formed" over "wellformed," as this is consistent with logic literature. This also gets abbreviated to WF in other parts of the dev guide / docs. @@ -209,19 +229,17 @@ Well-formedness checking is not "number of parameters" or "parameter type" check Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). -[^trait-solver]: Despite being called a trait solver, it solves other things too[^boxy]. +[^shallow]: It does not look deeper than the first "level." +[^horrible]: Instead, this bound is checked during "MIR borrowck" when the lifetimes are instantiated. [^fta]: Type aliases not associated with anything, i.e. a module-level `type Alias = Vec;`. -[^boxy]: Boxy said so. TODO: don't have any of these references :) -[^lcnr]: Lcnr said so. TODO: don't have any of these references :) [^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md). -[^terms]: Type expressions? TODO: this needs to be nailed down, and maybe inserted into the glossary. +[^terms]: AKA Type expressions and subexpressions, but not in the sense of referring to a specific struct or enum in the rust compiler. See the [glossary](../appendix/glossary.md). [^terms-abbreviated]: Abbreviated as "Terms" on this page in some areas. [^kind-checking]: AKA "kind checking", as we might see in languages like Haskell. -[^global-where-bound]: See: [next-gen trait solving candidate preferences](../solve/candidate-preference.md). -[^hir-ty-lower]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/hir_ty_lowering/index.html -[^tlt-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html -[^item-wf-module]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html -[^wf-ctx-construction]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/fn.enter_wf_checking_ctxt.html -[^item-wf-ctx]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/struct.WfCheckingCtxt.html -[^item-wf-global-bounds]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/struct.WfCheckingCtxt.html#method.check_false_global_bounds -[^tyck-const-generics]: https://rustc-dev-guide.rust-lang.org/const-generics.html#checking-types-of-const-arguments \ No newline at end of file +[^hir-ty-lower]: +[^tlt-wf-module]: +[^item-wf-module]: +[^wf-ctx-construction]: +[^item-wf-ctx]: +[^item-wf-global-bounds]: +[^tyck-const-generics]: \ No newline at end of file From ce64f2f2fb721d6e4fd4d840665e76a9f82c3836 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 19 Jun 2026 16:30:11 +0100 Subject: [PATCH 10/18] boxy feedback --- src/analysis/well-formed.md | 38 +++++++++++++++++++------------------ 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index c5b9732a20..ef837c81ca 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -39,7 +39,7 @@ This page shows the term/item and obligation split as: #### Determining Obligations -In the compiler, obligations of terms are found through the `obligations` function in the well-formedness module[^tlt-wf-module]. +In the compiler, obligations of terms are found through the [`obligations`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/fn.obligations.html) function in the [term well-formedness module](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html). #### Other Obligations @@ -47,7 +47,7 @@ Obligations are more than just trait and const generic bounds, but we've only me ### When Type-Level Terms Are Well-Formed -Type-Level Terms are considered Well-Formed when trait obligations within them are satisfied by the trait solver. As an example, the following is not well-formed: +Type-Level Terms are considered Well-Formed when obligations within them are satisfied by the trait solver. As an example, the following is not well-formed: ```rust,ignore Vec @@ -80,7 +80,7 @@ The call site will provide us with the obligation `6: usize` during well-formedn ## 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. +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. Items are a major entry point for term well-formedness. Because Items contain Terms, item-wfck can invoke term well-formedness checking. @@ -92,10 +92,10 @@ There are places where normalization of an Item happens before its Terms have go -Trait bounds are a common Obligation. Global and Trivial trait bounds are kinds of trait bounds where we already have enough information to determine if they are true or false. +Trait bounds are a common Obligation. Global and Trivial trait bounds are kinds of trait bounds where we already have enough information to determine if they are true or false. Item-wfck is responsible for finding and checking these bounds. -- **Global bounds** are post-normalization bounds that don't contain any generic parameters (like `` or `'a`) or bound variables (like `for<'b>`). -- **Trivial bounds** are bounds that do not need further normalization to determine if they're well-formed or not. +- **Global bounds** are, in the old solver, post-normalization bounds that don't contain any generic parameters (like `` or `'a`) or bound variables (like `for<'b>`). +- **Trivial bounds** are bounds that do not need further normalization to determine if they're well-formed or not. Consider the following function definition: @@ -166,22 +166,19 @@ fn main() { } ``` -This also applies to Const Generic Arguments in trait objects: +This exception does not apply to Const Generic Arguments in trait objects: ```rust,ignore trait Trait {} fn foo(_: &dyn Trait) {} --- -// This doesn't end up being generated, because it happens within a trait object. const N: usize const B: bool N = B // Substitution -// This fails once we coerce out of a trait object to a concrete type. -// But because we don't coerce, it passes wfck. const B: usize + bool ``` -The above shouldn't compile, but it does. The const generic argument of `foo` is a `bool`, while `Trait`'s is a `usize`. But because the well-formedness check of trait objects doesn't happen until we hit the boundary of concrete types, the above compiles just fine. +The above doesn't compile, unlike the previous example we gave. We're doing _some_ well-formedness checking here when it comes to the const generic arguments. ### Higher-Ranked Bounds @@ -206,7 +203,7 @@ The above HRB implies `'b: 'a` (a lifetime bound), rather than two completely se ### Free Type Aliases -The right-hand side of Free Type Aliases[^fta] do not go through a full well-formedness check at the definition site, with the exception of shallowly[^shallow] "type checking" const generic parameters of the RHS. +The right-hand side of Free Type Aliases[^fta] do not go through a full well-formedness check at the definition site, with the exception of "type checking" const generic arguments in the RHS. The following free type alias passes type checking, at time of writing: @@ -214,11 +211,21 @@ The following free type alias passes type checking, at time of writing: type WorksButShouldNot = Vec; --- // This should fail! But we skip the RHS of free type aliases -str: Sized +str: Sized // Not generated ``` This shouldn't work, as both `T: Sized`, `str: Sized` are implied by `Vec`. This "passes" item-wfck because the RHS of a free type alias doesn't go through well-formedness checking _until it's used_. Item-wfck is **deferred until use** for this specific case. +```rust,ignore +pub struct Consty; +type Alias = Consty<42>; +--- +// This _is_ generated as an obligation, so this fails. +42: bool // Is generated! +``` + + + ## "Well-Formed" or "Wellformed"? Prefer "well-formed" over "wellformed," as this is consistent with logic literature. This also gets abbreviated to WF in other parts of the dev guide / docs. @@ -229,7 +236,6 @@ Well-formedness checking is not "number of parameters" or "parameter type" check Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). -[^shallow]: It does not look deeper than the first "level." [^horrible]: Instead, this bound is checked during "MIR borrowck" when the lifetimes are instantiated. [^fta]: Type aliases not associated with anything, i.e. a module-level `type Alias = Vec;`. [^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md). @@ -237,9 +243,5 @@ Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](.. [^terms-abbreviated]: Abbreviated as "Terms" on this page in some areas. [^kind-checking]: AKA "kind checking", as we might see in languages like Haskell. [^hir-ty-lower]: -[^tlt-wf-module]: [^item-wf-module]: -[^wf-ctx-construction]: -[^item-wf-ctx]: -[^item-wf-global-bounds]: [^tyck-const-generics]: \ No newline at end of file From 2c4522b2e61d2f7dad2706d561c81c8c8dda4850 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Wed, 24 Jun 2026 14:30:04 +0100 Subject: [PATCH 11/18] Another pass, minor re-ordering and some additions --- src/analysis/well-formed.md | 37 +++++++++++++++++++++++++++---------- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index ef837c81ca..a68348286e 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -1,15 +1,19 @@ -# Well-Formedness of Items and Type-Level Terms +# Well-Formedness -"Well-formedness" is 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?" These questions are then handed off to the trait solver to answer. +## What is Well-Formedness? -Items and Type-Level Terms are "well formed" when they "follow rules" AKA "fulfill obligations" or "meet the necessary constraints." When we're performing well-formedness checks we're usually concerned about if Trait obligations are met, but this also includes making sure that the types of const generic parameters "type check." +At a high level, "well-formed" just means "correctly built."[^wf-history] Something is _well-formed_ when its structure follows rules, and _ill-formed_ when those rules are broken. -There are two different forms of well-formedness checking: +## Well-Formedness in Rust + +Items and Type-Level Terms are "well-formed" when they "fulfill obligations" or "meet the necessary constraints." When we're performing well-formedness checks we're usually concerned about if Trait obligations are met, but this also includes making sure that the types of const generic parameters "type check." + +In the Rust compiler there are two different forms of well-formedness checking: - **Type-Level Term**[^terms][^terms-abbreviated] well-formedness check. - Primary subject of "Well-Formedness Checking." - Abbreviated here to "Term well-formedness" or "Term well-formedness checking." - - Not a distinct analysis pass. + - This isn't a distinct "analysis pass," this gets performed throughout the compiler. - **Item**[^items] well-formedness check (item-wfck.) - "Item-wfck" can call into "Term well-formedness checking" as Items contain Terms. - Inner "Terms" can get normalized first. @@ -19,7 +23,7 @@ See: [What Well-Formedness Isn't](#what-well-formedness-isnt) ## Well-Formedness of Type-Level Terms -Type-Level Terms are the fundamental subject of well-formedness checking. We are also concerned with [Items](#well-formedness-of-items), but as a downstream consumer of type-level term well-formedness. +Well-formedness of type-level terms is the area of analysis that produces questions like "does `T: Debug` hold true?" or "is this const generic parameter `const B: bool` being handed a value of the right type?" These questions are then handed off to the trait solver to answer. ### Obligations for Well-Formedness @@ -43,7 +47,7 @@ In the compiler, obligations of terms are found through the [`obligations`](http #### Other Obligations -Obligations are more than just trait and const generic bounds, but we've only mentioned these specific obligations so far as they are what we care about when we do "well-formedness checking". For example, lifetime bounds (`'b: 'a` / `'b` outlives `'a`) can be part of the obligation output but _is not relevant to well-formedness_. This information is saved to part of the compiler's internal state for later use, rather than used during well-formedness checks. See: [`PredicateKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.PredicateKind.html) and [`ClauseKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.ClauseKind.html) for a full list of obligations. +Obligations are more than just trait and const generic bounds, but we've only mentioned these specific obligations so far as they are what we care about when we do "well-formedness checking" of terms. For example, lifetime bounds (`'b: 'a` / `'b` outlives `'a`) can be part of the obligation output but _is not relevant to well-formedness of terms_. This information is saved to part of the compiler's internal state for later use, rather than used during well-formedness checks. See: [`PredicateKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.PredicateKind.html) and [`ClauseKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.ClauseKind.html) for a full list of obligations. ### When Type-Level Terms Are Well-Formed @@ -63,6 +67,10 @@ We find the obligation for `Vec` that `T: Sized`. For `Vec` we find the [Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type. A type alias is considered well-formed if its underlying type is well-formed. The underlying type undergoes well-formedness checking at most definition and instantiation sites, but there are exceptions. +### We (Sometimes) Need Normalization + +There are places where normalization of an [Item](#well-formedness-of-items) happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). + ### Const Generic Arguments Term well-formedness is responsible for getting "type checking" obligations of const generic terms[^tyck-const-generics]. Let's look at the following use of const generics: @@ -82,11 +90,11 @@ The call site will provide us with the obligation `6: usize` during well-formedn 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. -Items are a major entry point for term well-formedness. Because Items contain Terms, item-wfck can invoke term well-formedness checking. +Items are a major entry point for performing term well-formedness. Because Items contain Terms, item-wfck can invoke term well-formedness checking. -### We (Sometimes) Need Normalization +Item-wfck has more responsibilities than just collecting the obligations of its internal type-level terms and passing them to the trait solver. We do not talk about all of these here, but they can be found at the individual `check_*` functions in [the item-wfck module](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html). -There are places where normalization of an Item happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). + ### Global and Trivial Bounds @@ -123,6 +131,12 @@ Here we have a trivial bound that does not hold, because `String` is not `Copy`. Trivial Bounds are not a subset of Global Bounds. A trivial bound that isn't Global is `for<'a> String: Clone` (trivially true, has a bound variable) or `&'a str: Copy` (trivially false, has a generic parameter). +#### Item-Wfck and Trivial/Global Bounds + + + +When checking items are well-formed we will check that there are no trivially false global bounds. + ## When We Don't Fully Do Well-Formedness Checking 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. @@ -236,6 +250,9 @@ Well-formedness checking is not "number of parameters" or "parameter type" check Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). +Well-formedness in rust doesn't correspond to "correct syntax" as it does in logic. The term has a history of general use in a mathematical context of "follows a given set of rules." + +[^wf-history]: In linguistics this is "grammatically correct," in logic it is "syntactically correct," and in mathematician general use it can be seen as a more general "follows the rules we set for this domain." [^horrible]: Instead, this bound is checked during "MIR borrowck" when the lifetimes are instantiated. [^fta]: Type aliases not associated with anything, i.e. a module-level `type Alias = Vec;`. [^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md). From a05c960de079a81011dbef2dd332436f4def89e9 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Wed, 24 Jun 2026 14:50:23 +0100 Subject: [PATCH 12/18] Mention the historical context way at the bottom --- src/analysis/well-formed.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index a68348286e..c3b8101f2f 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -250,7 +250,7 @@ Well-formedness checking is not "number of parameters" or "parameter type" check Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](../borrow-check.md). -Well-formedness in rust doesn't correspond to "correct syntax" as it does in logic. The term has a history of general use in a mathematical context of "follows a given set of rules." +Well-formedness in the Rust compiler doesn't correspond to "correct syntax" as it does in logic. The term has a history of general use in a mathematical context of "follows a given set of rules." In Rust, our original usage was closer to "this thing is internally consistent" with respect to the bounds on a type in places such as the original [clarification on projections and well-formedness RFC](https://github.com/rust-lang/rfcs/blob/master/text/1214-projections-lifetimes-and-wf.md). [^wf-history]: In linguistics this is "grammatically correct," in logic it is "syntactically correct," and in mathematician general use it can be seen as a more general "follows the rules we set for this domain." [^horrible]: Instead, this bound is checked during "MIR borrowck" when the lifetimes are instantiated. From f6ab4dd2888759e6e36c432cbc94be12bec1898e Mon Sep 17 00:00:00 2001 From: Fallible Algebra <118682743+fallible-algebra@users.noreply.github.com> Date: Wed, 24 Jun 2026 15:48:48 +0100 Subject: [PATCH 13/18] Apply suggestions from code review Co-authored-by: Boxy --- src/analysis/well-formed.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index c3b8101f2f..cecc2c754f 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -15,8 +15,8 @@ In the Rust compiler there are two different forms of well-formedness checking: - Abbreviated here to "Term well-formedness" or "Term well-formedness checking." - This isn't a distinct "analysis pass," this gets performed throughout the compiler. - **Item**[^items] well-formedness check (item-wfck.) - - "Item-wfck" can call into "Term well-formedness checking" as Items contain Terms. - - Inner "Terms" can get normalized first. + - "Item-wfck" will often wind up requiring Terms be well-formed. + - Inner "Terms" can (incorrectly) get normalized first. - Can be considered a more coherent "pass" in the compiler than "term well-formedness" (which is performed in many places.) See: [What Well-Formedness Isn't](#what-well-formedness-isnt) @@ -90,7 +90,7 @@ The call site will provide us with the obligation `6: usize` during well-formedn 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. -Items are a major entry point for performing term well-formedness. Because Items contain Terms, item-wfck can invoke term well-formedness checking. +Items are a major source of checking well-formedness of terms. Because Items contain Terms, item-wfck must check that those terms are well formed. Item-wfck has more responsibilities than just collecting the obligations of its internal type-level terms and passing them to the trait solver. We do not talk about all of these here, but they can be found at the individual `check_*` functions in [the item-wfck module](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html). @@ -217,7 +217,7 @@ The above HRB implies `'b: 'a` (a lifetime bound), rather than two completely se ### Free Type Aliases -The right-hand side of Free Type Aliases[^fta] do not go through a full well-formedness check at the definition site, with the exception of "type checking" const generic arguments in the RHS. +The right-hand side of Free Type Aliases[^fta] is not fully checked to be well-formed at the definition site, only the types of const generic arguments in the RHS are checked. The following free type alias passes type checking, at time of writing: From 2f40e5939aba58fba121d5df1e7e3b913c1c5927 Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 26 Jun 2026 11:43:43 +0100 Subject: [PATCH 14/18] More edits --- src/analysis/well-formed.md | 73 +++++++++++++++++++++++-------------- 1 file changed, 45 insertions(+), 28 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index cecc2c754f..a07f0813ed 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -2,34 +2,30 @@ ## What is Well-Formedness? -At a high level, "well-formed" just means "correctly built."[^wf-history] Something is _well-formed_ when its structure follows rules, and _ill-formed_ when those rules are broken. +At a high level, "Well-formed" just means "correctly built."[^wf-history] Something is _well-formed_ when its structure follows rules. ## Well-Formedness in Rust -Items and Type-Level Terms are "well-formed" when they "fulfill obligations" or "meet the necessary constraints." When we're performing well-formedness checks we're usually concerned about if Trait obligations are met, but this also includes making sure that the types of const generic parameters "type check." - In the Rust compiler there are two different forms of well-formedness checking: - **Type-Level Term**[^terms][^terms-abbreviated] well-formedness check. - - Primary subject of "Well-Formedness Checking." - - Abbreviated here to "Term well-formedness" or "Term well-formedness checking." - - This isn't a distinct "analysis pass," this gets performed throughout the compiler. -- **Item**[^items] well-formedness check (item-wfck.) - - "Item-wfck" will often wind up requiring Terms be well-formed. + - Major subject of "Well-Formedness Checking." + - Also called "Term well-formedness" or "Term well-formedness checking." + - Not a distinct analysis stage, this gets performed throughout analysis. +- **Item**[^items] well-formedness check (item-wfck.) + - "Item-wfck" will often wind up requiring Terms be well-formed, but skips some areas. - Inner "Terms" can (incorrectly) get normalized first. - - Can be considered a more coherent "pass" in the compiler than "term well-formedness" (which is performed in many places.) + - More coherent as a stage in the compiler than "term well-formedness" (which is performed in many places.) -See: [What Well-Formedness Isn't](#what-well-formedness-isnt) +See: [What Well-Formedness Isn't](#what-well-formedness-isnt). ## Well-Formedness of Type-Level Terms -Well-formedness of type-level terms is the area of analysis that produces questions like "does `T: Debug` hold true?" or "is this const generic parameter `const B: bool` being handed a value of the right type?" These questions are then handed off to the trait solver to answer. - -### Obligations for Well-Formedness +Determining Term well-formedness begins with building a list of things that need to be true for a term to be well-formed. We call these "Obligations"[^obligations]. -Term well-formedness begins with generating a list of things that need to be true for a term to be well-formed. +Type-Level Terms are considered Well-Formed when obligations within them are satisfied by the trait solver. -These predicates are referred to as Obligations, Requirements, or Constraints. Preferred term is "obligations", as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal." +### Obligations for Well-Formedness Specific obligations might be things like `String: Clone`, `A: usize`, or `::Item: Debug`. @@ -41,35 +37,47 @@ This page shows the term/item and obligation split as: ``` -#### Determining Obligations - -In the compiler, obligations of terms are found through the [`obligations`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/fn.obligations.html) function in the [term well-formedness module](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html). - -#### Other Obligations +Here is an example of a well-formed type-level term: -Obligations are more than just trait and const generic bounds, but we've only mentioned these specific obligations so far as they are what we care about when we do "well-formedness checking" of terms. For example, lifetime bounds (`'b: 'a` / `'b` outlives `'a`) can be part of the obligation output but _is not relevant to well-formedness of terms_. This information is saved to part of the compiler's internal state for later use, rather than used during well-formedness checks. See: [`PredicateKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.PredicateKind.html) and [`ClauseKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.ClauseKind.html) for a full list of obligations. +```rust,ignore +Vec +--- +// Obligations to fulfill +Vec where T: Sized +// Trait solver says `String: Sized` is true, so this is well-formed. +Vec where String: Sized +``` -### When Type-Level Terms Are Well-Formed +When we run a search for obligations on `Vec`, we'll find that `Vec` generates the obligation `T: Sized`. We substitute `T` with `String` in `Vec`, so we find the obligation `String: Sized`. -Type-Level Terms are considered Well-Formed when obligations within them are satisfied by the trait solver. As an example, the following is not well-formed: +The following **is not** well-formed: ```rust,ignore Vec --- // Obligations to fulfill Vec where T: Sized -Vec where str: Sized // This is not true, therefore the term is not well-formed. +// Trait solver says `str: Sized` is not true, so this is not well-formed. +Vec where str: Sized ``` We find the obligation for `Vec` that `T: Sized`. For `Vec` we find the obligation `str: Sized`, which cannot be satisfied/is false. +#### Determining Obligations + +In the compiler, obligations of terms are found through the [`obligations`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/fn.obligations.html) function in the [term well-formedness module](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/traits/wf/index.html). + +#### Other Obligations + +Obligations are more than just trait and const generic bounds, but we've only mentioned these specific obligations so far as they are what we care about when we do "well-formedness checking" of terms. For example, lifetime bounds (`'b: 'a` / `'b` outlives `'a`) can be part of the obligation output but _is not relevant to well-formedness of terms_. This information is saved to part of the compiler's internal state for later use, rather than used during well-formedness checks. See: [`PredicateKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.PredicateKind.html) and [`ClauseKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.ClauseKind.html) for a full list of obligations. + ### We Don't Need Normalization (Yet) [Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type. A type alias is considered well-formed if its underlying type is well-formed. The underlying type undergoes well-formedness checking at most definition and instantiation sites, but there are exceptions. ### We (Sometimes) Need Normalization -There are places where normalization of an [Item](#well-formedness-of-items) happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). +There are places where normalization of an Item happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). ### Const Generic Arguments @@ -139,11 +147,11 @@ When checking items are well-formed we will check that there are no trivially fa ## When We Don't Fully Do Well-Formedness Checking -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. +Well-formedness checking is not a coherent "stage" of type checking. There are many areas where well-formedness checking is performed, and some areas where we skip over well-formedness checking due to limitations in what kinds of analysis we can currently perform. Ideally, we would never skip or defer well-formedness checking. ### Trait Objects -Trait objects do not undergo well-formedness checking except at the boundaries of coercion into being a trait object or being downcast into a concrete type. +We do not require the where clauses of trait objects to be well-formed when determining if that trait object is well-formed. These where clauses still need to be well-formed when coercing into/out of a trait object, but this remains a hole in well-formedness checking. As an example, the following will compile because we don't have a point where we're constructing the trait object or coercing it back to a concrete type: @@ -230,12 +238,16 @@ str: Sized // Not generated This shouldn't work, as both `T: Sized`, `str: Sized` are implied by `Vec`. This "passes" item-wfck because the RHS of a free type alias doesn't go through well-formedness checking _until it's used_. Item-wfck is **deferred until use** for this specific case. +For Const Generics we still do a small amount of well-formedness checking at the definition site of a free type alias. This is consistent with our current special-casing of const generic well-formedness checking when we skip over things like where bounds. + +This means that the following, despite being of a similar form to the above example, fails as it should: + ```rust,ignore pub struct Consty; type Alias = Consty<42>; --- // This _is_ generated as an obligation, so this fails. -42: bool // Is generated! +42: bool // This is generated! ``` @@ -244,6 +256,10 @@ type Alias = Consty<42>; Prefer "well-formed" over "wellformed," as this is consistent with logic literature. This also gets abbreviated to WF in other parts of the dev guide / docs. +## Informal Usage + +In conversation, contributors may refer to something as "well-formed" and not necessarily mean what we cover here because "well-formedness" is a general phrase associated with the correctness of formal structures. This isn't necessarily in error, but it should be looked out for. + ## What Well-Formedness Isn't Well-formedness checking is not "number of parameters" or "parameter type" checking[^kind-checking]. Neither term well-formedness checking 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. @@ -252,6 +268,7 @@ Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](.. Well-formedness in the Rust compiler doesn't correspond to "correct syntax" as it does in logic. The term has a history of general use in a mathematical context of "follows a given set of rules." In Rust, our original usage was closer to "this thing is internally consistent" with respect to the bounds on a type in places such as the original [clarification on projections and well-formedness RFC](https://github.com/rust-lang/rfcs/blob/master/text/1214-projections-lifetimes-and-wf.md). +[^obligations]: These get referred to as Obligations, Requirements, or Constraints in the documentation. Preferred term is "obligations", as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal." [^wf-history]: In linguistics this is "grammatically correct," in logic it is "syntactically correct," and in mathematician general use it can be seen as a more general "follows the rules we set for this domain." [^horrible]: Instead, this bound is checked during "MIR borrowck" when the lifetimes are instantiated. [^fta]: Type aliases not associated with anything, i.e. a module-level `type Alias = Vec;`. From 32eca49068994613c07e1b578441f69338226d1e Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 26 Jun 2026 13:06:59 +0100 Subject: [PATCH 15/18] More more edits --- src/analysis/well-formed.md | 29 +++++++++++++---------------- src/appendix/glossary.md | 2 +- 2 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index a07f0813ed..60551f89db 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -2,14 +2,15 @@ ## What is Well-Formedness? -At a high level, "Well-formed" just means "correctly built."[^wf-history] Something is _well-formed_ when its structure follows rules. +"Well-formed" means "correctly built."[^wf-history] Something is _well-formed_ when its structure follows rules. When we use this term in the Rust compiler we are concerned with establishing some kind of _internal consistency_. ## Well-Formedness in Rust +To check that something is well-formed is to perform a "Well-formedness check." + In the Rust compiler there are two different forms of well-formedness checking: - **Type-Level Term**[^terms][^terms-abbreviated] well-formedness check. - - Major subject of "Well-Formedness Checking." - Also called "Term well-formedness" or "Term well-formedness checking." - Not a distinct analysis stage, this gets performed throughout analysis. - **Item**[^items] well-formedness check (item-wfck.) @@ -21,15 +22,15 @@ See: [What Well-Formedness Isn't](#what-well-formedness-isnt). ## Well-Formedness of Type-Level Terms -Determining Term well-formedness begins with building a list of things that need to be true for a term to be well-formed. We call these "Obligations"[^obligations]. +Term well-formedness checking begins with building a list of things that need to be true for a term to be well-formed. We call these "Obligations"[^obligations]. Type-Level Terms are considered Well-Formed when obligations within them are satisfied by the trait solver. ### Obligations for Well-Formedness -Specific obligations might be things like `String: Clone`, `A: usize`, or `::Item: Debug`. +Specific obligations are things like `String: Clone`, `A: usize`, or `::Item: Debug`. -This page shows the term/item and obligation split as: +On this page we show the split between obligations and terms/items as: ```rust,ignore @@ -96,11 +97,9 @@ The call site will provide us with the obligation `6: usize` during well-formedn ## Well-Formedness of 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. - -Items are a major source of checking well-formedness of terms. Because Items contain Terms, item-wfck must check that those terms are well formed. +Items are, generally speaking, "Things that get defined." Item-wfck happens at the signature level for types and functions, methods, and definitions/implementations of traits. -Item-wfck has more responsibilities than just collecting the obligations of its internal type-level terms and passing them to the trait solver. We do not talk about all of these here, but they can be found at the individual `check_*` functions in [the item-wfck module](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html). +Item-wfck has more responsibilities than only collecting the obligations of its internal type-level terms and passing them to the trait solver. We do not talk about all of these here, but they can be found at the individual `check_*` functions in [**the item-wfck module**](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html). @@ -119,8 +118,7 @@ Consider the following function definition: fn apartment_complex(block: T, name: String) where String: Clone { /* ... */ } --- String: Clone // Trivial & Global bound! There's no aliases to resolve. -// Maybe there's obligations on T but we don't care about them here. -// ... +// There could be bligations on T but we don't care about them here. ``` This produces a trait bound obligation `String: Clone` that is _Global_ (no generic parameters) and _Trivial_ (didn't require normalization to be well-formedness checked). The trait solver doesn't need to be given any additional information for it to be able to make a judgment on the well-formedness of `String: Clone`. @@ -180,7 +178,7 @@ fn foo(_: &dyn Trait) {} impl Trait for u8 where for<'a> [u8]: Sized {} fn main() { - // But no matter what we do, this boundary between concrete type and trait + // No matter what we do, this boundary between concrete type and trait // object will produce the obligation `[u8]: Sized`, which will fail when // handed over to the trait solver. let object: Box = Box::new(42u8); @@ -246,7 +244,7 @@ This means that the following, despite being of a similar form to the above exam pub struct Consty; type Alias = Consty<42>; --- -// This _is_ generated as an obligation, so this fails. +// This *is* generated as an obligation, so this (correctly) fails. 42: bool // This is generated! ``` @@ -269,13 +267,12 @@ Well-formedness doesn't check or validate lifetimes, this is handled in [MIR](.. Well-formedness in the Rust compiler doesn't correspond to "correct syntax" as it does in logic. The term has a history of general use in a mathematical context of "follows a given set of rules." In Rust, our original usage was closer to "this thing is internally consistent" with respect to the bounds on a type in places such as the original [clarification on projections and well-formedness RFC](https://github.com/rust-lang/rfcs/blob/master/text/1214-projections-lifetimes-and-wf.md). [^obligations]: These get referred to as Obligations, Requirements, or Constraints in the documentation. Preferred term is "obligations", as this matches the suffix of the type and the names of relevant functions. In future, this may be superseded by the new solver's term "Goal." -[^wf-history]: In linguistics this is "grammatically correct," in logic it is "syntactically correct," and in mathematician general use it can be seen as a more general "follows the rules we set for this domain." +[^wf-history]: In linguistics this is "grammatically correct," in logic it is "syntactically correct," and in casual mathematician use it can be read as a more general "follows the rules we set for this domain." [^horrible]: Instead, this bound is checked during "MIR borrowck" when the lifetimes are instantiated. [^fta]: Type aliases not associated with anything, i.e. a module-level `type Alias = Vec;`. [^items]: "Definition" style things in rust, See the [glossary](../appendix/glossary.md). -[^terms]: AKA Type expressions and subexpressions, but not in the sense of referring to a specific struct or enum in the rust compiler. See the [glossary](../appendix/glossary.md). +[^terms]: AKA Type expressions and subexpressions in the general sense, not a specific struct or enum in the rust compiler. See the [glossary](../appendix/glossary.md). [^terms-abbreviated]: Abbreviated as "Terms" on this page in some areas. [^kind-checking]: AKA "kind checking", as we might see in languages like Haskell. [^hir-ty-lower]: -[^item-wf-module]: [^tyck-const-generics]: \ No newline at end of file diff --git a/src/appendix/glossary.md b/src/appendix/glossary.md index 0c86ae391f..527da87b7b 100644 --- a/src/appendix/glossary.md +++ b/src/appendix/glossary.md @@ -102,7 +102,7 @@ Term | Meaning trans 👎 | Short for _translation_, the code to translate MIR into LLVM IR. **Renamed to** [codegen](#codegen). `Ty` | The internal representation of a type. ([see more](../ty.md)) `TyCtxt` | The data structure often referred to as [`tcx`](#tcx) in code which provides access to session data and the query system. -Type-Level Term | Type terms we're reasoning about and manipulating in an analysis context. Comparable/related to type expressions etc. +Type-Level Term | An expression at the type level, such as a Type or Const Generic. UFCS 👎 | Short for _universal function call syntax_, this is an unambiguous syntax for calling a method. **Term no longer in use!** Prefer _fully-qualified path / syntax_. ([see more](../hir-typeck/summary.md), [see the reference](https://doc.rust-lang.org/reference/expressions/call-expr.html#disambiguating-function-calls)) uninhabited type | A type which has _no_ values. This is not the same as a ZST, which has exactly 1 value. An example of an uninhabited type is `enum Foo {}`, which has no variants, and so, can never be created. The compiler can treat code that deals with uninhabited types as dead code, since there is no such value to be manipulated. `!` (the never type) is an uninhabited type. Uninhabited types are also called _empty types_. upvar | A variable captured by a closure from outside the closure. From 4f7f5c3f017f08edcefffe7aea0e4f35f5154dbe Mon Sep 17 00:00:00 2001 From: Fallible Algebra <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 26 Jun 2026 14:40:08 +0100 Subject: [PATCH 16/18] Apply suggestions from code review Co-authored-by: Boxy --- src/analysis/well-formed.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 60551f89db..cae2b4ca6d 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -24,7 +24,7 @@ See: [What Well-Formedness Isn't](#what-well-formedness-isnt). Term well-formedness checking begins with building a list of things that need to be true for a term to be well-formed. We call these "Obligations"[^obligations]. -Type-Level Terms are considered Well-Formed when obligations within them are satisfied by the trait solver. +Type-Level Terms are considered Well-Formed when their associated obligations are satisfied by the trait solver. ### Obligations for Well-Formedness @@ -49,7 +49,7 @@ Vec where T: Sized Vec where String: Sized ``` -When we run a search for obligations on `Vec`, we'll find that `Vec` generates the obligation `T: Sized`. We substitute `T` with `String` in `Vec`, so we find the obligation `String: Sized`. +When we compute the obligations for `Vec`, we'll find that `Vec` generates the obligation `T: Sized`. We substitute `T` with `String` in `Vec`, so we find the obligation `String: Sized`. The following **is not** well-formed: @@ -149,7 +149,7 @@ Well-formedness checking is not a coherent "stage" of type checking. There are m ### Trait Objects -We do not require the where clauses of trait objects to be well-formed when determining if that trait object is well-formed. These where clauses still need to be well-formed when coercing into/out of a trait object, but this remains a hole in well-formedness checking. +We do not require the where clauses of trait objects to be well-formed when determining if that trait object is well-formed. These where clauses are proven when coercing into/out of a trait object, but this remains a hole in well-formedness checking. As an example, the following will compile because we don't have a point where we're constructing the trait object or coercing it back to a concrete type: From d787d68c989353091265de9a2b1dfbd11fc998ad Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 26 Jun 2026 14:41:56 +0100 Subject: [PATCH 17/18] more more more edits --- src/analysis/well-formed.md | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index cae2b4ca6d..92fe51050c 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -74,11 +74,9 @@ Obligations are more than just trait and const generic bounds, but we've only me ### We Don't Need Normalization (Yet) -[Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type. A type alias is considered well-formed if its underlying type is well-formed. The underlying type undergoes well-formedness checking at most definition and instantiation sites, but there are exceptions. +[Normalization](../normalization.md) is the process of resolving [type aliases](../normalization.md#aliases) into their underlying type. -### We (Sometimes) Need Normalization - -There are places where normalization of an Item happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). +A type alias is considered well-formed if its where clauses are satisfied. The underlying type undergoes well-formedness checking at most definition and instantiation sites, but there are exceptions. ### Const Generic Arguments @@ -99,6 +97,17 @@ The call site will provide us with the obligation `6: usize` during well-formedn Items are, generally speaking, "Things that get defined." Item-wfck happens at the signature level for types and functions, methods, and definitions/implementations of traits. +```rust,ignore +// The `Vec` is checked during item wfck +fn foo(_: Vec) { + // The `Vec<[u8]>` is not handled by item wfck as it's not in the signature + let _: Vec<[u8]> +} +--- +Vec: Sized // Generated +Vec<[u8]>: Sized // Not done at item-wfck. Done elsewhere. +``` + Item-wfck has more responsibilities than only collecting the obligations of its internal type-level terms and passing them to the trait solver. We do not talk about all of these here, but they can be found at the individual `check_*` functions in [**the item-wfck module**](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_hir_analysis/check/wfcheck/index.html). @@ -147,6 +156,10 @@ When checking items are well-formed we will check that there are no trivially fa Well-formedness checking is not a coherent "stage" of type checking. There are many areas where well-formedness checking is performed, and some areas where we skip over well-formedness checking due to limitations in what kinds of analysis we can currently perform. Ideally, we would never skip or defer well-formedness checking. +### We (Sometimes) Need Normalization + +There are places where normalization of an Item happens before its Terms have gone through well-formedness checking. This is considered problematic as doing so allows some terms to [bypass term well-formedness checking entirely](https://github.com/rust-lang/rust/issues/100041). + ### Trait Objects We do not require the where clauses of trait objects to be well-formed when determining if that trait object is well-formed. These where clauses are proven when coercing into/out of a trait object, but this remains a hole in well-formedness checking. From 05cda52eca58ec7c4ec0dcced923fbecb0ce5e6e Mon Sep 17 00:00:00 2001 From: Fallible <118682743+fallible-algebra@users.noreply.github.com> Date: Fri, 26 Jun 2026 15:44:24 +0100 Subject: [PATCH 18/18] more more more more edits --- src/analysis/well-formed.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/analysis/well-formed.md b/src/analysis/well-formed.md index 92fe51050c..49c9509fea 100644 --- a/src/analysis/well-formed.md +++ b/src/analysis/well-formed.md @@ -49,7 +49,7 @@ Vec where T: Sized Vec where String: Sized ``` -When we compute the obligations for `Vec`, we'll find that `Vec` generates the obligation `T: Sized`. We substitute `T` with `String` in `Vec`, so we find the obligation `String: Sized`. +When we compute the obligations for `Vec`, we'll find that `Vec` generates the obligation `T: Sized`. We substitute `T` with `String` in `Vec`, so we find the obligation `String: Sized` which the trait solver will determine to be satisfied. The following **is not** well-formed: @@ -62,7 +62,7 @@ Vec where T: Sized Vec where str: Sized ``` -We find the obligation for `Vec` that `T: Sized`. For `Vec` we find the obligation `str: Sized`, which cannot be satisfied/is false. +The above computes the obligation `T: Sized`, like before, but we substitute `T` for `str` in the instance of `Vec` finding the obligation `str: sized`. This obligation will be determined by the trait solver to be _unsatisfied_. #### Determining Obligations @@ -70,7 +70,7 @@ In the compiler, obligations of terms are found through the [`obligations`](http #### Other Obligations -Obligations are more than just trait and const generic bounds, but we've only mentioned these specific obligations so far as they are what we care about when we do "well-formedness checking" of terms. For example, lifetime bounds (`'b: 'a` / `'b` outlives `'a`) can be part of the obligation output but _is not relevant to well-formedness of terms_. This information is saved to part of the compiler's internal state for later use, rather than used during well-formedness checks. See: [`PredicateKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.PredicateKind.html) and [`ClauseKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.ClauseKind.html) for a full list of obligations. +Obligations are more than just trait and const generic bounds, but we've only mentioned these specific obligations so far as they are what we care about when we do "well-formedness checking" of terms. See: [`PredicateKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.PredicateKind.html) and [`ClauseKind`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_type_ir/predicate_kind/enum.ClauseKind.html) for a full list of obligations. ### We Don't Need Normalization (Yet) @@ -162,9 +162,9 @@ There are places where normalization of an Item happens before its Terms have go ### Trait Objects -We do not require the where clauses of trait objects to be well-formed when determining if that trait object is well-formed. These where clauses are proven when coercing into/out of a trait object, but this remains a hole in well-formedness checking. +We do not require the where clauses of trait objects to be well-formed when determining if that trait object is well-formed. These where clauses are proven when coercing into a trait object, but this remains a hole in well-formedness checking. -As an example, the following will compile because we don't have a point where we're constructing the trait object or coercing it back to a concrete type: +As an example, the following will compile because we don't have a point where we're constructing the trait object from a concrete type: ```rust,ignore trait Trait @@ -213,9 +213,9 @@ const B: usize + bool The above doesn't compile, unlike the previous example we gave. We're doing _some_ well-formedness checking here when it comes to the const generic arguments. -### Higher-Ranked Bounds +### Binders / Higher-Ranked Types -Higher-Ranked Bounds skip well-formedness checking, leaving well-formedness checking to when the bound is instantiated: +Binders / Higher-Ranked Types reduce the amount well-formedness checking we do on a term, leaving well-formedness checking to when the bound is instantiated: ```rust,ignore let _: for<'a> fn(Vec<[&'a ()]>); @@ -224,6 +224,8 @@ let _: for<'a> fn(Vec<[&'a ()]>); [&'a ()]: Sized // slices aren't sized, this would fail! ``` +Specifically, obligations involving variables from binders (`for<'a>`) are only checked when the binder is instantiated. Some things are stilled checked under the `for<'a>`, but we still skip a lot of things. + A lot of unsoundness surrounds this behavior. See: [#25860](https://github.com/rust-lang/rust/issues/25860), [#84591](https://github.com/rust-lang/rust/issues/84591). Let's consider the following: