Auto merge of #98542 - jackh726:coinductive-wf, r=oli-obk · rust-lang/rust@116edb6 (original) (raw)

`@@ -488,20 +488,93 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {

488

489

490

491

ty::PredicateKind::WellFormed(arg) => match wf::obligations(

492

self.infcx,

493

obligation.param_env,

494

obligation.cause.body_id,

495

obligation.recursion_depth + 1,

496

arg,

497

obligation.cause.span,

498

) {

499

Some(mut obligations) => {

500

self.add_depth(obligations.iter_mut(), obligation.recursion_depth);

501

self.evaluate_predicates_recursively(previous_stack, obligations)

491

ty::PredicateKind::WellFormed(arg) => {

492

`` +

// So, there is a bit going on here. First, WellFormed predicates

493

// are coinductive, like trait predicates with auto traits.

494

// This means that we need to detect if we have recursively

495

`` +

// evaluated WellFormed(X). Otherwise, we would run into

496

// a "natural" overflow error.

497

498

// Now, the next question is whether we need to do anything

499

// special with caching. Considering the following tree:

500

`` +

// - WF(Foo<T>)

501

`` +

// - Bar<T>: Send

502

`` +

// - WF(Foo<T>)

503

`` +

// - Foo<T>: Trait

504

`` +

// In this case, the innermost WF(Foo<T>) should return

505

`` +

// EvaluatedToOk, since it's coinductive. Then if

506

`` +

// Bar<T>: Send is resolved to EvaluatedToOk, it can be

507

`` +

// inserted into a cache (because without thinking about WF

508

`` +

// goals, it isn't in a cycle). If Foo<T>: Trait later doesn't

509

`` +

// hold, then Bar<T>: Send shouldn't hold. Therefore, we

510

// do need to keep track of coinductive cycles.

511

+

512

let cache = previous_stack.cache;

513

let dfn = cache.next_dfn();

514

+

515

for stack_arg in previous_stack.cache.wf_args.borrow().iter().rev() {

516

if stack_arg.0 != arg {

517

continue;

518

}

519

debug!("WellFormed({:?}) on stack", arg);

520

if let Some(stack) = previous_stack.head {

521

// Okay, let's imagine we have two different stacks:

522

`` +

// T: NonAutoTrait -> WF(T) -> T: NonAutoTrait

523

`` +

// WF(T) -> T: NonAutoTrait -> WF(T)

524

// Because of this, we need to check that all

525

// predicates between the WF goals are coinductive.

526

`` +

// Otherwise, we can say that T: NonAutoTrait is

527

// true.

528

// Let's imagine we have a predicate stack like

529

`` +

// `Foo: Bar -> WF(T) -> T: NonAutoTrait -> T: Auto

530

// depth ^1 ^2 ^3

531

`` +

// and the current predicate is WF(T). wf_args

532

`` +

// would contain (T, 1). We want to check all

533

`` +

// trait predicates greater than 1. The previous

534

`` +

// stack would be T: Auto.

535

let cycle = stack.iter().take_while(|s| s.depth > stack_arg.1);

536

let tcx = self.tcx();

537

let cycle =

538

cycle.map(|stack| stack.obligation.predicate.to_predicate(tcx));

539

if self.coinductive_match(cycle) {

540

stack.update_reached_depth(stack_arg.1);

541

return Ok(EvaluatedToOk);

542

} else {

543

return Ok(EvaluatedToRecur);

544

}

545

}

546

return Ok(EvaluatedToOk);

502

547

503

None => Ok(EvaluatedToAmbig),

504

548

+

549

match wf::obligations(

550

self.infcx,

551

obligation.param_env,

552

obligation.cause.body_id,

553

obligation.recursion_depth + 1,

554

arg,

555

obligation.cause.span,

556

) {

557

Some(mut obligations) => {

558

self.add_depth(obligations.iter_mut(), obligation.recursion_depth);

559

+

560

cache.wf_args.borrow_mut().push((arg, previous_stack.depth()));

561

let result =

562

self.evaluate_predicates_recursively(previous_stack, obligations);

563

cache.wf_args.borrow_mut().pop();

564

+

565

let result = result?;

566

+

567

if !result.must_apply_modulo_regions() {

568

cache.on_failure(dfn);

569

}

570

+

571

cache.on_completion(dfn);

572

+

573

Ok(result)

574

}

575

None => Ok(EvaluatedToAmbig),

576

}

577

}

505

578

506

579

` ty::PredicateKind::TypeOutlives(pred) => {

507

580

`// A global type with no late-bound regions can only

`@@ -718,6 +791,8 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {

718

791

719

792

`debug!(?fresh_trait_pred);

720

793

794

// If a trait predicate is in the (local or global) evaluation cache,

795

// then we know it holds without cycles.

721

796

`if let Some(result) = self.check_evaluation_cache(param_env, fresh_trait_pred) {

722

797

`debug!(?result, "CACHE HIT");

723

798

`return Ok(result);

`@@ -921,7 +996,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {

921

996

`` /// - it also appears in the backtrace at some position X,

922

997

`` /// - all the predicates at positions X.. between X and the top are

923

998

`/// also defaulted traits.

924

pub fn coinductive_match(&mut self, mut cycle: I) -> bool

999

pub(crate) fn coinductive_match(&mut self, mut cycle: I) -> bool

925

1000

`where

926

1001

`I: Iterator<Item = ty::Predicate<'tcx>>,

927

1002

`@@ -931,6 +1006,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {

931

1006

`fn coinductive_predicate(&self, predicate: ty::Predicate<'tcx>) -> bool {

932

1007

`let result = match predicate.kind().skip_binder() {

933

1008

` ty::PredicateKind::Trait(ref data) => self.tcx().trait_is_auto(data.def_id()),

1009

ty::PredicateKind::WellFormed(_) => true,

934

1010

` _ => false,

935

1011

`};

936

1012

`debug!(?predicate, ?result, "coinductive_predicate");

`@@ -2410,6 +2486,15 @@ struct ProvisionalEvaluationCache<'tcx> {

2410

2486

`/// all cache values whose DFN is >= 4 -- in this case, that

2411

2487

`` /// means the cached value for F.

2412

2488

`map: RefCell<FxHashMap<ty::PolyTraitPredicate<'tcx>, ProvisionalEvaluation>>,

2489

+

2490

`` +

/// The stack of args that we assume to be true because a WF(arg) predicate

2491

/// is on the stack above (and because of wellformedness is coinductive).

2492

/// In an "ideal" world, this would share a stack with trait predicates in

2493

`` +

/// TraitObligationStack. However, trait predicates are much hotter than

2494

`` +

/// WellFormed predicates, and it's very likely that the additional matches

2495

`` +

/// will have a perf effect. The value here is the well-formed GenericArg

2496

/// and the depth of the trait predicate above that well-formed predicate.

2497

wf_args: RefCell<Vec<(ty::GenericArg<'tcx>, usize)>>,

2413

2498

2414

2499

2415

2500

`/// A cache value for the provisional cache: contains the depth-first

`@@ -2423,7 +2508,7 @@ struct ProvisionalEvaluation {

2423

2508

2424

2509

`impl<'tcx> Default for ProvisionalEvaluationCache<'tcx> {

2425

2510

`fn default() -> Self {

2426

Self { dfn: Cell::new(0), map: Default::default() }

2511

Self { dfn: Cell::new(0), map: Default::default(), wf_args: Default::default() }

2427

2512

2428

2513

2429

2514