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 1/6] 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 2/6] 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 3/6] 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 4/6] 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 5/6] 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 6/6] 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