diff --git a/src/test/ui/hrtb/hrtb-exists-forall-fn.rs b/src/test/ui/hrtb/hrtb-exists-forall-fn.rs
new file mode 100644
index 000000000000..bba1f4dfb86c
--- /dev/null
+++ b/src/test/ui/hrtb/hrtb-exists-forall-fn.rs
@@ -0,0 +1,23 @@
+// Test a `exists<'a> { forall<'b> { 'a = 'b } }` pattern -- which should not compile!
+//
+// In particular, we test this pattern in trait solving, where it is not connected
+// to any part of the source code.
+
+trait Trait<T> {}
+
+fn foo<'a>() -> fn(&'a u32) {
+    panic!()
+}
+
+fn main() {
+    // Here, proving that `(): Trait<for<'b> fn(&'b u32)>` uses the impl:
+    //
+    // - The impl provides the clause `forall<'a> { (): Trait<fn(&'a u32)> }`
+    // - We instantiate `'a` existentially to get `(): Trait<fn(&?a u32)>`
+    // - We unify `fn(&?a u32)` with `for<'b> fn(&'b u32)`
+    //   - This requires (among other things) instantiating `'b` universally,
+    //     yielding `fn(&!b u32)`, in a fresh universe U1
+    //   - So we get `?a = !b` but the universe U0 assigned to `?a` cannot name `!b`.
+
+    let _: for<'b> fn(&'b u32) = foo(); //~ ERROR cannot infer
+}
diff --git a/src/test/ui/hrtb/hrtb-exists-forall-fn.stderr b/src/test/ui/hrtb/hrtb-exists-forall-fn.stderr
new file mode 100644
index 000000000000..75ba89f58da1
--- /dev/null
+++ b/src/test/ui/hrtb/hrtb-exists-forall-fn.stderr
@@ -0,0 +1,24 @@
+error[E0495]: cannot infer an appropriate lifetime for lifetime parameter `'a` due to conflicting requirements
+  --> $DIR/hrtb-exists-forall-fn.rs:22:34
+   |
+LL |     let _: for<'b> fn(&'b u32) = foo(); //~ ERROR cannot infer
+   |                                  ^^^
+   |
+   = note: first, the lifetime cannot outlive lifetime RePlaceholder(Placeholder { universe: U1, name: BrNamed(crate0:DefIndex(1:11), 'b) })...
+   = note: ...so that the expression is assignable:
+           expected for<'b> fn(&'b u32)
+              found fn(&u32)
+note: but, the lifetime must be valid for the call at 22:34...
+  --> $DIR/hrtb-exists-forall-fn.rs:22:34
+   |
+LL |     let _: for<'b> fn(&'b u32) = foo(); //~ ERROR cannot infer
+   |                                  ^^^^^
+note: ...so type `fn(&u32)` of expression is valid during the expression
+  --> $DIR/hrtb-exists-forall-fn.rs:22:34
+   |
+LL |     let _: for<'b> fn(&'b u32) = foo(); //~ ERROR cannot infer
+   |                                  ^^^^^
+
+error: aborting due to previous error
+
+For more information about this error, try `rustc --explain E0495`.
diff --git a/src/test/ui/hrtb/hrtb-exists-forall-trait-contravariant.rs b/src/test/ui/hrtb/hrtb-exists-forall-trait-contravariant.rs
new file mode 100644
index 000000000000..8801760056ec
--- /dev/null
+++ b/src/test/ui/hrtb/hrtb-exists-forall-trait-contravariant.rs
@@ -0,0 +1,35 @@
+// Test a `exists<'a> { forall<'b> { 'a = 'b } }` pattern -- which should not compile!
+//
+// In particular, we test this pattern in trait solving, where it is not connected
+// to any part of the source code.
+//
+// compile-pass
+
+trait Trait<T> {}
+
+fn foo<T>()
+where
+    T: Trait<for<'b> fn(&'b u32)>,
+{
+}
+
+impl<'a> Trait<fn(&'a u32)> for () {}
+
+fn main() {
+    // Here, proving that `(): Trait<for<'b> fn(&'b u32)>` uses the impl:
+    //
+    // - The impl provides the clause `forall<'a> { (): Trait<fn(&'a u32)> }`
+    // - We instantiate `'a` existentially to get `(): Trait<fn(&?a u32)>`
+    // - We unify `fn(&?a u32)` with `for<'b> fn(&'b u32)` -- this does a
+    //   "bidirectional" subtyping check, so we wind up with:
+    //   - `fn(&?a u32) <: for<'b> fn(&'b u32)` :-
+    //     - `&'!b u32 <: &?a u32`
+    //     - `!'b: ?a` -- solveable if `?a` is inferred to `'empty`
+    //   - `for<'b> fn(&'b u32) <: fn(&?a u32)` :-
+    //     - `&?a u32 u32 <: &?b u32`
+    //     - `?a: ?b` -- solveable if `?b` is also inferred to `'empty`
+    // - So the subtyping check succeeds, somewhat surprisingly.
+    //   This is because we can use `'empty`.
+
+    foo::<()>();
+}
diff --git a/src/test/ui/hrtb/hrtb-exists-forall-trait-covariant.rs b/src/test/ui/hrtb/hrtb-exists-forall-trait-covariant.rs
new file mode 100644
index 000000000000..da1bb7cd5fd0
--- /dev/null
+++ b/src/test/ui/hrtb/hrtb-exists-forall-trait-covariant.rs
@@ -0,0 +1,37 @@
+// Test a `exists<'a> { forall<'b> { 'a = 'b } }` pattern -- which should not compile!
+//
+// In particular, we test this pattern in trait solving, where it is not connected
+// to any part of the source code.
+//
+// compile-pass
+
+trait Trait<T> {}
+
+fn foo<T>()
+where
+    T: Trait<for<'b> fn(fn(&'b u32))>,
+{
+}
+
+impl<'a> Trait<fn(fn(&'a u32))> for () {}
+
+fn main() {
+    // Here, proving that `(): Trait<for<'b> fn(&'b u32)>` uses the impl:
+    //
+    // - The impl provides the clause `forall<'a> { (): Trait<fn(fn(&'a u32))> }`
+    // - We instantiate `'a` existentially to get `(): Trait<fn(fn(&?a u32))>`
+    // - We unify `fn(fn(&?a u32))` with `for<'b> fn(fn(&'b u32))` -- this does a
+    //   "bidirectional" subtyping check, so we wind up with:
+    //   - `fn(fn(&?a u32)) <: for<'b> fn(fn(&'b u32))` :-
+    //     - `fn(&!b u32) <: fn(&?a u32)`
+    //       - `&?a u32 <: &!b u32`
+    //         - `?a: !'b` -- solveable if `?a` is inferred to `'static`
+    //   - `for<'b> fn(fn(&'b u32)) <: fn(fn(&?a u32))` :-
+    //     - `fn(&?a u32) <: fn(&?b u32)`
+    //       - `&?b u32 <: &?a u32`
+    //         - `?b: ?a` -- solveable if `?b` is inferred to `'static`
+    // - So the subtyping check succeeds, somewhat surprisingly.
+    //   This is because we can use `'static`.
+
+    foo::<()>();
+}
diff --git a/src/test/ui/hrtb/hrtb-exists-forall-trait-invariant.rs b/src/test/ui/hrtb/hrtb-exists-forall-trait-invariant.rs
new file mode 100644
index 000000000000..db589548d0e8
--- /dev/null
+++ b/src/test/ui/hrtb/hrtb-exists-forall-trait-invariant.rs
@@ -0,0 +1,29 @@
+// Test a `exists<'a> { forall<'b> { 'a = 'b } }` pattern -- which should not compile!
+//
+// In particular, we test this pattern in trait solving, where it is not connected
+// to any part of the source code.
+
+use std::cell::Cell;
+
+trait Trait<T> {}
+
+fn foo<T>()
+where
+    T: Trait<for<'b> fn(Cell<&'b u32>)>,
+{
+}
+
+impl<'a> Trait<fn(Cell<&'a u32>)> for () {}
+
+fn main() {
+    // Here, proving that `(): Trait<for<'b> fn(&'b u32)>` uses the impl:
+    //
+    // - The impl provides the clause `forall<'a> { (): Trait<fn(&'a u32)> }`
+    // - We instantiate `'a` existentially to get `(): Trait<fn(&?a u32)>`
+    // - We unify `fn(&?a u32)` with `for<'b> fn(&'b u32)`
+    //   - This requires (among other things) instantiating `'b` universally,
+    //     yielding `fn(&!b u32)`, in a fresh universe U1
+    //   - So we get `?a = !b` but the universe U0 assigned to `?a` cannot name `!b`.
+
+    foo::<()>(); //~ ERROR cannot infer
+}
diff --git a/src/test/ui/hrtb/hrtb-exists-forall-trait-invariant.stderr b/src/test/ui/hrtb/hrtb-exists-forall-trait-invariant.stderr
new file mode 100644
index 000000000000..7a0986ccdd93
--- /dev/null
+++ b/src/test/ui/hrtb/hrtb-exists-forall-trait-invariant.stderr
@@ -0,0 +1,15 @@
+error[E0495]: cannot infer an appropriate lifetime for lifetime parameter `'a` due to conflicting requirements
+  --> $DIR/hrtb-exists-forall-trait-invariant.rs:28:5
+   |
+LL |     foo::<()>(); //~ ERROR cannot infer
+   |     ^^^^^^^^^
+   |
+   = note: first, the lifetime cannot outlive lifetime RePlaceholder(Placeholder { universe: U3, name: BrNamed(crate0:DefIndex(1:11), 'b) })...
+   = note: ...but the lifetime must also be valid for lifetime RePlaceholder(Placeholder { universe: U3, name: BrNamed(crate0:DefIndex(1:11), 'b) })...
+   = note: ...so that the types are compatible:
+           expected Trait<for<'b> fn(std::cell::Cell<&'b u32>)>
+              found Trait<fn(std::cell::Cell<&u32>)>
+
+error: aborting due to previous error
+
+For more information about this error, try `rustc --explain E0495`.