base: Improve docs to clarify when finalizers may not be run

libraries/base/System/Mem/Weak.hs

@@ -67,6 +67,10 @@ module System.Mem.Weak (
         -- * A precise semantics
 
         -- $precise
+
+        -- * Implementation notes
+
+        -- $notes
    ) where
 
 import GHC.Weak
@@ -140,3 +144,25 @@ A heap object is /reachable/ if:
  * It is the value or finalizer of a weak pointer object whose key is reachable.
 -}
 
+{- $notes
+
+A finalizer is not always called after its weak pointer\'s object becomes
+unreachable. There are two situations that can cause this:
+
+ * If the object becomes unreachable right before the program exits,
+   then GC may not be performed. Finalizers run during GC, so finalizers
+   associated with the object do not run if GC does not happen.
+
+ * If a finalizer throws an exception, subsequent finalizers that had
+   been queued to run after it do not get run. This behavior may change
+   in a future release. See issue <https://ghc.haskell.org/trac/ghc/ticket/13167 13167>
+   on the issue tracker. Writing a finalizer that throws exceptions is
+   discouraged.
+
+Other than these two caveats, users can always expect that a finalizer
+will be run after its weak pointer\'s object becomes unreachable. However,
+the second caveat means that users need to trust that all of their
+transitive dependencies do not throw exceptions in finalizers, since
+any finalizers can end up queued together.
+
+-}