diff --git a/library/core/src/marker.rs b/library/core/src/marker.rs
index 07a7d45c7eb..de285c99cb1 100644
--- a/library/core/src/marker.rs
+++ b/library/core/src/marker.rs
@@ -668,16 +668,9 @@ impl<T: ?Sized> !Sync for *mut T {}
 ///
 /// ## Ownership and the drop check
 ///
-/// Adding a field of type `PhantomData<T>` indicates that your
-/// type owns data of type `T`. This in turn implies that when your
-/// type is dropped, it may drop one or more instances of the type
-/// `T`. This has bearing on the Rust compiler's [drop check]
-/// analysis.
-///
-/// If your struct does not in fact *own* the data of type `T`, it is
-/// better to use a reference type, like `PhantomData<&'a T>`
-/// (ideally) or `PhantomData<*const T>` (if no lifetime applies), so
-/// as not to indicate ownership.
+/// Adding a field of type `PhantomData<T>` indicates that your type *owns* data of type `T`. This
+/// in turn has effects on the Rust compiler's [drop check] analysis, but that only matters in very
+/// specific circumstances. For the exact rules, see the [drop check] documentation.
 ///
 /// ## Layout
 ///
@@ -685,7 +678,7 @@ impl<T: ?Sized> !Sync for *mut T {}
 /// * `size_of::<PhantomData<T>>() == 0`
 /// * `align_of::<PhantomData<T>>() == 1`
 ///
-/// [drop check]: ../../nomicon/dropck.html
+/// [drop check]: Drop#drop-check
 #[lang = "phantom_data"]
 #[stable(feature = "rust1", since = "1.0.0")]
 pub struct PhantomData<T: ?Sized>;
diff --git a/library/core/src/ops/drop.rs b/library/core/src/ops/drop.rs
index a2c3d978cc4..804d2c775fc 100644
--- a/library/core/src/ops/drop.rs
+++ b/library/core/src/ops/drop.rs
@@ -132,6 +132,73 @@
 /// are `Copy` get implicitly duplicated by the compiler, making it very
 /// hard to predict when, and how often destructors will be executed. As such,
 /// these types cannot have destructors.
+///
+/// ## Drop check
+///
+/// Dropping interacts with the borrow checker in subtle ways: when a type `T` is being implicitly
+/// dropped as some variable of this type goes out of scope, the borrow checker needs to ensure that
+/// calling `T`'s destructor at this moment is safe. In particular, it also needs to be safe to
+/// recursively drop all the fields of `T`. For example, it is crucial that code like the following
+/// is being rejected:
+///
+/// ```compile_fail,E0597
+/// use std::cell::Cell;
+///
+/// struct S<'a>(Cell<Option<&'a S<'a>>>, Box<i32>);
+/// impl Drop for S<'_> {
+///     fn drop(&mut self) {
+///         if let Some(r) = self.0.get() {
+///             // Print the contents of the `Box` in `r`.
+///             println!("{}", r.1);
+///         }
+///     }
+/// }
+///
+/// fn main() {
+///     // Set up two `S` that point to each other.
+///     let s1 = S(Cell::new(None), Box::new(42));
+///     let s2 = S(Cell::new(Some(&s1)), Box::new(42));
+///     s1.0.set(Some(&s2));
+///     // Now they both get dropped. But whichever is the 2nd one
+///     // to be dropped will access the `Box` in the first one,
+///     // which is a use-after-free!
+/// }
+/// ```
+///
+/// The Nomicon discusses the need for [drop check in more detail][drop check].
+///
+/// To reject such code, the "drop check" analysis determines which types and lifetimes need to
+/// still be live when `T` gets dropped:
+/// - If `T` has no drop glue, then trivially nothing is required to be live. This is the case if
+///   neither `T` nor any of its (recursive) fields have a destructor (`impl Drop`). [`PhantomData`]
+///   and [`ManuallyDrop`] are considered to never have a destructor, no matter their field type.
+/// - If `T` has drop glue, then, for all types `U` that are *owned* by any field of `T`,
+///   recursively add the types and lifetimes that need to be live when `U` gets dropped. The set of
+///   owned types is determined by recursively traversing `T`:
+///   - Recursively descend through `PhantomData`, `Box`, tuples, and arrays (including arrays of
+///     length 0).
+///   - Stop at reference and raw pointer types as well as function pointers and function items;
+///     they do not own anything.
+///   - Stop at non-composite types (type parameters that remain generic in the current context and
+///     base types such as integers and `bool`); these types are owned.
+///   - When hitting an ADT with `impl Drop`, stop there; this type is owned.
+///   - When hitting an ADT without `impl Drop`, recursively descend to its fields. (For an `enum`,
+///     consider all fields of all variants.)
+/// - Furthermore, if `T` implements `Drop`, then all generic (lifetime and type) parameters of `T`
+///   must be live.
+///
+/// In the above example, the last clause implies that `'a` must be live when `S<'a>` is dropped,
+/// and hence the example is rejected. If we remove the `impl Drop`, the liveness requirement
+/// disappears and the example is accepted.
+///
+/// There exists an unstable way for a type to opt-out of the last clause; this is called "drop
+/// check eyepatch" or `may_dangle`. For more details on this nightly-only feature, see the
+/// [discussion in the Nomicon][nomicon].
+///
+/// [`ManuallyDrop`]: crate::mem::ManuallyDrop
+/// [`PhantomData`]: crate::marker::PhantomData
+/// [drop check]: ../../nomicon/dropck.html
+/// [nomicon]: ../../nomicon/phantom-data.html#an-exception-the-special-case-of-the-standard-library-and-its-unstable-may_dangle
 #[lang = "drop"]
 #[stable(feature = "rust1", since = "1.0.0")]
 #[const_trait]