Skip to content
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

inductive cycles as ambig causes unintended breakage #114

Closed
lcnr opened this issue May 22, 2024 · 5 comments · Fixed by rust-lang/rust#137314
Closed

inductive cycles as ambig causes unintended breakage #114

lcnr opened this issue May 22, 2024 · 5 comments · Fixed by rust-lang/rust#137314
Assignees

Comments

@lcnr
Copy link
Contributor

lcnr commented May 22, 2024

trait Trait {
    type Item;
}

fn foo<A: Trait, B: Trait>()
where
    A::Item: Trait<Item = u32>,
    B::Item: Trait<Item = i32>,
{}

this should compile but fails with

error[E0283]: type annotations needed: cannot satisfy `<A as Trait>::Item: Trait`
 --> <source>:7:14
  |
7 |     A::Item: Trait<Item = u32>,
  |              ^^^^^^^^^^^^^^^^^
  |

The underlying issue is trying to prove <A as Trait>::Item: Trait normalizes the self type:

  • normalizes-to(<A as Trait>::Item)
    • candidate A::Item: Trait<Item = u32>
      • alias-relate(A::Item, A)
        • normalizes-to(<A as Trait>::Item) inductive cycle
    • candidate B::Item: Trait<Item = i32>
      • alias-relate(B::Item, A)
        • normalizes-to(<B as Trait>::Item)
          • candidate A::Item: Trait<Item = u32>
            • alias-relate(A::Item, B)
              • normalizes-to(<A as Trait>::Item) inductive cycle
          • candidate B::Item: Trait<Item = i32>
            • alias-relate(B::Item, B)
              • normalizes-to(<B as Trait>::Item) inductive cycle
@lcnr
Copy link
Contributor Author

lcnr commented May 22, 2024

original test by @aliemjay ❤️

pub trait ParallelIterator {
    type Item;
}

impl<T> ParallelIterator for T {
    type Item = u32;
}

trait Trait {}

impl<A, B> Trait for (A, B) where
    //~^ type annotations needed: cannot satisfy `<<A as ParallelIterator>::Item as ParallelIterator>::Item == u32`
    A: ParallelIterator,
    A::Item: ParallelIterator<Item = u32>,
    B: ParallelIterator,
    B::Item: ParallelIterator<Item = u32>,
{}


fn main() {}

@lcnr
Copy link
Contributor Author

lcnr commented May 22, 2024

this is the underlying reason for #111, closing that issue

trait Trait<'a> {
    type Assoc;
}

fn foo<'a, T: Trait<'a>>()
where
    T::Assoc: Trait<'a>,
{}

this may also be the root cause of #89

@lcnr
Copy link
Contributor Author

lcnr commented Feb 3, 2025

This affects nalgebra, thx @lqd for the minimization:

pub trait DimMin<D> {
    type Output;
}
pub fn repro<R: DimMin<C>, C>()
where
    <R as DimMin<C>>::Output: DimMin<C, Output = <R as DimMin<C>>::Output>,
{
}

@lcnr lcnr moved this from potentially irrelevant to unknown in -Znext-solver=globally Feb 3, 2025
@lcnr lcnr self-assigned this Feb 3, 2025
@lcnr lcnr moved this from unknown to in progress in -Znext-solver=globally 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`
@lcnr
Copy link
Contributor Author

lcnr commented Feb 18, 2025

also causes an ICE when normalizing for implied bounds fails:

  • tests/ui/associated-type-bounds/hrtb.rs
trait I<'a, 'b, 'c> {
    type As;
}
trait H<'d, 'e>: for<'f> I<'d, 'f, 'e> + 'd {}

struct X<'x, 'y> {
    x: std::marker::PhantomData<&'x ()>,
    y: std::marker::PhantomData<&'y ()>,
}

fn foo5<T>()
where
    T: for<'l, 'i> H<'l, 'i, As: for<'j> H<'j, 'i, As: for<'k> H<'j, 'k, As = X<'j, 'k>> + 'j> + 'i>
{
}

fn main() {}

@lcnr
Copy link
Contributor Author

lcnr commented Feb 18, 2025

also affects, in general this issue gets avoided by the old solver as its param_env normalization doesn't handle normalizeable aliases correctly

  • tests/ui/associated-type-bounds/supertrait-defines-ty.rs

jieyouxu added a commit to jieyouxu/rust that referenced this issue Mar 10, 2025
…ompiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? `@compiler-errors` `@nikomatsakis`
jieyouxu added a commit to jieyouxu/rust that referenced this issue Mar 10, 2025
…ompiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? ``@compiler-errors`` ``@nikomatsakis``
jieyouxu added a commit to jieyouxu/rust that referenced this issue Mar 11, 2025
…ompiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? ```@compiler-errors``` ```@nikomatsakis```
jieyouxu added a commit to jieyouxu/rust that referenced this issue Mar 11, 2025
…ompiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? ````@compiler-errors```` ````@nikomatsakis````
jieyouxu added a commit to jieyouxu/rust that referenced this issue Mar 12, 2025
…ompiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? `````@compiler-errors````` `````@nikomatsakis`````
jieyouxu added a commit to jieyouxu/rust that referenced this issue Mar 12, 2025
…ompiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? ``````@compiler-errors`````` ``````@nikomatsakis``````
matthiaskrgr added a commit to matthiaskrgr/rust that referenced this issue Mar 12, 2025
…ompiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? ```````@compiler-errors``````` ```````@nikomatsakis```````
rust-timer added a commit to rust-lang-ci/rust that referenced this issue Mar 12, 2025
Rollup merge of rust-lang#137314 - lcnr:cycles-with-unknown-kind, r=compiler-errors

change definitely unproductive cycles to error

builds on top of rust-lang#136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? ````````@compiler-errors```````` ````````@nikomatsakis````````
@lcnr lcnr moved this from in progress to done in -Znext-solver=globally Mar 13, 2025
github-actions bot pushed a commit to rust-lang/miri that referenced this issue Mar 14, 2025
…rrors

change definitely unproductive cycles to error

builds on top of #136824 by adding a third variant to `PathKind` for paths which may change to be coinductive in the future but must not be so right now. Most notably, impl where-clauses of not yet coinductive traits.

With this, we can change cycles which are definitely unproductive to a proper error. This fixes rust-lang/trait-system-refactor-initiative#114. This does not affect stable as we keep these cycles as ambiguous during coherence.

r? ````````@compiler-errors```````` ````````@nikomatsakis````````
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Development

Successfully merging a pull request may close this issue.

1 participant