Skip to content

-Ztrait-solver=next: deduplicate region constraints in query responses #109764

Closed
@lcnr

Description

@lcnr
pub struct Bar
where
    for<'a> &'a mut Self:;

fn main() {}

results in overflow in the new solver when checking WF(Bar) or `for<'a> WF(&'a mut Bar). The issue is as follows:

pub struct Bar
where
    for<'a> &'a mut Bar:;
  • for<'a> WF(&'a mut Bar) (attempt 0)
    • WF(&'a.1 mut Bar)
      • outlives(Bar, 'a.1) OK [Bar: 'a.1]
      • WF(Bar)
        • for<'a> WF(&'a mut Bar) cycle OK []
    • RESULT: OK [Bar: 'a.1]
  • for<'a> WF(&'a mut Bar) (attempt 1)
    • WF(&'a.1 mut Bar)
      • outlives(Bar, 'a.1) OK [Bar: 'a.1]
      • WF(Bar)
        • for<'a> WF(&'a mut Bar) cycle OK [Bar: 'a.2] (create new universe)
    • RESULT: OK [Bar: 'a.1, Bar: 'a.2]
  • for<'a> WF(&'a mut Bar) (attempt 2)
    • WF(&'a.1 mut Bar)
      • outlives(Bar, 'a.1) OK [Bar: 'a.1]
      • WF(Bar)
        • for<'a> WF(&'a mut Bar) cycle OK [Bar: 'a.2, Bar: 'a.3] (create new universe)
    • RESULT: OK [Bar: 'a.1, Bar: 'a.2, Bar: 'a.3]

starting with WF(BAR)

  • WF(Bar) iteration 0
    • for<'a> WF(&'a mut Bar)
      • WF(&'a.1 mut Bar)
        • outlives(Bar, 'a.1) OK [Bar: 'a.1]
        • WF(Bar) cycle OK []
  • WF(Bar) iteration 1
    • for<'a> WF(&'a mut Bar)
      • WF(&'a.1 mut Bar)
        • outlives(Bar, 'a.1) OK [Bar: 'a.1]
        • WF(Bar) cycle OK [Bar: 'a.?]

a similar issue is:

struct Foo
where
    Foo:,
    for<'a> &'a ():;
  • WF(Foo) iteration 0
    • WF(Foo) cycle OK []
    • for<'a> WF(&'a ()) OK [(): 'a.1] (new universe for unnameable placeholder)
    • result OK [(): 'a.1]
  • WF(Foo) iteration 1 (in new infcx)
    • WF(Foo) cycle OK [(): 'a.1] (new universe for unnameable placeholder)
    • for<'a> WF(&'a ()) OK [(): 'a.2] (new universe for unnameable placeholder)
    • result OK [(): 'a.1, (): 'a.2] yikes (have to rerun again)

The long term plan to solve this is to eagerly deal with new placeholders in the solver, short term we probably want to somehow deduplicate new placeholder constraints when creating the query response we're going to ignore this because hopefully this pattern does not exist in user-code.

Metadata

Metadata

Assignees

Labels

A-coinductionArea: Concerning coinduction, most often for auto traitsA-trait-systemArea: Trait systemT-compilerRelevant to the compiler team, which will review and decide on the PR/issue.WG-trait-system-refactorThe Rustc Trait System Refactor Initiative (-Znext-solver)

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions