diff --git a/compiler/rustc_trait_selection/src/traits/select/mod.rs b/compiler/rustc_trait_selection/src/traits/select/mod.rs
index f33864024b0..b2c39a4975e 100644
--- a/compiler/rustc_trait_selection/src/traits/select/mod.rs
+++ b/compiler/rustc_trait_selection/src/traits/select/mod.rs
@@ -512,13 +512,36 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
                     let cache = previous_stack.cache;
                     let dfn = cache.next_dfn();
 
-                    for stack_arg in previous_stack.cache.wf_tys.borrow().iter().rev() {
+                    for stack_arg in previous_stack.cache.wf_args.borrow().iter().rev() {
                         if stack_arg.0 != arg {
                             continue;
                         }
                         debug!("WellFormed({:?}) on stack", arg);
                         if let Some(stack) = previous_stack.head {
-                            stack.update_reached_depth(stack_arg.1);
+                            // Okay, let's imagine we have two different stacks:
+                            //   `T: NonAutoTrait -> WF(T) -> T: NonAutoTrait`
+                            //   `WF(T) -> T: NonAutoTrait -> WF(T)`
+                            // Because of this, we need to check that all
+                            // predicates between the WF goals are coinductive.
+                            // Otherwise, we can say that `T: NonAutoTrait` is
+                            // true.
+                            // Let's imagine we have a predicate stack like
+                            //         `Foo: Bar -> WF(T) -> T: NonAutoTrait -> T: Auto
+                            // depth   ^1                    ^2                 ^3
+                            // and the current predicate is `WF(T)`. `wf_args`
+                            // would contain `(T, 1)`. We want to check all
+                            // trait predicates greater than `1`. The previous
+                            // stack would be `T: Auto`.
+                            let cycle = stack.iter().take_while(|s| s.depth > stack_arg.1);
+                            let tcx = self.tcx();
+                            let cycle =
+                                cycle.map(|stack| stack.obligation.predicate.to_predicate(tcx));
+                            if self.coinductive_match(cycle) {
+                                stack.update_reached_depth(stack_arg.1);
+                                return Ok(EvaluatedToOk);
+                            } else {
+                                return Ok(EvaluatedToRecur);
+                            }
                         }
                         return Ok(EvaluatedToOk);
                     }
@@ -534,10 +557,10 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
                         Some(mut obligations) => {
                             self.add_depth(obligations.iter_mut(), obligation.recursion_depth);
 
-                            cache.wf_tys.borrow_mut().push((arg, previous_stack.depth()));
+                            cache.wf_args.borrow_mut().push((arg, previous_stack.depth()));
                             let result =
                                 self.evaluate_predicates_recursively(previous_stack, obligations);
-                            cache.wf_tys.borrow_mut().pop();
+                            cache.wf_args.borrow_mut().pop();
 
                             let result = result?;
 
@@ -2465,7 +2488,14 @@ struct ProvisionalEvaluationCache<'tcx> {
     ///   means the cached value for `F`.
     map: RefCell<FxHashMap<ty::PolyTraitPredicate<'tcx>, ProvisionalEvaluation>>,
 
-    wf_tys: RefCell<Vec<(ty::GenericArg<'tcx>, usize)>>,
+    /// The stack of args that we assume to be true because a `WF(arg)` predicate
+    /// is on the stack above (and because of wellformedness is coinductive).
+    /// In an "ideal" world, this would share a stack with trait predicates in
+    /// `TraitObligationStack`. However, trait predicates are *much* hotter than
+    /// `WellFormed` predicates, and it's very likely that the additional matches
+    /// will have a perf effect. The value here is the well-formed `GenericArg`
+    /// and the depth of the trait predicate *above* that well-formed predicate.
+    wf_args: RefCell<Vec<(ty::GenericArg<'tcx>, usize)>>,
 }
 
 /// A cache value for the provisional cache: contains the depth-first
@@ -2479,7 +2509,7 @@ struct ProvisionalEvaluation {
 
 impl<'tcx> Default for ProvisionalEvaluationCache<'tcx> {
     fn default() -> Self {
-        Self { dfn: Cell::new(0), map: Default::default(), wf_tys: Default::default() }
+        Self { dfn: Cell::new(0), map: Default::default(), wf_args: Default::default() }
     }
 }