From 071d7a1e0cb39c14053242ff81439c5cbe8915b8 Mon Sep 17 00:00:00 2001
From: Rodrigo Mesquita <rodrigo.m.mesquita@gmail.com>
Date: Tue, 14 May 2024 16:19:15 +0100
Subject: [PATCH] Improve docs on closed type families in hs-boots

Fixes #24776
---
 docs/users_guide/exts/type_families.rst   | 17 +++++++++++++----
 docs/users_guide/separate_compilation.rst |  9 +++++----
 2 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/docs/users_guide/exts/type_families.rst b/docs/users_guide/exts/type_families.rst
index 4a9636a2a3f..43f5592cd5e 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 abcc2f3e313..cae12ffc286 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 ..
 
-- 
GitLab