solver cycles are coinductive once they have one coinductive step by lcnr · Pull Request #136824 · rust-lang/rust (original) (raw)
Implements the new cycle semantics in the new solver, dealing with the fallout from rust-lang/trait-system-refactor-initiative#10.
The first commit has been extensively fuzzed via https://github.com/lcnr/search_graph_fuzz.
A trait solver cycle is now coinductive if it has at least one coinductive step. A step is only considered coinductive if it's a where-clause of an impl of a coinductive trait. The only coinductive traits are Sized and auto traits.
This differs from the current stable because where a cycle had to consist of exclusively coinductive goals. This is overly limiting and wasn't properly enforced as it (mostly) ignored all non-trait goals.
A more in-depth explanation of my reasoning can be found in this separate doc: https://gist.github.com/lcnr/c49d887bbd34f5d05c36d1cf7a1bf5a5. A summary:
- imagine using dictionary passing style: map where-bounds to additional "dictonary" fn arguments instead of monomorphization
- impls are the only source of truth and introduce a constructor of the dictionary type
- a trait goal holds if mapping its proof tree to dictionary passing style results in a valid corecursive function
- a corecursive function is valid if it is guarded: matching on it should result in a constructor in a finite amount of time. This property should recursively hold for all fields of the constructor
- a function is guarded if the recursive call is behind a constructor
- and this constructor is not moved out of, e.g. by accessing a field of the dictionary
- the "not moved out of" condition is difficult to guarantee in general, e.g. for item bounds of associated types. However, there is no way to move out of an auto trait as there is no information you can get from the inside of an auto trait bound in the trait system
- if we encounter a cycle/recursive call which involves an auto trait, we can always convert the proof tree into a non-recursive function which calls a corecursive function whose first step is the construction of the auto trait dict and which only recursively depends on itself (by inlining the original function until they reach the uses of the auto trait)
we can therefore make any cycle during which we step into an auto trait (or Sized) impl coinductive
To fix rust-lang/trait-system-refactor-initiative#10 we could go with a more restrictive version which tries to restrict cycles to only allow code already supported on stable, potentially forcing cycles to be ambiguous if they step through an impl-where clause of a non-coinductive trait.
PathKind should be a strictly ordered set to allow merging paths without worry. We could therefore add another variant PathKind::ForceUnknown which is greater than PathKind::Coinductive. We already have to add such a third PathKind in #137314 anyways.
I am not doing this here due to multiple reasons:
- I cannot think of a principled reason why cycles using an impl to normalize differ in any way from simply using that impl to prove a trait bound. It feels unnecessary and like it makes it more difficult to reason about our cycle semantics :<
- This PR does not affect stable as coherence doesn't care about whether a goal holds or is ambiguous. So we don't yet have to make a final decision