diff --git a/docs/users_guide/exts/type_families.rst b/docs/users_guide/exts/type_families.rst
index 4a9636a2a3f6d5393e5419bf47637726b0229319..43f5592cd5eb6ee1148554ae1e8fe4711aa71118 100644
--- a/docs/users_guide/exts/type_families.rst
+++ b/docs/users_guide/exts/type_families.rst
@@ -415,10 +415,19 @@ left hand side of an equation can be explicitly bound, such as in: ::
 A closed type family may be declared with no equations. Such closed type
 families are opaque type-level definitions that will never reduce, are
 not necessarily injective (unlike empty data types), and cannot be given
-any instances. This is different from omitting the equations of a closed
-type family in a ``hs-boot`` file, which uses the syntax ``where ..``,
-as in that case there may or may not be equations given in the ``hs``
-file.
+any instances.
+
+In an ``hs-boot`` file, closed type families must either have the same
+equations as those in the source file, or you can use the following syntax to
+omit the equations (note the literal ``..``) ::
+
+  type family R a where ..
+
+In this case, the closed type family ``R`` matching this "boot" declaration may
+have any number of equations given in the source ``hs`` file (including zero).
+For more information on mutual recursive modules with ``hs-boot`` modules
+(including type families) see :ref:`mutual-recursion`.
+
 
 .. _type-family-examples:
 
diff --git a/docs/users_guide/separate_compilation.rst b/docs/users_guide/separate_compilation.rst
index abcc2f3e313513f54c2f6a4604257d4fb948d7a9..cae12ffc2867fc3986bb531bd797a7ed9d2f6157 100644
--- a/docs/users_guide/separate_compilation.rst
+++ b/docs/users_guide/separate_compilation.rst
@@ -729,8 +729,8 @@ be recompiled.
 
 .. _mutual-recursion:
 
-How to compile mutually recursive modules
------------------------------------------
+Mutually recursive modules and hs-boot files
+--------------------------------------------
 
 .. index::
    single: module system, recursion
@@ -851,8 +851,9 @@ A hs-boot file is written in a subset of Haskell:
 
 -  Open type and data family declarations are exactly as in Haskell.
 
--  A closed type family may optionally omit its equations, as in the
-   following example: ::
+-  A closed type family may either be given in full (where all equations must
+   match the source module), or it can be given abstractly using the ``where ..``
+   syntax (thus omitting the equations), as in the following example: ::
 
         type family ClosedFam a where ..