Skip to content

projection obligations were accepted in - otherwise coinductive - global cycles #10

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
lcnr opened this issue Apr 17, 2023 · 3 comments · Fixed by rust-lang/rust#136824

Comments

@lcnr
Copy link
Contributor

lcnr commented Apr 17, 2023

rust-lang/rust#106040

While theoretically breaking, people tend to not write trait impls like that 😁

@lcnr
Copy link
Contributor Author

lcnr commented Mar 14, 2024

this does not impact coherence, as it only changes results from OK to Ambig without changing the resulting constraints. coherence only checks for goals which are known to not hold.

@compiler-errors
Copy link
Member

compiler-errors commented Apr 23, 2024

tests/ui/sized/coinductive-2.rs

//@ run-pass
struct Node<C: CollectionFactory<Self>> {
    _children: C::Collection,
}

trait CollectionFactory<T> {
    type Collection;
}

impl<T> CollectionFactory<T> for Vec<()> {
    type Collection = Vec<T>;
}

trait Collection<T>: Sized { //~ WARN trait `Collection` is never used
    fn push(&mut self, v: T);
}

impl<T> Collection<T> for Vec<T> {
    fn push(&mut self, v: T) {
        self.push(v)
    }
}

fn main() {
    let _ = Node::<Vec<()>> {
        _children: Vec::new(),
    };
}

@lcnr
Copy link
Contributor Author

lcnr commented Jan 21, 2025

affected test

  • tests/ui/sized/coinductive-1-gat.rs
  • tests/ui/sized/coinductive-1.rs
  • tests/ui/sized/coinductive-2.rs
  • tests/ui/traits/issue-82830.rs
  • tests/ui/traits/solver-cycles/129541-recursive-struct-and-array-impl.rs
  • tests/ui/traits/solver-cycles/129541-recursive-struct.rs

@lcnr lcnr moved this to unknown in -Znext-solver=globally Jan 29, 2025
@lcnr lcnr changed the title projection obligations were accepted in - otherwise coinductive - global cycles projection obligations were accepted in - otherwise coinductive - global cycles Jan 29, 2025
@lcnr lcnr moved this from unknown to in progress in -Znext-solver=globally Feb 10, 2025
@lcnr lcnr self-assigned this Feb 10, 2025
bors added a commit to rust-lang-ci/rust that referenced this issue Feb 13, 2025
solver cycles are coinductive once they have one coinductive step

Implements the new cycle semantics in the new solver, dealing with the fallout from rust-lang/trait-system-refactor-initiative#10.

I am currently also changing inductive cycles back to an error instead of ambiguity outside of coherence to deal with rust-lang/trait-system-refactor-initiative#114. This should allow nalgebra to compile without affecting anything on stable. Whether a cycle results in ambiguity or success should not matter for coherence, as it only checks for errors.

The first commit has been extensively fuzzed via https://github.com/lcnr/search_graph_fuzz.

TODO:
- [ ] fix issues from https://hackmd.io/JsblAvk4R5y30niSNQVYeA
- [ ] add ui tests
- [ ] explain this approach and why we believe it to be correct

r? `@compiler-errors` `@nikomatsakis`
rust-timer added a commit to rust-lang-ci/rust that referenced this issue Feb 28, 2025
Rollup merge of rust-lang#136824 - lcnr:yeet, r=compiler-errors

solver cycles are coinductive once they have one coinductive step

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 rust-lang#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

r? `@compiler-errors` `@nikomatsakis`
@lcnr lcnr moved this from in progress to done in -Znext-solver=globally Mar 5, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
Development

Successfully merging a pull request may close this issue.

2 participants