document trait bounds and candidate preference behavior #7

lcnr · 2025-08-20T15:27:04Z

cc https://github.com/joshtriplett/project-goal-reference-expansion/issues/3

documents http://github.com/rust-lang/rust/pull/120752

would be nice for somebody to quickly skim over this to detect

things which still need to be defined
should be moved

how to talk about X

how to talk about relating higher ranked types. "instantiating the for of the subtype with inference variables and the for of the supertype with placeholders before relating them as normal" seems quite cumbersome. This is where using judgements/actual code is actually ncier than text.

concepts which I don't know how to avoid

rigid types: a type which cannot be normalized in teh current context, whose equality is implemented by equating the type constructor and then recursively their corresponding generic arguments

why useful: we normalize aliases until we encounter a rigid type constructor? either a rigid alias or an a non-alias

joshtriplett

A couple of nits and a question, but the overall structure and organization of this seems potentially reasonable.

src/trait-bounds.md

src/types.md

src/types/alias-types.md

src/trait-bounds.md

lcnr · 2025-09-17T11:28:03Z

🤷 idk how to make progress here, would be nice if someone could look over this again.

src/items/generics.md

jackh726

Okay, here are lot of a comments. I started to realize that I think this is still meant to be fairly "outline-y".

Overall, I'm feeling weird - I don't think describing how trait solving works is actually fitting well into the existing structure. The existing structure feels very "syntax-focused", but I think to describe well trait solving, we need to be able to describe more precisely the underlying formal procedures. It's not impossible, but it's hard.

jackh726 · 2025-10-31T12:57:32Z

