summaryrefslogtreecommitdiff
path: root/docs
diff options
context:
space:
mode:
Diffstat (limited to 'docs')
-rw-r--r--docs/users_guide/glasgow_exts.rst3
-rw-r--r--docs/users_guide/using.rst31
2 files changed, 34 insertions, 0 deletions
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 67be116ae4..55562f863c 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -7921,6 +7921,9 @@ other hand, the two equations are compatible. Thus, GHC can ignore the
first equation when looking at the second. So, ``G a`` will simplify to
``a``.
+Incompatibilities between closed type family equations can be displayed
+in :ghci-cmd:`:info` when :ghc-flag:`-fprint-axiom-incomps` is enabled.
+
However see :ref:`ghci-decls` for the overlap rules in GHCi.
.. _type-family-decidability:
diff --git a/docs/users_guide/using.rst b/docs/users_guide/using.rst
index d11dedfb9a..b9dc114ae0 100644
--- a/docs/users_guide/using.rst
+++ b/docs/users_guide/using.rst
@@ -842,6 +842,37 @@ messages and in GHCi:
kinds, GHC uses type-level coercions. Users will rarely need to
see these, as they are meant to be internal.
+.. ghc-flag:: -fprint-axiom-incomps
+ :shortdesc: Display equation incompatibilities in closed type families
+ :type: dynamic
+ :reverse: -fno-print-axiom-incomps
+ :category: verbosity
+
+ Using :ghc-flag:`-fprint-axiom-incomps` tells GHC to display
+ incompatibilities between closed type families' equations, whenever they
+ are printed by :ghci-cmd:`:info` or :ghc-flag:`--show-iface ⟨file⟩`.
+
+ .. code-block:: none
+
+ ghci> :i Data.Type.Equality.==
+ type family (==) (a :: k) (b :: k) :: Bool
+ where
+ (==) (f a) (g b) = (f == g) && (a == b)
+ (==) a a = 'True
+ (==) _1 _2 = 'False
+ ghci> :set -fprint-axiom-incomps
+ ghci> :i Data.Type.Equality.==
+ type family (==) (a :: k) (b :: k) :: Bool
+ where
+ (==) (f a) (g b) = (f == g) && (a == b)
+ (==) a a = 'True
+ -- incompatible indices: 0
+ (==) _1 _2 = 'False
+ -- incompatible indices: 1, 0
+
+ The comment after each equation refers to the indices (0-indexed) of
+ preceding equations it is incompatible with.
+
.. ghc-flag:: -fprint-equality-relations
:shortdesc: Distinguish between equality relations when printing
:type: dynamic