Skip to content

Make inductive cycles always ambiguous#122791

Merged
bors merged 3 commits intorust-lang:masterfrom
compiler-errors:make-coinductive-always
Apr 3, 2024
Merged

Make inductive cycles always ambiguous#122791
bors merged 3 commits intorust-lang:masterfrom
compiler-errors:make-coinductive-always

Conversation

@compiler-errors
Copy link
Copy Markdown
Contributor

@compiler-errors compiler-errors commented Mar 20, 2024

This makes inductive cycles always result in ambiguity rather than be treated like a stack-dependent error.

This has some interactions with specialization, and so breaks a few UI tests that I don't agree should've ever worked in the first place, and also breaks a handful of crates in a way that I don't believe is a problem.

On the bright side, it puts us in a better spot when it comes to eventually enabling coinduction everywhere.

Results

This was cratered in #116494 (comment), which boils down to two regressions:

  • lu_packets - This code should have never compiled in the first place. More below.
  • ALL other regressions are due to commit_verify@0.11.0-beta.1 (edit: and commit_verify@0.10.x) - This actually seems to be fixed in version 0.11.0-beta.5, which is the most up to date version, but it's still prerelease on crates.io so I don't think cargo ends up picking beta.5 when building dependent crates.

lu_packets

Firstly, this crate uses specialization, so I think it's automatically worth breaking. However, I've minimized the regression to:

// Upstream crate
pub trait Serialize {}
impl Serialize for &() {}
impl<S> Serialize for &[S] where for<'a> &'a S: Serialize {}

// ----------------------------------------------------------------------- //

// Downstream crate
#![feature(specialization)]
#![allow(incomplete_features, unused)]

use upstream::Serialize;

trait Replica {
    fn serialize();
}

impl<T> Replica for T {
    default fn serialize() {}
}

impl<T> Replica for Option<T>
where
    for<'a> &'a T: Serialize,
{
    fn serialize() {}
}

Specifically this fails when computing the specialization graph for the downstream crate.

The code ends up cycling on &[?0]: Serialize when we equate &?0 = &[?1] during impl matching, which ends up needing to prove &[?1]: Serialize, which since cycles are treated like ambiguity, ends up in a fatal overflow. For some reason this requires two crates, squashing them into one crate doesn't work.

Side-note: This code is subtly order dependent. When minimizing, I ended up having the code start failing on nightly very easily after removing and reordering impls. This seems to me all the more reason to remove this behavior altogether.

Side-note: Item Bounds (edit: this was fixed independently in #121123)

Due to the changes in #120584 where we now consider an alias's item bounds and all the item bounds of the alias's nested self type aliases, I've had to add e6b64c6 which is a hack to make sure we're not eagerly normalizing bounds that have nothing to do with the predicate we're trying to solve, and which result in.

This is fixed in a more principled way in #121123.


r? lcnr for an initial review

Loading
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

disposition-merge This issue / PR is in PFCP or FCP with a disposition to merge it. finished-final-comment-period The final comment period is finished for this PR / Issue. merged-by-bors This PR was explicitly merged by bors. S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. T-types Relevant to the types team, which will review and decide on the PR/issue.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Order-dependence of dyn Trait: Supertrait goals causes incompleteness (old solver)

10 participants