src/items/generics.md

 }
 ```

+r[items.generics.instantiation]


This section feels hard :/

Do we define "instantiation" anywhere? I feel like could just be worded as

When using an item all occurrences of the its generics parameters are replaced with either the explicitly provided argument or a new inference variable.

Though, this is very imprecise, and kind of overlaps with other statements (e.g. items.fn.generics.mono).

(Quite note, but " with either the explicitly provided argument" isn't quite right? We substitute with all new inference variables, but some are later unified with known arguments? Certainly, there's a semantic identity and I think it's more clear to talk about it this way. I bring it up because I'll use it below.)

I almost kind of would expect a bit more of a baseline definition - what is monomorphization and that all generics must be defined for monomorphization to occur. Then, discuss how this happens: substitution. And for that, I would like go more technical (and, my example doesn't quite align with the technical wording we use elsewhere, but I imagine we want to it, just giving a rough example):

For an item with generic parameters `<P0..Pn>`, we define a _substitution_ `[S0, ..., Sn]` consisting of a new inference variable for each generic parameter. Then, occurrences of each parameter are substituted with the variable defined in the substitution: `P0 => S0, ..., Pn => Sn`. Explicitly provided arguments are unified with their respective inference variables.

jackh726 · 2025-10-31T13:02:09Z

src/items/generics.md

+r[items.generics.instantiation]
+When using an item its generic parameters have to get instantiated. This replaces all occurances of the parameter with either the explicitly provided argument or a new unconstrained inference variable.
+
+Instantiating the generic parameters of an item generally requires proving its where clauses.


Likely, the word "generally" here will want to be elaborated here - or the statement should be changed around a bit.

I could imagine us wanting to change this around a bit - focusing instead of what we want to ensure happens by proving its where clauses. I.e. what are the invariants we want to hold by proving its where clauses. Where clause solving during impl selection is also probably a specific thing we want to call out.

jackh726 · 2025-10-31T13:03:28Z

src/types/alias-types.md

+
+r[type.alias.rigid]
+
+Aliases might be treated as *rigid* in their current environment. In this case they behave like other types.


Definitely need to define what qualifies an alias as rigid, and what it means to "behave like other types"

jackh726 · 2025-10-31T13:06:56Z

src/types/alias-types.md

+r[type.alias.rigid]
+
+Aliases might be treated as *rigid* in their current environment. In this case they behave like other types.
+Their equality is structural, *rigid* aliases are only equal if both have the same type constructor and equal corresponding arguments.


I guess that second part is this. Wording here is a bit weird. I would kind of want to be more precise, but I'm wondering if this needs to be elsewhere in a more generic "type equality" section - where we define equality as the equality of both the type constructor and the pair-wise equality of the parameters.

jackh726 · 2025-10-31T13:07:29Z

src/types/alias-types.md

+r[type.alias.normalization]
+
+Alias types can be normalized to their underlying type.
+- for associated types this is the type provided by the corresponding impl


Certainly this could use a concrete code example.

jackh726 · 2025-10-31T13:11:57Z

src/trait-bounds.md

+
+Bounds which does not use the item's parameters or any higher-ranked lifetimes are considered global.
+
+An error is emitted if a global bound cannot be satisfied in an empty environment.


I'd probably reword this like:

"Global bounds must be satisfiable without relying on any where clauses."

jackh726 · 2025-10-31T13:14:09Z

src/trait-bounds.md

+
+r[bound.satisfaction.alias-bounds]
+
+If an alias type is rigid in the current environment, trait bounds using this alias as a self type can be satisfied by using its item bounds.


Oh, these are some of the code examples I had mentioned above. Would probably want to see this discussed outside of a "when an alias is rigid" example.

jackh726 · 2025-10-31T13:15:06Z

src/trait-bounds.md

+
+r[bound.satisfaction.candidate-preference]
+
+> This is purely descriptive. Candidate preference behavior may change in future releases and must not be relied upon for correctness or soundness.


Ah, great! Probably should just link the other section to this, then split this across aliases and trait bounds.

jackh726 · 2025-10-31T13:21:33Z

src/types.md

+Equality and subtyping of types is generally structural; if the outermost type constructors are the same,
+their corresponding generic arguments are pairwise compared. We say types with this equality behavior are *rigid*. The only exceptions from this rule are higher ranked types and alias types.


Hmm, okay, this is sort of what I meant in a previous comment on wanting to see this split out.

I'd probably just rephrase this as:

Two types are structurally equal if the following conditions are met: - their type constructors are the same - each generic parameter are pair-wise structurally equal

(q: is this second point too strong - do we structurally equate parameters, or do general equality?)

We say types with this equality behavior are rigid.

Kind of weird use of this terminology, but I guess not incorrect. It's pretty confusing that we refer to this as both "rigid" and "structural". We should probably decide on the precise definitions of these as a team.

The only exceptions from this rule are higher ranked types and alias types.

This probably deserves to be in an "intro" paragraph (and leave the definition of structural equality as it's own paragraph.

jackh726 · 2025-10-31T13:23:14Z

src/types.md

+
+r[types.equality.higher-ranked.eq]
+
+Equality is checked by both instantiating the `for` of the lhs with inference variables and the `for` of the rhs with placeholders before equating them, and also doing the opposite.


Do we define "placeholders" anywhere? I'm really afraid that these are kind of "just" words without a lot of "meaning" of what someone unfamiliar without the specifics of how our type system works would understand.

cool beans

68681fc

lcnr force-pushed the trait-bounds branch from fb35c66 to 68681fc Compare August 20, 2025 15:29

joshtriplett reviewed Aug 23, 2025

View reviewed changes

src/trait-bounds.md Outdated Show resolved Hide resolved

src/types.md Outdated Show resolved Hide resolved

src/types/alias-types.md Outdated Show resolved Hide resolved

nyaa

943f00c

lcnr commented Sep 10, 2025

View reviewed changes

src/trait-bounds.md Outdated Show resolved Hide resolved

Update src/trait-bounds.md

ec3a91d

lcnr commented Sep 17, 2025

View reviewed changes

src/trait-bounds.md Outdated Show resolved Hide resolved

rarw

7e3c7a8

lcnr commented Oct 17, 2025

View reviewed changes

src/items/generics.md Outdated Show resolved Hide resolved

Apply suggestion from @lcnr

24d0c28

jackh726 reviewed Oct 31, 2025

View reviewed changes


		r[type.alias.rigid]

		Aliases might be treated as rigid in their current environment. In this case they behave like other types.


		Bounds which does not use the item's parameters or any higher-ranked lifetimes are considered global.

		An error is emitted if a global bound cannot be satisfied in an empty environment.


		r[bound.satisfaction.alias-bounds]

		If an alias type is rigid in the current environment, trait bounds using this alias as a self type can be satisfied by using its item bounds.


		r[bound.satisfaction.candidate-preference]

		> This is purely descriptive. Candidate preference behavior may change in future releases and must not be relied upon for correctness or soundness.

		Equality and subtyping of types is generally structural; if the outermost type constructors are the same,
		their corresponding generic arguments are pairwise compared. We say types with this equality behavior are rigid. The only exceptions from this rule are higher ranked types and alias types.


		r[types.equality.higher-ranked.eq]

		Equality is checked by both instantiating the `for` of the lhs with inference variables and the `for` of the rhs with placeholders before equating them, and also doing the opposite.

document trait bounds and candidate preference behavior #7

Are you sure you want to change the base?

document trait bounds and candidate preference behavior #7

Uh oh!

Conversation

lcnr commented Aug 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

how to talk about X

concepts which I don't know how to avoid

Uh oh!

joshtriplett left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

lcnr commented Sep 17, 2025

Uh oh!

Uh oh!

jackh726 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

lcnr commented Aug 20, 2025 •

edited

Loading